9 report_timing := true;;
11 Theorem/Proof templates:
33 ∉ |- ∀ a l. a ∉ l ⇔ ¬(a ∈ l)
35 Interval_DEF |- ∀ A B X. open (A,B) = {X | Between A X B}
38 |- ∀ A B C. Collinear A B C ⇔ ∃ l. Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l
41 |- ∀ l A B. A,B same_side l ⇔ Line l ∧ ¬ ∃ X. X ∈ l ∧ X ∈ open (A,B)
43 Ray_DEF |- ∀ A B. ray A B =
44 {X | ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)}
49 B ∈ open (A,C) ∧ B ∈ open (A,D) ∧ C ∈ open (A,D) ∧ C ∈ open (B,D)
51 InteriorAngle_DEF |- ∀ A O B.
53 {P | ¬Collinear A O B ∧
55 Line a ∧ O ∈ a ∧ A ∈ a ∧
56 Line b ∧ O ∈ b ∧ B ∈ b ∧
58 P,B same_side a ∧ P,A same_side b}
63 {P | P ∈ int_angle A B C ∧
69 Tetralateral A B C D ⇔
70 ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D) ∧
71 ¬Collinear A B C ∧ ¬Collinear B C D ∧ ¬Collinear C D A ∧ ¬Collinear D A B
75 Quadrilateral A B C D ⇔
76 Tetralateral A B C D ∧
77 open (A,B) ∩ open (C,D) = ∅ ∧
78 open (B,C) ∩ open (D,A) = ∅
82 ConvexQuadrilateral A B C D ⇔
83 Quadrilateral A B C D ∧
89 Segment_DEF |- ∀ A B. seg A B = {A, B} ∪ open (A,B)
91 SEGMENT |- ∀ s. Segment s ⇔ ∃ A B. s = seg A B ∧ ¬(A = B)
97 ∃ C D X. t = seg C D ∧ X ∈ open (C,D) ∧ s ≡ seg C X
99 Angle_DEF |- ∀ A O B. ∡ A O B = ray O A ∪ ray O B
102 |- ∀ α. Angle α ⇔ ∃ A O B. α = ∡ A O B ∧ ¬Collinear A O B
109 ¬Collinear A O B ∧ β = ∡ A O B ∧
110 G ∈ int_angle A O B ∧ α ≡ ∡ A O G
112 RAY |- ∀ r. Ray r ⇔ ∃ O A. ¬(O = A) ∧ r = ray O A
117 ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
118 seg A B ≡ seg A' B' ∧
119 seg A C ≡ seg A' C' ∧
120 seg B C ≡ seg B' C' ∧
121 ∡ A B C ≡ ∡ A' B' C' ∧
122 ∡ B C A ≡ ∡ B' C' A' ∧
125 SupplementaryAngles_DEF
129 ¬Collinear A O B ∧ O ∈ open (A,A') ∧
130 α = ∡ A O B ∧ β = ∡ B O A'
133 |- ∀α. Right α ⇔ ∃ β. α suppl β ∧ α ≡ β
136 |- ∀ α. complement α = {P | P ∉ α}
140 ∀ A B. A ∈ α ∧ B ∈ α ⇒ open (A,B) ⊂ α
143 |- ∀ l k. l ∥ k ⇔ Line l ∧ Line k ∧ l ∩ k = ∅
147 Parallelogram A B C D ⇔
148 Quadrilateral A B C D ∧
150 Line a ∧ A ∈ a ∧ B ∈ a ∧ Line b ∧ B ∈ b ∧ C ∈ b ∧
151 Line c ∧ C ∈ c ∧ D ∈ d ∧ Line d ∧ D ∈ d ∧ A ∈ d ∧
155 |- ∀ O R. int_circle O R = {P | ¬(O = R) ∧ (P = O ∨ seg O P <__ seg O R)}
158 I1 |- ∀ A B. ¬(A = B) ⇒ (∃! l. Line l ∧ A ∈ l ∧ B ∈ l)
160 I2 |- ∀ l. Line l ⇒ (∃ A B. A ∈ l ∧ B ∈ l ∧ ¬(A = B))
162 I3 |- ∃ A B C. ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ ¬Collinear A B C
166 ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
167 Between C B A ∧ Collinear A B C
169 B2 |- ∀ A B. ¬(A = B) ⇒ ∃C. Between A B C
172 ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
173 ⇒ (Between A B C ∨ Between B C A ∨ Between C A B) ∧
174 ¬(Between A B C ∧ Between B C A) ∧
175 ¬(Between A B C ∧ Between C A B) ∧
176 ¬(Between B C A ∧ Between C A B)
181 A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
182 (∃X. X ∈ l ∧ Between A X C)
183 ⇒ (∃ Y. Y ∈ l ∧ Between A Y B) ∨
184 (∃ Y. Y ∈ l ∧ Between B Y C)
188 ⇒ ∃! P. P ∈ ray O Z ━ O ∧ seg O P ≡ s
190 C2Reflexive |- Segment s ⇒ s ≡ s
192 C2Symmetric |- Segment s ∧ Segment t ∧ s ≡ t ⇒ t ≡ s
195 |- Segment s ∧ Segment t ∧ Segment u ∧ s ≡ t ∧ t ≡ u ⇒ s ≡ u
197 C3 |- ∀ A B C A' B' C'.
198 B ∈ open (A,C) ∧ B' ∈ open (A',C') ∧
199 seg A B ≡ seg A' B' ∧ seg B C ≡ seg B' C'
200 ⇒ seg A C ≡ seg A' C'
203 Angle α ∧ ¬(O = A) ∧ Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l
204 ⇒ ∃! r. Ray r ∧ ∃ B. ¬(O = B) ∧ r = ray O B ∧
205 B ∉ l ∧ B,Y same_side l ∧ ∡ A O B ≡ α
207 C5Reflexive |- Angle α ⇒ α ≡ α
210 |- Angle α ∧ Angle β ∧ α ≡ β ⇒ β ≡ α
213 |- Angle α ∧ Angle β ∧ Angle γ ∧ α ≡ β ∧ β ≡ γ
216 C6 |- ∀A B C A' B' C'.
217 ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
218 seg B A ≡ seg B' A' ∧ seg B C ≡ seg B' C' ∧
220 ⇒ ∡ B C A ≡ ∡ B' C' A'
223 IN_Interval |- ∀ A B X. X ∈ open (A,B) ⇔ Between A X B
226 X ∈ ray A B ⇔ ¬(A = B) ∧ Collinear A B X ∧ A ∉ open (X,B)
228 IN_InteriorAngle |- ∀A O B P.
229 P ∈ int_angle A O B ⇔ ¬Collinear A O B ∧ ∃ a b.
230 Line a ∧ O ∈ a ∧ A ∈ a ∧ Line b ∧ O ∈ b ∧ B ∈ b ∧
231 P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b
235 P ∈ int_triangle A B C ⇔
236 P ∈ int_angle A B C ∧ P ∈ int_angle B C A ∧ P ∈ int_angle C A B
239 |- ∀α P. P ∈ complement α ⇔ P ∉ α
243 P ∈ int_circle O R ⇔ ¬(O = R) ∧ (P = O ∨ seg O P <__ seg O R)
247 ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧
248 B ∈ open (C,A) ∧ Collinear A B C
250 B2' |- ∀ A B. ¬(A = B) ⇒ (∃ C. B ∈ open (A,C))
253 ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C) ∧ Collinear A B C
254 ⇒ (B ∈ open (A,C) ∨ C ∈ open (B,A) ∨ A ∈ open (C,B)) ∧
255 ¬(B ∈ open (A,C) ∧ C ∈ open (B,A)) ∧
256 ¬(B ∈ open (A,C) ∧ A ∈ open (C,B)) ∧
257 ¬(C ∈ open (B,A) ∧ A ∈ open (C,B))
260 Line l ∧ ¬Collinear A B C ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
261 (∃ X. X ∈ l ∧ X ∈ open (A,C))
262 ⇒ (∃ Y. Y ∈ l ∧ Y ∈ open (A,B)) ∨
263 (∃ Y. Y ∈ l ∧ Y ∈ open (B,C))
266 Line l ∧ ¬Collinear A B C ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
267 A,B same_side l ∧ B,C same_side l
271 |- ∀ l m. (∀x. x ∈ m ⇒ x ∉ l) ⇔ l ∩ m = ∅
273 EquivIntersectionHelp
275 (l ∩ m = {x} ∨ m ∩ l = {x}) ∧ e ∈ m ━ x ⇒ e ∉ l
280 ⇒ Collinear A C B ∧ Collinear B A C ∧
281 Collinear B C A ∧ Collinear C A B ∧ Collinear C B A
284 |- ∀ P l. Line l ∧ P ∈ l ⇒ ∃ Q. Q ∈ l ∧ ¬(P = Q)
286 ExistsPointOffLine |- ∀ l. Line l ⇒ ∃ Q. Q ∉ l
290 Line m ∧ A ∈ m ∧ C ∈ m ∧
291 B ∈ open (A,C) ∨ C ∈ open (B,A) ∨ A ∈ open (C,B)
296 Line m ∧ A ∈ m ∧ C ∈ m ∧ ¬(A = C) ∧
297 Collinear A B C ∨ Collinear B C A ∨ Collinear C A B
300 NonCollinearImpliesDistinct
301 |- ∀ A B C. ¬Collinear A B C ⇒ ¬(A = B) ∧ ¬(A = C) ∧ ¬(B = C)
305 ¬(A = C) ∧ Line l ∧ A ∈ l ∧ C ∈ l ∧ B ∉ l
308 TwoSidesTriangle1Intersection
310 ¬Collinear A B C ∧ Collinear B C Y ∧ Collinear A C Y ⇒ Y = C
312 OriginInRay |- ∀ O Q. ¬(Q = O) ⇒ O ∈ ray O Q
314 EndpointInRay |- ∀ O Q. ¬(Q = O) ⇒ Q ∈ ray O Q
318 Line l ∧ Line m ∧ ¬(l = m) ∧ X ∈ l ∧ X ∈ m
323 Line l ∧ Line m ∧ l ∩ m = {X} ∧
324 A ∈ m ━ X ∧ B ∈ m ━ X ∧ X ∉ open (A,B)
328 |- ∀ O P l. Line l ∧ O ∈ l ∧ P ∈ l ⇒ ray O P ⊂ l
332 Line l ∧ O ∈ l ∧ A ∉ l ∧ P ∈ ray O A ━ O
333 ⇒ P ∉ l ∧ P,A same_side l
337 B ∈ open (A,C) ⇒ B ∈ ray A C ━ A ∧ C ∈ ray A B ━ A
339 NoncollinearityExtendsToLine
341 ¬Collinear A O B ∧ Collinear O B X ∧ ¬(X = O)
345 |- ∀ l A. Line l ∧ A ∉ l ⇒ A,A same_side l
349 Line l ∧ A ∉ l ∧ B ∉ l ∧ A,B same_side l
354 Line l ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
355 A,B same_side l ∧ B,C same_side l
359 |- ∀ O A B G. ¬Collinear A O B ∧ G ∈ open (A,B) ⇒ G ∈ int_angle A O B
363 Line a ∧ O ∈ a ∧ A ∈ a ∧
364 Line b ∧ O ∈ b ∧ B ∈ b ∧
366 ⇒ P ∉ a ∧ P ∉ b ∧ P,B same_side a ∧ P,A same_side b
371 ⇒ ¬(P = A) ∧ ¬(P = O) ∧ ¬(P = B) ∧ ¬Collinear A O P
373 InteriorAngleSymmetry
374 |- ∀ A O B P. P ∈ int_angle A O B ⇒ P ∈ int_angle B O A
378 P ∈ int_angle A O B ∧ X ∈ ray O B ━ O ⇒ P ∈ int_angle A O X
382 X ∈ int_angle A O B ∧ P ∈ ray O X ━ O
383 ⇒ P ∈ int_angle A O B
387 ¬(O = A) ∧ Line a ∧ O ∈ a ∧ A ∈ a ∧ P ∉ a ∧ Q ∉ a ∧
388 P,Q same_side a ∧ ¬Collinear P O Q
389 ⇒ P ∈ int_angle Q O A ∨ Q ∈ int_angle P O A
391 InteriorsDisjointSupplement
393 ¬Collinear A O B ∧ O ∈ open (A,A')
394 ⇒ int_angle A O B ∩ int_angle B O A' = ∅
396 InteriorReflectionInterior
398 O ∈ open (A,A') ∧ D ∈ int_angle A O B ⇒ B ∈ int_angle D O A'
403 ⇒ ∃ G. G ∈ open (A,B) ∧ G ∈ ray O D ━ O
405 AlternateConverseCrossbar
406 |- ∀ O A B G. Collinear A G B ∧ G ∈ int_angle A O B ⇒ G ∈ open (A,B)
410 P ∈ int_angle A O B ∧ Line p ∧ O ∈ p ∧ P ∈ p
416 P ∈ m ━ O ∧ Q ∈ m ━ O ∧ R ∈ m ━ O ∧
417 O ∉ open (P,Q) ∧ O ∉ open (Q,R)
420 RayWellDefinedHalfway
421 |- ∀ O P Q. ¬(Q = O) ∧ P ∈ ray O Q ━ O ⇒ ray O P ⊂ ray O Q
424 |- ∀ O P Q. ¬(Q = O) ∧ P ∈ ray O Q ━ O ⇒ ray O P = ray O Q
426 OppositeRaysIntersect1pointHelp
428 O ∈ open (A,B) ∧ X ∈ ray O B ━ O
429 ⇒ X ∉ ray O A ∧ O ∈ open (X,A)
431 OppositeRaysIntersect1point
432 |- ∀ A O B. O ∈ open (A,B) ⇒ ray O A ∩ ray O B = {O}
435 |- ∀ A B C. B ∈ open (A,C) ⇒ ray A B = ray A C
438 |- ∀ A B C D. ordered A B C D ⇒ ordered D C B A
440 TransitivityBetweennessHelp
441 |- ∀ A B C D. B ∈ open (A,C) ∧ C ∈ open (B,D) ⇒ B ∈ open (A,D)
443 TransitivityBetweenness
444 |- ∀ A B C D. B ∈ open (A,C) ∧ C ∈ open (B,D) ⇒ ordered A B C D
447 |- ∀ A B C. B ∈ open (A,C) ⇒ open (A,B) ⊂ open (A,C)
449 TransitivityBetweennessVariant
450 |- ∀ A X B C. X ∈ open (A,B) ∧ B ∈ open (A,C) ⇒ ordered A X B C
452 Interval2sides2aLineHelp
453 |- ∀ A B C X. B ∈ open (A,C) ⇒ X ∉ open (A,B) ∨ X ∉ open (B,C)
458 ⇒ X ∉ open (A,B) ∨ X ∉ open (A,C) ∨ X ∉ open (B,C)
460 TwosidesTriangle2aLine
462 Line l ∧ ¬Collinear A B C ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l ∧
463 Line m ∧ A ∈ m ∧ C ∈ m ∧
464 Y ∈ l ∧ Y ∈ m ∧ ¬(A,B same_side l) ∧ ¬(B,C same_side l)
469 Line l ∧ A ∈ l ∧ B ∈ l ∧ O ∈ open (A,B)
470 ⇒ l = ray O A ∪ ray O B
474 Line l ∧ A ∉ l ∧ B ∉ l ∧ C ∉ l
475 ⇒ A,B same_side l ∨ A,C same_side l ∨ B,C same_side l
479 Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ X ∈ l ∧ B ∈ open (A,C) ∧
480 ¬(X = A) ∧ ¬(X = B) ∧ ¬(X = C)
481 ⇒ ordered X A B C ∨ ordered A X B C ∨ ordered A B X C ∨ ordered A B C X
483 HilbertAxiomRedundantByMoore
485 Line l ∧ A ∈ l ∧ B ∈ l ∧ C ∈ l ∧ D ∈ l ∧
486 ¬(A = B) ∧ ¬(A = C) ∧ ¬(A = D) ∧ ¬(B = C) ∧ ¬(B = D) ∧ ¬(C = D)
487 ⇒ ordered D A B C ∨ ordered A D B C ∨ ordered A B D C ∨
488 ordered A B C D ∨ ordered D A C B ∨ ordered A D C B ∨
489 ordered A C D B ∨ ordered A C B D ∨ ordered D C A B ∨
490 ordered C D A B ∨ ordered C A D B ∨ ordered C A B D
494 G ∈ int_angle A O B ∧ F ∈ int_angle A O G
495 ⇒ F ∈ int_angle A O B
497 HalfPlaneConvexNonempty
499 Line l ∧ A ∉ l ∧ H = {X | X ∉ l ∧ X,A same_side l}
500 ⇒ ¬(H = ∅) ∧ H ⊂ complement l ∧ Convex H
505 H1 ∩ H2 = ∅ ∧ ¬(H1 = ∅) ∧ ¬(H2 = ∅) ∧
506 Convex H1 ∧ Convex H2 ∧ complement l = H1 ∪ H2 ∧
507 ∀ P Q. P ∈ H1 ∧ Q ∈ H2 ⇒ ¬(P,Q same_side l)
512 ⇒ Tetralateral B C D A ∧ Tetralateral A B D C
514 EasyEmptyIntersectionsTetralateralHelp
515 |- ∀ A B C D. Tetralateral A B C D ⇒ open (A,B) ∩ open (B,C) = ∅
517 EasyEmptyIntersectionsTetralateral
520 ⇒ open (A,B) ∩ open (B,C) = ∅ ∧ open (B,C) ∩ open (C,D) = ∅ ∧
521 open (C,D) ∩ open (D,A) = ∅ ∧ open (D,A) ∩ open (A,B) = ∅
523 SegmentSameSideOppositeLine
525 Quadrilateral A B C D ∧
526 Line a ∧ A ∈ a ∧ B ∈ a ∧ Line c ∧ C ∈ c ∧ D ∈ c
527 ⇒ A,B same_side c ∨ C,D same_side a
531 Tetralateral A B C D ∧
532 C ∈ int_angle D A B ∧ D ∈ int_angle A B C
533 ⇒ Quadrilateral A B C D
535 DiagonalsIntersectImpliesConvexQuad
537 ¬Collinear B C D ∧ G ∈ open (A,C) ∧ G ∈ open (B,D)
538 ⇒ ConvexQuadrilateral A B C D
540 DoubleNotSimImpliesDiagonalsIntersect
542 Line l ∧ A ∈ l ∧ C ∈ l ∧
543 Line m ∧ B ∈ m ∧ D ∈ m ∧
544 Tetralateral A B C D ∧
545 ¬(B,D same_side l) ∧ ¬(A,C same_side m)
546 ⇒ (∃ G. G ∈ open (A,C) ∩ open (B,D)) ∧
547 ConvexQuadrilateral A B C D
549 ConvexQuadImpliesDiagonalsIntersect
551 Line l ∧ A ∈ l ∧ C ∈ l ∧
552 Line m ∧ B ∈ m ∧ D ∈ m ∧
553 ConvexQuadrilateral A B C D
554 ⇒ ¬(B,D same_side l) ∧ ¬(A,C same_side m) ∧
555 (∃ G. G ∈ open (A,C) ∩ open (B,D)) ∧
556 ¬Quadrilateral A B D C
558 FourChoicesTetralateralHelp
560 Tetralateral A B C D ∧ C ∈ int_angle D A B
561 ⇒ ConvexQuadrilateral A B C D ∨ C ∈ int_triangle D A B
563 InteriorTriangleSymmetry
564 |- ∀ A B C P. P ∈ int_triangle A B C ⇒ P ∈ int_triangle B C A
566 FourChoicesTetralateral
568 Tetralateral A B C D ∧ Line a ∧ A ∈ a ∧ B ∈ a ∧
570 ⇒ ConvexQuadrilateral A B C D ∨ ConvexQuadrilateral A B D C ∨
571 D ∈ int_triangle A B C ∨ C ∈ int_triangle D A B
573 QuadrilateralSymmetry
575 Quadrilateral A B C D
576 ⇒ Quadrilateral B C D A ∧
577 Quadrilateral C D A B ∧
578 Quadrilateral D A B C
580 FiveChoicesQuadrilateral
582 Quadrilateral A B C D ∧
583 Line l ∧ A ∈ l ∧ C ∈ l ∧
584 Line m ∧ B ∈ m ∧ D ∈ m
585 ⇒ (ConvexQuadrilateral A B C D ∨
586 A ∈ int_triangle B C D ∨ B ∈ int_triangle C D A ∨
587 C ∈ int_triangle D A B ∨ D ∈ int_triangle A B C) ∧
588 (¬(B,D same_side l) ∨ ¬(A,C same_side m))
590 IntervalSymmetry |- ∀ A B. open (A,B) = open (B,A)
592 SegmentSymmetry |- ∀ A B. seg A B = seg B A
596 Segment s ∧ ¬(O = P) ⇒ ∃ Q. P ∈ open (O,Q) ∧ seg P Q ≡ s
598 OrderedCongruentSegments
600 ¬(A = C) ∧ ¬(D = F) ∧ seg A C ≡ seg D F ∧ B ∈ open (A,C)
601 ⇒ ∃ E. E ∈ open (D,F) ∧ seg A B ≡ seg D E
605 B ∈ open (A,C) ∧ B' ∈ open (A',C') ∧
606 seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C'
607 ⇒ seg B C ≡ seg B' C'
611 Segment s ∧ ¬(A = B) ∧ s <__ seg A B
612 ⇒ ∃ G. G ∈ open (A,B) ∧ s ≡ seg A G
614 SegmentTrichotomy1 |- ∀ s t. s <__ t ⇒ ¬(s ≡ t)
617 |- ∀ s t u. s <__ t ∧ Segment u ∧ t ≡ u ⇒ s <__ u
619 SegmentOrderTransitivity
620 |- ∀ s t u. s <__ t ∧ t <__ u ⇒ s <__ u
624 Segment s ∧ Segment t
625 ⇒ (s ≡ t ∨ s <__ t ∨ t <__ s) ∧
626 ¬(s ≡ t ∧ s <__ t) ∧ ¬(s ≡ t ∧ t <__ s) ∧ ¬(s <__ t ∧ t <__ s)
630 Line l ∧ O ∈ l ∧ A ∈ l ∧ ¬(O = A) ∧
631 B ∉ l ∧ P ∉ l ∧ P,B same_side l ∧ ∡ A O P ≡ ∡ A O B
634 AngleSymmetry |- ∀ A O B. ∡ A O B = ∡ B O A
639 ⇒ A,C,B ≅ A',C',B' ∧ B,A,C ≅ B',A',C' ∧
640 B,C,A ≅ B',C',A' ∧ C,A,B ≅ C',A',B' ∧ C,B,A ≅ C',B',A'
644 ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
645 seg B A ≡ seg B' A' ∧ seg B C ≡ seg B' C' ∧
651 ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
652 seg A C ≡ seg A' C' ∧
653 ∡ C A B ≡ ∡ C' A' B' ∧ ∡ B C A ≡ ∡ B' C' A'
657 |- ∀ A O B A' O' B' G G'.
658 G ∈ int_angle A O B ∧ G' ∈ int_angle A' O' B' ∧
659 ∡ A O B ≡ ∡ A' O' B' ∧ ∡ A O G ≡ ∡ A' O' G'
660 ⇒ ∡ G O B ≡ ∡ G' O' B'
662 OrderedCongruentAngles
663 |- ∀ A O B A' O' B' G.
664 ¬Collinear A' O' B' ∧ ∡ A O B ≡ ∡ A' O' B' ∧
666 ⇒ ∃ G'. G' ∈ int_angle A' O' B' ∧ ∡ A O G ≡ ∡ A' O' G'
669 |- ∀ A O B A' O' B' G G'.
670 G ∈ int_angle A O B ∧ G' ∈ int_angle A' O' B' ∧
671 ∡ A O G ≡ ∡ A' O' G' ∧ ∡ G O B ≡ ∡ G' O' B' ∧
672 ⇒ ∡ A O B ≡ ∡ A' O' B'
676 Angle α ∧ ¬Collinear A O B ∧ α <_ang ∡ A O B
677 ⇒ (∃ G. G ∈ int_angle A O B ∧ α ≡ ∡ A O G)
680 |- ∀ α β. α <_ang β ⇒ ¬(α ≡ β)
684 α <_ang β ∧ Angle γ ∧ β ≡ γ
687 AngleOrderTransitivity
689 α <_ang β ∧ β <_ang γ
695 ⇒ (α ≡ β ∨ α <_ang β ∨ β <_ang α) ∧
696 ¬(α ≡ β ∧ α <_ang β) ∧
697 ¬(α ≡ β ∧ β <_ang α) ∧
698 ¬(α <_ang β ∧ β <_ang α)
701 |- ∀ α. Angle α ⇒ ∃ α'. α suppl α'
703 SupplementImpliesAngle
704 |- ∀ α β. α suppl β ⇒ Angle α ∧ Angle β
706 RightImpliesAngle |- ∀ α. Right α ⇒ Angle α
709 |- ∀ α β. α suppl β ⇒ β suppl α
711 SupplementsCongAnglesCong
713 α suppl α' ∧ β suppl β' ∧ α ≡ β
718 α suppl β ∧ α suppl β' ⇒ β ≡ β'
720 CongRightImpliesRight
722 Angle α ∧ Right β ∧ α ≡ β ⇒ Right α
724 RightAnglesCongruentHelp
726 ¬Collinear A O B ∧ O ∈ open (A,A')
727 Right (∡ A O B) ∧ Right (∡ A O P)
728 ⇒ P ∉ int_angle A O B
731 |- ∀ α β. Right α ∧ Right β ⇒ α ≡ β
733 OppositeRightAnglesLinear
735 ¬Collinear A O H ∧ ¬Collinear H O B ∧
736 Right (∡ A O H) ∧ Right (∡ H O B) ∧
737 Line h ∧ O ∈ h ∧ H ∈ h ∧ ¬(A,B same_side h)
740 RightImpliesSupplRight
742 ¬Collinear A O B ∧ O ∈ open (A,A') ∧ Right (∡ A O B)
745 IsoscelesCongBaseAngles
747 ¬Collinear A B C ∧ seg B A ≡ seg B C
752 Angle α ∧ ¬(O = A) ∧ ¬(P = Q) ∧
753 Line l ∧ O ∈ l ∧ A ∈ l ∧ Y ∉ l
754 ⇒ ∃ N. ¬(O = N) ∧ N ∉ l ∧ N,Y same_side l ∧
755 seg O N ≡ seg P Q ∧ ∡ A O N ≡ α
759 Angle α ∧ ¬(O = A) ∧ ¬(P = Q) ∧
760 Line l ∧ O ∈ l ∧ A ∈ l ∧ Z ∉ l
761 ⇒ ∃ N. ¬(O = N) ∧ N ∉ l ∧ ¬(Z,N same_side l) ∧
762 seg O N ≡ seg P Q ∧ ∡ A O N ≡ α
766 ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
767 seg A B ≡ seg A' B' ∧ seg A C ≡ seg A' C' ∧ seg B C ≡ seg B' C'
773 ⇒ ∃ F. F ∈ int_angle B A C ∧ ∡ B A F ≡ ∡ F A C
777 ¬Collinear A B C ∧ ∡ B A C ≡ ∡ B C A
781 |- ∀ A B. ¬(A = B) ⇒ ∃ D. ¬Collinear A D B ∧ seg D A ≡ seg D B
784 |- ∀ A B. ¬(A = B) ⇒ ∃ M. M ∈ open (A,B) ∧ seg A M ≡ seg M B
786 EuclidPropositionI_7short
788 ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a ∧ ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧
789 C,D same_side a ∧ seg A C ≡ seg A D
790 ⇒ ¬(seg B C ≡ seg B D)
794 ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a ∧ ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧
795 C,D same_side a ∧ seg A C ≡ seg A D ∧
796 (C ∈ int_triangle D A B ∨ ConvexQuadrilateral A B C D)
797 ⇒ ¬(seg B C ≡ seg B D)
801 ¬(A = B) ∧ Line a ∧ A ∈ a ∧ B ∈ a ∧ ¬(C = D) ∧ C ∉ a ∧ D ∉ a ∧
802 C,D same_side a ∧ seg A C ≡ seg A D
803 ⇒ ¬(seg B C ≡ seg B D)
805 EuclidPropositionI_11
806 |- ∀A B. ¬(A = B) ⇒ ∃ F. Right (∡ A B F)
808 DropPerpendicularToLine
811 ⇒ ∃ E Q. E ∈ l ∧ Q ∈ l ∧ Right (∡ P Q E)
813 EuclidPropositionI_14
815 Line l ∧ A ∈ l ∧ B ∈ l ∧ ¬(A = B) ∧
816 C ∉ l ∧ D ∉ l ∧ ¬(C,D same_side l) ∧
817 ∡ C B A suppl ∡ A B D
822 ¬Collinear A O B ∧ O ∈ open (A,A') ∧ O ∈ open (B,B')
823 ⇒ ∡ B O A' ≡ ∡ B' O A
825 EuclidPropositionI_16
827 ¬Collinear A B C ∧ C ∈ open (B,D)
828 ⇒ ∡ B A C <_ang ∡ D C A
832 ¬Collinear A B C ∧ C ∈ open (B,D)
833 ⇒ ∡ A B C <_ang ∡ A C D
835 EuclidPropositionI_17
837 ¬Collinear A B C ∧ α = ∡ A B C ∧ β = ∡ B C A ∧ β suppl γ
840 EuclidPropositionI_18
842 ¬Collinear A B C ∧ seg A C <__ seg A B
843 ⇒ ∡ A B C <_ang ∡ B C A
845 EuclidPropositionI_19
847 ¬Collinear A B C ∧ ∡ A B C <_ang ∡ B C A
848 ⇒ seg A C <__ seg A B
850 EuclidPropositionI_20
852 ¬Collinear A B C ∧ A ∈ open (B,D) ∧ seg A D ≡ seg A C
853 ⇒ seg B C <__ seg B D
855 EuclidPropositionI_21
857 ¬Collinear A B C ∧ D ∈ int_triangle A B C
858 ⇒ ∡ A B C <_ang ∡ C D A
862 α <_ang β ∧ Angle γ ∧ γ ≡ α
865 InteriorCircleConvexHelp
867 ¬Collinear A O C ∧ B ∈ open (A,C) ∧
868 seg O A <__ seg O C ∨ seg O A ≡ seg O C
869 ⇒ seg O B <__ seg O C
873 ¬(O = R) ∧ B ∈ open (A,C) ∧
874 A ∈ int_circle O R ∧ C ∈ int_circle O R
878 |- ∀ s t u. s <__ t ∧ Segment u ∧ u ≡ s ⇒ u <__ t
880 EuclidPropositionI_24Help
882 ¬Collinear A O C ∧ ¬Collinear D O' F ∧
883 seg O' D ≡ seg O A ∧ seg O' F ≡ seg O C ∧
884 ∡ D O' F <_ang ∡ A O C ∧
885 seg O A <__ seg O C ∨ seg O A ≡ seg O C
886 ⇒ seg D F <__ seg A C
888 EuclidPropositionI_24
890 ¬Collinear A O C ∧ ¬Collinear D O' F ∧
891 seg O' D ≡ seg O A ∧ seg O' F ≡ seg O C ∧
892 ∡ D O' F <_ang ∡ A O C
893 ⇒ seg D F <__ seg A C
895 EuclidPropositionI_25
897 ¬Collinear A O C ∧ ¬Collinear D O' F ∧
898 seg O' D ≡ seg O A ∧ seg O' F ≡ seg O C ∧
900 ⇒ ∡ D O' F <_ang ∡ A O C
904 ¬Collinear A B C ∧ ¬Collinear A' B' C' ∧
905 ∡ A B C ≡ ∡ A' B' C' ∧ ∡ B C A ≡ ∡ B' C' A' ∧
909 ParallelSymmetry |- ∀ l k. l ∥ k ⇒ k ∥ l
911 AlternateInteriorAngles
913 Line l ∧ A ∈ l ∧ E ∈ l ∧
914 Line m ∧ B ∈ m ∧ C ∈ m ∧
915 Line t ∧ A ∈ t ∧ B ∈ t ∧
916 ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t ∧
917 ¬(C,E same_side t) ∧ ∡ E A B ≡ ∡ C B A
920 EuclidPropositionI_28
921 |- ∀ A B C D E F G H l m t.
922 Line l ∧ A ∈ l ∧ B ∈ l ∧ G ∈ l ∧
923 Line m ∧ C ∈ m ∧ D ∈ m ∧ H ∈ m ∧
924 Line t ∧ G ∈ t ∧ H ∈ t ∧ G ∉ m ∧ H ∉ l ∧
925 G ∈ open (A,B) ∧ H ∈ open (C,D) ∧
926 G ∈ open (E,H) ∧ H ∈ open (F,G) ∧ ¬(D,A same_side t) ∧
927 ∡ E G B ≡ ∡ G H D ∨ ∡ B G H suppl ∡ G H D
930 OppositeSidesCongImpliesParallelogram
932 Quadrilateral A B C D ∧
933 seg A B ≡ seg C D ∧ seg B C ≡ seg D A
934 ⇒ Parallelogram A B C D
936 OppositeAnglesCongImpliesParallelogramHelp
938 Quadrilateral A B C D ∧
939 ∡ A B C ≡ ∡ C D A ∧ ∡ D A B ≡ ∡ B C D ∧
940 Line a ∧ A ∈ a ∧ B ∈ a ∧ Line c ∧ C ∈ c ∧ D ∈ c
943 OppositeAnglesCongImpliesParallelogram
945 Quadrilateral A B C D ∧
946 ∡ A B C ≡ ∡ C D A ∧ ∡ D A B ≡ ∡ B C D
947 ⇒ Parallelogram A B C D
950 P |- ∀ P l. Line l ∧ P ∉ l ⇒ ∃! m. Line m ∧ P ∈ m ∧ m ∥ l
952 AMa |- ∀ α. Angle α ⇒ &0 < μ α ∧ μ α < &180
954 AMb |- ∀ α. Right α ⇒ μ α = &90
956 AMc |- ∀ α β. Angle α ∧ Angle β ∧ α ≡ β ⇒ μ α = μ β
958 AMd |- ∀ A O B P. P ∈ int_angle A O B
959 ⇒ μ (∡ A O B) = μ (∡ A O P) + μ (∡ P O B)
962 ConverseAlternateInteriorAngles
964 Line l ∧ A ∈ l ∧ E ∈ l ∧
965 Line m ∧ B ∈ m ∧ C ∈ m ∧
966 Line t ∧ A ∈ t ∧ B ∈ t ∧
967 ¬(A = E) ∧ ¬(B = C) ∧ ¬(A = B) ∧ E ∉ t ∧ C ∉ t ∧
968 ¬(C,E same_side t) ∧ l ∥ m
975 B ∈ open (E,F) ∧ C ∈ int_angle A B F ∧
976 ∡ E B A ≡ ∡ C A B ∧ ∡ C B F ≡ ∡ B C A
978 EuclidPropositionI_13
980 ¬Collinear A O B ∧ O ∈ open (A,A')
981 ⇒ μ (∡ A O B) + μ (∡ B O A') = &180
986 ⇒ μ (∡ A B C) + μ (∡ B C A) + μ (∡ C A B) = &180