← elements / Elements 2.0 (G Index)

G.102 intersecting circles have distinct centers¶

Two intersecting circles do not have the same center.

intersecting_circles_distinct_centers(( A B C ), ( C D G ), B, C)
given ( A B C ) ∩ ( C D G ) = {B, C}
prove center(( A B C )) ≠ center(( C D G ))

∵ circle_radiigiven ( A B C ) and ( C D G ) cut one another at B, C

∵ circle_center, segmentconstruct Suppose E is their common center; segment(E, C) → / E C /, draw / E F G / through at random

∵ circle_radiiassert E is center of ( A B C ) → / E C / = / E F /

∵ circle_radiiassert E is center of ( C D G ) → / E C / = / E G /

∵ equal_transitive, whole_greater_than_partassert / E F / = / E G /, the less to the greater ⇒⇐

∵ circle_center∴ E is not the common center of ( A B C ) and ( C D G )

Dependency Graph¶