(* ========================================================================= *) (* HOL Light Hilbert geometry axiomatic proofs *) (* *) (* (c) Copyright, Bill Richter 2013 *) (* Distributed under the same license as HOL Light *) (* *) (* High school students can learn rigorous axiomatic geometry proofs, as in *) (* http://www.math.northwestern.edu/~richter/hilbert.pdf, using Hilbert's *) (* axioms, and code up readable formal proofs like these here. Thanks to the *) (* Mizar folks for their influential language, Freek Wiedijk for his dialect *) (* miz3 of HOL Light, John Harrison for explaining how to port Mizar code to *) (* miz3 and writing the first 100+ lines of code here, the hol-info list for *) (* explaining features of HOL, and Benjamin Kordesh for carefully reading *) (* much of the paper and the code. Formal proofs are given for the first 7 *) (* sections of the paper, the results cited there from Greenberg's book, and *) (* most of Euclid's book I propositions up to Proposition I.29, following *) (* Hartshorne, whose book seems the most exciting axiomatic geometry text. *) (* A proof assistant is an invaluable tool to help read it, as Hartshorne's *) (* proofs are often sketchy and even have gaps. *) (* *) (* M. Greenberg, Euclidean and non-Euclidean geometries, Freeman, 1974. *) (* R. Hartshorne, Geometry, Euclid and Beyond, UTM series, Springer, 2000. *) (* ========================================================================= *) needs "RichterHilbertAxiomGeometry/readable.ml";; new_type("point", 0);; NewConstant("Between", `:point->point->point->bool`);; NewConstant("Line", `:(point->bool)->bool`);; NewConstant("â‰¡", `:(point->bool)->(point->bool)->bool`);; ParseAsInfix("â‰…", (12, "right"));; ParseAsInfix("same_side", (12, "right"));; ParseAsInfix("â‰¡", (12, "right"));; ParseAsInfix("<__", (12, "right"));; ParseAsInfix("<_ang", (12, "right"));; ParseAsInfix("suppl", (12, "right"));; ParseAsInfix("âˆ‰", (11, "right"));; ParseAsInfix("âˆ¥", (12, "right"));; let NOTIN = NewDefinition `; âˆ€a l. a âˆ‰ l â‡” Â¬(a âˆˆ l)`;; let INTER_TENSOR = theorem `; âˆ€s s' t t'. s âŠ‚ s' âˆ§ t âŠ‚ t' â‡’ s âˆ© t âŠ‚ s' âˆ© t' by set`;; let Interval_DEF = NewDefinition `; âˆ€A B. Open (A, B) = {X | Between A X B}`;; let Collinear_DEF = NewDefinition `; Collinear A B C â‡” âˆƒl. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l`;; let SameSide_DEF = NewDefinition `; A,B same_side l â‡” Line l âˆ§ Â¬ âˆƒX. X âˆˆ l âˆ§ X âˆˆ Open (A, B)`;; let Ray_DEF = NewDefinition `; âˆ€A B. ray A B = {X | Â¬(A = B) âˆ§ Collinear A B X âˆ§ A âˆ‰ Open (X, B)}`;; let Ordered_DEF = NewDefinition `; ordered A B C D â‡” B âˆˆ Open (A, C) âˆ§ B âˆˆ Open (A, D) âˆ§ C âˆˆ Open (A, D) âˆ§ C âˆˆ Open (B, D)`;; let InteriorAngle_DEF = NewDefinition `; âˆ€A O B. int_angle A O B = {P | Â¬Collinear A O B âˆ§ âˆƒa b. Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ P âˆ‰ a âˆ§ P âˆ‰ b âˆ§ P,B same_side a âˆ§ P,A same_side b}`;; let InteriorTriangle_DEF = NewDefinition `; âˆ€A B C. int_triangle A B C = {P | P âˆˆ int_angle A B C âˆ§ P âˆˆ int_angle B C A âˆ§ P âˆˆ int_angle C A B}`;; let Tetralateral_DEF = NewDefinition `; Tetralateral A B C D â‡” Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬(C = D) âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B`;; let Quadrilateral_DEF = NewDefinition `; Quadrilateral A B C D â‡” Tetralateral A B C D âˆ§ Open (A, B) âˆ© Open (C, D) = âˆ… âˆ§ Open (B, C) âˆ© Open (D, A) = âˆ…`;; let ConvexQuad_DEF = NewDefinition `; ConvexQuadrilateral A B C D â‡” Quadrilateral A B C D âˆ§ A âˆˆ int_angle B C D âˆ§ B âˆˆ int_angle C D A âˆ§ C âˆˆ int_angle D A B âˆ§ D âˆˆ int_angle A B C`;; let Segment_DEF = NewDefinition `; seg A B = {A, B} âˆª Open (A, B)`;; let SEGMENT = NewDefinition `; Segment s â‡” âˆƒA B. s = seg A B âˆ§ Â¬(A = B)`;; let SegmentOrdering_DEF = NewDefinition `; s <__ t â‡” Segment s âˆ§ âˆƒC D X. t = seg C D âˆ§ X âˆˆ Open (C, D) âˆ§ s â‰¡ seg C X`;; let Angle_DEF = NewDefinition `; âˆ¡ A O B = ray O A âˆª ray O B`;; let ANGLE = NewDefinition `; Angle Î± â‡” âˆƒA O B. Î± = âˆ¡ A O B âˆ§ Â¬Collinear A O B`;; let AngleOrdering_DEF = NewDefinition `; Î± <_ang Î² â‡” Angle Î± âˆ§ âˆƒA O B G. Â¬Collinear A O B âˆ§ Î² = âˆ¡ A O B âˆ§ G âˆˆ int_angle A O B âˆ§ Î± â‰¡ âˆ¡ A O G`;; let RAY = NewDefinition `; Ray r â‡” âˆƒO A. Â¬(O = A) âˆ§ r = ray O A`;; let TriangleCong_DEF = NewDefinition `; âˆ€A B C A' B' C'. (A, B, C) â‰… (A', B', C') â‡” Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' âˆ§ seg A B â‰¡ seg A' B' âˆ§ seg A C â‰¡ seg A' C' âˆ§ seg B C â‰¡ seg B' C' âˆ§ âˆ¡ A B C â‰¡ âˆ¡ A' B' C' âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B' C' A' âˆ§ âˆ¡ C A B â‰¡ âˆ¡ C' A' B'`;; let SupplementaryAngles_DEF = NewDefinition `; âˆ€Î± Î². Î± suppl Î² â‡” âˆƒA O B A'. Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î² = âˆ¡ B O A'`;; let RightAngle_DEF = NewDefinition `; âˆ€Î±. Right Î± â‡” âˆƒÎ². Î± suppl Î² âˆ§ Î± â‰¡ Î²`;; let PlaneComplement_DEF = NewDefinition `; âˆ€Î±. complement Î± = {P | P âˆ‰ Î±}`;; let CONVEX = NewDefinition `; Convex Î± â‡” âˆ€A B. A âˆˆ Î± âˆ§ B âˆˆ Î± â‡’ Open (A, B) âŠ‚ Î±`;; let PARALLEL = NewDefinition `; âˆ€l k. l âˆ¥ k â‡” Line l âˆ§ Line k âˆ§ l âˆ© k = âˆ…`;; let Parallelogram_DEF = NewDefinition `; âˆ€A B C D. Parallelogram A B C D â‡” Quadrilateral A B C D âˆ§ âˆƒa b c d. Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a âˆ§ Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b âˆ§ Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ d âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d âˆ§ a âˆ¥ c âˆ§ b âˆ¥ d`;; let InteriorCircle_DEF = NewDefinition `; âˆ€O R. int_circle O R = {P | Â¬(O = R) âˆ§ (P = O âˆ¨ seg O P <__ seg O R)} `;; (* ------------------------------------------------------------------------- *) (* Hilbert's geometry axioms, except the parallel axiom P, defined later. *) (* ------------------------------------------------------------------------- *) let I1 = NewAxiom `;âˆ€A B. Â¬(A = B) â‡’ âˆƒ! l. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l`;; let I2 = NewAxiom `;âˆ€l. Line l â‡’ âˆƒA B. A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B)`;; let I3 = NewAxiom `;âˆƒA B C. Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear A B C`;; let B1 = NewAxiom `;âˆ€A B C. Between A B C â‡’ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Between C B A âˆ§ Collinear A B C`;; let B2 = NewAxiom `;âˆ€A B. Â¬(A = B) â‡’ âˆƒC. Between A B C`;; let B3 = NewAxiom `;âˆ€A B C. Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Collinear A B C â‡’ (Between A B C âˆ¨ Between B C A âˆ¨ Between C A B) âˆ§ Â¬(Between A B C âˆ§ Between B C A) âˆ§ Â¬(Between A B C âˆ§ Between C A B) âˆ§ Â¬(Between B C A âˆ§ Between C A B)`;; let B4 = NewAxiom `;âˆ€l A B C. Line l âˆ§ Â¬Collinear A B C âˆ§ A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l âˆ§ (âˆƒX. X âˆˆ l âˆ§ Between A X C) â‡’ (âˆƒY. Y âˆˆ l âˆ§ Between A Y B) âˆ¨ (âˆƒY. Y âˆˆ l âˆ§ Between B Y C)`;; let C1 = NewAxiom `;âˆ€s O Z. Segment s âˆ§ Â¬(O = Z) â‡’ âˆƒ! P. P âˆˆ ray O Z â” {O} âˆ§ seg O P â‰¡ s`;; let C2Reflexive = NewAxiom `;Segment s â‡’ s â‰¡ s`;; let C2Symmetric = NewAxiom `;Segment s âˆ§ Segment t âˆ§ s â‰¡ t â‡’ t â‰¡ s`;; let C2Transitive = NewAxiom `;Segment s âˆ§ Segment t âˆ§ Segment u âˆ§ s â‰¡ t âˆ§ t â‰¡ u â‡’ s â‰¡ u`;; let C3 = NewAxiom `;âˆ€A B C A' B' C'. B âˆˆ Open (A, C) âˆ§ B' âˆˆ Open (A', C') âˆ§ seg A B â‰¡ seg A' B' âˆ§ seg B C â‰¡ seg B' C' â‡’ seg A C â‰¡ seg A' C'`;; let C4 = NewAxiom `;âˆ€Î± O A l Y. Angle Î± âˆ§ Â¬(O = A) âˆ§ Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ Y âˆ‰ l â‡’ âˆƒ! r. Ray r âˆ§ âˆƒB. Â¬(O = B) âˆ§ r = ray O B âˆ§ B âˆ‰ l âˆ§ B,Y same_side l âˆ§ âˆ¡ A O B â‰¡ Î±`;; let C5Reflexive = NewAxiom `;Angle Î± â‡’ Î± â‰¡ Î±`;; let C5Symmetric = NewAxiom `;Angle Î± âˆ§ Angle Î² âˆ§ Î± â‰¡ Î² â‡’ Î² â‰¡ Î±`;; let C5Transitive = NewAxiom `;Angle Î± âˆ§ Angle Î² âˆ§ Angle Î³ âˆ§ Î± â‰¡ Î² âˆ§ Î² â‰¡ Î³ â‡’ Î± â‰¡ Î³`;; let C6 = NewAxiom `;âˆ€A B C A' B' C'. Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' âˆ§ seg B A â‰¡ seg B' A' âˆ§ seg B C â‰¡ seg B' C' âˆ§ âˆ¡ A B C â‰¡ âˆ¡ A' B' C' â‡’ âˆ¡ B C A â‰¡ âˆ¡ B' C' A'`;; (* ----------------------------------------------------------------- *) (* Theorems. *) (* ----------------------------------------------------------------- *) let IN_Interval = theorem `; âˆ€A B X. X âˆˆ Open (A, B) â‡” Between A X B by rewrite Interval_DEF IN_ELIM_THM`;; let IN_Ray = theorem `; âˆ€A B X. X âˆˆ ray A B â‡” Â¬(A = B) âˆ§ Collinear A B X âˆ§ A âˆ‰ Open (X, B) by rewrite Ray_DEF IN_ELIM_THM`;; let IN_InteriorAngle = theorem `; âˆ€A O B P. P âˆˆ int_angle A O B â‡” Â¬Collinear A O B âˆ§ âˆƒa b. Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ P âˆ‰ a âˆ§ P âˆ‰ b âˆ§ P,B same_side a âˆ§ P,A same_side b by rewrite InteriorAngle_DEF IN_ELIM_THM`;; let IN_InteriorTriangle = theorem `; âˆ€A B C P. P âˆˆ int_triangle A B C â‡” P âˆˆ int_angle A B C âˆ§ P âˆˆ int_angle B C A âˆ§ P âˆˆ int_angle C A B by rewrite InteriorTriangle_DEF IN_ELIM_THM`;; let IN_PlaneComplement = theorem `; âˆ€Î±. âˆ€P. P âˆˆ complement Î± â‡” P âˆ‰ Î± by rewrite PlaneComplement_DEF IN_ELIM_THM`;; let IN_InteriorCircle = theorem `; âˆ€O R P. P âˆˆ int_circle O R â‡” Â¬(O = R) âˆ§ (P = O âˆ¨ seg O P <__ seg O R) by rewrite InteriorCircle_DEF IN_ELIM_THM`;; let B1' = theorem `; âˆ€A B C. B âˆˆ Open (A, C) â‡’ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ B âˆˆ Open (C, A) âˆ§ Collinear A B C by fol IN_Interval B1`;; let B2' = theorem `; âˆ€A B. Â¬(A = B) â‡’ âˆƒC. B âˆˆ Open (A, C) by fol IN_Interval B2`;; let B3' = theorem `; âˆ€A B C. Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Collinear A B C â‡’ (B âˆˆ Open (A, C) âˆ¨ C âˆˆ Open (B, A) âˆ¨ A âˆˆ Open (C, B)) âˆ§ Â¬(B âˆˆ Open (A, C) âˆ§ C âˆˆ Open (B, A)) âˆ§ Â¬(B âˆˆ Open (A, C) âˆ§ A âˆˆ Open (C, B)) âˆ§ Â¬(C âˆˆ Open (B, A) âˆ§ A âˆˆ Open (C, B)) by fol IN_Interval B3`;; let B4' = theorem `; âˆ€l A B C. Line l âˆ§ Â¬Collinear A B C âˆ§ A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l âˆ§ (âˆƒX. X âˆˆ l âˆ§ X âˆˆ Open (A, C)) â‡’ (âˆƒY. Y âˆˆ l âˆ§ Y âˆˆ Open (A, B)) âˆ¨ (âˆƒY. Y âˆˆ l âˆ§ Y âˆˆ Open (B, C)) by rewrite IN_Interval B4`;; let B4'' = theorem `; âˆ€l A B C. Line l âˆ§ Â¬Collinear A B C âˆ§ A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l âˆ§ A,B same_side l âˆ§ B,C same_side l â‡’ A,C same_side l proof rewrite SameSide_DEF; fol B4'; qed; `;; let DisjointOneNotOther = theorem `; âˆ€l m. (âˆ€x:A. x âˆˆ m â‡’ x âˆ‰ l) â‡” l âˆ© m = âˆ… by fol âˆ‰ IN_INTER MEMBER_NOT_EMPTY`;; let EquivIntersectionHelp = theorem `; âˆ€e x:A. âˆ€l m:A->bool. (l âˆ© m = {x} âˆ¨ m âˆ© l = {x}) âˆ§ e âˆˆ m â” {x} â‡’ e âˆ‰ l by fol âˆ‰ IN_INTER IN_SING IN_DIFF`;; let CollinearSymmetry = theorem `; âˆ€A B C. Collinear A B C â‡’ Collinear A C B âˆ§ Collinear B A C âˆ§ Collinear B C A âˆ§ Collinear C A B âˆ§ Collinear C B A proof intro_TAC âˆ€A B C, H1; consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l [l_line] by fol H1 Collinear_DEF; fol - Collinear_DEF; qed; `;; let ExistsNewPointOnLine = theorem `; âˆ€P. Line l âˆ§ P âˆˆ l â‡’ âˆƒQ. Q âˆˆ l âˆ§ Â¬(P = Q) proof intro_TAC âˆ€P, H1; consider A B such that A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B) [l_line] by fol H1 I2; fol - l_line; qed; `;; let ExistsPointOffLine = theorem `; âˆ€l. Line l â‡’ âˆƒQ. Q âˆ‰ l proof intro_TAC âˆ€l, H1; consider A B C such that Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear A B C [Distinct] by fol I3; assume (A âˆˆ l) âˆ§ (B âˆˆ l) âˆ§ (C âˆˆ l) [all_on] by fol âˆ‰; Collinear A B C [] by fol H1 - Collinear_DEF; fol - Distinct; qed; `;; let BetweenLinear = theorem `; âˆ€A B C m. Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m âˆ§ (B âˆˆ Open (A, C) âˆ¨ C âˆˆ Open (B, A) âˆ¨ A âˆˆ Open (C, B)) â‡’ B âˆˆ m proof intro_TAC âˆ€A B C m, H1m H1A H1C H2; Â¬(A = C) âˆ§ (Collinear A B C âˆ¨ Collinear B C A âˆ¨ Collinear C A B) [X1] by fol H2 B1'; consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l [X2] by fol - Collinear_DEF; l = m [] by fol X1 - H2 H1m H1A H1C I1; fol - X2; qed; `;; let CollinearLinear = theorem `; âˆ€A B C m. Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m âˆ§ (Collinear A B C âˆ¨ Collinear B C A âˆ¨ Collinear C A B) âˆ§ Â¬(A = C) â‡’ B âˆˆ m proof intro_TAC âˆ€A B C m, H1m H1A H1C H2 H3; consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l [X1] by fol H2 Collinear_DEF; l = m [] by fol H3 - H1m H1A H1C I1; fol - X1; qed; `;; let NonCollinearImpliesDistinct = theorem `; âˆ€A B C. Â¬Collinear A B C â‡’ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) proof intro_TAC âˆ€A B C, H1; assume A = B âˆ§ B = C [equal] by fol H1 I1 Collinear_DEF; consider Q such that Â¬(Q = A) [notQA] by fol I3; fol - equal H1 I1 Collinear_DEF; qed; `;; let NonCollinearRaa = theorem `; âˆ€A B C l. Â¬(A = C) â‡’ Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l â‡’ B âˆ‰ l â‡’ Â¬Collinear A B C proof intro_TAC âˆ€A B C l, Distinct, l_line, notBl; assume Collinear A B C [ANCcol] by fol; consider m such that Line m âˆ§ A âˆˆ m âˆ§ B âˆˆ m âˆ§ C âˆˆ m [m_line] by fol - Collinear_DEF; m = l [] by fol - l_line Distinct I1; B âˆˆ l [] by fol m_line -; fol - notBl âˆ‰; qed; `;; let TwoSidesTriangle1Intersection = theorem `; âˆ€A B C Y. Â¬Collinear A B C âˆ§ Collinear B C Y âˆ§ Collinear A C Y â‡’ Y = C proof intro_TAC âˆ€A B C Y, ABCcol BCYcol ACYcol; assume Â¬(C = Y) [notCY] by fol; consider l such that Line l âˆ§ C âˆˆ l âˆ§ Y âˆˆ l [l_line] by fol - I1; B âˆˆ l âˆ§ A âˆˆ l [] by fol - BCYcol ACYcol Collinear_DEF notCY I1; fol - l_line Collinear_DEF ABCcol; qed; `;; let OriginInRay = theorem `; âˆ€O Q. Â¬(Q = O) â‡’ O âˆˆ ray O Q proof intro_TAC âˆ€O Q, H1; O âˆ‰ Open (O, Q) [OOQ] by fol B1' âˆ‰; Collinear O Q O [] by fol H1 I1 Collinear_DEF; fol H1 - OOQ IN_Ray; qed; `;; let EndpointInRay = theorem `; âˆ€O Q. Â¬(Q = O) â‡’ Q âˆˆ ray O Q proof intro_TAC âˆ€O Q, H1; O âˆ‰ Open (Q, Q) [notOQQ] by fol B1' âˆ‰; Collinear O Q Q [] by fol H1 I1 Collinear_DEF; fol H1 - notOQQ IN_Ray; qed; `;; let I1Uniqueness = theorem `; âˆ€X l m. Line l âˆ§ Line m âˆ§ Â¬(l = m) âˆ§ X âˆˆ l âˆ§ X âˆˆ m â‡’ l âˆ© m = {X} proof intro_TAC âˆ€X l m, H0l H0m H1 H2l H2m; assume Â¬(l âˆ© m = {X}) [H3] by fol; consider A such that A âˆˆ l âˆ© m âˆ§ Â¬(A = X) [X1] by fol H2l H2m IN_INTER H3 EXTENSION IN_SING; fol H0l H0m H2l H2m IN_INTER X1 I1 H1; qed; `;; let DisjointLinesImplySameSide = theorem `; âˆ€l m A B. Line l âˆ§ Line m âˆ§ A âˆˆ m âˆ§ B âˆˆ m âˆ§ l âˆ© m = âˆ… â‡’ A,B same_side l proof intro_TAC âˆ€l m A B, l_line m_line Am Bm lm0; l âˆ© Open (A,B) = âˆ… [] by fol Am Bm m_line BetweenLinear SUBSET lm0 SUBSET_REFL INTER_TENSOR SUBSET_EMPTY; fol l_line - SameSide_DEF SUBSET IN_INTER MEMBER_NOT_EMPTY; qed; `;; let EquivIntersection = theorem `; âˆ€A B X l m. Line l âˆ§ Line m âˆ§ l âˆ© m = {X} âˆ§ A âˆˆ m â” {X} âˆ§ B âˆˆ m â” {X} âˆ§ X âˆ‰ Open (A, B) â‡’ A,B same_side l proof intro_TAC âˆ€A B X l m, l_line m_line H1 H2l H2m H3; Open (A, B) âŠ‚ m [] by fol l_line m_line SUBSET_DIFF IN_DIFF IN_SING H2l H2m BetweenLinear SUBSET; l âˆ© Open (A, B) âŠ‚ {X} [] by fol - H1 SUBSET_REFL INTER_TENSOR; l âˆ© Open (A, B) âŠ‚ âˆ… [] by fol - SUBSET IN_SING IN_INTER H3 âˆ‰; fol l_line - SameSide_DEF SUBSET IN_INTER NOT_IN_EMPTY; qed; `;; let RayLine = theorem `; âˆ€O P l. Line l âˆ§ O âˆˆ l âˆ§ P âˆˆ l â‡’ ray O P âŠ‚ l by fol IN_Ray CollinearLinear SUBSET`;; let RaySameSide = theorem `; âˆ€l O A P. Line l âˆ§ O âˆˆ l âˆ§ A âˆ‰ l âˆ§ P âˆˆ ray O A â” {O} â‡’ P âˆ‰ l âˆ§ P,A same_side l proof intro_TAC âˆ€l O A P, l_line Ol notAl PrOA; Â¬(O = A) [notOA] by fol l_line Ol notAl âˆ‰; consider d such that Line d âˆ§ O âˆˆ d âˆ§ A âˆˆ d [d_line] by fol notOA I1; Â¬(l = d) [] by fol - notAl âˆ‰; l âˆ© d = {O} [ldO] by fol l_line Ol d_line - I1Uniqueness; A âˆˆ d â” {O} [Ad_O] by fol d_line notOA IN_DIFF IN_SING; ray O A âŠ‚ d [] by fol d_line RayLine; P âˆˆ d â” {O} [Pd_O] by fol PrOA - SUBSET IN_DIFF IN_SING; P âˆ‰ l [notPl] by fol ldO - EquivIntersectionHelp; O âˆ‰ Open (P, A) [] by fol PrOA IN_DIFF IN_SING IN_Ray; P,A same_side l [] by fol l_line Ol d_line ldO Ad_O Pd_O - EquivIntersection; fol notPl -; qed; `;; let IntervalRayEZ = theorem `; âˆ€A B C. B âˆˆ Open (A, C) â‡’ B âˆˆ ray A C â” {A} âˆ§ C âˆˆ ray A B â” {A} proof intro_TAC âˆ€A B C, H1; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Collinear A B C [ABC] by fol H1 B1'; A âˆ‰ Open (B, C) âˆ§ A âˆ‰ Open (C, B) [] by fol - H1 B3' B1' âˆ‰; fol ABC - CollinearSymmetry IN_Ray âˆ‰ IN_DIFF IN_SING; qed; `;; let NoncollinearityExtendsToLine = theorem `; âˆ€A O B X. Â¬Collinear A O B â‡’ Collinear O B X âˆ§ Â¬(X = O) â‡’ Â¬Collinear A O X proof intro_TAC âˆ€A O B X, H1, H2; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) [Distinct] by fol H1 NonCollinearImpliesDistinct; consider b such that Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [b_line] by fol Distinct I1; A âˆ‰ b [notAb] by fol b_line H1 Collinear_DEF âˆ‰; X âˆˆ b [] by fol H2 b_line Distinct I1 Collinear_DEF; fol b_line - H2 notAb I1 Collinear_DEF âˆ‰; qed; `;; let SameSideReflexive = theorem `; âˆ€l A. Line l âˆ§ A âˆ‰ l â‡’ A,A same_side l by fol B1' SameSide_DEF`;; let SameSideSymmetric = theorem `; âˆ€l A B. Line l âˆ§ A âˆ‰ l âˆ§ B âˆ‰ l â‡’ A,B same_side l â‡’ B,A same_side l by fol SameSide_DEF B1'`;; let SameSideTransitive = theorem `; âˆ€l A B C. Line l â‡’ A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l â‡’ A,B same_side l â‡’ B,C same_side l â‡’ A,C same_side l proof intro_TAC âˆ€l A B C, l_line, notABCl, Asim_lB, Bsim_lC; assume Collinear A B C âˆ§ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [Distinct] by fol l_line notABCl Asim_lB Bsim_lC B4'' SameSideReflexive; consider m such that Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m [m_line] by fol Distinct I1; B âˆˆ m [Bm] by fol - Distinct CollinearLinear; assume Â¬(m âˆ© l = âˆ…) [Intersect] by fol m_line l_line BetweenLinear SameSide_DEF IN_INTER NOT_IN_EMPTY; consider X such that X âˆˆ l âˆ§ X âˆˆ m [Xlm] by fol - MEMBER_NOT_EMPTY IN_INTER; Collinear A X B âˆ§ Collinear B A C âˆ§ Collinear A B C [ABXcol] by fol m_line Bm - Collinear_DEF; consider E such that E âˆˆ l âˆ§ Â¬(E = X) [El_X] by fol l_line Xlm ExistsNewPointOnLine; Â¬Collinear E A X [EAXncol] by fol l_line El_X Xlm notABCl I1 Collinear_DEF âˆ‰; consider B' such that Â¬(B = E) âˆ§ B âˆˆ Open (E, B') [EBB'] by fol notABCl El_X âˆ‰ B2'; Â¬(B' = E) âˆ§ Â¬(B' = B) âˆ§ Collinear B E B' [EBB'col] by fol - B1' CollinearSymmetry; Â¬Collinear A B B' âˆ§ Â¬Collinear B' B A âˆ§ Â¬Collinear B' A B [ABB'ncol] by fol EAXncol ABXcol Distinct - NoncollinearityExtendsToLine CollinearSymmetry; Â¬Collinear B' B C âˆ§ Â¬Collinear B' A C âˆ§ Â¬Collinear A B' C [AB'Cncol] by fol ABB'ncol ABXcol Distinct NoncollinearityExtendsToLine CollinearSymmetry; B' âˆˆ ray E B â” {E} âˆ§ B âˆˆ ray E B' â” {E} [] by fol EBB' IntervalRayEZ; B' âˆ‰ l âˆ§ B',B same_side l âˆ§ B,B' same_side l [notB'l] by fol l_line El_X notABCl - RaySameSide; A,B' same_side l âˆ§ B',C same_side l [] by fol l_line ABB'ncol notABCl notB'l Asim_lB - AB'Cncol Bsim_lC B4''; fol l_line AB'Cncol notABCl notB'l - B4''; qed; `;; let ConverseCrossbar = theorem `; âˆ€O A B G. Â¬Collinear A O B âˆ§ G âˆˆ Open (A, B) â‡’ G âˆˆ int_angle A O B proof intro_TAC âˆ€O A B G, H1 H2; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) [Distinct] by fol H1 NonCollinearImpliesDistinct; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by fol - I1; consider b such that Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [b_line] by fol Distinct I1; consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l [l_line] by fol Distinct I1; B âˆ‰ a âˆ§ A âˆ‰ b [] by fol H1 a_line b_line Collinear_DEF âˆ‰; Â¬(a = l) âˆ§ Â¬(b = l) [] by fol - l_line âˆ‰; a âˆ© l = {A} âˆ§ b âˆ© l = {B} [alA] by fol - a_line l_line b_line I1Uniqueness; Â¬(A = G) âˆ§ Â¬(A = B) âˆ§ Â¬(G = B) [AGB] by fol H2 B1'; A âˆ‰ Open (G, B) âˆ§ B âˆ‰ Open (G, A) [notGAB] by fol H2 B3' B1' âˆ‰; G âˆˆ l [Gl] by fol l_line H2 BetweenLinear; G âˆ‰ a âˆ§ G âˆ‰ b [notGa] by fol alA Gl AGB IN_DIFF IN_SING EquivIntersectionHelp; G âˆˆ l â” {A} âˆ§ B âˆˆ l â” {A} âˆ§ G âˆˆ l â” {B} âˆ§ A âˆˆ l â” {B} [] by fol Gl l_line AGB IN_DIFF IN_SING; G,B same_side a âˆ§ G,A same_side b [] by fol a_line l_line alA - notGAB b_line EquivIntersection; fol H1 a_line b_line notGa - IN_InteriorAngle; qed; `;; let InteriorUse = theorem `; âˆ€A O B P a b. Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b â‡’ P âˆˆ int_angle A O B â‡’ P âˆ‰ a âˆ§ P âˆ‰ b âˆ§ P,B same_side a âˆ§ P,A same_side b proof intro_TAC âˆ€A O B P a b, aOAbOB, P_AOB; consider Î± Î² such that Â¬Collinear A O B âˆ§ Line Î± âˆ§ O âˆˆ Î± âˆ§ A âˆˆ Î± âˆ§ Line Î² âˆ§ O âˆˆ Î² âˆ§B âˆˆ Î² âˆ§ P âˆ‰ Î± âˆ§ P âˆ‰ Î² âˆ§ P,B same_side Î± âˆ§ P,A same_side Î² [exists] by fol P_AOB IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) [] by fol - NonCollinearImpliesDistinct; Î± = a âˆ§ Î² = b [] by fol - aOAbOB exists I1; fol - exists; qed; `;; let InteriorEZHelp = theorem `; âˆ€A O B P. P âˆˆ int_angle A O B â‡’ Â¬(P = A) âˆ§ Â¬(P = O) âˆ§ Â¬(P = B) âˆ§ Â¬Collinear A O P proof intro_TAC âˆ€A O B P, P_AOB; consider a b such that Â¬Collinear A O B âˆ§ Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§B âˆˆ b âˆ§ P âˆ‰ a âˆ§ P âˆ‰ b [def_int] by fol P_AOB IN_InteriorAngle; Â¬(P = A) âˆ§ Â¬(P = O) âˆ§ Â¬(P = B) [PnotAOB] by fol - âˆ‰; Â¬(A = O) [] by fol def_int NonCollinearImpliesDistinct; Â¬Collinear A O P [] by fol def_int - NonCollinearRaa CollinearSymmetry; fol PnotAOB -; qed; `;; let InteriorAngleSymmetry = theorem `; âˆ€A O B P: point. P âˆˆ int_angle A O B â‡’ P âˆˆ int_angle B O A proof rewrite IN_InteriorAngle; fol CollinearSymmetry; qed; `;; let InteriorWellDefined = theorem `; âˆ€A O B X P. P âˆˆ int_angle A O B âˆ§ X âˆˆ ray O B â” {O} â‡’ P âˆˆ int_angle A O X proof intro_TAC âˆ€A O B X P, H1 H2; consider a b such that Â¬Collinear A O B âˆ§ Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ P âˆ‰ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ P âˆ‰ b âˆ§ P,B same_side a âˆ§ P,A same_side b [def_int] by fol H1 IN_InteriorAngle; Â¬(X = O) âˆ§ Â¬(O = B) âˆ§ Collinear O B X [H2'] by fol H2 IN_Ray IN_DIFF IN_SING; B âˆ‰ a [notBa] by fol def_int Collinear_DEF âˆ‰; Â¬Collinear A O X [AOXnoncol] by fol def_int H2' NoncollinearityExtendsToLine; X âˆˆ b [Xb] by fol def_int H2' CollinearLinear; X âˆ‰ a âˆ§ B,X same_side a [] by fol def_int notBa H2 RaySameSide SameSideSymmetric; P,X same_side a [] by fol def_int - notBa SameSideTransitive; fol AOXnoncol def_int Xb - IN_InteriorAngle; qed; `;; let WholeRayInterior = theorem `; âˆ€A O B X P. X âˆˆ int_angle A O B âˆ§ P âˆˆ ray O X â” {O} â‡’ P âˆˆ int_angle A O B proof intro_TAC âˆ€A O B X P, XintAOB PrOX; consider a b such that Â¬Collinear A O B âˆ§ Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ X âˆ‰ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ X âˆ‰ b âˆ§ X,B same_side a âˆ§ X,A same_side b [def_int] by fol XintAOB IN_InteriorAngle; P âˆ‰ a âˆ§ P,X same_side a âˆ§ P âˆ‰ b âˆ§ P,X same_side b [Psim_abX] by fol def_int PrOX RaySameSide; P,B same_side a âˆ§ P,A same_side b [] by fol - def_int Collinear_DEF SameSideTransitive âˆ‰; fol def_int Psim_abX - IN_InteriorAngle; qed; `;; let AngleOrdering = theorem `; âˆ€O A P Q a. Â¬(O = A) â‡’ Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a â‡’ P âˆ‰ a âˆ§ Q âˆ‰ a â‡’ P,Q same_side a â‡’ Â¬Collinear P O Q â‡’ P âˆˆ int_angle Q O A âˆ¨ Q âˆˆ int_angle P O A proof intro_TAC âˆ€O A P Q a, H1, H2, H3, H4, H5; Â¬(P = O) âˆ§ Â¬(P = Q) âˆ§ Â¬(O = Q) [Distinct] by fol H5 NonCollinearImpliesDistinct; consider q such that Line q âˆ§ O âˆˆ q âˆ§ Q âˆˆ q [q_line] by fol Distinct I1; P âˆ‰ q [notPq] by fol - H5 Collinear_DEF âˆ‰; assume Â¬(P âˆˆ int_angle Q O A) [notPintQOA] by fol; Â¬Collinear Q O A âˆ§ Â¬Collinear P O A [POAncol] by fol H1 H2 H3 I1 Collinear_DEF âˆ‰; Â¬(P,A same_side q) [] by fol - H2 q_line H3 notPq H4 notPintQOA IN_InteriorAngle; consider G such that G âˆˆ q âˆ§ G âˆˆ Open (P, A) [existG] by fol q_line - SameSide_DEF; G âˆˆ int_angle P O A [G_POA] by fol POAncol existG ConverseCrossbar; G âˆ‰ a âˆ§ G,P same_side a âˆ§ Â¬(G = O) [Gsim_aP] by fol - H1 H2 IN_InteriorAngle I1 âˆ‰; G,Q same_side a [] by fol H2 Gsim_aP H3 H4 SameSideTransitive; O âˆ‰ Open (Q, G) [notQOG] by fol - H2 SameSide_DEF B1' âˆ‰; Collinear O G Q [] by fol q_line existG Collinear_DEF; Q âˆˆ ray O G â” {O} [] by fol Gsim_aP - notQOG Distinct IN_Ray IN_DIFF IN_SING; fol G_POA - WholeRayInterior; qed; `;; let InteriorsDisjointSupplement = theorem `; âˆ€A O B A'. Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') â‡’ int_angle B O A' âˆ© int_angle A O B = âˆ… proof intro_TAC âˆ€A O B A', H1 H2; âˆ€D. D âˆˆ int_angle A O B â‡’ D âˆ‰ int_angle B O A' [] proof intro_TAC âˆ€D, H3; Â¬(A = O) âˆ§ Â¬(O = B) [] by fol H1 NonCollinearImpliesDistinct; consider a b such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ A' âˆˆ a [ab_line] by fol - H2 I1 BetweenLinear; Â¬Collinear B O A' [] by fol H1 H2 CollinearSymmetry B1' NoncollinearityExtendsToLine; A âˆ‰ b âˆ§ A' âˆ‰ b [notAb] by fol ab_line H1 - Collinear_DEF âˆ‰; Â¬(A',A same_side b) [A'nsim_bA] by fol ab_line H2 B1' SameSide_DEF; D âˆ‰ b âˆ§ D,A same_side b [DintAOB] by fol ab_line H3 InteriorUse; Â¬(D,A' same_side b) [] by fol ab_line notAb DintAOB A'nsim_bA SameSideSymmetric SameSideTransitive; fol ab_line - InteriorUse âˆ‰; qed; fol - DisjointOneNotOther; qed; `;; let InteriorReflectionInterior = theorem `; âˆ€A O B D A'. O âˆˆ Open (A, A') âˆ§ D âˆˆ int_angle A O B â‡’ B âˆˆ int_angle D O A' proof intro_TAC âˆ€A O B D A', H1 H2; consider a b such that Â¬Collinear A O B âˆ§ Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ D âˆ‰ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ D âˆ‰ b âˆ§ D,B same_side a [DintAOB] by fol H2 IN_InteriorAngle; Â¬(O = B) âˆ§ Â¬(O = A') âˆ§ B âˆ‰ a [Distinct] by fol - H1 NonCollinearImpliesDistinct B1' Collinear_DEF âˆ‰; Â¬Collinear D O B [DOB_ncol] by fol DintAOB - NonCollinearRaa CollinearSymmetry; A' âˆˆ a [A'a] by fol H1 DintAOB BetweenLinear; D âˆ‰ int_angle B O A' [] by fol DintAOB H1 H2 InteriorsDisjointSupplement DisjointOneNotOther; fol Distinct DintAOB A'a DOB_ncol - AngleOrdering âˆ‰; qed; `;; let Crossbar_THM = theorem `; âˆ€O A B D. D âˆˆ int_angle A O B â‡’ âˆƒG. G âˆˆ Open (A, B) âˆ§ G âˆˆ ray O D â” {O} proof intro_TAC âˆ€O A B D, H1; consider a b such that Â¬Collinear A O B âˆ§ Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ D âˆ‰ a âˆ§ D âˆ‰ b âˆ§ D,B same_side a âˆ§ D,A same_side b [DintAOB] by fol H1 IN_InteriorAngle; B âˆ‰ a [notBa] by fol DintAOB Collinear_DEF âˆ‰; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) âˆ§ Â¬(D = O) [Distinct] by fol DintAOB NonCollinearImpliesDistinct âˆ‰; consider l such that Line l âˆ§ O âˆˆ l âˆ§ D âˆˆ l [l_line] by fol - I1; consider A' such that O âˆˆ Open (A, A') [AOA'] by fol Distinct B2'; A' âˆˆ a âˆ§ Collinear A O A' âˆ§ Â¬(A' = O) [A'a] by fol DintAOB - BetweenLinear B1'; Â¬(A,A' same_side l) [Ansim_lA'] by fol l_line AOA' SameSide_DEF; B âˆˆ int_angle D O A' [] by fol H1 AOA' InteriorReflectionInterior; B,A' same_side l [Bsim_lA'] by fol l_line DintAOB A'a - InteriorUse; Â¬Collinear A O D âˆ§ Â¬Collinear B O D [AODncol] by fol H1 InteriorEZHelp InteriorAngleSymmetry; Â¬Collinear D O A' [] by fol - A'a CollinearSymmetry NoncollinearityExtendsToLine; A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ A' âˆ‰ l [] by fol l_line AODncol - Collinear_DEF âˆ‰; Â¬(A,B same_side l) [] by fol l_line - Bsim_lA' Ansim_lA' SameSideTransitive; consider G such that G âˆˆ Open (A, B) âˆ§ G âˆˆ l [AGB] by fol l_line - SameSide_DEF; Collinear O D G [ODGcol] by fol - l_line Collinear_DEF; G âˆˆ int_angle A O B [] by fol DintAOB AGB ConverseCrossbar; G âˆ‰ a âˆ§ G,B same_side a âˆ§ Â¬(G = O) [Gsim_aB] by fol DintAOB - InteriorUse âˆ‰; B,D same_side a [] by fol DintAOB notBa SameSideSymmetric; G,D same_side a [Gsim_aD] by fol DintAOB Gsim_aB notBa - SameSideTransitive; O âˆ‰ Open (G, D) [] by fol DintAOB - SameSide_DEF âˆ‰; G âˆˆ ray O D â” {O} [] by fol Distinct ODGcol - Gsim_aB IN_Ray IN_DIFF IN_SING; fol AGB -; qed; `;; let AlternateConverseCrossbar = theorem `; âˆ€O A B G. Collinear A G B âˆ§ G âˆˆ int_angle A O B â‡’ G âˆˆ Open (A, B) proof intro_TAC âˆ€O A B G, H1; consider a b such that Â¬Collinear A O B âˆ§ Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ G,B same_side a âˆ§ G,A same_side b [GintAOB] by fol H1 IN_InteriorAngle; Â¬(A = B) âˆ§ Â¬(G = A) âˆ§ Â¬(G = B) âˆ§ A âˆ‰ Open (G, B) âˆ§ B âˆ‰ Open (G, A) [] by fol - H1 NonCollinearImpliesDistinct InteriorEZHelp SameSide_DEF âˆ‰; fol - H1 B1' B3' âˆ‰; qed; `;; let InteriorOpposite = theorem `; âˆ€A O B P p. P âˆˆ int_angle A O B â‡’ Line p âˆ§ O âˆˆ p âˆ§ P âˆˆ p â‡’ Â¬(A,B same_side p) proof intro_TAC âˆ€A O B P p, PintAOB, p_line; consider G such that G âˆˆ Open (A, B) âˆ§ G âˆˆ ray O P [Gexists] by fol PintAOB Crossbar_THM IN_DIFF; fol p_line p_line - RayLine SUBSET Gexists SameSide_DEF; qed; `;; let IntervalTransitivity = theorem `; âˆ€O P Q R m. Line m âˆ§ O âˆˆ m â‡’ P âˆˆ m â” {O} âˆ§ Q âˆˆ m â” {O} âˆ§ R âˆˆ m â” {O} â‡’ O âˆ‰ Open (P, Q) âˆ§ O âˆ‰ Open (Q, R) â‡’ O âˆ‰ Open (P, R) proof intro_TAC âˆ€O P Q R m, H0, H2, H3; consider E such that E âˆ‰ m âˆ§ Â¬(O = E) [notEm] by fol H0 ExistsPointOffLine âˆ‰; consider l such that Line l âˆ§ O âˆˆ l âˆ§ E âˆˆ l [l_line] by fol - I1; Â¬(m = l) [] by fol notEm - âˆ‰; l âˆ© m = {O} [lmO] by fol l_line H0 - l_line I1Uniqueness; P âˆ‰ l âˆ§ Q âˆ‰ l âˆ§ R âˆ‰ l [notPQRl] by fol - H2 EquivIntersectionHelp; P,Q same_side l âˆ§ Q,R same_side l [] by fol l_line H0 lmO H2 H3 EquivIntersection; P,R same_side l [Psim_lR] by fol l_line notPQRl - SameSideTransitive; fol l_line - SameSide_DEF âˆ‰; qed; `;; let RayWellDefinedHalfway = theorem `; âˆ€O P Q. Â¬(Q = O) âˆ§ P âˆˆ ray O Q â” {O} â‡’ ray O P âŠ‚ ray O Q proof intro_TAC âˆ€O P Q, H1 H2; consider m such that Line m âˆ§ O âˆˆ m âˆ§ Q âˆˆ m [OQm] by fol H1 I1; P âˆˆ ray O Q âˆ§ Â¬(P = O) âˆ§ O âˆ‰ Open (P, Q) [H2'] by fol H2 IN_Ray IN_DIFF IN_SING; P âˆˆ m âˆ§ P âˆˆ m â” {O} âˆ§ Q âˆˆ m â” {O} [PQm_O] by fol OQm H2' RayLine SUBSET H2' OQm H1 IN_DIFF IN_SING; O âˆ‰ Open (P, Q) [notPOQ] by fol H2' IN_Ray; rewrite SUBSET; X_genl_TAC X; intro_TAC XrayOP; X âˆˆ m âˆ§ O âˆ‰ Open (X, P) [XrOP] by fol - SUBSET OQm PQm_O H2' RayLine IN_Ray; Collinear O Q X [OQXcol] by fol OQm - Collinear_DEF; assume Â¬(X = O) [notXO] by fol H1 OriginInRay; X âˆˆ m â” {O} [] by fol XrOP - IN_DIFF IN_SING; O âˆ‰ Open (X, Q) [] by fol OQm - PQm_O XrOP H2' IntervalTransitivity; fol H1 OQXcol - IN_Ray; qed; `;; let RayWellDefined = theorem `; âˆ€O P Q. Â¬(Q = O) âˆ§ P âˆˆ ray O Q â” {O} â‡’ ray O P = ray O Q proof intro_TAC âˆ€O P Q, H1 H2; ray O P âŠ‚ ray O Q [PsubsetQ] by fol H1 H2 RayWellDefinedHalfway; Â¬(P = O) âˆ§ Collinear O Q P âˆ§ O âˆ‰ Open (P, Q) [H2'] by fol H2 IN_Ray IN_DIFF IN_SING; Q âˆˆ ray O P â” {O} [] by fol H2' B1' âˆ‰ CollinearSymmetry IN_Ray H1 IN_DIFF IN_SING; ray O Q âŠ‚ ray O P [QsubsetP] by fol H2' - RayWellDefinedHalfway; fol PsubsetQ QsubsetP SUBSET_ANTISYM; qed; `;; let OppositeRaysIntersect1pointHelp = theorem `; âˆ€A O B X. O âˆˆ Open (A, B) âˆ§ X âˆˆ ray O B â” {O} â‡’ X âˆ‰ ray O A âˆ§ O âˆˆ Open (X, A) proof intro_TAC âˆ€A O B X, H1 H2; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) âˆ§ Collinear A O B [AOB] by fol H1 B1'; Â¬(X = O) âˆ§ Collinear O B X âˆ§ O âˆ‰ Open (X, B) [H2'] by fol H2 IN_Ray IN_DIFF IN_SING; consider m such that Line m âˆ§ A âˆˆ m âˆ§ B âˆˆ m [m_line] by fol AOB I1; O âˆˆ m âˆ§ X âˆˆ m [Om] by fol m_line H2' AOB CollinearLinear; A âˆˆ m â” {O} âˆ§ X âˆˆ m â” {O} âˆ§ B âˆˆ m â” {O} [] by fol m_line - H2' AOB IN_DIFF IN_SING; fol H1 m_line Om - H2' IntervalTransitivity âˆ‰ B1' IN_Ray; qed; `;; let OppositeRaysIntersect1point = theorem `; âˆ€A O B. O âˆˆ Open (A, B) â‡’ ray O A âˆ© ray O B = {O} proof intro_TAC âˆ€A O B, H1; Â¬(A = O) âˆ§ Â¬(O = B) [] by fol H1 B1'; rewrite GSYM SUBSET_ANTISYM_EQ SUBSET IN_INTER; conj_tac [Right] by fol - OriginInRay IN_SING; fol H1 OppositeRaysIntersect1pointHelp IN_DIFF IN_SING âˆ‰; qed; `;; let IntervalRay = theorem `; âˆ€A B C. B âˆˆ Open (A, C) â‡’ ray A B = ray A C by fol B1' IntervalRayEZ RayWellDefined`;; let Reverse4Order = theorem `; âˆ€A B C D. ordered A B C D â‡’ ordered D C B A proof rewrite Ordered_DEF; fol B1'; qed; `;; let TransitivityBetweennessHelp = theorem `; âˆ€A B C D. B âˆˆ Open (A, C) âˆ§ C âˆˆ Open (B, D) â‡’ B âˆˆ Open (A, D) proof intro_TAC âˆ€A B C D, H1; D âˆˆ ray B C â” {B} [] by fol H1 IntervalRayEZ; fol H1 - OppositeRaysIntersect1pointHelp B1'; qed; `;; let TransitivityBetweenness = theorem `; âˆ€A B C D. B âˆˆ Open (A, C) âˆ§ C âˆˆ Open (B, D) â‡’ ordered A B C D proof intro_TAC âˆ€A B C D, H1; B âˆˆ Open (A, D) [ABD] by fol H1 TransitivityBetweennessHelp; C âˆˆ Open (D, B) âˆ§ B âˆˆ Open (C, A) [] by fol H1 B1'; C âˆˆ Open (D, A) [] by fol - TransitivityBetweennessHelp; fol H1 ABD - B1' Ordered_DEF; qed; `;; let IntervalsAreConvex = theorem `; âˆ€A B C. B âˆˆ Open (A, C) â‡’ Open (A, B) âŠ‚ Open (A, C) proof intro_TAC âˆ€A B C, H1; âˆ€X. X âˆˆ Open (A, B) â‡’ X âˆˆ Open (A, C) [] proof intro_TAC âˆ€X, AXB; X âˆˆ ray B A â” {B} [] by fol AXB B1' IntervalRayEZ; B âˆˆ Open (X, C) [] by fol H1 B1' - OppositeRaysIntersect1pointHelp; fol AXB - TransitivityBetweennessHelp; qed; fol - SUBSET; qed; `;; let TransitivityBetweennessVariant = theorem `; âˆ€A X B C. X âˆˆ Open (A, B) âˆ§ B âˆˆ Open (A, C) â‡’ ordered A X B C proof intro_TAC âˆ€A X B C, H1; X âˆˆ ray B A â” {B} [] by fol H1 B1' IntervalRayEZ; B âˆˆ Open (X, C) [] by fol H1 B1' - OppositeRaysIntersect1pointHelp; fol H1 - TransitivityBetweenness; qed; `;; let Interval2sides2aLineHelp = theorem `; âˆ€A B C X. B âˆˆ Open (A, C) â‡’ X âˆ‰ Open (A, B) âˆ¨ X âˆ‰ Open (B, C) proof intro_TAC âˆ€A B C X, H1; assume Â¬(X âˆ‰ Open (A, B)) [AXB] by fol; ordered A X B C [] by fol - âˆ‰ H1 TransitivityBetweennessVariant; fol MESON [-; Ordered_DEF] [B âˆˆ Open (X, C)] B1' B3' âˆ‰; qed; `;; let Interval2sides2aLine = theorem `; âˆ€A B C X. Collinear A B C â‡’ X âˆ‰ Open (A, B) âˆ¨ X âˆ‰ Open (A, C) âˆ¨ X âˆ‰ Open (B, C) proof intro_TAC âˆ€A B C X, H1; assume Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [Distinct] by fol B1' âˆ‰; B âˆˆ Open (A, C) âˆ¨ C âˆˆ Open (B, A) âˆ¨ A âˆˆ Open (C, B) [] by fol - H1 B3'; fol - Interval2sides2aLineHelp B1' âˆ‰; qed; `;; let TwosidesTriangle2aLine = theorem `; âˆ€A B C l. Line l âˆ§ Â¬Collinear A B C â‡’ A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l â‡’ Â¬(A,B same_side l) âˆ§ Â¬(B,C same_side l) â‡’ A,C same_side l proof intro_TAC âˆ€ A B C l, H1, off_l, H2; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [ABCdistinct] by fol H1 NonCollinearImpliesDistinct; consider m such that Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m [m_line] by fol - I1; assume Â¬(l âˆ© m = âˆ…) [lmIntersect] by fol H1 m_line DisjointLinesImplySameSide; consider Y such that Y âˆˆ l âˆ§ Y âˆˆ m [Ylm] by fol lmIntersect MEMBER_NOT_EMPTY IN_INTER; consider X Z such that X âˆˆ l âˆ§ X âˆˆ Open (A, B) âˆ§ Z âˆˆ l âˆ§ Z âˆˆ Open (C, B) [H2'] by fol H1 H2 SameSide_DEF B1'; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Y âˆˆ m â” {A} âˆ§ Y âˆˆ m â” {C} âˆ§ C âˆˆ m â” {A} âˆ§ A âˆˆ m â” {C} [Distinct] by fol H1 NonCollinearImpliesDistinct Ylm off_l âˆ‰ m_line IN_DIFF IN_SING; consider p such that Line p âˆ§ B âˆˆ p âˆ§ A âˆˆ p [p_line] by fol Distinct I1; consider q such that Line q âˆ§ B âˆˆ q âˆ§ C âˆˆ q [q_line] by fol Distinct I1; X âˆˆ p âˆ§ Z âˆˆ q [Xp] by fol p_line H2' BetweenLinear q_line H2'; A âˆ‰ q âˆ§ B âˆ‰ m âˆ§ C âˆ‰ p [vertex_off_line] by fol q_line m_line p_line H1 Collinear_DEF âˆ‰; X âˆ‰ q âˆ§ X,A same_side q âˆ§ Z âˆ‰ p âˆ§ Z,C same_side p [Xsim_qA] by fol q_line p_line - H2' B1' IntervalRayEZ RaySameSide; Â¬(m = p) âˆ§ Â¬(m = q) [] by fol m_line vertex_off_line âˆ‰; p âˆ© m = {A} âˆ§ q âˆ© m = {C} [pmA] by fol p_line m_line q_line H1 - Xp H2' I1Uniqueness; Y âˆ‰ p âˆ§ Y âˆ‰ q [notYpq] by fol - Distinct EquivIntersectionHelp; X âˆˆ ray A B â” {A} âˆ§ Z âˆˆ ray C B â” {C} [] by fol H2' IntervalRayEZ H2' B1'; X âˆ‰ m âˆ§ Z âˆ‰ m âˆ§ X,B same_side m âˆ§ B,Z same_side m [notXZm] by fol m_line vertex_off_line - RaySameSide SameSideSymmetric; X,Z same_side m [] by fol m_line - vertex_off_line SameSideTransitive; Collinear X Y Z âˆ§ Y âˆ‰ Open (X, Z) âˆ§ Â¬(Y = X) âˆ§ Â¬(Y = Z) âˆ§ Â¬(X = Z) [] by fol H1 H2' Ylm Collinear_DEF m_line - SameSide_DEF notXZm Xsim_qA Xp âˆ‰; Z âˆˆ Open (X, Y) âˆ¨ X âˆˆ Open (Z, Y) [] by fol - B3' âˆ‰ B1'; case_split ZXY | XZY by fol -; suppose X âˆˆ Open (Z, Y); Â¬(Z,Y same_side p) [] by fol p_line Xp - SameSide_DEF; Â¬(C,Y same_side p) [] by fol p_line Xsim_qA vertex_off_line notYpq - SameSideTransitive; A âˆˆ Open (C, Y) [] by fol p_line m_line pmA Distinct - EquivIntersection âˆ‰; fol H1 Ylm off_l - B1' IntervalRayEZ RaySameSide; end; suppose Z âˆˆ Open (X, Y); Â¬(X,Y same_side q) [] by fol q_line Xp - SameSide_DEF; Â¬(A,Y same_side q) [] by fol q_line Xsim_qA vertex_off_line notYpq - SameSideTransitive; C âˆˆ Open (Y, A) [] by fol q_line m_line pmA Distinct - EquivIntersection âˆ‰ B1'; fol H1 Ylm off_l - IntervalRayEZ RaySameSide; end; qed; `;; let LineUnionOf2Rays = theorem `; âˆ€A O B l. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l â‡’ O âˆˆ Open (A, B) â‡’ l = ray O A âˆª ray O B proof intro_TAC âˆ€A O B l, H1, H2; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ O âˆˆ l [Distinct] by fol H2 B1' H1 BetweenLinear; ray O A âˆª ray O B âŠ‚ l [AOBsub_l] by fol H1 - RayLine UNION_SUBSET; âˆ€X. X âˆˆ l â‡’ X âˆˆ ray O A âˆ¨ X âˆˆ ray O B [] proof intro_TAC âˆ€X, Xl; assume Â¬(X âˆˆ ray O B) [notXrOB] by fol; Collinear O B X âˆ§ Collinear X A B âˆ§ Collinear O A X [XABcol] by fol Distinct H1 Xl Collinear_DEF; O âˆˆ Open (X, B) [] by fol notXrOB Distinct - IN_Ray âˆ‰; O âˆ‰ Open (X, A) [] by fol âˆ‰ B1' XABcol - H2 Interval2sides2aLine; fol Distinct XABcol - IN_Ray; qed; l âŠ‚ ray O A âˆª ray O B [] by fol - IN_UNION SUBSET; fol - AOBsub_l SUBSET_ANTISYM; qed; `;; let AtMost2Sides = theorem `; âˆ€A B C l. Line l â‡’ A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l â‡’ A,B same_side l âˆ¨ A,C same_side l âˆ¨ B,C same_side l proof intro_TAC âˆ€A B C l, l_line, H2; assume Â¬(A = C) [notAC] by fol l_line H2 SameSideReflexive; assume Collinear A B C [ABCcol] by fol l_line H2 TwosidesTriangle2aLine; consider m such that Line m âˆ§ A âˆˆ m âˆ§ B âˆˆ m âˆ§ C âˆˆ m [m_line] by fol notAC - I1 Collinear_DEF; assume Â¬(m âˆ© l = âˆ…) [m_lNot0] by fol m_line l_line BetweenLinear SameSide_DEF IN_INTER NOT_IN_EMPTY; consider X such that X âˆˆ l âˆ§ X âˆˆ m [Xlm] by fol - IN_INTER MEMBER_NOT_EMPTY; A âˆˆ m â” {X} âˆ§ B âˆˆ m â” {X} âˆ§ C âˆˆ m â” {X} [ABCm_X] by fol m_line - H2 âˆ‰ IN_DIFF IN_SING; X âˆ‰ Open (A, B) âˆ¨ X âˆ‰ Open (A, C) âˆ¨ X âˆ‰ Open (B, C) [] by fol ABCcol Interval2sides2aLine; fol l_line m_line m_line Xlm H2 âˆ‰ I1Uniqueness ABCm_X - EquivIntersection; qed; `;; let FourPointsOrder = theorem `; âˆ€A B C X l. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l âˆ§ X âˆˆ l â‡’ Â¬(X = A) âˆ§ Â¬(X = B) âˆ§ Â¬(X = C) â‡’ B âˆˆ Open (A, C) â‡’ ordered X A B C âˆ¨ ordered A X B C âˆ¨ ordered A B X C âˆ¨ ordered A B C X proof intro_TAC âˆ€A B C X l, H1, H2, H3; A âˆˆ Open (X, B) âˆ¨ X âˆˆ Open (A, B) âˆ¨ X âˆˆ Open (B, C) âˆ¨ C âˆˆ Open (B, X) [] proof Â¬(A = B) âˆ§ Â¬(B = C) [ABCdistinct] by fol H3 B1'; Collinear A B X âˆ§ Collinear A C X âˆ§ Collinear C B X [ACXcol] by fol H1 Collinear_DEF; A âˆˆ Open (X, B) âˆ¨ X âˆˆ Open (A, B) âˆ¨ B âˆˆ Open (A, X) [3pos] by fol H2 ABCdistinct - B3' B1'; assume B âˆˆ Open (A, X) [ABX] by fol 3pos; B âˆ‰ Open (C, X) [] by fol ACXcol H3 - Interval2sides2aLine âˆ‰; fol H2 ABCdistinct ACXcol - B3' B1' âˆ‰; qed; fol - H3 B1' TransitivityBetweenness TransitivityBetweennessVariant Reverse4Order; qed; `;; let HilbertAxiomRedundantByMoore = theorem `; âˆ€A B C D l. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l âˆ§ D âˆˆ l â‡’ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬(C = D) â‡’ ordered D A B C âˆ¨ ordered A D B C âˆ¨ ordered A B D C âˆ¨ ordered A B C D âˆ¨ ordered D A C B âˆ¨ ordered A D C B âˆ¨ ordered A C D B âˆ¨ ordered A C B D âˆ¨ ordered D C A B âˆ¨ ordered C D A B âˆ¨ ordered C A D B âˆ¨ ordered C A B D proof intro_TAC âˆ€A B C D l, H1, H2; Collinear A B C [] by fol H1 Collinear_DEF; B âˆˆ Open (A, C) âˆ¨ C âˆˆ Open (A, B) âˆ¨ A âˆˆ Open (C, B) [] by fol H2 - B3' B1'; fol - H1 H2 FourPointsOrder; qed; `;; let InteriorTransitivity = theorem `; âˆ€A O B M G. G âˆˆ int_angle A O B âˆ§ M âˆˆ int_angle A O G â‡’ M âˆˆ int_angle A O B proof intro_TAC âˆ€A O B M G, GintAOB MintAOG; Â¬Collinear A O B [AOBncol] by fol GintAOB IN_InteriorAngle; consider G' such that G' âˆˆ Open (A, B) âˆ§ G' âˆˆ ray O G â” {O} [CrossG] by fol GintAOB Crossbar_THM; M âˆˆ int_angle A O G' [] by fol MintAOG - InteriorWellDefined; consider M' such that M' âˆˆ Open (A, G') âˆ§ M' âˆˆ ray O M â” {O} [CrossM] by fol - Crossbar_THM; Â¬(M' = O) âˆ§ Â¬(M = O) âˆ§ Collinear O M M' âˆ§ O âˆ‰ Open (M', M) [] by fol - IN_Ray IN_DIFF IN_SING; M âˆˆ ray O M' â” {O} [MrOM'] by fol - CollinearSymmetry B1' âˆ‰ IN_Ray IN_DIFF IN_SING; Open (A, G') âŠ‚ Open (A, B) âˆ§ M' âˆˆ Open (A, B) [] by fol CrossG IntervalsAreConvex CrossM SUBSET; M' âˆˆ int_angle A O B [] by fol AOBncol - ConverseCrossbar; fol - MrOM' WholeRayInterior; qed; `;; let HalfPlaneConvexNonempty = theorem `; âˆ€l H A. Line l âˆ§ A âˆ‰ l â‡’ H = {X | X âˆ‰ l âˆ§ X,A same_side l} â‡’ Â¬(H = âˆ…) âˆ§ H âŠ‚ complement l âˆ§ Convex H proof intro_TAC âˆ€l H A, l_line, HalfPlane; âˆ€X. X âˆˆ H â‡” X âˆ‰ l âˆ§ X,A same_side l [Hdef] by simplify HalfPlane IN_ELIM_THM; H âŠ‚ complement l [Hsub] by fol - IN_PlaneComplement SUBSET; A,A same_side l âˆ§ A âˆˆ H [] by fol l_line SameSideReflexive Hdef; Â¬(H = âˆ…) [Hnonempty] by fol - MEMBER_NOT_EMPTY; âˆ€P Q X. P âˆˆ H âˆ§ Q âˆˆ H âˆ§ X âˆˆ Open (P, Q) â‡’ X âˆˆ H [] proof intro_TAC âˆ€P Q X, PXQ; P âˆ‰ l âˆ§ P,A same_side l âˆ§ Q âˆ‰ l âˆ§ Q,A same_side l [PQinH] by fol - Hdef; P,Q same_side l [Psim_lQ] by fol l_line - SameSideSymmetric SameSideTransitive; X âˆ‰ l [notXl] by fol - PXQ SameSide_DEF âˆ‰; Open (X, P) âŠ‚ Open (P, Q) [] by fol PXQ IntervalsAreConvex B1' SUBSET; X,P same_side l [] by fol l_line - SUBSET Psim_lQ SameSide_DEF; X,A same_side l [] by fol l_line notXl PQinH - Psim_lQ PQinH SameSideTransitive; fol - notXl Hdef; qed; fol Hnonempty Hsub - SUBSET CONVEX; qed; `;; let PlaneSeparation = theorem `; âˆ€l. Line l â‡’ âˆƒH1 H2. H1 âˆ© H2 = âˆ… âˆ§ Â¬(H1 = âˆ…) âˆ§ Â¬(H2 = âˆ…) âˆ§ Convex H1 âˆ§ Convex H2 âˆ§ complement l = H1 âˆª H2 âˆ§ âˆ€P Q. P âˆˆ H1 âˆ§ Q âˆˆ H2 â‡’ Â¬(P,Q same_side l) proof intro_TAC âˆ€l, l_line; consider A such that A âˆ‰ l [notAl] by fol l_line ExistsPointOffLine; consider E such that E âˆˆ l âˆ§ Â¬(A = E) [El] by fol l_line I2 - âˆ‰; consider B such that E âˆˆ Open (A, B) âˆ§ Â¬(E = B) âˆ§ Collinear A E B [AEB] by fol - B2' B1'; B âˆ‰ l [notBl] by fol - l_line El âˆ‰ notAl NonCollinearRaa CollinearSymmetry; Â¬(A,B same_side l) [Ansim_lB] by fol l_line El AEB SameSide_DEF; consider H1 H2 such that H1 = {X | X âˆ‰ l âˆ§ X,A same_side l} âˆ§ H2 = {X | X âˆ‰ l âˆ§ X,B same_side l} [H12sets] by fol; âˆ€X. (X âˆˆ H1 â‡” X âˆ‰ l âˆ§ X,A same_side l) âˆ§ (X âˆˆ H2 â‡” X âˆ‰ l âˆ§ X,B same_side l) [H12def] by simplify IN_ELIM_THM -; H1 âˆ© H2 = âˆ… [H12disjoint] proof assume Â¬(H1 âˆ© H2 = âˆ…) [nonempty] by fol; consider V such that V âˆˆ H1 âˆ§ V âˆˆ H2 [VinH12] by fol - MEMBER_NOT_EMPTY IN_INTER; V âˆ‰ l âˆ§ V,A same_side l âˆ§ V âˆ‰ l âˆ§ V,B same_side l [] by fol - H12def; A,B same_side l [] by fol l_line - notAl notBl SameSideSymmetric SameSideTransitive; fol - Ansim_lB; qed; Â¬(H1 = âˆ…) âˆ§ Â¬(H2 = âˆ…) âˆ§ H1 âŠ‚ complement l âˆ§ H2 âŠ‚ complement l âˆ§ Convex H1 âˆ§ Convex H2 [H12convex_nonempty] by fol l_line notAl notBl H12sets HalfPlaneConvexNonempty; H1 âˆª H2 âŠ‚ complement l [H12sub] by fol H12convex_nonempty UNION_SUBSET; âˆ€C. C âˆˆ complement l â‡’ C âˆˆ H1 âˆª H2 [] proof intro_TAC âˆ€C, compl; C âˆ‰ l [notCl] by fol - IN_PlaneComplement; C,A same_side l âˆ¨ C,B same_side l [] by fol l_line notAl notBl - Ansim_lB AtMost2Sides; fol notCl - H12def IN_UNION; qed; complement l âŠ‚ H1 âˆª H2 [] by fol - SUBSET; complement l = H1 âˆª H2 [compl_H1unionH2] by fol H12sub - SUBSET_ANTISYM; âˆ€P Q. P âˆˆ H1 âˆ§ Q âˆˆ H2 â‡’ Â¬(P,Q same_side l) [opp_sides] proof intro_TAC âˆ€P Q, both; P âˆ‰ l âˆ§ P,A same_side l âˆ§ Q âˆ‰ l âˆ§ Q,B same_side l [PH1_QH2] by fol - H12def IN; fol l_line - notAl SameSideSymmetric notBl Ansim_lB SameSideTransitive; qed; fol H12disjoint H12convex_nonempty compl_H1unionH2 opp_sides; qed; `;; let TetralateralSymmetry = theorem `; âˆ€A B C D. Tetralateral A B C D â‡’ Tetralateral B C D A âˆ§ Tetralateral A B D C proof intro_TAC âˆ€A B C D, H1; Â¬Collinear A B D âˆ§ Â¬Collinear B D C âˆ§ Â¬Collinear D C A âˆ§ Â¬Collinear C A B [TetraABCD] by fol H1 Tetralateral_DEF CollinearSymmetry; simplify H1 - Tetralateral_DEF; fol H1 Tetralateral_DEF; qed; `;; let EasyEmptyIntersectionsTetralateralHelp = theorem `; âˆ€A B C D. Tetralateral A B C D â‡’ Open (A, B) âˆ© Open (B, C) = âˆ… proof intro_TAC âˆ€A B C D, H1; âˆ€X. X âˆˆ Open (B, C) â‡’ X âˆ‰ Open (A, B) [] proof intro_TAC âˆ€X, BXC; Â¬Collinear A B C âˆ§ Collinear B X C âˆ§ Â¬(X = B) [] by fol H1 Tetralateral_DEF - B1'; Â¬Collinear A X B [] by fol - CollinearSymmetry B1' NoncollinearityExtendsToLine; fol - B1' âˆ‰; qed; fol - DisjointOneNotOther; qed; `;; let EasyEmptyIntersectionsTetralateral = theorem `; âˆ€A B C D. Tetralateral A B C D â‡’ Open (A, B) âˆ© Open (B, C) = âˆ… âˆ§ Open (B, C) âˆ© Open (C, D) = âˆ… âˆ§ Open (C, D) âˆ© Open (D, A) = âˆ… âˆ§ Open (D, A) âˆ© Open (A, B) = âˆ… proof intro_TAC âˆ€A B C D, H1; Tetralateral B C D A âˆ§ Tetralateral C D A B âˆ§ Tetralateral D A B C [] by fol H1 TetralateralSymmetry; fol H1 - EasyEmptyIntersectionsTetralateralHelp; qed; `;; let SegmentSameSideOppositeLine = theorem `; âˆ€A B C D a c. Quadrilateral A B C D â‡’ Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a â‡’ Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c â‡’ A,B same_side c âˆ¨ C,D same_side a proof intro_TAC âˆ€A B C D a c, H1, a_line, c_line; assume Â¬(C,D same_side a) [CDnsim_a] by fol; consider G such that G âˆˆ a âˆ§ G âˆˆ Open (C, D) [CGD] by fol - a_line SameSide_DEF; G âˆˆ c âˆ§ Collinear G B A [Gc] by fol c_line - BetweenLinear a_line Collinear_DEF; Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Open (A, B) âˆ© Open (C, D) = âˆ… [quadABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF; A âˆ‰ c âˆ§ B âˆ‰ c âˆ§ Â¬(A = G) âˆ§ Â¬(B = G) [Distinct] by fol - c_line Collinear_DEF âˆ‰ Gc; G âˆ‰ Open (A, B) [] by fol quadABCD CGD DisjointOneNotOther; A âˆˆ ray G B â” {G} [] by fol Distinct Gc - IN_Ray IN_DIFF IN_SING; fol c_line Gc Distinct - RaySameSide; qed; `;; let ConvexImpliesQuad = theorem `; âˆ€A B C D. Tetralateral A B C D â‡’ C âˆˆ int_angle D A B âˆ§ D âˆˆ int_angle A B C â‡’ Quadrilateral A B C D proof intro_TAC âˆ€A B C D, H1, H2; Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬(A = D) [TetraABCD] by fol H1 Tetralateral_DEF; consider a such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line] by fol TetraABCD I1; consider b such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b [b_line] by fol TetraABCD I1; consider d such that Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [d_line] by fol TetraABCD I1; Open (B, C) âŠ‚ b âˆ§ Open (A, B) âŠ‚ a [BCbABa] by fol b_line a_line BetweenLinear SUBSET; D,A same_side b âˆ§ C,D same_side a [] by fol H2 a_line b_line d_line InteriorUse; b âˆ© Open (D, A) = âˆ… âˆ§ a âˆ© Open (C, D) = âˆ… [] by fol - b_line SameSide_DEF IN_INTER MEMBER_NOT_EMPTY; fol H1 BCbABa - INTER_TENSOR SUBSET_REFL SUBSET_EMPTY Quadrilateral_DEF; qed; `;; let DiagonalsIntersectImpliesConvexQuad = theorem `; âˆ€A B C D G. Â¬Collinear B C D â‡’ G âˆˆ Open (A, C) âˆ§ G âˆˆ Open (B, D) â‡’ ConvexQuadrilateral A B C D proof intro_TAC âˆ€A B C D G, BCDncol, DiagInt; Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬(C = D) âˆ§ Â¬(C = A) âˆ§ Â¬(A = G) âˆ§ Â¬(D = G) âˆ§ Â¬(B = G) [Distinct] by fol BCDncol NonCollinearImpliesDistinct DiagInt B1'; Collinear A G C âˆ§ Collinear B G D [Gcols] by fol DiagInt B1'; Â¬Collinear C D G âˆ§ Â¬Collinear B C G [Gncols] by fol BCDncol CollinearSymmetry Distinct Gcols NoncollinearityExtendsToLine; Â¬Collinear C D A [CDAncol] by fol - CollinearSymmetry Distinct Gcols NoncollinearityExtendsToLine; Â¬Collinear A B C âˆ§ Â¬Collinear D A G [ABCncol] by fol Gncols - CollinearSymmetry Distinct Gcols NoncollinearityExtendsToLine; Â¬Collinear D A B [DABncol] by fol - CollinearSymmetry Distinct Gcols NoncollinearityExtendsToLine; Â¬(A = B) âˆ§ Â¬(A = D) [] by fol DABncol NonCollinearImpliesDistinct; Tetralateral A B C D [TetraABCD] by fol Distinct - BCDncol CDAncol DABncol ABCncol Tetralateral_DEF; A âˆˆ ray C G â” {C} âˆ§ B âˆˆ ray D G â” {D} âˆ§ C âˆˆ ray A G â” {A} âˆ§ D âˆˆ ray B G â” {B} [ArCG] by fol DiagInt B1' IntervalRayEZ; G âˆˆ int_angle B C D âˆ§ G âˆˆ int_angle C D A âˆ§ G âˆˆ int_angle D A B âˆ§ G âˆˆ int_angle A B C [] by fol BCDncol CDAncol DABncol ABCncol DiagInt B1' ConverseCrossbar; A âˆˆ int_angle B C D âˆ§ B âˆˆ int_angle C D A âˆ§ C âˆˆ int_angle D A B âˆ§ D âˆˆ int_angle A B C [] by fol - ArCG WholeRayInterior; fol TetraABCD - ConvexImpliesQuad ConvexQuad_DEF; qed; `;; let DoubleNotSimImpliesDiagonalsIntersect = theorem `; âˆ€A B C D l m. Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l â‡’ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m â‡’ Tetralateral A B C D â‡’ Â¬(B,D same_side l) â‡’ Â¬(A,C same_side m) â‡’ (âˆƒG. G âˆˆ Open (A, C) âˆ© Open (B, D)) âˆ§ ConvexQuadrilateral A B C D proof intro_TAC âˆ€A B C D l m, l_line, m_line, H1, H2, H3; Â¬Collinear A B C âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B [TetraABCD] by fol H1 Tetralateral_DEF; consider G such that G âˆˆ Open (A, C) âˆ§ G âˆˆ m [AGC] by fol H3 m_line SameSide_DEF; G âˆˆ l [Gl] by fol l_line - BetweenLinear; A âˆ‰ m âˆ§ B âˆ‰ l âˆ§ D âˆ‰ l [] by fol TetraABCD m_line l_line Collinear_DEF âˆ‰; Â¬(l = m) âˆ§ B âˆˆ m â” {G} âˆ§ D âˆˆ m â” {G} [BDm_G] by fol - l_line âˆ‰ m_line Gl IN_DIFF IN_SING; l âˆ© m = {G} [] by fol l_line m_line - Gl AGC I1Uniqueness; G âˆˆ Open (B, D) [] by fol l_line m_line - BDm_G H2 EquivIntersection âˆ‰; fol AGC - IN_INTER TetraABCD DiagonalsIntersectImpliesConvexQuad; qed; `;; let ConvexQuadImpliesDiagonalsIntersect = theorem `; âˆ€A B C D l m. Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l â‡’ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m â‡’ ConvexQuadrilateral A B C D â‡’ Â¬(B,D same_side l) âˆ§ Â¬(A,C same_side m) âˆ§ (âˆƒG. G âˆˆ Open (A, C) âˆ© Open (B, D)) âˆ§ Â¬Quadrilateral A B D C proof intro_TAC âˆ€A B C D l m, l_line, m_line, ConvQuadABCD; Tetralateral A B C D âˆ§ A âˆˆ int_angle B C D âˆ§ D âˆˆ int_angle A B C [convquadABCD] by fol ConvQuadABCD ConvexQuad_DEF Quadrilateral_DEF; Â¬(B,D same_side l) âˆ§ Â¬(A,C same_side m) [opp_sides] by fol convquadABCD l_line m_line InteriorOpposite; consider G such that G âˆˆ Open (A, C) âˆ© Open (B, D) [Gexists] by fol l_line m_line convquadABCD opp_sides DoubleNotSimImpliesDiagonalsIntersect; Â¬(Open (B, D) âˆ© Open (C, A) = âˆ…) [] by fol - IN_INTER B1' MEMBER_NOT_EMPTY; Â¬Quadrilateral A B D C [] by fol - Quadrilateral_DEF; fol opp_sides Gexists -; qed; `;; let FourChoicesTetralateralHelp = theorem `; âˆ€A B C D. Tetralateral A B C D âˆ§ C âˆˆ int_angle D A B â‡’ ConvexQuadrilateral A B C D âˆ¨ C âˆˆ int_triangle D A B proof intro_TAC âˆ€A B C D, H1 CintDAB; Â¬(A = B) âˆ§ Â¬(D = A) âˆ§ Â¬(A = C) âˆ§ Â¬(B = D) âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B [TetraABCD] by fol H1 Tetralateral_DEF; consider a d such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [ad_line] by fol TetraABCD I1; consider l m such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l âˆ§ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [lm_line] by fol TetraABCD I1; C âˆ‰ a âˆ§ C âˆ‰ d âˆ§ B âˆ‰ l âˆ§ D âˆ‰ l âˆ§ A âˆ‰ m âˆ§ C âˆ‰ m âˆ§ Â¬Collinear A B D âˆ§ Â¬Collinear B D A [tetra'] by fol TetraABCD ad_line lm_line Collinear_DEF âˆ‰ CollinearSymmetry; Â¬(B,D same_side l) [Bsim_lD] by fol CintDAB lm_line InteriorOpposite - SameSideSymmetric; assume A,C same_side m [same] by fol lm_line H1 Bsim_lD DoubleNotSimImpliesDiagonalsIntersect; C,A same_side m [Csim_mA] by fol lm_line - tetra' SameSideSymmetric; C,B same_side d âˆ§ C,D same_side a [] by fol ad_line CintDAB InteriorUse; C âˆˆ int_angle A B D âˆ§ C âˆˆ int_angle B D A [] by fol tetra' ad_line lm_line Csim_mA - IN_InteriorAngle; fol CintDAB - IN_InteriorTriangle; qed; `;; let FourChoicesTetralateralHelp = theorem `; âˆ€A B C D. Tetralateral A B C D âˆ§ C âˆˆ int_angle D A B â‡’ ConvexQuadrilateral A B C D âˆ¨ C âˆˆ int_triangle D A B proof intro_TAC âˆ€A B C D, H1 CintDAB; Â¬(A = B) âˆ§ Â¬(D = A) âˆ§ Â¬(A = C) âˆ§ Â¬(B = D) âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B [TetraABCD] by fol H1 Tetralateral_DEF; consider a d such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [ad_line] by fol TetraABCD I1; consider l m such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l âˆ§ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [lm_line] by fol TetraABCD I1; C âˆ‰ a âˆ§ C âˆ‰ d âˆ§ B âˆ‰ l âˆ§ D âˆ‰ l âˆ§ A âˆ‰ m âˆ§ C âˆ‰ m âˆ§ Â¬Collinear A B D âˆ§ Â¬Collinear B D A [tetra'] by fol TetraABCD ad_line lm_line Collinear_DEF âˆ‰ CollinearSymmetry; Â¬(B,D same_side l) [Bsim_lD] by fol CintDAB lm_line InteriorOpposite - SameSideSymmetric; assume A,C same_side m [same] by fol lm_line H1 Bsim_lD DoubleNotSimImpliesDiagonalsIntersect; C,A same_side m [Csim_mA] by fol lm_line - tetra' SameSideSymmetric; C,B same_side d âˆ§ C,D same_side a [] by fol ad_line CintDAB InteriorUse; C âˆˆ int_angle A B D âˆ§ C âˆˆ int_angle B D A [] by fol tetra' ad_line lm_line Csim_mA - IN_InteriorAngle; fol CintDAB - IN_InteriorTriangle; qed; `;; let InteriorTriangleSymmetry = theorem `; âˆ€A B C P. P âˆˆ int_triangle A B C â‡’ P âˆˆ int_triangle B C A by fol IN_InteriorTriangle`;; let FourChoicesTetralateral = theorem `; âˆ€A B C D a. Tetralateral A B C D â‡’ Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a â‡’ C,D same_side a â‡’ ConvexQuadrilateral A B C D âˆ¨ ConvexQuadrilateral A B D C âˆ¨ D âˆˆ int_triangle A B C âˆ¨ C âˆˆ int_triangle D A B proof intro_TAC âˆ€A B C D a, H1, a_line, Csim_aD; Â¬(A = B) âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B âˆ§ Tetralateral A B D C [TetraABCD] by fol H1 Tetralateral_DEF TetralateralSymmetry; Â¬Collinear C A D âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a [notCDa] by fol TetraABCD CollinearSymmetry a_line Collinear_DEF âˆ‰; C âˆˆ int_angle D A B âˆ¨ D âˆˆ int_angle C A B [] by fol TetraABCD a_line - Csim_aD AngleOrdering; case_split CintDAB | DintCAB by fol -; suppose C âˆˆ int_angle D A B; ConvexQuadrilateral A B C D âˆ¨ C âˆˆ int_triangle D A B [] by fol H1 - FourChoicesTetralateralHelp; fol -; end; suppose D âˆˆ int_angle C A B; ConvexQuadrilateral A B D C âˆ¨ D âˆˆ int_triangle C A B [] by fol TetraABCD - FourChoicesTetralateralHelp; fol - InteriorTriangleSymmetry; end; qed; `;; let QuadrilateralSymmetry = theorem `; âˆ€A B C D. Quadrilateral A B C D â‡’ Quadrilateral B C D A âˆ§ Quadrilateral C D A B âˆ§ Quadrilateral D A B C by fol Quadrilateral_DEF INTER_COMM TetralateralSymmetry Quadrilateral_DEF`;; let FiveChoicesQuadrilateral = theorem `; âˆ€A B C D l m. Quadrilateral A B C D â‡’ Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l âˆ§ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m â‡’ (ConvexQuadrilateral A B C D âˆ¨ A âˆˆ int_triangle B C D âˆ¨ B âˆˆ int_triangle C D A âˆ¨ C âˆˆ int_triangle D A B âˆ¨ D âˆˆ int_triangle A B C) âˆ§ (Â¬(B,D same_side l) âˆ¨ Â¬(A,C same_side m)) proof intro_TAC âˆ€A B C D l m, H1, lm_line; Tetralateral A B C D [H1Tetra] by fol H1 Quadrilateral_DEF; Â¬(A = B) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(C = D) [Distinct] by fol H1Tetra Tetralateral_DEF; consider a c such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a âˆ§ Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c [ac_line] by fol Distinct I1; Quadrilateral C D A B âˆ§ Tetralateral C D A B [tetraCDAB] by fol H1 QuadrilateralSymmetry Quadrilateral_DEF; Â¬ConvexQuadrilateral A B D C âˆ§ Â¬ConvexQuadrilateral C D B A [notconvquad] by fol Distinct I1 H1 - ConvexQuadImpliesDiagonalsIntersect; ConvexQuadrilateral A B C D âˆ¨ A âˆˆ int_triangle B C D âˆ¨ B âˆˆ int_triangle C D A âˆ¨ C âˆˆ int_triangle D A B âˆ¨ D âˆˆ int_triangle A B C [5choices] proof A,B same_side c âˆ¨ C,D same_side a [2pos] by fol H1 ac_line SegmentSameSideOppositeLine; assume A,B same_side c [Asym_cB] by fol 2pos H1Tetra ac_line notconvquad FourChoicesTetralateral; ConvexQuadrilateral C D A B âˆ¨ B âˆˆ int_triangle C D A âˆ¨ A âˆˆ int_triangle B C D [X1] by fol tetraCDAB ac_line - notconvquad FourChoicesTetralateral; fol - QuadrilateralSymmetry ConvexQuad_DEF; qed; Â¬(B,D same_side l) âˆ¨ Â¬(A,C same_side m) [] by fol - lm_line ConvexQuadImpliesDiagonalsIntersect IN_InteriorTriangle InteriorAngleSymmetry InteriorOpposite; fol 5choices -; qed; `;; let IntervalSymmetry = theorem `; âˆ€A B. Open (A, B) = Open (B, A) by fol B1' EXTENSION`;; let SegmentSymmetry = theorem `; âˆ€A B. seg A B = seg B A by fol Segment_DEF INSERT_COMM IntervalSymmetry`;; let C1OppositeRay = theorem `; âˆ€O P s. Segment s âˆ§ Â¬(O = P) â‡’ âˆƒQ. P âˆˆ Open (O, Q) âˆ§ seg P Q â‰¡ s proof intro_TAC âˆ€O P s, H1; consider Z such that P âˆˆ Open (O, Z) âˆ§ Â¬(P = Z) [OPZ] by fol H1 B2' B1'; consider Q such that Q âˆˆ ray P Z â” {P} âˆ§ seg P Q â‰¡ s [PQeq] by fol H1 - C1; P âˆˆ Open (Q, O) [] by fol OPZ - OppositeRaysIntersect1pointHelp; fol - B1' PQeq; qed; `;; let OrderedCongruentSegments = theorem `; âˆ€A B C D G. Â¬(A = C) âˆ§ Â¬(D = G) â‡’ seg A C â‰¡ seg D G â‡’ B âˆˆ Open (A, C) â‡’ âˆƒE. E âˆˆ Open (D, G) âˆ§ seg A B â‰¡ seg D E proof intro_TAC âˆ€A B C D G, H1, H2, H3; Segment (seg A B) âˆ§ Segment (seg A C) âˆ§ Segment (seg B C) âˆ§ Segment (seg D G) [segs] by fol H3 B1' H1 SEGMENT; seg D G â‰¡ seg A C [DGeqAC] by fol - H2 C2Symmetric; consider E such that E âˆˆ ray D G â” {D} âˆ§ seg D E â‰¡ seg A B [DEeqAB] by fol segs H1 C1; Â¬(E = D) âˆ§ Collinear D E G âˆ§ D âˆ‰ Open (G, E) [ErDG] by fol - IN_DIFF IN_SING IN_Ray B1' CollinearSymmetry âˆ‰; consider G' such that E âˆˆ Open (D, G') âˆ§ seg E G' â‰¡ seg B C [DEG'] by fol segs - C1OppositeRay; seg D G' â‰¡ seg A C [DG'eqAC] by fol DEG' H3 DEeqAB C3; Segment (seg D G') âˆ§ Segment (seg D E) [] by fol DEG' B1' SEGMENT; seg A C â‰¡ seg D G' âˆ§ seg A B â‰¡ seg D E [ABeqDE] by fol segs - DG'eqAC C2Symmetric DEeqAB; G' âˆˆ ray D E â” {D} âˆ§ G âˆˆ ray D E â” {D} [] by fol DEG' IntervalRayEZ ErDG IN_Ray H1 IN_DIFF IN_SING; G' = G [] by fol ErDG segs - DG'eqAC DGeqAC C1; fol - DEG' ABeqDE; qed; `;; let SegmentSubtraction = theorem `; âˆ€A B C A' B' C'. B âˆˆ Open (A, C) âˆ§ B' âˆˆ Open (A', C') â‡’ seg A B â‰¡ seg A' B' â‡’ seg A C â‰¡ seg A' C' â‡’ seg B C â‰¡ seg B' C' proof intro_TAC âˆ€A B C A' B' C', H1, H2, H3; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Collinear A B C âˆ§ Segment (seg A' C') âˆ§ Segment (seg B' C') [Distinct] by fol H1 B1' SEGMENT; consider Q such that B âˆˆ Open (A, Q) âˆ§ seg B Q â‰¡ seg B' C' [defQ] by fol - C1OppositeRay; seg A Q â‰¡ seg A' C' [AQ_A'C'] by fol H1 H2 - C3; Â¬(A = Q) âˆ§ Collinear A B Q âˆ§ A âˆ‰ Open (C, B) âˆ§ A âˆ‰ Open (Q, B) [] proof simplify defQ B1' âˆ‰; fol defQ B1' H1 B3'; qed; C âˆˆ ray A B â” {A} âˆ§ Q âˆˆ ray A B â” {A} [] by fol Distinct - IN_Ray IN_DIFF IN_SING; fol defQ Distinct - AQ_A'C' H3 C1; qed; `;; let SegmentOrderingUse = theorem `; âˆ€A B s. Segment s âˆ§ Â¬(A = B) â‡’ s <__ seg A B â‡’ âˆƒG. G âˆˆ Open (A, B) âˆ§ s â‰¡ seg A G proof intro_TAC âˆ€A B s, H1, H2; consider A' B' G' such that seg A B = seg A' B' âˆ§ G' âˆˆ Open (A', B') âˆ§ s â‰¡ seg A' G' [H2'] by fol H2 SegmentOrdering_DEF; Â¬(A' = G') âˆ§ Â¬(A' = B') âˆ§ seg A' B' â‰¡ seg A B [A'notB'G'] by fol - B1' H1 SEGMENT C2Reflexive; consider G such that G âˆˆ Open (A, B) âˆ§ seg A' G' â‰¡ seg A G [AGB] by fol A'notB'G' H1 H2' - OrderedCongruentSegments; s â‰¡ seg A G [] by fol H1 A'notB'G' - B1' SEGMENT H2' C2Transitive; fol AGB -; qed; `;; let SegmentTrichotomy1 = theorem `; âˆ€s t. s <__ t â‡’ Â¬(s â‰¡ t) proof intro_TAC âˆ€s t, H1; consider A B G such that Segment s âˆ§ t = seg A B âˆ§ G âˆˆ Open (A, B) âˆ§ s â‰¡ seg A G [H1'] by fol H1 SegmentOrdering_DEF; Â¬(A = G) âˆ§ Â¬(A = B) âˆ§ Â¬(G = B) [Distinct] by fol H1' B1'; seg A B â‰¡ seg A B [ABrefl] by fol - SEGMENT C2Reflexive; G âˆˆ ray A B â” {A} âˆ§ B âˆˆ ray A B â” {A} [] by fol H1' IntervalRay EndpointInRay Distinct IN_DIFF IN_SING; Â¬(seg A G â‰¡ seg A B) âˆ§ seg A G â‰¡ s [] by fol Distinct SEGMENT - ABrefl C1 H1' C2Symmetric; fol Distinct H1' SEGMENT - C2Transitive; qed; `;; let SegmentTrichotomy2 = theorem `; âˆ€s t u. s <__ t âˆ§ Segment u âˆ§ t â‰¡ u â‡’ s <__ u proof intro_TAC âˆ€s t u, H1 H2; consider A B P such that Segment s âˆ§ t = seg A B âˆ§ P âˆˆ Open (A, B) âˆ§ s â‰¡ seg A P [H1'] by fol H1 SegmentOrdering_DEF; Â¬(A = B) âˆ§ Â¬(A = P) [Distinct] by fol - B1'; consider X Y such that u = seg X Y âˆ§ Â¬(X = Y) [uXY] by fol H2 SEGMENT; consider Q such that Q âˆˆ Open (X, Y) âˆ§ seg A P â‰¡ seg X Q [XQY] by fol Distinct - H1' H2 OrderedCongruentSegments; Â¬(X = Q) âˆ§ s â‰¡ seg X Q [] by fol - B1' H1' Distinct SEGMENT XQY C2Transitive; fol H1' uXY XQY - SegmentOrdering_DEF; qed; `;; let SegmentOrderTransitivity = theorem `; âˆ€s t u. s <__ t âˆ§ t <__ u â‡’ s <__ u proof intro_TAC âˆ€s t u, H1; consider A B G such that u = seg A B âˆ§ G âˆˆ Open (A, B) âˆ§ t â‰¡ seg A G [H1'] by fol H1 SegmentOrdering_DEF; Â¬(A = B) âˆ§ Â¬(A = G) âˆ§ Segment s [Distinct] by fol H1' B1' H1 SegmentOrdering_DEF; s <__ seg A G [] by fol H1 H1' Distinct SEGMENT SegmentTrichotomy2; consider F such that F âˆˆ Open (A, G) âˆ§ s â‰¡ seg A F [AFG] by fol Distinct - SegmentOrderingUse; F âˆˆ Open (A, B) [] by fol H1' IntervalsAreConvex - SUBSET; fol Distinct H1' - AFG SegmentOrdering_DEF; qed; `;; let SegmentTrichotomy = theorem `; âˆ€s t. Segment s âˆ§ Segment t â‡’ (s â‰¡ t âˆ¨ s <__ t âˆ¨ t <__ s) âˆ§ Â¬(s â‰¡ t âˆ§ s <__ t) âˆ§ Â¬(s â‰¡ t âˆ§ t <__ s) âˆ§ Â¬(s <__ t âˆ§ t <__ s) proof intro_TAC âˆ€s t, H1; Â¬(s â‰¡ t âˆ§ s <__ t) [Not12] by fol - SegmentTrichotomy1; Â¬(s â‰¡ t âˆ§ t <__ s) [Not13] by fol H1 - SegmentTrichotomy1 C2Symmetric; Â¬(s <__ t âˆ§ t <__ s) [Not23] by fol H1 - SegmentOrderTransitivity SegmentTrichotomy1 H1 C2Reflexive; consider O P such that s = seg O P âˆ§ Â¬(O = P) [sOP] by fol H1 SEGMENT; consider Q such that Q âˆˆ ray O P â” {O} âˆ§ seg O Q â‰¡ t [QrOP] by fol H1 - C1; O âˆ‰ Open (Q, P) âˆ§ Collinear O P Q âˆ§ Â¬(O = Q) [notQOP] by fol - IN_DIFF IN_SING IN_Ray; s â‰¡ seg O P âˆ§ t â‰¡ seg O Q âˆ§ seg O Q â‰¡ t âˆ§ seg O P â‰¡ s [stOPQ] by fol H1 sOP - SEGMENT QrOP C2Reflexive C2Symmetric; assume Â¬(Q = P) [notQP] by fol stOPQ sOP QrOP Not12 Not13 Not23; P âˆˆ Open (O, Q) âˆ¨ Q âˆˆ Open (O, P) [] by fol sOP - notQOP B3' B1' âˆ‰; s <__ seg O Q âˆ¨ t <__ seg O P [] by fol H1 - stOPQ SegmentOrdering_DEF; s <__ t âˆ¨ t <__ s [] by fol - H1 stOPQ SegmentTrichotomy2; fol - Not12 Not13 Not23; qed; `;; let C4Uniqueness = theorem `; âˆ€O A B P l. Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ Â¬(O = A) â‡’ B âˆ‰ l âˆ§ P âˆ‰ l âˆ§ P,B same_side l â‡’ âˆ¡ A O P â‰¡ âˆ¡ A O B â‡’ ray O B = ray O P proof intro_TAC âˆ€O A B P l, H1, H2, H3; Â¬(O = B) âˆ§ Â¬(O = P) âˆ§ Ray (ray O B) âˆ§ Ray (ray O P) [Distinct] by fol H2 H1 âˆ‰ RAY; Â¬Collinear A O B âˆ§ B,B same_side l [Bsim_lB] by fol H1 H2 I1 Collinear_DEF âˆ‰ SameSideReflexive; Angle (âˆ¡ A O B) âˆ§ âˆ¡ A O B â‰¡ âˆ¡ A O B [] by fol - ANGLE C5Reflexive; fol - H1 H2 Distinct Bsim_lB H3 C4; qed; `;; let AngleSymmetry = theorem `; âˆ€A O B. âˆ¡ A O B = âˆ¡ B O A by fol Angle_DEF UNION_COMM`;; let TriangleCongSymmetry = theorem `; âˆ€A B C A' B' C'. A,B,C â‰… A',B',C' â‡’ A,C,B â‰… A',C',B' âˆ§ B,A,C â‰… B',A',C' âˆ§ B,C,A â‰… B',C',A' âˆ§ C,A,B â‰… C',A',B' âˆ§ C,B,A â‰… C',B',A' proof intro_TAC âˆ€A B C A' B' C', H1; Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' âˆ§ seg A B â‰¡ seg A' B' âˆ§ seg A C â‰¡ seg A' C' âˆ§ seg B C â‰¡ seg B' C' âˆ§ âˆ¡ A B C â‰¡ âˆ¡ A' B' C' âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B' C' A' âˆ§ âˆ¡ C A B â‰¡ âˆ¡ C' A' B' [H1'] by fol H1 TriangleCong_DEF; seg B A â‰¡ seg B' A' âˆ§ seg C A â‰¡ seg C' A' âˆ§ seg C B â‰¡ seg C' B' [segments] by fol H1' SegmentSymmetry; âˆ¡ C B A â‰¡ âˆ¡ C' B' A' âˆ§ âˆ¡ A C B â‰¡ âˆ¡ A' C' B' âˆ§ âˆ¡ B A C â‰¡ âˆ¡ B' A' C' [] by fol H1' AngleSymmetry; fol CollinearSymmetry H1' segments - TriangleCong_DEF; qed; `;; let SAS = theorem `; âˆ€A B C A' B' C'. Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' â‡’ seg B A â‰¡ seg B' A' âˆ§ seg B C â‰¡ seg B' C' â‡’ âˆ¡ A B C â‰¡ âˆ¡ A' B' C' â‡’ A,B,C â‰… A',B',C' proof intro_TAC âˆ€A B C A' B' C', H1, H2, H3; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(A' = C') [Distinct] by fol H1 NonCollinearImpliesDistinct; consider c such that Line c âˆ§ A âˆˆ c âˆ§ B âˆˆ c [c_line] by fol Distinct I1; C âˆ‰ c [notCc] by fol H1 c_line Collinear_DEF âˆ‰; âˆ¡ B C A â‰¡ âˆ¡ B' C' A' [BCAeq] by fol H1 H2 H3 C6; âˆ¡ B A C â‰¡ âˆ¡ B' A' C' [BACeq] by fol H1 CollinearSymmetry H2 H3 AngleSymmetry C6; consider Y such that Y âˆˆ ray A C â” {A} âˆ§ seg A Y â‰¡ seg A' C' [YrAC] by fol Distinct SEGMENT C1; Y âˆ‰ c âˆ§ Y,C same_side c [Ysim_cC] by fol c_line notCc - RaySameSide; Â¬Collinear Y A B [YABncol] by fol Distinct c_line - NonCollinearRaa CollinearSymmetry; ray A Y = ray A C âˆ§ âˆ¡ Y A B = âˆ¡ C A B [] by fol Distinct YrAC RayWellDefined Angle_DEF; âˆ¡ Y A B â‰¡ âˆ¡ C' A' B' [] by fol BACeq - AngleSymmetry; âˆ¡ A B Y â‰¡ âˆ¡ A' B' C' [ABYeq] by fol YABncol H1 CollinearSymmetry H2 SegmentSymmetry YrAC - C6; Angle (âˆ¡ A B C) âˆ§ Angle (âˆ¡ A' B' C') âˆ§ Angle (âˆ¡ A B Y) [] by fol H1 CollinearSymmetry YABncol ANGLE; âˆ¡ A B Y â‰¡ âˆ¡ A B C [ABYeqABC] by fol - ABYeq - H3 C5Symmetric C5Transitive; ray B C = ray B Y âˆ§ Â¬(Y = B) âˆ§ Y âˆˆ ray B C [] by fol c_line Distinct notCc Ysim_cC ABYeqABC C4Uniqueness âˆ‰ - EndpointInRay; Collinear B C Y âˆ§ Collinear A C Y [ABCYcol] by fol - YrAC IN_DIFF IN_SING IN_Ray; C = Y [] by fol H1 ABCYcol TwoSidesTriangle1Intersection; seg A C â‰¡ seg A' C' [] by fol - YrAC; fol H1 H2 SegmentSymmetry - H3 BCAeq BACeq AngleSymmetry TriangleCong_DEF; qed; `;; let ASA = theorem `; âˆ€A B C A' B' C'. Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' â‡’ seg A C â‰¡ seg A' C' â‡’ âˆ¡ C A B â‰¡ âˆ¡ C' A' B' âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B' C' A' â‡’ A,B,C â‰… A',B',C' proof intro_TAC âˆ€A B C A' B' C', H1, H2, H3; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬(A' = B') âˆ§ Â¬(A' = C') âˆ§ Â¬(B' = C') âˆ§ Segment (seg C' B') [Distinct] by fol H1 NonCollinearImpliesDistinct SEGMENT; consider D such that D âˆˆ ray C B â” {C} âˆ§ seg C D â‰¡ seg C' B' âˆ§ Â¬(D = C) [DrCB] by fol - C1 IN_DIFF IN_SING; Collinear C B D [CBDcol] by fol - IN_DIFF IN_SING IN_Ray; Â¬Collinear D C A âˆ§ Angle (âˆ¡ C A D) âˆ§ Angle (âˆ¡ C' A' B') âˆ§ Angle (âˆ¡ C A B) [DCAncol] by fol H1 CollinearSymmetry - DrCB NoncollinearityExtendsToLine H1 ANGLE; consider b such that Line b âˆ§ A âˆˆ b âˆ§ C âˆˆ b [b_line] by fol Distinct I1; B âˆ‰ b âˆ§ Â¬(D = A) [notBb] by fol H1 - Collinear_DEF âˆ‰ DCAncol NonCollinearImpliesDistinct; D âˆ‰ b âˆ§ D,B same_side b [Dsim_bB] by fol b_line - DrCB RaySameSide; ray C D = ray C B [] by fol Distinct DrCB RayWellDefined; âˆ¡ D C A â‰¡ âˆ¡ B' C' A' [] by fol H3 - Angle_DEF; D,C,A â‰… B',C',A' [] by fol DCAncol H1 CollinearSymmetry DrCB H2 SegmentSymmetry - SAS; âˆ¡ C A D â‰¡ âˆ¡ C' A' B' [] by fol - TriangleCong_DEF; âˆ¡ C A D â‰¡ âˆ¡ C A B [] by fol DCAncol - H3 C5Symmetric C5Transitive; ray A B = ray A D âˆ§ D âˆˆ ray A B [] by fol b_line Distinct notBb Dsim_bB - C4Uniqueness notBb EndpointInRay; Collinear A B D [ABDcol] by fol - IN_Ray; D = B [] by fol H1 CBDcol ABDcol CollinearSymmetry TwoSidesTriangle1Intersection; seg C B â‰¡ seg C' B' [] by fol - DrCB; B,C,A â‰… B',C',A' [] by fol H1 CollinearSymmetry - H2 SegmentSymmetry H3 SAS; fol - TriangleCongSymmetry; qed; `;; let AngleSubtraction = theorem `; âˆ€A O B A' O' B' G G'. G âˆˆ int_angle A O B âˆ§ G' âˆˆ int_angle A' O' B' â‡’ âˆ¡ A O B â‰¡ âˆ¡ A' O' B' âˆ§ âˆ¡ A O G â‰¡ âˆ¡ A' O' G' â‡’ âˆ¡ G O B â‰¡ âˆ¡ G' O' B' proof intro_TAC âˆ€A O B A' O' B' G G', H1, H2; Â¬Collinear A O B âˆ§ Â¬Collinear A' O' B' [A'O'B'ncol] by fol H1 IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬(G = O) âˆ§ Â¬(G' = O') âˆ§ Segment (seg O' A') âˆ§ Segment (seg O' B') [Distinct] by fol - NonCollinearImpliesDistinct H1 InteriorEZHelp SEGMENT; consider X Y such that X âˆˆ ray O A â” {O} âˆ§ seg O X â‰¡ seg O' A' âˆ§ Y âˆˆ ray O B â” {O} âˆ§ seg O Y â‰¡ seg O' B' [XYexists] by fol - C1; G âˆˆ int_angle X O Y [GintXOY] by fol H1 XYexists InteriorWellDefined InteriorAngleSymmetry; consider H H' such that H âˆˆ Open (X, Y) âˆ§ H âˆˆ ray O G â” {O} âˆ§ H' âˆˆ Open (A', B') âˆ§ H' âˆˆ ray O' G' â” {O'} [Hexists] by fol - H1 Crossbar_THM; H âˆˆ int_angle X O Y âˆ§ H' âˆˆ int_angle A' O' B' [HintXOY] by fol GintXOY H1 - WholeRayInterior; ray O X = ray O A âˆ§ ray O Y = ray O B âˆ§ ray O H = ray O G âˆ§ ray O' H' = ray O' G' [Orays] by fol Distinct XYexists Hexists RayWellDefined; âˆ¡ X O Y â‰¡ âˆ¡ A' O' B' âˆ§ âˆ¡ X O H â‰¡ âˆ¡ A' O' H' [H2'] by fol H2 - Angle_DEF; Â¬Collinear X O Y [] by fol GintXOY IN_InteriorAngle; X,O,Y â‰… A',O',B' [] by fol - A'O'B'ncol H2' XYexists SAS; seg X Y â‰¡ seg A' B' âˆ§ âˆ¡ O Y X â‰¡ âˆ¡ O' B' A' âˆ§ âˆ¡ Y X O â‰¡ âˆ¡ B' A' O' [XOYcong] by fol - TriangleCong_DEF; Â¬Collinear O H X âˆ§ Â¬Collinear O' H' A' âˆ§ Â¬Collinear O Y H âˆ§ Â¬Collinear O' B' H' [OHXncol] by fol HintXOY InteriorEZHelp InteriorAngleSymmetry CollinearSymmetry; ray X H = ray X Y âˆ§ ray A' H' = ray A' B' âˆ§ ray Y H = ray Y X âˆ§ ray B' H' = ray B' A' [Hrays] by fol Hexists B1' IntervalRay; âˆ¡ H X O â‰¡ âˆ¡ H' A' O' [] by fol XOYcong - Angle_DEF; O,H,X â‰… O',H',A' [] by fol OHXncol XYexists - H2' ASA; seg X H â‰¡ seg A' H' [] by fol - TriangleCong_DEF SegmentSymmetry; seg H Y â‰¡ seg H' B' [] by fol Hexists XOYcong - SegmentSubtraction; seg Y O â‰¡ seg B' O' âˆ§ seg Y H â‰¡ seg B' H' [YHeq] by fol XYexists - SegmentSymmetry; âˆ¡ O Y H â‰¡ âˆ¡ O' B' H' [] by fol XOYcong Hrays Angle_DEF; O,Y,H â‰… O',B',H' [] by fol OHXncol YHeq - SAS; âˆ¡ H O Y â‰¡ âˆ¡ H' O' B' [] by fol - TriangleCong_DEF; fol - Orays Angle_DEF; qed; `;; let OrderedCongruentAngles = theorem `; âˆ€A O B A' O' B' G. Â¬Collinear A' O' B' âˆ§ âˆ¡ A O B â‰¡ âˆ¡ A' O' B' âˆ§ G âˆˆ int_angle A O B â‡’ âˆƒG'. G' âˆˆ int_angle A' O' B' âˆ§ âˆ¡ A O G â‰¡ âˆ¡ A' O' G' proof intro_TAC âˆ€A O B A' O' B' G, H1 H2 H3; Â¬Collinear A O B [AOBncol] by fol H3 IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬(A' = B') âˆ§ Â¬(O = G) âˆ§ Segment (seg O' A') âˆ§ Segment (seg O' B') [Distinct] by fol AOBncol H1 NonCollinearImpliesDistinct H3 InteriorEZHelp SEGMENT; consider X Y such that X âˆˆ ray O A â” {O} âˆ§ seg O X â‰¡ seg O' A' âˆ§ Y âˆˆ ray O B â” {O} âˆ§ seg O Y â‰¡ seg O' B' [defXY] by fol - C1; G âˆˆ int_angle X O Y [GintXOY] by fol H3 - InteriorWellDefined InteriorAngleSymmetry; Â¬Collinear X O Y âˆ§ Â¬(X = Y) [XOYncol] by fol - IN_InteriorAngle NonCollinearImpliesDistinct; consider H such that H âˆˆ Open (X, Y) âˆ§ H âˆˆ ray O G â” {O} [defH] by fol GintXOY Crossbar_THM; ray O X = ray O A âˆ§ ray O Y = ray O B âˆ§ ray O H = ray O G [Orays] by fol Distinct defXY - RayWellDefined; âˆ¡ X O Y â‰¡ âˆ¡ A' O' B' [] by fol H2 - Angle_DEF; X,O,Y â‰… A',O',B' [] by fol XOYncol H1 defXY - SAS; seg X Y â‰¡ seg A' B' âˆ§ âˆ¡ O X Y â‰¡ âˆ¡ O' A' B' [YXOcong] by fol - TriangleCong_DEF AngleSymmetry; consider G' such that G' âˆˆ Open (A', B') âˆ§ seg X H â‰¡ seg A' G' [A'G'B'] by fol XOYncol Distinct - defH OrderedCongruentSegments; G' âˆˆ int_angle A' O' B' [G'intA'O'B'] by fol H1 - ConverseCrossbar; ray X H = ray X Y âˆ§ ray A' G' = ray A' B' [] by fol defH A'G'B' IntervalRay; âˆ¡ O X H â‰¡ âˆ¡ O' A' G' [HXOeq] by fol - Angle_DEF YXOcong; H âˆˆ int_angle X O Y [] by fol GintXOY defH WholeRayInterior; Â¬Collinear O X H âˆ§ Â¬Collinear O' A' G' [] by fol - G'intA'O'B' InteriorEZHelp CollinearSymmetry; O,X,H â‰… O',A',G' [] by fol - A'G'B' defXY SegmentSymmetry HXOeq SAS; âˆ¡ X O H â‰¡ âˆ¡ A' O' G' [] by fol - TriangleCong_DEF AngleSymmetry; fol G'intA'O'B' - Orays Angle_DEF; qed; `;; let AngleAddition = theorem `; âˆ€A O B A' O' B' G G'. G âˆˆ int_angle A O B âˆ§ G' âˆˆ int_angle A' O' B' â‡’ âˆ¡ A O G â‰¡ âˆ¡ A' O' G' âˆ§ âˆ¡ G O B â‰¡ âˆ¡ G' O' B' â‡’ âˆ¡ A O B â‰¡ âˆ¡ A' O' B' proof intro_TAC âˆ€A O B A' O' B' G G', H1, H2; Â¬Collinear A O B âˆ§ Â¬Collinear A' O' B' [AOBncol] by fol H1 IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) âˆ§ Â¬(A' = O') âˆ§ Â¬(A' = B') âˆ§ Â¬(O' = B') âˆ§ Â¬(G = O) [Distinct] by fol - NonCollinearImpliesDistinct H1 InteriorEZHelp; consider a b such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [a_line] by fol Distinct I1; consider g such that Line g âˆ§ O âˆˆ g âˆ§ G âˆˆ g [g_line] by fol Distinct I1; G âˆ‰ a âˆ§ G,B same_side a [H1'] by fol a_line H1 InteriorUse; Â¬Collinear A O G âˆ§ Â¬Collinear A' O' G' [AOGncol] by fol H1 InteriorEZHelp IN_InteriorAngle; Angle (âˆ¡ A O B) âˆ§ Angle (âˆ¡ A' O' B') âˆ§ Angle (âˆ¡ A O G) âˆ§ Angle (âˆ¡ A' O' G') [angles] by fol AOBncol - ANGLE; âˆƒ! r. Ray r âˆ§ âˆƒX. Â¬(O = X) âˆ§ r = ray O X âˆ§ X âˆ‰ a âˆ§ X,G same_side a âˆ§ âˆ¡ A O X â‰¡ âˆ¡ A' O' B' [] by simplify C4 - angles Distinct a_line H1'; consider X such that X âˆ‰ a âˆ§ X,G same_side a âˆ§ âˆ¡ A O X â‰¡ âˆ¡ A' O' B' [Xexists] by fol -; Â¬Collinear A O X [AOXncol] by fol Distinct a_line Xexists NonCollinearRaa CollinearSymmetry; âˆ¡ A' O' B' â‰¡ âˆ¡ A O X [] by fol - AOBncol ANGLE Xexists C5Symmetric; consider Y such that Y âˆˆ int_angle A O X âˆ§ âˆ¡ A' O' G' â‰¡ âˆ¡ A O Y [YintAOX] by fol AOXncol - H1 OrderedCongruentAngles; Â¬Collinear A O Y [] by fol - InteriorEZHelp; âˆ¡ A O Y â‰¡ âˆ¡ A O G [AOGeq] by fol - angles - ANGLE YintAOX H2 C5Transitive C5Symmetric; consider x such that Line x âˆ§ O âˆˆ x âˆ§ X âˆˆ x [x_line] by fol Distinct I1; Y âˆ‰ a âˆ§ Y,X same_side a [] by fol a_line - YintAOX InteriorUse; Y âˆ‰ a âˆ§ Y,G same_side a [] by fol a_line - Xexists H1' SameSideTransitive; ray O G = ray O Y [] by fol a_line Distinct H1' - AOGeq C4Uniqueness; G âˆˆ ray O Y â” {O} [] by fol Distinct - EndpointInRay IN_DIFF IN_SING; G âˆˆ int_angle A O X [GintAOX] by fol YintAOX - WholeRayInterior; âˆ¡ G O X â‰¡ âˆ¡ G' O' B' [GOXeq] by fol - H1 Xexists H2 AngleSubtraction; Â¬Collinear G O X âˆ§ Â¬Collinear G O B âˆ§ Â¬Collinear G' O' B' [GOXncol] by fol GintAOX H1 InteriorAngleSymmetry InteriorEZHelp CollinearSymmetry; Angle (âˆ¡ G O X) âˆ§ Angle (âˆ¡ G O B) âˆ§ Angle (âˆ¡ G' O' B') [] by fol - ANGLE; âˆ¡ G O X â‰¡ âˆ¡ G O B [G'O'Xeq] by fol angles - GOXeq C5Symmetric H2 C5Transitive; Â¬(A,X same_side g) âˆ§ Â¬(A,B same_side g) [Ansim_aXB] by fol g_line GintAOX H1 InteriorOpposite; A âˆ‰ g âˆ§ B âˆ‰ g âˆ§ X âˆ‰ g [notABXg] by fol g_line AOGncol GOXncol Distinct I1 Collinear_DEF âˆ‰; X,B same_side g [] by fol g_line - Ansim_aXB AtMost2Sides; ray O X = ray O B [] by fol g_line Distinct notABXg - G'O'Xeq C4Uniqueness; fol - Xexists Angle_DEF; qed; `;; let AngleOrderingUse = theorem `; âˆ€A O B Î±. Angle Î± âˆ§ Â¬Collinear A O B â‡’ Î± <_ang âˆ¡ A O B â‡’ âˆƒG. G âˆˆ int_angle A O B âˆ§ Î± â‰¡ âˆ¡ A O G proof intro_TAC âˆ€A O B Î±, H1, H3; consider A' O' B' G' such that Â¬Collinear A' O' B' âˆ§ âˆ¡ A O B = âˆ¡ A' O' B' âˆ§ G' âˆˆ int_angle A' O' B' âˆ§ Î± â‰¡ âˆ¡ A' O' G' [H3'] by fol H3 AngleOrdering_DEF; Angle (âˆ¡ A O B) âˆ§ Angle (âˆ¡ A' O' B') âˆ§ Angle (âˆ¡ A' O' G') [angles] by fol H1 - ANGLE InteriorEZHelp; âˆ¡ A' O' B' â‰¡ âˆ¡ A O B [] by fol - H3' C5Reflexive; consider G such that G âˆˆ int_angle A O B âˆ§ âˆ¡ A' O' G' â‰¡ âˆ¡ A O G [GintAOB] by fol H1 H3' - OrderedCongruentAngles; Î± â‰¡ âˆ¡ A O G [] by fol H1 angles - InteriorEZHelp ANGLE H3' GintAOB C5Transitive; fol - GintAOB; qed; `;; let AngleTrichotomy1 = theorem `; âˆ€Î± Î². Î± <_ang Î² â‡’ Â¬(Î± â‰¡ Î²) proof intro_TAC âˆ€Î± Î², H1; assume Î± â‰¡ Î² [Con] by fol; consider A O B G such that Angle Î± âˆ§ Â¬Collinear A O B âˆ§ Î² = âˆ¡ A O B âˆ§ G âˆˆ int_angle A O B âˆ§ Î± â‰¡ âˆ¡ A O G [H1'] by fol H1 AngleOrdering_DEF; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬Collinear A O G [Distinct] by fol H1' NonCollinearImpliesDistinct InteriorEZHelp; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by fol Distinct I1; consider b such that Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [b_line] by fol Distinct I1; B âˆ‰ a [notBa] by fol a_line H1' Collinear_DEF âˆ‰; G âˆ‰ a âˆ§ G âˆ‰ b âˆ§ G,B same_side a [GintAOB] by fol a_line b_line H1' InteriorUse; âˆ¡ A O G â‰¡ Î± [] by fol H1' Distinct ANGLE C5Symmetric; âˆ¡ A O G â‰¡ âˆ¡ A O B [] by fol H1' Distinct ANGLE - Con C5Transitive; ray O B = ray O G [] by fol a_line Distinct notBa GintAOB - C4Uniqueness; G âˆˆ b [] by fol Distinct - EndpointInRay b_line RayLine SUBSET; fol - GintAOB âˆ‰; qed; `;; let AngleTrichotomy2 = theorem `; âˆ€Î± Î² Î³. Î± <_ang Î² âˆ§ Angle Î³ âˆ§ Î² â‰¡ Î³ â‡’ Î± <_ang Î³ proof intro_TAC âˆ€Î± Î² Î³, H1 H2 H3; consider A O B G such that Angle Î± âˆ§ Â¬Collinear A O B âˆ§ Î² = âˆ¡ A O B âˆ§ G âˆˆ int_angle A O B âˆ§ Î± â‰¡ âˆ¡ A O G [H1'] by fol H1 AngleOrdering_DEF; consider A' O' B' such that Î³ = âˆ¡ A' O' B' âˆ§ Â¬Collinear A' O' B' [Î³A'O'B'] by fol H2 ANGLE; consider G' such that G' âˆˆ int_angle A' O' B' âˆ§ âˆ¡ A O G â‰¡ âˆ¡ A' O' G' [G'intA'O'B'] by fol Î³A'O'B' H1' H3 OrderedCongruentAngles; Â¬Collinear A O G âˆ§ Â¬Collinear A' O' G' [ncol] by fol H1' - InteriorEZHelp; Î± â‰¡ âˆ¡ A' O' G' [] by fol H1' ANGLE - G'intA'O'B' C5Transitive; fol H1' - ncol Î³A'O'B' G'intA'O'B' - AngleOrdering_DEF; qed; `;; let AngleOrderTransitivity = theorem `; âˆ€Î± Î² Î³. Î± <_ang Î² âˆ§ Î² <_ang Î³ â‡’ Î± <_ang Î³ proof intro_TAC âˆ€Î± Î² Î³, H1 H2; consider A O B G such that Angle Î² âˆ§ Â¬Collinear A O B âˆ§ Î³ = âˆ¡ A O B âˆ§ G âˆˆ int_angle A O B âˆ§ Î² â‰¡ âˆ¡ A O G [H2'] by fol H2 AngleOrdering_DEF; Â¬Collinear A O G [AOGncol] by fol H2' InteriorEZHelp; Angle Î± âˆ§ Angle (âˆ¡ A O G) âˆ§ Angle Î³ [angles] by fol H1 AngleOrdering_DEF H2' - ANGLE; Î± <_ang âˆ¡ A O G [] by fol H1 H2' - AngleTrichotomy2; consider F such that F âˆˆ int_angle A O G âˆ§ Î± â‰¡ âˆ¡ A O F [FintAOG] by fol angles AOGncol - AngleOrderingUse; F âˆˆ int_angle A O B [] by fol H2' - InteriorTransitivity; fol angles H2' - FintAOG AngleOrdering_DEF; qed; `;; let AngleTrichotomy = theorem `; âˆ€Î± Î². Angle Î± âˆ§ Angle Î² â‡’ (Î± â‰¡ Î² âˆ¨ Î± <_ang Î² âˆ¨ Î² <_ang Î±) âˆ§ Â¬(Î± â‰¡ Î² âˆ§ Î± <_ang Î²) âˆ§ Â¬(Î± â‰¡ Î² âˆ§ Î² <_ang Î±) âˆ§ Â¬(Î± <_ang Î² âˆ§ Î² <_ang Î±) proof intro_TAC âˆ€Î± Î², H1; Â¬(Î± â‰¡ Î² âˆ§ Î± <_ang Î²) [Not12] by fol AngleTrichotomy1; Â¬(Î± â‰¡ Î² âˆ§ Î² <_ang Î±) [Not13] by fol H1 C5Symmetric AngleTrichotomy1; Â¬(Î± <_ang Î² âˆ§ Î² <_ang Î±) [Not23] by fol H1 AngleOrderTransitivity AngleTrichotomy1 C5Reflexive; consider P O A such that Î± = âˆ¡ P O A âˆ§ Â¬Collinear P O A [POA] by fol H1 ANGLE; Â¬(P = O) âˆ§ Â¬(O = A) [Distinct] by fol - NonCollinearImpliesDistinct; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by fol - I1; P âˆ‰ a [notPa] by fol - Distinct I1 POA Collinear_DEF âˆ‰; âˆƒ! r. Ray r âˆ§ âˆƒQ. Â¬(O = Q) âˆ§ r = ray O Q âˆ§ Q âˆ‰ a âˆ§ Q,P same_side a âˆ§ âˆ¡ A O Q â‰¡ Î² [] by simplify H1 Distinct a_line C4 -; consider Q such that Â¬(O = Q) âˆ§ Q âˆ‰ a âˆ§ Q,P same_side a âˆ§ âˆ¡ A O Q â‰¡ Î² [Qexists] by fol -; O âˆ‰ Open (Q, P) [notQOP] by fol a_line Qexists SameSide_DEF âˆ‰; Â¬Collinear A O P [AOPncol] by fol POA CollinearSymmetry; Â¬Collinear A O Q [AOQncol] by fol a_line Distinct I1 Collinear_DEF Qexists âˆ‰; Angle (âˆ¡ A O P) âˆ§ Angle (âˆ¡ A O Q) [] by fol AOPncol - ANGLE; Î± â‰¡ âˆ¡ A O P âˆ§ Î² â‰¡ âˆ¡ A O Q âˆ§ âˆ¡ A O P â‰¡ Î± [flip] by fol H1 - POA AngleSymmetry C5Reflexive Qexists C5Symmetric; case_split QOPcol | QOPcolncol by fol -; suppose Collinear Q O P; Collinear O P Q [] by fol - CollinearSymmetry; Q âˆˆ ray O P â” {O} [] by fol Distinct - notQOP IN_Ray Qexists IN_DIFF IN_SING; ray O Q = ray O P [] by fol Distinct - RayWellDefined; âˆ¡ P O A = âˆ¡ A O Q [] by fol - Angle_DEF AngleSymmetry; fol - POA Qexists Not12 Not13 Not23; end; suppose Â¬Collinear Q O P; P âˆˆ int_angle Q O A âˆ¨ Q âˆˆ int_angle P O A [] by fol Distinct a_line Qexists notPa - AngleOrdering; P âˆˆ int_angle A O Q âˆ¨ Q âˆˆ int_angle A O P [] by fol - InteriorAngleSymmetry; Î± <_ang âˆ¡ A O Q âˆ¨ Î² <_ang âˆ¡ A O P [] by fol H1 AOQncol AOPncol - flip AngleOrdering_DEF; Î± <_ang Î² âˆ¨ Î² <_ang Î± [] by fol H1 - Qexists flip AngleTrichotomy2; fol - Not12 Not13 Not23; end; qed; `;; let SupplementExists = theorem `; âˆ€Î±. Angle Î± â‡’ âˆƒÎ±'. Î± suppl Î±' proof intro_TAC âˆ€Î±, H1; consider A O B such that Î± = âˆ¡ A O B âˆ§ Â¬Collinear A O B âˆ§ Â¬(A = O) [def_Î±] by fol H1 ANGLE NonCollinearImpliesDistinct; consider A' such that O âˆˆ Open (A, A') [AOA'] by fol - B2'; âˆ¡ A O B suppl âˆ¡ A' O B [AOBsup] by fol def_Î± - SupplementaryAngles_DEF AngleSymmetry; fol - def_Î±; qed; `;; let SupplementImpliesAngle = theorem `; âˆ€Î± Î². Î± suppl Î² â‡’ Angle Î± âˆ§ Angle Î² proof intro_TAC âˆ€Î± Î², H1; consider A O B A' such that Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î² = âˆ¡ B O A' [H1'] by fol H1 SupplementaryAngles_DEF; Â¬(O = A') âˆ§ Collinear A O A' [Distinct] by fol - NonCollinearImpliesDistinct B1'; Â¬Collinear B O A' [] by fol H1' CollinearSymmetry - NoncollinearityExtendsToLine; fol H1' - ANGLE; qed; `;; let RightImpliesAngle = theorem `; âˆ€Î±. Right Î± â‡’ Angle Î± by fol RightAngle_DEF SupplementImpliesAngle`;; let SupplementSymmetry = theorem `; âˆ€Î± Î². Î± suppl Î² â‡’ Î² suppl Î± proof intro_TAC âˆ€Î± Î², H1; consider A O B A' such that Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î² = âˆ¡ B O A' [H1'] by fol H1 SupplementaryAngles_DEF; Â¬(O = A') âˆ§ Collinear A O A' [] by fol - NonCollinearImpliesDistinct B1'; Â¬Collinear A' O B [A'OBncol] by fol H1' CollinearSymmetry - NoncollinearityExtendsToLine; O âˆˆ Open (A', A) âˆ§ Î² = âˆ¡ A' O B âˆ§ Î± = âˆ¡ B O A [] by fol H1' B1' AngleSymmetry; fol A'OBncol - SupplementaryAngles_DEF; qed; `;; let SupplementsCongAnglesCong = theorem `; âˆ€Î± Î² Î±' Î²'. Î± suppl Î±' âˆ§ Î² suppl Î²' â‡’ Î± â‰¡ Î² â‡’ Î±' â‰¡ Î²' proof intro_TAC âˆ€Î± Î² Î±' Î²', H1, H2; consider A O B A' such that Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î±' = âˆ¡ B O A' [def_Î±] by fol H1 SupplementaryAngles_DEF; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬(A = A') âˆ§ Â¬(O = A') âˆ§ Collinear A O A' [DistinctÎ±] by fol - NonCollinearImpliesDistinct B1'; Â¬Collinear B A A' âˆ§ Â¬Collinear O A' B [BAA'ncol] by fol def_Î± CollinearSymmetry - NoncollinearityExtendsToLine; Segment (seg O A) âˆ§ Segment (seg O B) âˆ§ Segment (seg O A') [Osegments] by fol DistinctÎ± SEGMENT; consider C P D C' such that Â¬Collinear C P D âˆ§ P âˆˆ Open (C, C') âˆ§ Î² = âˆ¡ C P D âˆ§ Î²' = âˆ¡ D P C' [def_Î²] by fol H1 SupplementaryAngles_DEF; Â¬(C = P) âˆ§ Â¬(P = D) âˆ§ Â¬(P = C') [DistinctÎ²] by fol def_Î² NonCollinearImpliesDistinct B1'; consider X such that X âˆˆ ray P C â” {P} âˆ§ seg P X â‰¡ seg O A [defX] by fol Osegments DistinctÎ² C1; consider Y such that Y âˆˆ ray P D â” {P} âˆ§ seg P Y â‰¡ seg O B âˆ§ Â¬(Y = P) [defY] by fol Osegments DistinctÎ² C1 IN_DIFF IN_SING; consider X' such that X' âˆˆ ray P C' â” {P} âˆ§ seg P X' â‰¡ seg O A' [defX'] by fol Osegments DistinctÎ² C1; P âˆˆ Open (X', C) âˆ§ P âˆˆ Open (X, X') [XPX'] by fol def_Î² - OppositeRaysIntersect1pointHelp defX; Â¬(X = P) âˆ§ Â¬(X' = P) âˆ§ Collinear X P X' âˆ§ Â¬(X = X') âˆ§ ray A' O = ray A' A âˆ§ ray X' P = ray X' X [XPX'line] by fol defX defX' IN_DIFF IN_SING - B1' def_Î± IntervalRay; Collinear P D Y âˆ§ Collinear P C X [] by fol defY defX IN_DIFF IN_SING IN_Ray; Â¬Collinear C P Y âˆ§ Â¬Collinear X P Y [XPYncol] by fol def_Î² - defY NoncollinearityExtendsToLine CollinearSymmetry XPX'line; Â¬Collinear Y X X' âˆ§ Â¬Collinear P X' Y [YXX'ncol] by fol - CollinearSymmetry XPX' XPX'line NoncollinearityExtendsToLine; ray P X = ray P C âˆ§ ray P Y = ray P D âˆ§ ray P X' = ray P C' [equalPrays] by fol DistinctÎ² defX defY defX' RayWellDefined; Î² = âˆ¡ X P Y âˆ§ Î²' = âˆ¡ Y P X' âˆ§ âˆ¡ A O B â‰¡ âˆ¡ X P Y [AOBeqXPY] by fol def_Î² - Angle_DEF H2 def_Î±; seg O A â‰¡ seg P X âˆ§ seg O B â‰¡ seg P Y âˆ§ seg A' O â‰¡ seg X' P [OAeq] by fol Osegments XPX'line SEGMENT defX defY defX' C2Symmetric SegmentSymmetry; seg A A' â‰¡ seg X X' [AA'eq] by fol def_Î± XPX'line XPX' - SegmentSymmetry C3; A,O,B â‰… X,P,Y [] by fol def_Î± XPYncol OAeq AOBeqXPY SAS; seg A B â‰¡ seg X Y âˆ§ âˆ¡ B A O â‰¡ âˆ¡ Y X P [AOBâ‰…] by fol - TriangleCong_DEF AngleSymmetry; ray A O = ray A A' âˆ§ ray X P = ray X X' âˆ§ âˆ¡ B A A' â‰¡ âˆ¡ Y X X' [] by fol def_Î± XPX' IntervalRay - Angle_DEF; B,A,A' â‰… Y,X,X' [] by fol BAA'ncol YXX'ncol AOBâ‰… - AA'eq - SAS; seg A' B â‰¡ seg X' Y âˆ§ âˆ¡ A A' B â‰¡ âˆ¡ X X' Y [] by fol - TriangleCong_DEF SegmentSymmetry; O,A',B â‰… P,X',Y [] by fol BAA'ncol YXX'ncol OAeq - XPX'line Angle_DEF SAS; âˆ¡ B O A' â‰¡ âˆ¡ Y P X' [] by fol - TriangleCong_DEF; fol - equalPrays def_Î² Angle_DEF def_Î±; qed; `;; let SupplementUnique = theorem `; âˆ€Î± Î² Î²'. Î± suppl Î² âˆ§ Î± suppl Î²' â‡’ Î² â‰¡ Î²' by fol SupplementaryAngles_DEF ANGLE C5Reflexive SupplementsCongAnglesCong`;; let CongRightImpliesRight = theorem `; âˆ€Î± Î². Angle Î± âˆ§ Right Î² â‡’ Î± â‰¡ Î² â‡’ Right Î± proof intro_TAC âˆ€Î± Î², H1, H2; consider Î±' Î²' such that Î± suppl Î±' âˆ§ Î² suppl Î²' âˆ§ Î² â‰¡ Î²' [suppl] by fol H1 SupplementExists H1 RightAngle_DEF; Î±' â‰¡ Î²' [Î±'eqÎ²'] by fol suppl H2 SupplementsCongAnglesCong; Angle Î² âˆ§ Angle Î±' âˆ§ Angle Î²' [] by fol suppl SupplementImpliesAngle; Î± â‰¡ Î±' [] by fol H1 - H2 suppl Î±'eqÎ²' C5Symmetric C5Transitive; fol suppl - RightAngle_DEF; qed; `;; let RightAnglesCongruentHelp = theorem `; âˆ€A O B A' P a. Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') â‡’ Right (âˆ¡ A O B) âˆ§ Right (âˆ¡ A O P) â‡’ P âˆ‰ int_angle A O B proof intro_TAC âˆ€A O B A' P a, H1, H2; assume Â¬(P âˆ‰ int_angle A O B) [Con] by fol; P âˆˆ int_angle A O B [PintAOB] by fol - âˆ‰; B âˆˆ int_angle P O A' âˆ§ B âˆˆ int_angle A' O P [BintA'OP] by fol H1 - InteriorReflectionInterior InteriorAngleSymmetry ; Â¬Collinear A O P âˆ§ Â¬Collinear P O A' [AOPncol] by fol PintAOB InteriorEZHelp - IN_InteriorAngle; âˆ¡ A O B suppl âˆ¡ B O A' âˆ§ âˆ¡ A O P suppl âˆ¡ P O A' [AOBsup] by fol H1 - SupplementaryAngles_DEF; consider Î±' Î²' such that âˆ¡ A O B suppl Î±' âˆ§ âˆ¡ A O B â‰¡ Î±' âˆ§ âˆ¡ A O P suppl Î²' âˆ§ âˆ¡ A O P â‰¡ Î²' [supplÎ±'] by fol H2 RightAngle_DEF; Î±' â‰¡ âˆ¡ B O A' âˆ§ Î²' â‰¡ âˆ¡ P O A' [Î±'eqA'OB] by fol - AOBsup SupplementUnique; Angle (âˆ¡ A O B) âˆ§ Angle Î±' âˆ§ Angle (âˆ¡ B O A') âˆ§ Angle (âˆ¡ A O P) âˆ§ Angle Î²' âˆ§ Angle (âˆ¡ P O A') [angles] by fol AOBsup supplÎ±' SupplementImpliesAngle AngleSymmetry; âˆ¡ A O B â‰¡ âˆ¡ B O A' âˆ§ âˆ¡ A O P â‰¡ âˆ¡ P O A' [H2'] by fol - supplÎ±' Î±'eqA'OB C5Transitive; âˆ¡ A O P â‰¡ âˆ¡ A O P âˆ§ âˆ¡ B O A' â‰¡ âˆ¡ B O A' [refl] by fol angles C5Reflexive; âˆ¡ A O P <_ang âˆ¡ A O B âˆ§ âˆ¡ B O A' <_ang âˆ¡ P O A' [BOA'lessPOA'] by fol angles H1 PintAOB - AngleOrdering_DEF AOPncol CollinearSymmetry BintA'OP AngleSymmetry; âˆ¡ A O P <_ang âˆ¡ B O A' [] by fol - angles H2' AngleTrichotomy2; âˆ¡ A O P <_ang âˆ¡ P O A' [] by fol - BOA'lessPOA' AngleOrderTransitivity; fol - H2' AngleTrichotomy1; qed; `;; let RightAnglesCongruent = theorem `; âˆ€Î± Î². Right Î± âˆ§ Right Î² â‡’ Î± â‰¡ Î² proof intro_TAC âˆ€Î± Î², H1; consider Î±' such that Î± suppl Î±' âˆ§ Î± â‰¡ Î±' [Î±right] by fol H1 RightAngle_DEF; consider A O B A' such that Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î±' = âˆ¡ B O A' [def_Î±] by fol - SupplementaryAngles_DEF; Â¬(A = O) âˆ§ Â¬(O = B) [Distinct] by fol def_Î± NonCollinearImpliesDistinct B1'; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by fol Distinct I1; B âˆ‰ a [notBa] by fol - def_Î± Collinear_DEF âˆ‰; Angle Î² [] by fol H1 RightImpliesAngle; âˆƒ! r. Ray r âˆ§ âˆƒP. Â¬(O = P) âˆ§ r = ray O P âˆ§ P âˆ‰ a âˆ§ P,B same_side a âˆ§ âˆ¡ A O P â‰¡ Î² [] by simplify C4 - Distinct a_line notBa; consider P such that Â¬(O = P) âˆ§ P âˆ‰ a âˆ§ P,B same_side a âˆ§ âˆ¡ A O P â‰¡ Î² [defP] by fol -; O âˆ‰ Open (P, B) [notPOB] by fol a_line - SameSide_DEF âˆ‰; Â¬Collinear A O P [AOPncol] by fol a_line Distinct defP NonCollinearRaa CollinearSymmetry; Right (âˆ¡ A O P) [AOPright] by fol - ANGLE H1 defP CongRightImpliesRight; P âˆ‰ int_angle A O B âˆ§ B âˆ‰ int_angle A O P [] by fol def_Î± H1 - AOPncol AOPright RightAnglesCongruentHelp; Collinear P O B [] by fol Distinct a_line defP notBa - AngleOrdering InteriorAngleSymmetry âˆ‰; P âˆˆ ray O B â” {O} [] by fol Distinct - CollinearSymmetry notPOB IN_Ray defP IN_DIFF IN_SING; ray O P = ray O B âˆ§ âˆ¡ A O P = âˆ¡ A O B [] by fol Distinct - RayWellDefined Angle_DEF; fol - defP def_Î±; qed; `;; let OppositeRightAnglesLinear = theorem `; âˆ€A B O H h. Â¬Collinear A O H âˆ§ Â¬Collinear H O B â‡’ Right (âˆ¡ A O H) âˆ§ Right (âˆ¡ H O B) â‡’ Line h âˆ§ O âˆˆ h âˆ§ H âˆˆ h âˆ§ Â¬(A,B same_side h) â‡’ O âˆˆ Open (A, B) proof intro_TAC âˆ€A B O H h, H0, H1, H2; Â¬(A = O) âˆ§ Â¬(O = H) âˆ§ Â¬(O = B) [Distinct] by fol H0 NonCollinearImpliesDistinct; A âˆ‰ h âˆ§ B âˆ‰ h [notABh] by fol H0 H2 Collinear_DEF âˆ‰; consider E such that O âˆˆ Open (A, E) âˆ§ Â¬(E = O) [AOE] by fol Distinct B2' B1'; âˆ¡ A O H suppl âˆ¡ H O E [AOHsupplHOE] by fol H0 - SupplementaryAngles_DEF; E âˆ‰ h [notEh] by fol H2 âˆ‰ AOE BetweenLinear notABh; Â¬(A,E same_side h) [] by fol H2 AOE SameSide_DEF; B,E same_side h [Bsim_hE] by fol H2 notABh notEh - H2 AtMost2Sides; consider Î±' such that âˆ¡ A O H suppl Î±' âˆ§ âˆ¡ A O H â‰¡ Î±' [AOHsupplÎ±'] by fol H1 RightAngle_DEF; Angle (âˆ¡ H O B) âˆ§ Angle (âˆ¡ A O H) âˆ§ Angle Î±' âˆ§ Angle (âˆ¡ H O E) [angÎ±'] by fol H1 RightImpliesAngle - AOHsupplHOE SupplementImpliesAngle; âˆ¡ H O B â‰¡ âˆ¡ A O H âˆ§ Î±' â‰¡ âˆ¡ H O E [] by fol H1 RightAnglesCongruent AOHsupplÎ±' AOHsupplHOE SupplementUnique; âˆ¡ H O B â‰¡ âˆ¡ H O E [] by fol angÎ±' - AOHsupplÎ±' C5Transitive; ray O B = ray O E [] by fol H2 Distinct notABh notEh Bsim_hE - C4Uniqueness; B âˆˆ ray O E â” {O} [] by fol Distinct EndpointInRay - IN_DIFF IN_SING; fol AOE - OppositeRaysIntersect1pointHelp B1'; qed; `;; let RightImpliesSupplRight = theorem `; âˆ€A O B A'. Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') âˆ§ Right (âˆ¡ A O B) â‡’ Right (âˆ¡ B O A') proof intro_TAC âˆ€A O B A', H1 H2 H3; âˆ¡ A O B suppl âˆ¡ B O A' âˆ§ Angle (âˆ¡ A O B) âˆ§ Angle (âˆ¡ B O A') [AOBsuppl] by fol H1 H2 SupplementaryAngles_DEF SupplementImpliesAngle; consider Î² such that âˆ¡ A O B suppl Î² âˆ§ âˆ¡ A O B â‰¡ Î² [Î²suppl] by fol H3 RightAngle_DEF; Angle Î² âˆ§ Î² â‰¡ âˆ¡ A O B [angÎ²] by fol - SupplementImpliesAngle C5Symmetric; âˆ¡ B O A' â‰¡ Î² [] by fol AOBsuppl Î²suppl SupplementUnique; âˆ¡ B O A' â‰¡ âˆ¡ A O B [] by fol AOBsuppl angÎ² - Î²suppl C5Transitive; fol AOBsuppl H3 - CongRightImpliesRight; qed; `;; let IsoscelesCongBaseAngles = theorem `; âˆ€A B C. Â¬Collinear A B C âˆ§ seg B A â‰¡ seg B C â‡’ âˆ¡ C A B â‰¡ âˆ¡ A C B proof intro_TAC âˆ€A B C, H1 H2; Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear C B A [CBAncol] by fol H1 NonCollinearImpliesDistinct CollinearSymmetry; seg B C â‰¡ seg B A âˆ§ âˆ¡ A B C â‰¡ âˆ¡ C B A [] by fol - SEGMENT H2 C2Symmetric H1 ANGLE AngleSymmetry C5Reflexive; fol H1 CBAncol H2 - SAS TriangleCong_DEF; qed; `;; let C4withC1 = theorem `; âˆ€Î± l O A Y P Q. Angle Î± âˆ§ Â¬(O = A) âˆ§ Â¬(P = Q) â‡’ Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ Y âˆ‰ l â‡’ âˆƒN. Â¬(O = N) âˆ§ N âˆ‰ l âˆ§ N,Y same_side l âˆ§ seg O N â‰¡ seg P Q âˆ§ âˆ¡ A O N â‰¡ Î± proof intro_TAC âˆ€Î± l O A Y P Q, H1, l_line; âˆƒ! r. Ray r âˆ§ âˆƒB. Â¬(O = B) âˆ§ r = ray O B âˆ§ B âˆ‰ l âˆ§ B,Y same_side l âˆ§ âˆ¡ A O B â‰¡ Î± [] by simplify C4 H1 l_line; consider B such that Â¬(O = B) âˆ§ B âˆ‰ l âˆ§ B,Y same_side l âˆ§ âˆ¡ A O B â‰¡ Î± [Bexists] by fol -; consider N such that N âˆˆ ray O B â” {O} âˆ§ seg O N â‰¡ seg P Q [Nexists] by fol H1 - SEGMENT C1; N âˆ‰ l âˆ§ N,B same_side l [notNl] by fol l_line Bexists Nexists RaySameSide; N,Y same_side l [Nsim_lY] by fol l_line - Bexists SameSideTransitive; ray O N = ray O B [] by fol Bexists Nexists RayWellDefined; âˆ¡ A O N â‰¡ Î± [] by fol - Bexists Angle_DEF; fol Nexists IN_DIFF IN_SING notNl Nsim_lY Nexists -; qed; `;; let C4OppositeSide = theorem `; âˆ€Î± l O A Z P Q. Angle Î± âˆ§ Â¬(O = A) âˆ§ Â¬(P = Q) â‡’ Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ Z âˆ‰ l â‡’ âˆƒN. Â¬(O = N) âˆ§ N âˆ‰ l âˆ§ Â¬(Z,N same_side l) âˆ§ seg O N â‰¡ seg P Q âˆ§ âˆ¡ A O N â‰¡ Î± proof intro_TAC âˆ€Î± l O A Z P Q, H1, l_line; Â¬(Z = O) [] by fol l_line âˆ‰; consider Y such that O âˆˆ Open (Z, Y) [ZOY] by fol - B2'; Â¬(O = Y) âˆ§ Collinear O Z Y [notOY] by fol - B1' CollinearSymmetry; Y âˆ‰ l [notYl] by fol notOY l_line NonCollinearRaa âˆ‰; consider N such that Â¬(O = N) âˆ§ N âˆ‰ l âˆ§ N,Y same_side l âˆ§ seg O N â‰¡ seg P Q âˆ§ âˆ¡ A O N â‰¡ Î± [Nexists] by simplify C4withC1 H1 l_line -; Â¬(Z,Y same_side l) [] by fol l_line ZOY SameSide_DEF; Â¬(Z,N same_side l) [] by fol l_line Nexists notYl - SameSideTransitive; fol - Nexists; qed; `;; let SSS = theorem `; âˆ€A B C A' B' C'. Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' â‡’ seg A B â‰¡ seg A' B' âˆ§ seg A C â‰¡ seg A' C' âˆ§ seg B C â‰¡ seg B' C' â‡’ A,B,C â‰… A',B',C' proof intro_TAC âˆ€A B C A' B' C', H1, H2; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬(A' = B') âˆ§ Â¬(B' = C') [Distinct] by fol H1 NonCollinearImpliesDistinct; consider h such that Line h âˆ§ A âˆˆ h âˆ§ C âˆˆ h [h_line] by fol Distinct I1; B âˆ‰ h [notBh] by fol h_line H1 âˆ‰ Collinear_DEF; Segment (seg A B) âˆ§ Segment (seg C B) âˆ§ Segment (seg A' B') âˆ§ Segment (seg C' B') [segments] by fol Distinct - SEGMENT; Angle (âˆ¡ C' A' B') [] by fol H1 CollinearSymmetry ANGLE; consider N such that Â¬(A = N) âˆ§ N âˆ‰ h âˆ§ Â¬(B,N same_side h) âˆ§ seg A N â‰¡ seg A' B' âˆ§ âˆ¡ C A N â‰¡ âˆ¡ C' A' B' [Nexists] by simplify C4OppositeSide - Distinct h_line notBh; Â¬(C = N) [] by fol h_line Nexists âˆ‰; Segment (seg A N) âˆ§ Segment (seg C N) [segN] by fol Nexists - SEGMENT; Â¬Collinear A N C [ANCncol] by fol Distinct h_line Nexists NonCollinearRaa; Angle (âˆ¡ A B C) âˆ§ Angle (âˆ¡ A' B' C') âˆ§ Angle (âˆ¡ A N C) [angles] by fol H1 - ANGLE; seg A B â‰¡ seg A N [ABeqAN] by fol segments segN Nexists H2 C2Symmetric C2Transitive; C,A,N â‰… C',A',B' [] by fol ANCncol H1 CollinearSymmetry H2 Nexists SAS; âˆ¡ A N C â‰¡ âˆ¡ A' B' C' âˆ§ seg C N â‰¡ seg C' B' [ANCeq] by fol - TriangleCong_DEF; seg C B â‰¡ seg C N [CBeqCN] by fol segments segN - H2 SegmentSymmetry C2Symmetric C2Transitive; consider G such that G âˆˆ h âˆ§ G âˆˆ Open (B, N) [BGN] by fol Nexists h_line SameSide_DEF; Â¬(B = N) [notBN] by fol - B1'; ray B G = ray B N âˆ§ ray N G = ray N B [Grays] by fol BGN B1' IntervalRay; consider v such that Line v âˆ§ B âˆˆ v âˆ§ N âˆˆ v [v_line] by fol notBN I1; G âˆˆ v âˆ§ Â¬(h = v) [] by fol v_line BGN BetweenLinear notBh âˆ‰; h âˆ© v = {G} [hvG] by fol h_line v_line - BGN I1Uniqueness; Â¬(G = A) â‡’ âˆ¡ A B G â‰¡ âˆ¡ A N G [ABGeqANG] proof intro_TAC notGA; A âˆ‰ v [] by fol hvG h_line - EquivIntersectionHelp IN_DIFF IN_SING; Â¬Collinear B A N [] by fol v_line notBN I1 Collinear_DEF - âˆ‰; âˆ¡ N B A â‰¡ âˆ¡ B N A [] by fol - ABeqAN IsoscelesCongBaseAngles; âˆ¡ G B A â‰¡ âˆ¡ G N A [] by fol - Grays Angle_DEF notGA; fol - AngleSymmetry; qed; Â¬(G = C) â‡’ âˆ¡ G B C â‰¡ âˆ¡ G N C [GBCeqGNC] proof intro_TAC notGC; C âˆ‰ v [] by fol hvG h_line - EquivIntersectionHelp IN_DIFF IN_SING; Â¬Collinear B C N [] by fol v_line notBN I1 Collinear_DEF - âˆ‰; âˆ¡ N B C â‰¡ âˆ¡ B N C [] by fol - CBeqCN IsoscelesCongBaseAngles AngleSymmetry; fol - Grays Angle_DEF; qed; âˆ¡ A B C â‰¡ âˆ¡ A N C [] proof assume Â¬(G = A) âˆ§ Â¬(G = C) [AGCdistinct] by fol Distinct GBCeqGNC ABGeqANG; âˆ¡ A B G â‰¡ âˆ¡ A N G âˆ§ âˆ¡ G B C â‰¡ âˆ¡ G N C [Gequivs] by fol - ABGeqANG GBCeqGNC; Â¬Collinear G B C âˆ§ Â¬Collinear G N C âˆ§ Â¬Collinear G B A âˆ§ Â¬Collinear G N A [Gncols] by fol AGCdistinct h_line BGN notBh Nexists NonCollinearRaa; Collinear A G C [] by fol h_line BGN Collinear_DEF; G âˆˆ Open (A, C) âˆ¨ C âˆˆ Open (G, A) âˆ¨ A âˆˆ Open (C, G) [] by fol Distinct AGCdistinct - B3'; case_split AGC | GAC | CAG by fol -; suppose G âˆˆ Open (A, C); G âˆˆ int_angle A B C âˆ§ G âˆˆ int_angle A N C [] by fol H1 ANCncol - ConverseCrossbar; fol - Gequivs AngleAddition; end; suppose C âˆˆ Open (G, A); C âˆˆ int_angle G B A âˆ§ C âˆˆ int_angle G N A [] by fol Gncols - B1' ConverseCrossbar; fol - Gequivs AngleSubtraction AngleSymmetry; end; suppose A âˆˆ Open (C, G); A âˆˆ int_angle G B C âˆ§ A âˆˆ int_angle G N C [] by fol Gncols - B1' ConverseCrossbar; fol - Gequivs AngleSymmetry AngleSubtraction; end; qed; âˆ¡ A B C â‰¡ âˆ¡ A' B' C' [] by fol angles - ANCeq C5Transitive; fol H1 H2 SegmentSymmetry - SAS; qed; `;; let AngleBisector = theorem `; âˆ€A B C. Â¬Collinear B A C â‡’ âˆƒM. M âˆˆ int_angle B A C âˆ§ âˆ¡ B A M â‰¡ âˆ¡ M A C proof intro_TAC âˆ€A B C, H1; Â¬(A = B) âˆ§ Â¬(A = C) [Distinct] by fol H1 NonCollinearImpliesDistinct; consider D such that B âˆˆ Open (A, D) [ABD] by fol Distinct B2'; Â¬(A = D) âˆ§ Collinear A B D âˆ§ Segment (seg A D) [ABD'] by fol - B1' SEGMENT; consider E such that E âˆˆ ray A C â” {A} âˆ§ seg A E â‰¡ seg A D âˆ§ Â¬(A = E) [ErAC] by fol - Distinct C1 IN_Ray IN_DIFF IN_SING; Collinear A C E âˆ§ D âˆˆ ray A B â” {A} [notAE] by fol - IN_Ray ABD IntervalRayEZ IN_DIFF IN_SING; ray A D = ray A B âˆ§ ray A E = ray A C [equalrays] by fol Distinct notAE ErAC RayWellDefined; Â¬Collinear D A E âˆ§ Â¬Collinear E A D âˆ§ Â¬Collinear A E D [EADncol] by fol H1 ABD' notAE ErAC CollinearSymmetry NoncollinearityExtendsToLine; âˆ¡ D E A â‰¡ âˆ¡ E D A [DEAeq] by fol EADncol ErAC IsoscelesCongBaseAngles; Â¬Collinear E D A âˆ§ Angle (âˆ¡ E D A) âˆ§ Â¬Collinear A D E âˆ§ Â¬Collinear D E A [angEDA] by fol EADncol CollinearSymmetry ANGLE; Â¬(D = E) [notDE] by fol EADncol NonCollinearImpliesDistinct; consider h such that Line h âˆ§ D âˆˆ h âˆ§ E âˆˆ h [h_line] by fol - I1; A âˆ‰ h [notAh] by fol - Collinear_DEF EADncol âˆ‰; consider M such that Â¬(D = M) âˆ§ M âˆ‰ h âˆ§ Â¬(A,M same_side h) âˆ§ seg D M â‰¡ seg D A âˆ§ âˆ¡ E D M â‰¡ âˆ¡ E D A [Mexists] by simplify C4OppositeSide angEDA notDE ABD' h_line -; Â¬(A = M) [notAM] by fol h_line - SameSideReflexive; Â¬Collinear E D M âˆ§ Â¬Collinear D E M âˆ§ Â¬Collinear M E D [EDMncol] by fol notDE h_line Mexists NonCollinearRaa CollinearSymmetry; seg D E â‰¡ seg D E âˆ§ seg M A â‰¡ seg M A [MArefl] by fol notDE notAM SEGMENT C2Reflexive; E,D,M â‰… E,D,A [] by fol EDMncol angEDA - Mexists SAS; seg M E â‰¡ seg A E âˆ§ âˆ¡ M E D â‰¡ âˆ¡ A E D âˆ§ âˆ¡ D E M â‰¡ âˆ¡ D E A [MEDâ‰…] by fol - TriangleCong_DEF SegmentSymmetry AngleSymmetry; âˆ¡ E D A â‰¡ âˆ¡ D E A âˆ§ âˆ¡ E D A â‰¡ âˆ¡ E D M âˆ§ âˆ¡ D E A â‰¡ âˆ¡ D E M [EDAeqEDM] by fol EDMncol ANGLE angEDA Mexists MEDâ‰… DEAeq C5Symmetric; consider G such that G âˆˆ h âˆ§ G âˆˆ Open (A, M) [AGM] by fol Mexists h_line SameSide_DEF; M âˆˆ ray A G â” {A} [MrAG] by fol - IntervalRayEZ; consider v such that Line v âˆ§ A âˆˆ v âˆ§ M âˆˆ v âˆ§ G âˆˆ v [v_line] by fol notAM I1 AGM BetweenLinear; Â¬(v = h) âˆ§ v âˆ© h = {G} [vhG] by fol - notAh âˆ‰ h_line AGM I1Uniqueness; D âˆ‰ v [notDv] proof assume Â¬(D âˆ‰ v) [Con] by fol; D âˆˆ v âˆ§ D = G [DG] by fol h_line - âˆ‰ vhG IN_INTER IN_SING; D âˆˆ Open (A, M) [] by fol DG AGM; âˆ¡ E D A suppl âˆ¡ E D M [EDAsuppl] by fol angEDA - SupplementaryAngles_DEF AngleSymmetry; Right (âˆ¡ E D A) [] by fol EDAsuppl EDAeqEDM RightAngle_DEF; Right (âˆ¡ A E D) [RightAED] by fol angEDA ANGLE - DEAeq CongRightImpliesRight AngleSymmetry; Right (âˆ¡ D E M) [] by fol EDMncol ANGLE - MEDâ‰… CongRightImpliesRight AngleSymmetry; E âˆˆ Open (A, M) [] by fol EADncol EDMncol RightAED - h_line Mexists OppositeRightAnglesLinear; E âˆˆ v âˆ§ E = G [] by fol v_line - BetweenLinear h_line vhG IN_INTER IN_SING; fol - DG notDE; qed; E âˆ‰ v [notEv] proof assume Â¬(E âˆ‰ v) [Con] by fol; E âˆˆ v âˆ§ E = G [EG] by fol h_line - âˆ‰ vhG IN_INTER IN_SING; E âˆˆ Open (A, M) [] by fol - AGM; âˆ¡ D E A suppl âˆ¡ D E M [DEAsuppl] by fol EADncol - SupplementaryAngles_DEF AngleSymmetry; Right (âˆ¡ D E A) [RightDEA] by fol DEAsuppl EDAeqEDM RightAngle_DEF; Right (âˆ¡ E D A) [RightEDA] by fol angEDA RightDEA EDAeqEDM CongRightImpliesRight; Right (âˆ¡ E D M) [] by fol EDMncol ANGLE RightEDA Mexists CongRightImpliesRight; D âˆˆ Open (A, M) [] by fol angEDA EDMncol RightEDA AngleSymmetry - h_line Mexists OppositeRightAnglesLinear; D âˆˆ v âˆ§ D = G [] by fol v_line - BetweenLinear h_line vhG IN_INTER IN_SING; fol - EG notDE; qed; Â¬Collinear M A E âˆ§ Â¬Collinear M A D âˆ§ Â¬(M = E) [MAEncol] by fol notAM v_line notEv notDv NonCollinearRaa CollinearSymmetry NonCollinearImpliesDistinct; seg M E â‰¡ seg A D [MEeqAD] by fol - ErAC ABD' SEGMENT MEDâ‰… ErAC C2Transitive; seg A D â‰¡ seg M D [] by fol SegmentSymmetry ABD' Mexists SEGMENT C2Symmetric; seg M E â‰¡ seg M D [] by fol MAEncol ABD' Mexists SEGMENT MEeqAD - C2Transitive; M,A,E â‰… M,A,D [] by fol MAEncol MArefl - ErAC SSS; âˆ¡ M A E â‰¡ âˆ¡ M A D [MAEeq] by fol - TriangleCong_DEF; âˆ¡ D A M â‰¡ âˆ¡ M A E [] by fol MAEncol ANGLE MAEeq C5Symmetric AngleSymmetry; âˆ¡ B A M â‰¡ âˆ¡ M A C [BAMeqMAC] by fol - equalrays Angle_DEF; Â¬(E,D same_side v) [] proof assume E,D same_side v [Con] by fol; ray A D = ray A E [] by fol v_line notAM notDv notEv - MAEeq C4Uniqueness; fol ABD' EndpointInRay - IN_Ray EADncol; qed; consider H such that H âˆˆ v âˆ§ H âˆˆ Open (E, D) [EHD] by fol v_line - SameSide_DEF; H = G [] by fol - h_line BetweenLinear IN_INTER vhG IN_SING; G âˆˆ int_angle E A D [GintEAD] by fol EADncol - EHD ConverseCrossbar; M âˆˆ int_angle E A D [MintEAD] by fol GintEAD MrAG WholeRayInterior; B âˆˆ ray A D â” {A} âˆ§ C âˆˆ ray A E â” {A} [] by fol equalrays Distinct EndpointInRay IN_DIFF IN_SING; M âˆˆ int_angle B A C [] by fol MintEAD - InteriorWellDefined InteriorAngleSymmetry; fol - BAMeqMAC; qed; `;; let EuclidPropositionI_6 = theorem `; âˆ€A B C. Â¬Collinear A B C âˆ§ âˆ¡ B A C â‰¡ âˆ¡ B C A â‡’ seg B A â‰¡ seg B C proof intro_TAC âˆ€A B C, H1 H2; Â¬(A = C) [] by fol H1 NonCollinearImpliesDistinct; seg C A â‰¡ seg A C [CAeqAC] by fol SegmentSymmetry - SEGMENT C2Reflexive; Â¬Collinear B C A âˆ§ Â¬Collinear C B A âˆ§ Â¬Collinear B A C [BCAncol] by fol H1 CollinearSymmetry; âˆ¡ A C B â‰¡ âˆ¡ C A B [] by fol - ANGLE H2 C5Symmetric AngleSymmetry; C,B,A â‰… A,B,C [] by fol H1 BCAncol CAeqAC H2 - ASA; fol - TriangleCong_DEF; qed; `;; let IsoscelesExists = theorem `; âˆ€A B. Â¬(A = B) â‡’ âˆƒD. Â¬Collinear A D B âˆ§ seg D A â‰¡ seg D B proof intro_TAC âˆ€A B, H1; consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l [l_line] by fol H1 I1; consider C such that C âˆ‰ l [notCl] by fol - ExistsPointOffLine; Â¬Collinear C A B âˆ§ Â¬Collinear C B A âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear A C B âˆ§ Â¬Collinear B A C [CABncol] by fol l_line H1 I1 Collinear_DEF - âˆ‰; âˆ¡ C A B â‰¡ âˆ¡ C B A âˆ¨ âˆ¡ C A B <_ang âˆ¡ C B A âˆ¨ âˆ¡ C B A <_ang âˆ¡ C A B [] by fol - ANGLE AngleTrichotomy; case_split cong | less | greater by fol -; suppose âˆ¡ C A B â‰¡ âˆ¡ C B A; fol - CABncol EuclidPropositionI_6; end; suppose âˆ¡ C A B <_ang âˆ¡ C B A; âˆ¡ C A B <_ang âˆ¡ A B C [] by fol - AngleSymmetry; consider E such that E âˆˆ int_angle A B C âˆ§ âˆ¡ C A B â‰¡ âˆ¡ A B E [Eexists] by fol CABncol ANGLE - AngleOrderingUse; Â¬(B = E) [notBE] by fol - InteriorEZHelp; consider D such that D âˆˆ Open (A, C) âˆ§ D âˆˆ ray B E â” {B} [Dexists] by fol Eexists Crossbar_THM; D âˆˆ int_angle A B C [] by fol Eexists - WholeRayInterior; Â¬Collinear A D B [ADBncol] by fol - InteriorEZHelp CollinearSymmetry; ray B D = ray B E âˆ§ ray A D = ray A C [] by fol notBE Dexists RayWellDefined IntervalRay; âˆ¡ D A B â‰¡ âˆ¡ A B D [] by fol Eexists - Angle_DEF; fol ADBncol - AngleSymmetry EuclidPropositionI_6; end; suppose âˆ¡ C B A <_ang âˆ¡ C A B; âˆ¡ C B A <_ang âˆ¡ B A C [] by fol - AngleSymmetry; consider E such that E âˆˆ int_angle B A C âˆ§ âˆ¡ C B A â‰¡ âˆ¡ B A E [Eexists] by fol CABncol ANGLE - AngleOrderingUse; Â¬(A = E) [notAE] by fol - InteriorEZHelp; consider D such that D âˆˆ Open (B, C) âˆ§ D âˆˆ ray A E â” {A} [Dexists] by fol Eexists Crossbar_THM; D âˆˆ int_angle B A C [] by fol Eexists - WholeRayInterior; Â¬Collinear A D B âˆ§ Â¬Collinear D A B âˆ§ Â¬Collinear D B A [ADBncol] by fol - InteriorEZHelp CollinearSymmetry; ray A D = ray A E âˆ§ ray B D = ray B C [] by fol notAE Dexists RayWellDefined IntervalRay; âˆ¡ D B A â‰¡ âˆ¡ B A D [] by fol Eexists - Angle_DEF; âˆ¡ D A B â‰¡ âˆ¡ D B A [] by fol AngleSymmetry ADBncol ANGLE - C5Symmetric; fol ADBncol - EuclidPropositionI_6; end; qed; `;; let MidpointExists = theorem `; âˆ€A B. Â¬(A = B) â‡’ âˆƒM. M âˆˆ Open (A, B) âˆ§ seg A M â‰¡ seg M B proof intro_TAC âˆ€A B, H1; consider D such that Â¬Collinear A D B âˆ§ seg D A â‰¡ seg D B [Dexists] by fol H1 IsoscelesExists; consider F such that F âˆˆ int_angle A D B âˆ§ âˆ¡ A D F â‰¡ âˆ¡ F D B [Fexists] by fol - AngleBisector; Â¬(D = F) [notDF] by fol - InteriorEZHelp; consider M such that M âˆˆ Open (A, B) âˆ§ M âˆˆ ray D F â” {D} [Mexists] by fol Fexists Crossbar_THM; ray D M = ray D F [] by fol notDF - RayWellDefined; âˆ¡ A D M â‰¡ âˆ¡ M D B [ADMeqMDB] by fol Fexists - Angle_DEF; M âˆˆ int_angle A D B [] by fol Fexists Mexists WholeRayInterior; Â¬(D = M) âˆ§ Â¬Collinear A D M âˆ§ Â¬Collinear B D M [ADMncol] by fol - InteriorEZHelp InteriorAngleSymmetry; seg D M â‰¡ seg D M [] by fol - SEGMENT C2Reflexive; A,D,M â‰… B,D,M [] by fol ADMncol Dexists - ADMeqMDB AngleSymmetry SAS; fol Mexists - TriangleCong_DEF SegmentSymmetry; qed; `;; let EuclidPropositionI_7short = theorem `; âˆ€A B C D a. Â¬(A = B) âˆ§ Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a â‡’ Â¬(C = D) âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a âˆ§ C,D same_side a â‡’ seg A C â‰¡ seg A D â‡’ Â¬(seg B C â‰¡ seg B D) proof intro_TAC âˆ€A B C D a, a_line, Csim_aD, ACeqAD; Â¬(A = C) âˆ§ Â¬(A = D) [AnotCD] by fol a_line Csim_aD âˆ‰; assume seg B C â‰¡ seg B D [Con] by fol; seg C B â‰¡ seg D B âˆ§ seg A B â‰¡ seg A B âˆ§ seg A D â‰¡ seg A D [segeqs] by fol - SegmentSymmetry a_line AnotCD SEGMENT C2Reflexive; Â¬Collinear A C B âˆ§ Â¬Collinear A D B [] by fol a_line I1 Csim_aD Collinear_DEF âˆ‰; A,C,B â‰… A,D,B [] by fol - ACeqAD segeqs SSS; âˆ¡ B A C â‰¡ âˆ¡ B A D [] by fol - TriangleCong_DEF; ray A D = ray A C [] by fol a_line Csim_aD - C4Uniqueness; C âˆˆ ray A D â” {A} âˆ§ D âˆˆ ray A D â” {A} [] by fol AnotCD - EndpointInRay IN_DIFF IN_SING; C = D [] by fol AnotCD SEGMENT - ACeqAD segeqs C1; fol - Csim_aD; qed; `;; let EuclidPropositionI_7Help = theorem `; âˆ€A B C D a. Â¬(A = B) â‡’ Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a â‡’ Â¬(C = D) âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a âˆ§ C,D same_side a â‡’ seg A C â‰¡ seg A D â‡’ C âˆˆ int_triangle D A B âˆ¨ ConvexQuadrilateral A B C D â‡’ Â¬(seg B C â‰¡ seg B D) proof intro_TAC âˆ€A B C D a, notAB, a_line, Csim_aD, ACeqAD, Int_ConvQuad; Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) [Distinct] by fol a_line Csim_aD âˆ‰ SameSide_DEF; case_split convex | CintDAB by fol Int_ConvQuad; suppose ConvexQuadrilateral A B C D; A âˆˆ int_angle B C D âˆ§ B âˆˆ int_angle C D A âˆ§ Tetralateral A B C D [ABint] by fol - ConvexQuad_DEF Quadrilateral_DEF; Â¬Collinear B C D âˆ§ Â¬Collinear D C B âˆ§ Â¬Collinear C B D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A C âˆ§ Angle (âˆ¡ D C A) âˆ§ Angle (âˆ¡ C D B) [angCDB] by fol - Tetralateral_DEF CollinearSymmetry ANGLE; âˆ¡ C D A â‰¡ âˆ¡ D C A [CDAeqDCA] by fol angCDB Distinct SEGMENT ACeqAD C2Symmetric IsoscelesCongBaseAngles; A âˆˆ int_angle D C B âˆ§ âˆ¡ D C A â‰¡ âˆ¡ D C A âˆ§ âˆ¡ C D B â‰¡ âˆ¡ C D B [] by fol ABint InteriorAngleSymmetry angCDB ANGLE C5Reflexive; âˆ¡ D C A <_ang âˆ¡ D C B âˆ§ âˆ¡ C D B <_ang âˆ¡ C D A [] by fol angCDB ABint - AngleOrdering_DEF; âˆ¡ C D B <_ang âˆ¡ D C B [] by fol - angCDB CDAeqDCA AngleTrichotomy2 AngleOrderTransitivity; Â¬(âˆ¡ D C B â‰¡ âˆ¡ C D B) [] by fol - AngleTrichotomy1 angCDB ANGLE C5Symmetric; fol angCDB - IsoscelesCongBaseAngles; end; suppose C âˆˆ int_triangle D A B; C âˆˆ int_angle A D B âˆ§ C âˆˆ int_angle D A B [CintADB] by fol - IN_InteriorTriangle InteriorAngleSymmetry; Â¬Collinear A D C âˆ§ Â¬Collinear B D C [ADCncol] by fol CintADB InteriorEZHelp InteriorAngleSymmetry; Â¬Collinear D A C âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear A C D âˆ§ Â¬Collinear A D C [DACncol] by fol - CollinearSymmetry; Â¬Collinear B C D âˆ§ Angle (âˆ¡ D C A) âˆ§ Angle (âˆ¡ C D B) âˆ§ Â¬Collinear D C B [angCDB] by fol ADCncol - CollinearSymmetry ANGLE; âˆ¡ C D A â‰¡ âˆ¡ D C A [CDAeqDCA] by fol DACncol Distinct ADCncol SEGMENT ACeqAD C2Symmetric IsoscelesCongBaseAngles; consider E such that D âˆˆ Open (A, E) âˆ§ Â¬(D = E) âˆ§ Collinear A D E [ADE] by fol Distinct B2' B1'; B âˆˆ int_angle C D E âˆ§ Collinear D A E [BintCDE] by fol CintADB - InteriorReflectionInterior CollinearSymmetry; Â¬Collinear C D E [CDEncol] by fol DACncol - ADE NoncollinearityExtendsToLine; consider F such that F âˆˆ Open (B, D) âˆ§ F âˆˆ ray A C â” {A} [Fexists] by fol CintADB Crossbar_THM B1'; F âˆˆ int_angle B C D [FintBCD] by fol ADCncol CollinearSymmetry - ConverseCrossbar; Â¬Collinear D C F [DCFncol] by fol Distinct ADCncol CollinearSymmetry Fexists B1' NoncollinearityExtendsToLine; Collinear A C F âˆ§ F âˆˆ ray D B â” {D} âˆ§ C âˆˆ int_angle A D F [] by fol Fexists IN_DIFF IN_SING IN_Ray B1' IntervalRayEZ CintADB InteriorWellDefined; C âˆˆ Open (A, F) [] by fol - AlternateConverseCrossbar; âˆ¡ A D C suppl âˆ¡ C D E âˆ§ âˆ¡ A C D suppl âˆ¡ D C F [] by fol ADE DACncol - SupplementaryAngles_DEF; âˆ¡ C D E â‰¡ âˆ¡ D C F [CDEeqDCF] by fol - CDAeqDCA AngleSymmetry SupplementsCongAnglesCong; âˆ¡ C D B <_ang âˆ¡ C D E [] by fol angCDB CDEncol BintCDE C5Reflexive AngleOrdering_DEF; âˆ¡ C D B <_ang âˆ¡ D C F [CDBlessDCF] by fol - DCFncol ANGLE CDEeqDCF AngleTrichotomy2; âˆ¡ D C F <_ang âˆ¡ D C B [] by fol DCFncol ANGLE angCDB FintBCD InteriorAngleSymmetry C5Reflexive AngleOrdering_DEF; âˆ¡ C D B <_ang âˆ¡ D C B [] by fol CDBlessDCF - AngleOrderTransitivity; Â¬(âˆ¡ D C B â‰¡ âˆ¡ C D B) [] by fol - AngleTrichotomy1 angCDB CollinearSymmetry ANGLE C5Symmetric; fol Distinct ADCncol CollinearSymmetry - IsoscelesCongBaseAngles; end; qed; `;; let EuclidPropositionI_7 = theorem `; âˆ€A B C D a. Â¬(A = B) â‡’ Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a â‡’ Â¬(C = D) âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a âˆ§ C,D same_side a â‡’ seg A C â‰¡ seg A D â‡’ Â¬(seg B C â‰¡ seg B D) proof intro_TAC âˆ€A B C D a, notAB, a_line, Csim_aD, ACeqAD; Â¬Collinear A B C âˆ§ Â¬Collinear D A B [ABCncol] by fol a_line notAB Csim_aD NonCollinearRaa CollinearSymmetry; Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ A âˆ‰ Open (C, D) [Distinct] by fol a_line Csim_aD âˆ‰ SameSide_DEF; Â¬Collinear A D C [ADCncol] proof assume Collinear A D C [Con] by fol; C âˆˆ ray A D â” {A} âˆ§ D âˆˆ ray A D â” {A} âˆ§ seg A D â‰¡ seg A D [] by fol Distinct - IN_Ray EndpointInRay IN_DIFF IN_SING SEGMENT C2Reflexive; fol Distinct SEGMENT - ACeqAD C1 Csim_aD; qed; D,C same_side a [Dsim_aC] by fol a_line Csim_aD SameSideSymmetric; seg A D â‰¡ seg A C âˆ§ seg B D â‰¡ seg B D [ADeqAC] by fol Distinct SEGMENT ACeqAD C2Symmetric C2Reflexive; Â¬Collinear D A C âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear A C D âˆ§ Â¬Collinear A D C [DACncol] by fol ADCncol CollinearSymmetry; Â¬(seg B D â‰¡ seg B C) â‡’ Â¬(seg B C â‰¡ seg B D) [BswitchDC] by fol Distinct SEGMENT C2Symmetric; case_split BDCcol | BDCncol by fol -; suppose Collinear B D C; B âˆ‰ Open (C, D) âˆ§ C âˆˆ ray B D â” {B} âˆ§ D âˆˆ ray B D â” {B} [] by fol a_line Csim_aD SameSide_DEF âˆ‰ Distinct - IN_Ray Distinct IN_DIFF IN_SING EndpointInRay; fol Distinct SEGMENT - ACeqAD ADeqAC C1 Csim_aD; end; suppose Â¬Collinear B D C; Tetralateral A B C D [] by fol notAB Distinct Csim_aD ABCncol - CollinearSymmetry DACncol Tetralateral_DEF; ConvexQuadrilateral A B C D âˆ¨ C âˆˆ int_triangle D A B âˆ¨ ConvexQuadrilateral A B D C âˆ¨ D âˆˆ int_triangle C A B [] by fol - a_line Csim_aD FourChoicesTetralateral InteriorTriangleSymmetry; fol notAB a_line Csim_aD Dsim_aC ACeqAD ADeqAC - EuclidPropositionI_7Help BswitchDC; end; qed; `;; let EuclidPropositionI_11 = theorem `; âˆ€A B. Â¬(A = B) â‡’ âˆƒF. Right (âˆ¡ A B F) proof intro_TAC âˆ€A B, notAB; consider C such that B âˆˆ Open (A, C) âˆ§ seg B C â‰¡ seg B A [ABC] by fol notAB SEGMENT C1OppositeRay; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Collinear A B C [Distinct] by fol ABC B1'; seg B A â‰¡ seg B C [BAeqBC] by fol - SEGMENT ABC C2Symmetric; consider F such that Â¬Collinear A F C âˆ§ seg F A â‰¡ seg F C [Fexists] by fol Distinct IsoscelesExists; Â¬Collinear B F A âˆ§ Â¬Collinear B F C [BFAncol] by fol - CollinearSymmetry Distinct NoncollinearityExtendsToLine; Â¬Collinear A B F âˆ§ Angle (âˆ¡ A B F) [angABF] by fol BFAncol CollinearSymmetry ANGLE; âˆ¡ A B F suppl âˆ¡ F B C [ABFsuppl] by fol - ABC SupplementaryAngles_DEF; Â¬(B = F) âˆ§ seg B F â‰¡ seg B F [] by fol BFAncol NonCollinearImpliesDistinct SEGMENT C2Reflexive; B,F,A â‰… B,F,C [] by fol BFAncol - BAeqBC Fexists SSS; âˆ¡ A B F â‰¡ âˆ¡ F B C [] by fol - TriangleCong_DEF AngleSymmetry; fol angABF ABFsuppl - RightAngle_DEF; qed; `;; let DropPerpendicularToLine = theorem `; âˆ€P l. Line l âˆ§ P âˆ‰ l â‡’ âˆƒE Q. E âˆˆ l âˆ§ Q âˆˆ l âˆ§ Right (âˆ¡ P Q E) proof intro_TAC âˆ€P l, l_line; consider A B such that A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B) [ABl] by fol l_line I2; Â¬Collinear B A P âˆ§ Â¬Collinear P A B âˆ§ Â¬(A = P) [BAPncol] by fol ABl l_line NonCollinearRaa CollinearSymmetry âˆ‰; Angle (âˆ¡ B A P) âˆ§ Angle (âˆ¡ P A B) [angBAP] by fol - ANGLE AngleSymmetry; consider P' such that Â¬(A = P') âˆ§ P' âˆ‰ l âˆ§ Â¬(P,P' same_side l) âˆ§ seg A P' â‰¡ seg A P âˆ§ âˆ¡ B A P' â‰¡ âˆ¡ B A P [P'exists] by simplify C4OppositeSide - ABl BAPncol l_line; consider Q such that Q âˆˆ l âˆ§ Q âˆˆ Open (P, P') âˆ§ Collinear A B Q [Qexists] by fol l_line - SameSide_DEF ABl Collinear_DEF; Â¬Collinear B A P' [BAP'ncol] by fol l_line ABl I1 Collinear_DEF P'exists âˆ‰; âˆ¡ B A P â‰¡ âˆ¡ B A P' [BAPeqBAP'] by fol - ANGLE angBAP P'exists C5Symmetric; âˆƒE. E âˆˆ l âˆ§ Â¬Collinear P Q E âˆ§ âˆ¡ P Q E â‰¡ âˆ¡ E Q P' [] proof assume Â¬(A = Q) [notAQ] by fol ABl BAPncol BAPeqBAP' AngleSymmetry; seg A Q â‰¡ seg A Q âˆ§ seg A P â‰¡ seg A P' [APeqAP'] by fol - SEGMENT C2Reflexive BAPncol P'exists C2Symmetric; Â¬Collinear Q A P' âˆ§ Â¬Collinear Q A P [QAP'ncol] by fol notAQ l_line ABl Qexists P'exists NonCollinearRaa CollinearSymmetry; âˆ¡ Q A P â‰¡ âˆ¡ Q A P' [] proof case_split QAB | notQAB by fol - âˆ‰; suppose A âˆˆ Open (Q, B); âˆ¡ B A P suppl âˆ¡ P A Q âˆ§ âˆ¡ B A P' suppl âˆ¡ P' A Q [] by fol BAPncol BAP'ncol - B1' SupplementaryAngles_DEF; fol - BAPeqBAP' SupplementsCongAnglesCong AngleSymmetry; end; suppose A âˆ‰ Open (Q, B); Q âˆˆ ray A B â” {A} [QrayAB_A] by fol ABl Qexists notQAB IN_Ray notAQ IN_DIFF IN_SING; ray A Q = ray A B [] by fol - ABl RayWellDefined; fol notAQ QrayAB_A - BAPeqBAP' Angle_DEF; end; qed; Q,A,P â‰… Q,A,P' [] by fol QAP'ncol APeqAP' - SAS; fol - TriangleCong_DEF AngleSymmetry ABl QAP'ncol CollinearSymmetry; qed; consider E such that E âˆˆ l âˆ§ Â¬Collinear P Q E âˆ§ âˆ¡ P Q E â‰¡ âˆ¡ E Q P' [Eexists] by fol -; âˆ¡ P Q E suppl âˆ¡ E Q P' âˆ§ Right (âˆ¡ P Q E) [] by fol - Qexists SupplementaryAngles_DEF RightAngle_DEF; fol Eexists Qexists -; qed; `;; let EuclidPropositionI_14 = theorem `; âˆ€A B C D l. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B) â‡’ C âˆ‰ l âˆ§ D âˆ‰ l âˆ§ Â¬(C,D same_side l) â‡’ âˆ¡ C B A suppl âˆ¡ A B D â‡’ B âˆˆ Open (C, D) proof intro_TAC âˆ€A B C D l, l_line, Cnsim_lD, CBAsupplABD; Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬Collinear C B A [Distinct] by fol l_line Cnsim_lD âˆ‰ I1 Collinear_DEF; consider E such that B âˆˆ Open (C, E) [CBE] by fol Distinct B2'; E âˆ‰ l âˆ§ Â¬(C,E same_side l) [Csim_lE] by fol l_line âˆ‰ - BetweenLinear Cnsim_lD SameSide_DEF; D,E same_side l [Dsim_lE] by fol l_line Cnsim_lD - AtMost2Sides; âˆ¡ C B A suppl âˆ¡ A B E [] by fol Distinct CBE SupplementaryAngles_DEF; âˆ¡ A B D â‰¡ âˆ¡ A B E [] by fol CBAsupplABD - SupplementUnique; ray B E = ray B D [] by fol l_line Csim_lE Cnsim_lD Dsim_lE - C4Uniqueness; D âˆˆ ray B E â” {B} [] by fol Distinct - EndpointInRay IN_DIFF IN_SING; fol CBE - OppositeRaysIntersect1pointHelp B1'; qed; `;; (* Euclid's Proposition I.15 *) let VerticalAnglesCong = theorem `; âˆ€A B O A' B'. Â¬Collinear A O B â‡’ O âˆˆ Open (A, A') âˆ§ O âˆˆ Open (B, B') â‡’ âˆ¡ B O A' â‰¡ âˆ¡ B' O A proof intro_TAC âˆ€A B O A' B', H1, H2; âˆ¡ A O B suppl âˆ¡ B O A' [AOBsupplBOA'] by fol H1 H2 SupplementaryAngles_DEF; âˆ¡ B O A suppl âˆ¡ A O B' [] by fol H1 CollinearSymmetry H2 SupplementaryAngles_DEF; fol AOBsupplBOA' - AngleSymmetry SupplementUnique; qed; `;; let EuclidPropositionI_16 = theorem `; âˆ€A B C D. Â¬Collinear A B C âˆ§ C âˆˆ Open (B, D) â‡’ âˆ¡ B A C <_ang âˆ¡ D C A proof intro_TAC âˆ€A B C D, H1 H2; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [Distinct] by fol H1 NonCollinearImpliesDistinct; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line] by fol Distinct I1; consider m such that Line m âˆ§ B âˆˆ m âˆ§ C âˆˆ m [m_line] by fol Distinct I1; D âˆˆ m [Dm] by fol m_line H2 BetweenLinear; consider E such that E âˆˆ Open (A, C) âˆ§ seg A E â‰¡ seg E C [AEC] by fol Distinct MidpointExists; Â¬(A = E) âˆ§ Â¬(E = C) âˆ§ Collinear A E C âˆ§ Â¬(B = E) [AECcol] by fol - B1' H1; E âˆˆ l [El] by fol l_line AEC BetweenLinear; consider F such that E âˆˆ Open (B, F) âˆ§ seg E F â‰¡ seg E B [BEF] by fol AECcol SEGMENT C1OppositeRay; Â¬(B = E) âˆ§ Â¬(B = F) âˆ§ Â¬(E = F) âˆ§ Collinear B E F [BEF'] by fol BEF B1'; B âˆ‰ l [notBl] by fol l_line Distinct I1 Collinear_DEF H1 âˆ‰; Â¬Collinear A E B âˆ§ Â¬Collinear C E B [AEBncol] by fol AECcol l_line El notBl NonCollinearRaa CollinearSymmetry; Angle (âˆ¡ B A E) [angBAE] by fol - CollinearSymmetry ANGLE; Â¬Collinear C E F [CEFncol] by fol AEBncol BEF' CollinearSymmetry NoncollinearityExtendsToLine; âˆ¡ B E A â‰¡ âˆ¡ F E C [BEAeqFEC] by fol AEBncol AEC B1' BEF VerticalAnglesCong; seg E A â‰¡ seg E C âˆ§ seg E B â‰¡ seg E F [] by fol AEC SegmentSymmetry AECcol BEF' SEGMENT BEF C2Symmetric; A,E,B â‰… C,E,F [] by fol AEBncol CEFncol - BEAeqFEC AngleSymmetry SAS; âˆ¡ B A E â‰¡ âˆ¡ F C E [BAEeqFCE] by fol - TriangleCong_DEF; Â¬Collinear E C D [ECDncol] by fol AEBncol H2 B1' CollinearSymmetry NoncollinearityExtendsToLine; F âˆ‰ l âˆ§ D âˆ‰ l [notFl] by fol l_line El Collinear_DEF CEFncol - âˆ‰; F âˆˆ ray B E â” {B} âˆ§ E âˆ‰ m [] by fol BEF IntervalRayEZ m_line Collinear_DEF AEBncol âˆ‰; F âˆ‰ m âˆ§ F,E same_side m [Fsim_mE] by fol m_line - RaySameSide; Â¬(B,F same_side l) âˆ§ Â¬(B,D same_side l) [] by fol El l_line BEF H2 SameSide_DEF; F,D same_side l [] by fol l_line notBl notFl - AtMost2Sides; F âˆˆ int_angle E C D [] by fol ECDncol l_line El m_line Dm notFl Fsim_mE - IN_InteriorAngle; âˆ¡ B A E <_ang âˆ¡ E C D [BAElessECD] by fol angBAE ECDncol - BAEeqFCE AngleSymmetry AngleOrdering_DEF; ray A E = ray A C âˆ§ ray C E = ray C A [] by fol AEC B1' IntervalRay; âˆ¡ B A C <_ang âˆ¡ A C D [] by fol BAElessECD - Angle_DEF; fol - AngleSymmetry; qed; `;; let ExteriorAngle = theorem `; âˆ€A B C D. Â¬Collinear A B C âˆ§ C âˆˆ Open (B, D) â‡’ âˆ¡ A B C <_ang âˆ¡ A C D proof intro_TAC âˆ€A B C D, H1 H2; Â¬(C = D) âˆ§ C âˆˆ Open (D, B) âˆ§ Collinear B C D [H2'] by fol H2 BetweenLinear B1'; Â¬Collinear B A C âˆ§ Â¬(A = C) [BACncol] by fol H1 CollinearSymmetry NonCollinearImpliesDistinct; consider E such that C âˆˆ Open (A, E) [ACE] by fol - B2'; Â¬(C = E) âˆ§ C âˆˆ Open (E, A) âˆ§ Collinear A C E [ACE'] by fol - B1'; Â¬Collinear A C D âˆ§ Â¬Collinear D C E [DCEncol] by fol H1 CollinearSymmetry H2' - NoncollinearityExtendsToLine; âˆ¡ A B C <_ang âˆ¡ E C B [ABClessECB] by fol BACncol ACE EuclidPropositionI_16; âˆ¡ E C B â‰¡ âˆ¡ A C D [] by fol DCEncol ACE' H2' VerticalAnglesCong; fol ABClessECB DCEncol ANGLE - AngleTrichotomy2; qed; `;; let EuclidPropositionI_17 = theorem `; âˆ€A B C Î± Î² Î³. Â¬Collinear A B C âˆ§ Î± = âˆ¡ A B C âˆ§ Î² = âˆ¡ B C A â‡’ Î² suppl Î³ â‡’ Î± <_ang Î³ proof intro_TAC âˆ€A B C Î± Î² Î³, H1, H2; Angle Î³ [angÎ³] by fol H2 SupplementImpliesAngle; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [Distinct] by fol H1 NonCollinearImpliesDistinct; Â¬Collinear B A C âˆ§ Â¬Collinear A C B [BACncol] by fol H1 CollinearSymmetry; consider D such that C âˆˆ Open (A, D) [ACD] by fol Distinct B2'; âˆ¡ A B C <_ang âˆ¡ D C B [ABClessDCB] by fol BACncol ACD EuclidPropositionI_16; Î² suppl âˆ¡ B C D [] by fol - H1 AngleSymmetry BACncol ACD SupplementaryAngles_DEF; âˆ¡ B C D â‰¡ Î³ [] by fol H2 - SupplementUnique; fol ABClessDCB H1 AngleSymmetry angÎ³ - AngleTrichotomy2; qed; `;; let EuclidPropositionI_18 = theorem `; âˆ€A B C. Â¬Collinear A B C âˆ§ seg A C <__ seg A B â‡’ âˆ¡ A B C <_ang âˆ¡ B C A proof intro_TAC âˆ€A B C, H1 H2; Â¬(A = B) âˆ§ Â¬(A = C) [Distinct] by fol H1 NonCollinearImpliesDistinct; consider D such that D âˆˆ Open (A, B) âˆ§ seg A C â‰¡ seg A D [ADB] by fol Distinct SEGMENT H2 SegmentOrderingUse; Â¬(D = A) âˆ§ Â¬(D = B) âˆ§ D âˆˆ Open (B, A) âˆ§ Collinear A D B âˆ§ ray B D = ray B A [ADB'] by fol - B1' IntervalRay; D âˆˆ int_angle A C B âˆ§ Â¬Collinear A C B [DintACB] by fol H1 CollinearSymmetry ADB ConverseCrossbar; Â¬Collinear D A C âˆ§ Â¬Collinear C B D âˆ§ Â¬Collinear C D A [DACncol] by fol H1 CollinearSymmetry ADB' NoncollinearityExtendsToLine; seg A D â‰¡ seg A C [] by fol ADB' Distinct SEGMENT ADB C2Symmetric; âˆ¡ C D A â‰¡ âˆ¡ A C D [] by fol DACncol - IsoscelesCongBaseAngles AngleSymmetry; âˆ¡ C D A <_ang âˆ¡ A C B [CDAlessACB] by fol DACncol ANGLE H1 DintACB - AngleOrdering_DEF; âˆ¡ B D C suppl âˆ¡ C D A [] by fol DACncol CollinearSymmetry ADB' SupplementaryAngles_DEF; âˆ¡ C B D <_ang âˆ¡ C D A [] by fol DACncol - EuclidPropositionI_17; âˆ¡ C B D <_ang âˆ¡ A C B [] by fol - CDAlessACB AngleOrderTransitivity; fol - ADB' Angle_DEF AngleSymmetry; qed; `;; let EuclidPropositionI_19 = theorem `; âˆ€A B C. Â¬Collinear A B C âˆ§ âˆ¡ A B C <_ang âˆ¡ B C A â‡’ seg A C <__ seg A B proof intro_TAC âˆ€A B C, H1 H2; Â¬Collinear B A C âˆ§ Â¬Collinear B C A âˆ§ Â¬Collinear A C B [BACncol] by fol H1 CollinearSymmetry; Â¬(A = B) âˆ§ Â¬(A = C) [Distinct] by fol H1 NonCollinearImpliesDistinct; assume Â¬(seg A C <__ seg A B) [Con] by fol; seg A B â‰¡ seg A C âˆ¨ seg A B <__ seg A C [] by fol Distinct SEGMENT - SegmentTrichotomy; case_split cong | less by fol -; suppose seg A B â‰¡ seg A C; âˆ¡ C B A â‰¡ âˆ¡ B C A [] by fol BACncol - IsoscelesCongBaseAngles; fol - AngleSymmetry H2 AngleTrichotomy1; end; suppose seg A B <__ seg A C; âˆ¡ A C B <_ang âˆ¡ C B A [] by fol BACncol - EuclidPropositionI_18; fol H1 BACncol ANGLE - AngleSymmetry H2 AngleTrichotomy; end; qed; `;; let EuclidPropositionI_20 = theorem `; âˆ€A B C D. Â¬Collinear A B C â‡’ A âˆˆ Open (B, D) âˆ§ seg A D â‰¡ seg A C â‡’ seg B C <__ seg B D proof intro_TAC âˆ€A B C D, H1, H2; Â¬(B = D) âˆ§ Â¬(A = D) âˆ§ A âˆˆ Open (D, B) âˆ§ Collinear B A D âˆ§ ray D A = ray D B [BAD'] by fol H2 B1' IntervalRay; Â¬Collinear C A D [CADncol] by fol H1 CollinearSymmetry BAD' NoncollinearityExtendsToLine; Â¬Collinear D C B âˆ§ Â¬Collinear B D C [DCBncol] by fol H1 CollinearSymmetry BAD' NoncollinearityExtendsToLine; Angle (âˆ¡ C D A) [angCDA] by fol CADncol CollinearSymmetry ANGLE; âˆ¡ C D A â‰¡ âˆ¡ D C A [CDAeqDCA] by fol CADncol CollinearSymmetry H2 IsoscelesCongBaseAngles; A âˆˆ int_angle D C B [] by fol DCBncol BAD' ConverseCrossbar; âˆ¡ C D A <_ang âˆ¡ D C B [] by fol angCDA DCBncol - CDAeqDCA AngleOrdering_DEF; âˆ¡ B D C <_ang âˆ¡ D C B [] by fol - BAD' Angle_DEF AngleSymmetry; fol DCBncol - EuclidPropositionI_19; qed; `;; let EuclidPropositionI_21 = theorem `; âˆ€A B C D. Â¬Collinear A B C âˆ§ D âˆˆ int_triangle A B C â‡’ âˆ¡ A B C <_ang âˆ¡ C D A proof intro_TAC âˆ€A B C D, H1 H2; Â¬(B = A) âˆ§ Â¬(B = C) âˆ§ Â¬(A = C) [Distinct] by fol H1 NonCollinearImpliesDistinct; D âˆˆ int_angle B A C âˆ§ D âˆˆ int_angle C B A [DintTri] by fol H2 IN_InteriorTriangle InteriorAngleSymmetry; consider E such that E âˆˆ Open (B, C) âˆ§ E âˆˆ ray A D â” {A} [BEC] by fol - Crossbar_THM; Â¬(B = E) âˆ§ Â¬(E = C) âˆ§ Collinear B E C âˆ§ Collinear A D E [BEC'] by fol - B1' IN_Ray IN_DIFF IN_SING; ray B E = ray B C âˆ§ E âˆˆ ray B C â” {B} [rBErBC] by fol BEC IntervalRay IntervalRayEZ; D âˆˆ int_angle A B E [DintABE] by fol DintTri - InteriorAngleSymmetry InteriorWellDefined; D âˆˆ Open (A, E) [ADE] by fol BEC' - AlternateConverseCrossbar; ray E D = ray E A [rEDrEA] by fol - B1' IntervalRay; Â¬Collinear A B E âˆ§ Â¬Collinear B E A âˆ§ Â¬Collinear C B D âˆ§ Â¬(A = D) [ABEncol] by fol DintABE IN_InteriorAngle CollinearSymmetry DintTri InteriorEZHelp; Â¬Collinear E D C âˆ§ Â¬Collinear C E D [EDCncol] by fol - CollinearSymmetry BEC' NoncollinearityExtendsToLine; âˆ¡ A B E <_ang âˆ¡ A E C âˆ§ âˆ¡ C E D = âˆ¡ D E C [] by fol ABEncol BEC ExteriorAngle AngleSymmetry; âˆ¡ A B C <_ang âˆ¡ C E D [ABClessAEC] by fol - rBErBC rEDrEA Angle_DEF; âˆ¡ C E D <_ang âˆ¡ C D A [] by fol EDCncol ADE B1' ExteriorAngle; fol ABClessAEC - AngleOrderTransitivity; qed; `;; let AngleTrichotomy3 = theorem `; âˆ€Î± Î² Î³. Î± <_ang Î² âˆ§ Angle Î³ âˆ§ Î³ â‰¡ Î± â‡’ Î³ <_ang Î² proof intro_TAC âˆ€Î± Î² Î³, H1; consider A O B G such that Angle Î± âˆ§ Â¬Collinear A O B âˆ§ Î² = âˆ¡ A O B âˆ§ G âˆˆ int_angle A O B âˆ§ Î± â‰¡ âˆ¡ A O G [H1'] by fol H1 AngleOrdering_DEF; Â¬Collinear A O G [] by fol - InteriorEZHelp; Î³ â‰¡ âˆ¡ A O G [] by fol H1 H1' - ANGLE C5Transitive; fol H1 H1' - AngleOrdering_DEF; qed; `;; let InteriorCircleConvexHelp = theorem `; âˆ€O A B C. Â¬Collinear A O C â‡’ B âˆˆ Open (A, C) â‡’ seg O A <__ seg O C âˆ¨ seg O A â‰¡ seg O C â‡’ seg O B <__ seg O C proof intro_TAC âˆ€O A B C, H1, H2, H3; Â¬Collinear O C A âˆ§ Â¬Collinear C O A âˆ§ Â¬(O = A) âˆ§ Â¬(O = C) [H1'] by fol H1 CollinearSymmetry NonCollinearImpliesDistinct; ray A B = ray A C âˆ§ ray C B = ray C A [equal_rays] by fol H2 IntervalRay B1'; âˆ¡ O C A <_ang âˆ¡ C A O âˆ¨ âˆ¡ O C A â‰¡ âˆ¡ C A O [] proof assume seg O A â‰¡ seg O C [seg_eq] by fol H3 H1' EuclidPropositionI_18; seg O C â‰¡ seg O A [] by fol H1' SEGMENT - C2Symmetric; fol H1' - IsoscelesCongBaseAngles AngleSymmetry; qed; âˆ¡ O C B <_ang âˆ¡ B A O âˆ¨ âˆ¡ O C B â‰¡ âˆ¡ B A O [] by fol - equal_rays Angle_DEF; âˆ¡ B C O <_ang âˆ¡ O A B âˆ¨ âˆ¡ B C O â‰¡ âˆ¡ O A B [BCOlessOAB] by fol - AngleSymmetry; Â¬Collinear O A B âˆ§ Â¬Collinear B C O âˆ§ Â¬Collinear O C B [OABncol] by fol H1 CollinearSymmetry H2 B1' NoncollinearityExtendsToLine; âˆ¡ O A B <_ang âˆ¡ O B C [] by fol - H2 ExteriorAngle; âˆ¡ B C O <_ang âˆ¡ O B C [] by fol BCOlessOAB - AngleOrderTransitivity OABncol ANGLE - AngleTrichotomy3; fol OABncol - AngleSymmetry EuclidPropositionI_19; qed; `;; let InteriorCircleConvex = theorem `; âˆ€O R A B C. Â¬(O = R) â‡’ B âˆˆ Open (A, C) â‡’ A âˆˆ int_circle O R âˆ§ C âˆˆ int_circle O R â‡’ B âˆˆ int_circle O R proof intro_TAC âˆ€O R A B C, H1, H2, H3; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ B âˆˆ Open (C, A) [H2'] by fol H2 B1'; (A = O âˆ¨ seg O A <__ seg O R) âˆ§ (C = O âˆ¨ seg O C <__ seg O R) [ACintOR] by fol H3 H1 IN_InteriorCircle; case_split OAC | OnotAC by fol -; suppose O = A âˆ¨ O = C; B âˆˆ Open (O, C) âˆ¨ B âˆˆ Open (O, A) [] by fol - H2 B1'; seg O B <__ seg O A âˆ§ Â¬(O = A) âˆ¨ seg O B <__ seg O C âˆ§ Â¬(O = C) [] by fol - B1' SEGMENT C2Reflexive SegmentOrdering_DEF; seg O B <__ seg O R [] by fol - ACintOR SegmentOrderTransitivity; fol - H1 IN_InteriorCircle; end; suppose Â¬(O = A) âˆ§ Â¬(O = C); case_split AOCncol | AOCcol by fol -; suppose Â¬Collinear A O C; seg O A <__ seg O C âˆ¨ seg O A â‰¡ seg O C âˆ¨ seg O C <__ seg O A [] by fol OnotAC SEGMENT SegmentTrichotomy; seg O B <__ seg O C âˆ¨ seg O B <__ seg O A [] by fol AOCncol H2 - InteriorCircleConvexHelp CollinearSymmetry B1'; fol OnotAC ACintOR - SegmentOrderTransitivity H1 IN_InteriorCircle; end; suppose Collinear A O C; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line] by fol H2' I1; Collinear B A O âˆ§ Collinear B C O [OABCcol] by fol - H2 BetweenLinear H2' AOCcol CollinearLinear Collinear_DEF; B âˆ‰ Open (O, A) âˆ§ B âˆ‰ Open (O, C) â‡’ B = O [] proof intro_TAC Assumption; O âˆˆ ray B A âˆ© ray B C [] by fol H2' OABCcol - IN_Ray IN_INTER; fol - H2 OppositeRaysIntersect1point IN_SING; qed; B âˆˆ Open (O, A) âˆ¨ B âˆˆ Open (O, C) âˆ¨ B = O [] by fol - âˆ‰; seg O B <__ seg O A âˆ¨ seg O B <__ seg O C âˆ¨ B = O [] by fol - B1' SEGMENT C2Reflexive SegmentOrdering_DEF; seg O B <__ seg O R âˆ¨ B = O [] by fol - ACintOR OnotAC SegmentOrderTransitivity; fol - H1 IN_InteriorCircle; end; end; qed; `;; let SegmentTrichotomy3 = theorem `; âˆ€s t u. s <__ t âˆ§ Segment u âˆ§ u â‰¡ s â‡’ u <__ t proof intro_TAC âˆ€s t u, H1; consider C D X such that Segment s âˆ§ t = seg C D âˆ§ X âˆˆ Open (C, D) âˆ§ s â‰¡ seg C X âˆ§ Â¬(C = X) [H1'] by fol H1 SegmentOrdering_DEF B1'; u â‰¡ seg C X [] by fol H1 - SEGMENT C2Transitive; fol H1 H1' - SegmentOrdering_DEF; qed; `;; let EuclidPropositionI_24Help = theorem `; âˆ€O A C O' D M. Â¬Collinear A O C âˆ§ Â¬Collinear D O' M â‡’ seg O' D â‰¡ seg O A âˆ§ seg O' M â‰¡ seg O C â‡’ âˆ¡ D O' M <_ang âˆ¡ A O C â‡’ seg O A <__ seg O C âˆ¨ seg O A â‰¡ seg O C â‡’ seg D M <__ seg A C proof intro_TAC âˆ€O A C O' D M, H1, H2, H3, H4; consider K such that K âˆˆ int_angle A O C âˆ§ âˆ¡ D O' M â‰¡ âˆ¡ A O K [KintAOC] by fol H1 ANGLE H3 AngleOrderingUse; Â¬(O = C) âˆ§ Â¬(D = M) âˆ§ Â¬(O' = M) âˆ§ Â¬(O = K) [Distinct] by fol H1 NonCollinearImpliesDistinct - InteriorEZHelp; consider B such that B âˆˆ ray O K â” {O} âˆ§ seg O B â‰¡ seg O C [BrOK] by fol Distinct SEGMENT - C1; ray O B = ray O K [] by fol Distinct - RayWellDefined; âˆ¡ D O' M â‰¡ âˆ¡ A O B [DO'MeqAOB] by fol KintAOC - Angle_DEF; B âˆˆ int_angle A O C [BintAOC] by fol KintAOC BrOK WholeRayInterior; Â¬(B = O) âˆ§ Â¬Collinear A O B [AOBncol] by fol - InteriorEZHelp; seg O C â‰¡ seg O B [OCeqOB] by fol Distinct - SEGMENT BrOK C2Symmetric; seg O' M â‰¡ seg O B [] by fol Distinct SEGMENT AOBncol H2 - C2Transitive; D,O',M â‰… A,O,B [] by fol H1 AOBncol H2 - DO'MeqAOB SAS; seg D M â‰¡ seg A B [DMeqAB] by fol - TriangleCong_DEF; consider G such that G âˆˆ Open (A, C) âˆ§ G âˆˆ ray O B â” {O} âˆ§ Â¬(G = O) [AGC] by fol BintAOC Crossbar_THM B1' IN_DIFF IN_SING; Segment (seg O G) âˆ§ Â¬(O = B) [notOB] by fol - SEGMENT BrOK IN_DIFF IN_SING; seg O G <__ seg O C [] by fol H1 AGC H4 InteriorCircleConvexHelp; seg O G <__ seg O B [] by fol - OCeqOB BrOK SEGMENT SegmentTrichotomy2 IN_DIFF IN_SING; consider G' such that G' âˆˆ Open (O, B) âˆ§ seg O G â‰¡ seg O G' [OG'B] by fol notOB - SegmentOrderingUse; Â¬(G' = O) âˆ§ seg O G' â‰¡ seg O G' âˆ§ Segment (seg O G') [notG'O] by fol - B1' SEGMENT C2Reflexive SEGMENT; G' âˆˆ ray O B â” {O} [] by fol OG'B IntervalRayEZ; G' = G âˆ§ G âˆˆ Open (B, O) [] by fol notG'O notOB - AGC OG'B C1 B1'; ConvexQuadrilateral B A O C [] by fol H1 - AGC DiagonalsIntersectImpliesConvexQuad; A âˆˆ int_angle O C B âˆ§ O âˆˆ int_angle C B A âˆ§ Quadrilateral B A O C [OintCBA] by fol - ConvexQuad_DEF; A âˆˆ int_angle B C O [AintBCO] by fol - InteriorAngleSymmetry; Tetralateral B A O C [] by fol OintCBA Quadrilateral_DEF; Â¬Collinear C B A âˆ§ Â¬Collinear B C O âˆ§ Â¬Collinear C O B âˆ§ Â¬Collinear C B O [BCOncol] by fol - Tetralateral_DEF CollinearSymmetry; âˆ¡ B C O â‰¡ âˆ¡ C B O [BCOeqCBO] by fol - OCeqOB IsoscelesCongBaseAngles; Â¬Collinear B C A âˆ§ Â¬Collinear A C B [ACBncol] by fol AintBCO InteriorEZHelp CollinearSymmetry; âˆ¡ B C A â‰¡ âˆ¡ B C A âˆ§ Angle (âˆ¡ B C A) âˆ§ âˆ¡ C B O â‰¡ âˆ¡ C B O [CBOref] by fol - ANGLE BCOncol C5Reflexive; âˆ¡ B C A <_ang âˆ¡ B C O [] by fol - BCOncol ANGLE AintBCO AngleOrdering_DEF; âˆ¡ B C A <_ang âˆ¡ C B O [BCAlessCBO] by fol - BCOncol ANGLE BCOeqCBO AngleTrichotomy2; âˆ¡ C B O <_ang âˆ¡ C B A [] by fol BCOncol ANGLE OintCBA CBOref AngleOrdering_DEF; âˆ¡ A C B <_ang âˆ¡ C B A [] by fol BCAlessCBO - AngleOrderTransitivity AngleSymmetry; seg A B <__ seg A C [] by fol ACBncol - EuclidPropositionI_19; fol - Distinct SEGMENT DMeqAB SegmentTrichotomy3; qed; `;; let EuclidPropositionI_24 = theorem `; âˆ€O A C O' D M. Â¬Collinear A O C âˆ§ Â¬Collinear D O' M â‡’ seg O' D â‰¡ seg O A âˆ§ seg O' M â‰¡ seg O C â‡’ âˆ¡ D O' M <_ang âˆ¡ A O C â‡’ seg D M <__ seg A C proof intro_TAC âˆ€O A C O' D M, H1, H2, H3; Â¬(O = A) âˆ§ Â¬(O = C) âˆ§ Â¬Collinear C O A âˆ§ Â¬Collinear M O' D [Distinct] by fol H1 NonCollinearImpliesDistinct CollinearSymmetry; seg O A â‰¡ seg O C âˆ¨ seg O A <__ seg O C âˆ¨ seg O C <__ seg O A [3pos] by fol - SEGMENT SegmentTrichotomy; assume seg O C <__ seg O A [H4] by fol 3pos H1 H2 H3 EuclidPropositionI_24Help; âˆ¡ M O' D <_ang âˆ¡ C O A [] by fol H3 AngleSymmetry; fol Distinct H3 AngleSymmetry H2 H4 EuclidPropositionI_24Help SegmentSymmetry; qed; `;; let EuclidPropositionI_25 = theorem `; âˆ€O A C O' D M. Â¬Collinear A O C âˆ§ Â¬Collinear D O' M â‡’ seg O' D â‰¡ seg O A âˆ§ seg O' M â‰¡ seg O C â‡’ seg D M <__ seg A C â‡’ âˆ¡ D O' M <_ang âˆ¡ A O C proof intro_TAC âˆ€O A C O' D M, H1, H2, H3; Â¬(O = A) âˆ§ Â¬(O = C) âˆ§ Â¬(A = C) âˆ§ Â¬(D = M) âˆ§ Â¬(O' = D) âˆ§ Â¬(O' = M) [Distinct] by fol H1 NonCollinearImpliesDistinct; assume Â¬(âˆ¡ D O' M <_ang âˆ¡ A O C) [Contradiction] by fol; âˆ¡ D O' M â‰¡ âˆ¡ A O C âˆ¨ âˆ¡ A O C <_ang âˆ¡ D O' M [] by fol H1 ANGLE - AngleTrichotomy; case_split Cong | Con by fol -; suppose âˆ¡ D O' M â‰¡ âˆ¡ A O C; D,O',M â‰… A,O,C [] by fol H1 H2 - SAS; seg D M â‰¡ seg A C [] by fol - TriangleCong_DEF; fol Distinct SEGMENT - H3 SegmentTrichotomy; end; suppose âˆ¡ A O C <_ang âˆ¡ D O' M; seg O A â‰¡ seg O' D âˆ§ seg O C â‰¡ seg O' M [H2'] by fol Distinct SEGMENT H2 C2Symmetric; seg A C <__ seg D M [] by fol H1 - Con EuclidPropositionI_24; fol Distinct SEGMENT - H3 SegmentTrichotomy; end; qed; `;; let AAS = theorem `; âˆ€A B C A' B' C'. Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' â‡’ âˆ¡ A B C â‰¡ âˆ¡ A' B' C' âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B' C' A' â‡’ seg A B â‰¡ seg A' B' â‡’ A,B,C â‰… A',B',C' proof intro_TAC âˆ€A B C A' B' C', H1, H2, H3; Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬(B' = C') [Distinct] by fol H1 NonCollinearImpliesDistinct; consider G such that G âˆˆ ray B C â” {B} âˆ§ seg B G â‰¡ seg B' C' [Gexists] by fol Distinct SEGMENT C1; Â¬(G = B) âˆ§ B âˆ‰ Open (G, C) âˆ§ Collinear G B C [notGBC] by fol - IN_Ray CollinearSymmetry IN_DIFF IN_SING; Â¬Collinear A B G âˆ§ Â¬Collinear B G A [ABGncol] by fol H1 notGBC CollinearSymmetry NoncollinearityExtendsToLine; ray B G = ray B C [] by fol Distinct Gexists RayWellDefined; âˆ¡ A B G = âˆ¡ A B C [] by fol Distinct - Angle_DEF; A,B,G â‰… A',B',C' [ABGâ‰…A'B'C'] by fol H1 ABGncol H3 SegmentSymmetry H2 - Gexists SAS; âˆ¡ B G A â‰¡ âˆ¡ B' C' A' [BGAeqB'C'A'] by fol - TriangleCong_DEF; Â¬Collinear B C A âˆ§ Â¬Collinear B' C' A' [BCAncol] by fol H1 CollinearSymmetry; âˆ¡ B' C' A' â‰¡ âˆ¡ B C A âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B C A [BCArefl] by fol - ANGLE H2 C5Symmetric C5Reflexive; âˆ¡ B G A â‰¡ âˆ¡ B C A [BGAeqBCA] by fol ABGncol BCAncol ANGLE BGAeqB'C'A' - C5Transitive; assume Â¬(G = C) [notGC] by fol BGAeqBCA ABGâ‰…A'B'C'; Â¬Collinear A C G âˆ§ Â¬Collinear A G C [ACGncol] by fol H1 notGBC - CollinearSymmetry NoncollinearityExtendsToLine; C âˆˆ Open (B, G) âˆ¨ G âˆˆ Open (C, B) [] by fol notGBC notGC Distinct B3' âˆ‰; case_split BCG | CGB by fol -; suppose C âˆˆ Open (B, G) ; C âˆˆ Open (G, B) âˆ§ ray G C = ray G B [rGCrBG] by fol - B1' IntervalRay; âˆ¡ A G C <_ang âˆ¡ A C B [] by fol ACGncol - ExteriorAngle; âˆ¡ B G A <_ang âˆ¡ B C A [] by fol - rGCrBG Angle_DEF AngleSymmetry AngleSymmetry; fol ABGncol BCAncol ANGLE - AngleSymmetry BGAeqBCA AngleTrichotomy; end; suppose G âˆˆ Open (C, B); ray C G = ray C B âˆ§ âˆ¡ A C G <_ang âˆ¡ A G B [] by fol - IntervalRay ACGncol ExteriorAngle; âˆ¡ A C B <_ang âˆ¡ B G A [] by fol - Angle_DEF AngleSymmetry; âˆ¡ B C A <_ang âˆ¡ B C A [] by fol - BCAncol ANGLE BGAeqBCA AngleTrichotomy2 AngleSymmetry; fol - BCArefl AngleTrichotomy1; end; qed; `;; let ParallelSymmetry = theorem `; âˆ€l k. l âˆ¥ k â‡’ k âˆ¥ l by fol PARALLEL INTER_COMM`;; let AlternateInteriorAngles = theorem `; âˆ€A B C E l m t. Line l âˆ§ A âˆˆ l âˆ§ E âˆˆ l â‡’ Line m âˆ§ B âˆˆ m âˆ§ C âˆˆ m â‡’ Line t âˆ§ A âˆˆ t âˆ§ B âˆˆ t â‡’ Â¬(A = E) âˆ§ Â¬(B = C) âˆ§ Â¬(A = B) âˆ§ E âˆ‰ t âˆ§ C âˆ‰ t â‡’ Â¬(C,E same_side t) â‡’ âˆ¡ E A B â‰¡ âˆ¡ C B A â‡’ l âˆ¥ m proof intro_TAC âˆ€A B C E l m t, l_line, m_line, t_line, Distinct, Cnsim_tE, AltIntAngCong; Â¬Collinear E A B âˆ§ Â¬Collinear C B A [EABncol] by fol t_line Distinct NonCollinearRaa CollinearSymmetry; B âˆ‰ l âˆ§ A âˆ‰ m [notAmBl] by fol l_line m_line Collinear_DEF - âˆ‰; assume Â¬(l âˆ¥ m) [Con] by fol; Â¬(l âˆ© m = âˆ…) [] by fol - l_line m_line PARALLEL; consider G such that G âˆˆ l âˆ§ G âˆˆ m [Glm] by fol - MEMBER_NOT_EMPTY IN_INTER; Â¬(G = A) âˆ§ Â¬(G = B) âˆ§ Collinear B G C âˆ§ Collinear B C G âˆ§ Collinear A E G âˆ§ Collinear A G E [GnotAB] by fol - notAmBl âˆ‰ m_line l_line Collinear_DEF; Â¬Collinear A G B âˆ§ Â¬Collinear B G A âˆ§ G âˆ‰ t [AGBncol] by fol EABncol CollinearSymmetry - NoncollinearityExtendsToLine t_line Collinear_DEF âˆ‰; Â¬(E,C same_side t) [Ensim_tC] by fol t_line - Distinct Cnsim_tE SameSideSymmetric; E âˆˆ l â” {A} âˆ§ G âˆˆ l â” {A} [] by fol l_line Glm Distinct GnotAB IN_DIFF IN_SING; Â¬(G,E same_side t) [] proof assume G,E same_side t [Gsim_tE] by fol; A âˆ‰ Open (G, E) [notGAE] by fol t_line - SameSide_DEF âˆ‰; G âˆˆ ray A E â” {A} [] by fol Distinct GnotAB notGAE IN_Ray GnotAB IN_DIFF IN_SING; ray A G = ray A E [rAGrAE] by fol Distinct - RayWellDefined; Â¬(C,G same_side t) [Cnsim_tG] by fol t_line AGBncol Distinct Gsim_tE Cnsim_tE SameSideTransitive; C âˆ‰ ray B G [notCrBG] by fol - IN_Ray Distinct t_line AGBncol RaySameSide Cnsim_tG IN_DIFF IN_SING âˆ‰; B âˆˆ Open (C, G) [] by fol - GnotAB âˆ‰ IN_Ray; âˆ¡ G A B <_ang âˆ¡ C B A [] by fol AGBncol notCrBG - B1' EuclidPropositionI_16; âˆ¡ E A B <_ang âˆ¡ C B A [] by fol - rAGrAE Angle_DEF; fol EABncol ANGLE AltIntAngCong - AngleTrichotomy1; qed; G,C same_side t [Gsim_tC] by fol t_line AGBncol Distinct - Cnsim_tE AtMost2Sides; B âˆ‰ Open (G, C) [notGBC] by fol t_line - SameSide_DEF âˆ‰; G âˆˆ ray B C â” {B} [] by fol Distinct GnotAB notGBC IN_Ray GnotAB IN_DIFF IN_SING; ray B G = ray B C [rBGrBC] by fol Distinct - RayWellDefined; âˆ¡ C B A â‰¡ âˆ¡ E A B [flipAltIntAngCong] by fol EABncol ANGLE AltIntAngCong C5Symmetric; Â¬(E,G same_side t) [Ensim_tG] by fol t_line AGBncol Distinct Gsim_tC Ensim_tC SameSideTransitive; E âˆ‰ ray A G [notErAG] by fol - IN_Ray Distinct t_line AGBncol RaySameSide Ensim_tG IN_DIFF IN_SING âˆ‰; A âˆˆ Open (E, G) [] by fol - GnotAB âˆ‰ IN_Ray; âˆ¡ G B A <_ang âˆ¡ E A B [] by fol AGBncol notErAG - B1' EuclidPropositionI_16; âˆ¡ C B A <_ang âˆ¡ E A B [] by fol - rBGrBC Angle_DEF; fol EABncol ANGLE flipAltIntAngCong - AngleTrichotomy1; qed; `;; let EuclidPropositionI_28 = theorem `; âˆ€A B C D E F G H l m t. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ G âˆˆ l â‡’ Line m âˆ§ C âˆˆ m âˆ§ D âˆˆ m âˆ§ H âˆˆ m â‡’ Line t âˆ§ G âˆˆ t âˆ§ H âˆˆ t â‡’ G âˆ‰ m âˆ§ H âˆ‰ l â‡’ G âˆˆ Open (A, B) âˆ§ H âˆˆ Open (C, D) â‡’ G âˆˆ Open (E, H) âˆ§ H âˆˆ Open (F, G) â‡’ Â¬(D,A same_side t) â‡’ âˆ¡ E G B â‰¡ âˆ¡ G H D âˆ¨ âˆ¡ B G H suppl âˆ¡ G H D â‡’ l âˆ¥ m proof intro_TAC âˆ€A B C D E F G H l m t, l_line, m_line, t_line, notGmHl, H1, H2, H3, H4; Â¬(A = G) âˆ§ Â¬(G = B) âˆ§ Â¬(H = D) âˆ§ Â¬(E = G) âˆ§ Â¬(G = H) âˆ§ Collinear A G B âˆ§ Collinear E G H [Distinct] by fol H1 H2 B1'; Â¬Collinear H G A âˆ§ Â¬Collinear G H D âˆ§ A âˆ‰ t âˆ§ D âˆ‰ t [HGAncol] by fol Distinct l_line m_line notGmHl NonCollinearRaa CollinearSymmetry Collinear_DEF t_line âˆ‰; Â¬Collinear B G H âˆ§ Â¬Collinear A G E âˆ§ Â¬Collinear E G B [BGHncol] by fol - Distinct CollinearSymmetry NoncollinearityExtendsToLine; âˆ¡ A G H â‰¡ âˆ¡ D H G [] proof case_split EGBeqGHD | BGHeqGHD by fol H4; suppose âˆ¡ E G B â‰¡ âˆ¡ G H D; âˆ¡ E G B â‰¡ âˆ¡ H G A âˆ§ Angle (âˆ¡ E G B) âˆ§ Angle (âˆ¡ H G A) âˆ§ Angle (âˆ¡ G H D) [boo] by fol BGHncol H1 H2 VerticalAnglesCong HGAncol ANGLE; âˆ¡ H G A â‰¡ âˆ¡ E G B [] by fol - C5Symmetric; âˆ¡ H G A â‰¡ âˆ¡ G H D [] by fol boo - EGBeqGHD C5Transitive; fol - AngleSymmetry; end; suppose âˆ¡ B G H suppl âˆ¡ G H D; âˆ¡ B G H suppl âˆ¡ H G A [] by fol BGHncol H1 B1' SupplementaryAngles_DEF; fol - BGHeqGHD AngleSymmetry SupplementUnique AngleSymmetry; end; qed; fol l_line m_line t_line Distinct HGAncol H3 - AlternateInteriorAngles; qed; `;; let OppositeSidesCongImpliesParallelogram = theorem `; âˆ€A B C D. Quadrilateral A B C D â‡’ seg A B â‰¡ seg C D âˆ§ seg B C â‰¡ seg D A â‡’ Parallelogram A B C D proof intro_TAC âˆ€A B C D, H1, H2; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬(C = D) âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B [TetraABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF; consider a c such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a âˆ§ Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c [ac_line] by fol TetraABCD I1; consider b d such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [bd_line] by fol TetraABCD I1; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line] by fol TetraABCD I1; consider m such that Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [m_line] by fol TetraABCD I1; B âˆ‰ l âˆ§ D âˆ‰ l âˆ§ A âˆ‰ m âˆ§ C âˆ‰ m [notBDlACm] by fol l_line m_line TetraABCD Collinear_DEF âˆ‰; seg A C â‰¡ seg C A âˆ§ seg B D â‰¡ seg D B [seg_refl] by fol TetraABCD SEGMENT C2Reflexive SegmentSymmetry; A,B,C â‰… C,D,A [] by fol TetraABCD H2 - SSS; âˆ¡ B C A â‰¡ âˆ¡ D A C âˆ§ âˆ¡ C A B â‰¡ âˆ¡ A C D [BCAeqDAC] by fol - TriangleCong_DEF; seg C D â‰¡ seg A B [CDeqAB] by fol TetraABCD SEGMENT H2 C2Symmetric; B,C,D â‰… D,A,B [] by fol TetraABCD H2 - seg_refl SSS; âˆ¡ C D B â‰¡ âˆ¡ A B D âˆ§ âˆ¡ D B C â‰¡ âˆ¡ B D A âˆ§ âˆ¡ C B D â‰¡ âˆ¡ A D B [CDBeqABD] by fol - TriangleCong_DEF AngleSymmetry; Â¬(B,D same_side l) âˆ¨ Â¬(A,C same_side m) [] by fol H1 l_line m_line FiveChoicesQuadrilateral; case_split Case1 | Ansim_mC by fol -; suppose Â¬(B,D same_side l); Â¬(D,B same_side l) [] by fol l_line notBDlACm - SameSideSymmetric; a âˆ¥ c âˆ§ b âˆ¥ d [] by fol ac_line l_line TetraABCD notBDlACm - BCAeqDAC AngleSymmetry AlternateInteriorAngles bd_line BCAeqDAC; fol H1 ac_line bd_line - Parallelogram_DEF; end; suppose Â¬(A,C same_side m); b âˆ¥ d [bâˆ¥d] by fol bd_line m_line TetraABCD notBDlACm - CDBeqABD AlternateInteriorAngles; c âˆ¥ a [] by fol ac_line m_line TetraABCD notBDlACm Ansim_mC CDBeqABD AlternateInteriorAngles; fol H1 ac_line bd_line bâˆ¥d - ParallelSymmetry Parallelogram_DEF; end; qed; `;; let OppositeAnglesCongImpliesParallelogramHelp = theorem `; âˆ€A B C D a c. Quadrilateral A B C D â‡’ âˆ¡ A B C â‰¡ âˆ¡ C D A âˆ§ âˆ¡ D A B â‰¡ âˆ¡ B C D â‡’ Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a â‡’ Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c â‡’ a âˆ¥ c proof intro_TAC âˆ€A B C D a c, H1, H2, a_line, c_line; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬(C = D) âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B [TetraABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF; âˆ¡ C D A â‰¡ âˆ¡ A B C âˆ§ âˆ¡ B C D â‰¡ âˆ¡ D A B [H2'] by fol TetraABCD ANGLE H2 C5Symmetric; consider l m such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l âˆ§ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [lm_line] by fol TetraABCD I1; consider b d such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [bd_line] by fol TetraABCD I1; A âˆ‰ c âˆ§ B âˆ‰ c âˆ§ A âˆ‰ b âˆ§ D âˆ‰ b âˆ§ B âˆ‰ d âˆ§ C âˆ‰ d [point_off_line] by fol c_line bd_line Collinear_DEF TetraABCD âˆ‰; Â¬(A âˆˆ int_triangle B C D âˆ¨ B âˆˆ int_triangle C D A âˆ¨ C âˆˆ int_triangle D A B âˆ¨ D âˆˆ int_triangle A B C) [] proof assume A âˆˆ int_triangle B C D âˆ¨ B âˆˆ int_triangle C D A âˆ¨ C âˆˆ int_triangle D A B âˆ¨ D âˆˆ int_triangle A B C [Con] by fol; âˆ¡ B C D <_ang âˆ¡ D A B âˆ¨ âˆ¡ C D A <_ang âˆ¡ A B C âˆ¨ âˆ¡ D A B <_ang âˆ¡ B C D âˆ¨ âˆ¡ A B C <_ang âˆ¡ C D A [] by fol TetraABCD - EuclidPropositionI_21; fol - H2' H2 AngleTrichotomy1; qed; ConvexQuadrilateral A B C D [] by fol H1 lm_line - FiveChoicesQuadrilateral; A âˆˆ int_angle B C D âˆ§ B âˆˆ int_angle C D A âˆ§ C âˆˆ int_angle D A B âˆ§ D âˆˆ int_angle A B C [AintBCD] by fol - ConvexQuad_DEF; B,A same_side c âˆ§ B,C same_side d [Bsim_cA] by fol c_line bd_line - InteriorUse; A,D same_side b [Asim_bD] by fol bd_line c_line AintBCD InteriorUse; assume Â¬(a âˆ¥ c) [Con] by fol; consider G such that G âˆˆ a âˆ§ G âˆˆ c [Gac] by fol - a_line c_line PARALLEL MEMBER_NOT_EMPTY IN_INTER; Collinear A B G âˆ§ Collinear D G C âˆ§ Collinear C G D [ABGcol] by fol a_line - Collinear_DEF c_line; Â¬(G = A) âˆ§ Â¬(G = B) âˆ§ Â¬(G = C) âˆ§ Â¬(G = D) [GnotABCD] by fol Gac ABGcol TetraABCD CollinearSymmetry Collinear_DEF; Â¬Collinear B G C âˆ§ Â¬Collinear A D G [BGCncol] by fol c_line Gac GnotABCD point_off_line NonCollinearRaa CollinearSymmetry; Â¬Collinear B C G âˆ§ Â¬Collinear G B C âˆ§ Â¬Collinear G A D âˆ§ Â¬Collinear A G D [BCGncol] by fol - CollinearSymmetry; G âˆ‰ b âˆ§ G âˆ‰ d [notGb] by fol bd_line Collinear_DEF BGCncol âˆ‰; G âˆ‰ Open (B, A) [notBGA] by fol Bsim_cA Gac SameSide_DEF âˆ‰; B âˆ‰ Open (A, G) [notABG] proof assume Â¬(B âˆ‰ Open (A, G)) [Con] by fol; B âˆˆ Open (A, G) [ABG] by fol - âˆ‰; ray A B = ray A G [rABrAG] by fol - IntervalRay; Â¬(A,G same_side b) [] by fol bd_line ABG SameSide_DEF; Â¬(D,G same_side b) [] by fol bd_line point_off_line notGb Asim_bD - SameSideTransitive; D âˆ‰ ray C G [] by fol bd_line notGb - RaySameSide TetraABCD IN_DIFF IN_SING âˆ‰; C âˆˆ Open (D, G) [DCG] by fol GnotABCD ABGcol - IN_Ray âˆ‰; consider M such that D âˆˆ Open (C, M) [CDM] by fol TetraABCD B2'; D âˆˆ Open (G, M) [GDM] by fol - B1' DCG TransitivityBetweennessHelp; âˆ¡ C D A suppl âˆ¡ A D M âˆ§ âˆ¡ A B C suppl âˆ¡ C B G [] by fol TetraABCD CDM ABG SupplementaryAngles_DEF; âˆ¡ M D A â‰¡ âˆ¡ G B C [MDAeqGBC] by fol - H2' SupplementsCongAnglesCong AngleSymmetry; âˆ¡ G A D <_ang âˆ¡ M D A âˆ§ âˆ¡ G B C <_ang âˆ¡ D C B [] by fol BCGncol BGCncol GDM DCG B1' EuclidPropositionI_16; âˆ¡ G A D <_ang âˆ¡ D C B [] by fol - BCGncol ANGLE MDAeqGBC AngleTrichotomy2 AngleOrderTransitivity; âˆ¡ D A B <_ang âˆ¡ B C D [] by fol - rABrAG Angle_DEF AngleSymmetry; fol - H2 AngleTrichotomy1; qed; A âˆ‰ Open (G, B) [] proof assume Â¬(A âˆ‰ Open (G, B)) [Con] by fol; A âˆˆ Open (B, G) [BAG] by fol - B1' âˆ‰; ray B A = ray B G [rBArBG] by fol - IntervalRay; Â¬(B,G same_side d) [] by fol bd_line BAG SameSide_DEF; Â¬(C,G same_side d) [] by fol bd_line point_off_line notGb Bsim_cA - SameSideTransitive; C âˆ‰ ray D G [] by fol bd_line notGb - RaySameSide TetraABCD IN_DIFF IN_SING âˆ‰; D âˆˆ Open (C, G) [CDG] by fol GnotABCD ABGcol - IN_Ray âˆ‰; consider M such that C âˆˆ Open (D, M) [DCM] by fol B2' TetraABCD; C âˆˆ Open (G, M) [GCM] by fol - B1' CDG TransitivityBetweennessHelp; âˆ¡ B C D suppl âˆ¡ M C B âˆ§ âˆ¡ D A B suppl âˆ¡ G A D [] by fol TetraABCD CollinearSymmetry DCM BAG SupplementaryAngles_DEF AngleSymmetry; âˆ¡ M C B â‰¡ âˆ¡ G A D [GADeqMCB] by fol - H2' SupplementsCongAnglesCong; âˆ¡ G B C <_ang âˆ¡ M C B âˆ§ âˆ¡ G A D <_ang âˆ¡ C D A [] by fol BGCncol GCM BCGncol CDG B1' EuclidPropositionI_16; âˆ¡ G B C <_ang âˆ¡ C D A [] by fol - BCGncol ANGLE GADeqMCB AngleTrichotomy2 AngleOrderTransitivity; âˆ¡ A B C <_ang âˆ¡ C D A [] by fol - rBArBG Angle_DEF; fol - H2 AngleTrichotomy1; qed; fol TetraABCD GnotABCD ABGcol notABG notBGA - B3' âˆ‰; qed; `;; let OppositeAnglesCongImpliesParallelogram = theorem `; âˆ€A B C D. Quadrilateral A B C D â‡’ âˆ¡ A B C â‰¡ âˆ¡ C D A âˆ§ âˆ¡ D A B â‰¡ âˆ¡ B C D â‡’ Parallelogram A B C D proof intro_TAC âˆ€A B C D, H1, H2; Quadrilateral B C D A [QuadBCDA] by fol H1 QuadrilateralSymmetry; Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬(C = D) âˆ§ Â¬(D = A) âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear D A B [TetraABCD] by fol H1 Quadrilateral_DEF Tetralateral_DEF; âˆ¡ B C D â‰¡ âˆ¡ D A B [H2'] by fol TetraABCD ANGLE H2 C5Symmetric; consider a such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line] by fol TetraABCD I1; consider b such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b [b_line] by fol TetraABCD I1; consider c such that Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c [c_line] by fol TetraABCD I1; consider d such that Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [d_line] by fol TetraABCD I1; fol H1 QuadBCDA H2 H2' a_line b_line c_line d_line OppositeAnglesCongImpliesParallelogramHelp Parallelogram_DEF; qed; `;; let P = NewAxiom `;âˆ€P l. Line l âˆ§ P âˆ‰ l â‡’ âˆƒ! m. Line m âˆ§ P âˆˆ m âˆ§ m âˆ¥ l`;; NewConstant("Î¼",`:(point->bool)->real`);; let AMa = NewAxiom `;âˆ€Î±. Angle Î± â‡’ &0 < Î¼ Î± âˆ§ Î¼ Î± < &180`;; let AMb = NewAxiom `;âˆ€Î±. Right Î± â‡’ Î¼ Î± = &90`;; let AMc = NewAxiom `;âˆ€Î± Î². Angle Î± âˆ§ Angle Î² âˆ§ Î± â‰¡ Î² â‡’ Î¼ Î± = Î¼ Î²`;; let AMd = NewAxiom `;âˆ€A O B P. P âˆˆ int_angle A O B â‡’ Î¼ (âˆ¡ A O B) = Î¼ (âˆ¡ A O P) + Î¼ (âˆ¡ P O B)`;; let ConverseAlternateInteriorAngles = theorem `; âˆ€A B C E l m. Line l âˆ§ A âˆˆ l âˆ§ E âˆˆ l â‡’ Line m âˆ§ B âˆˆ m âˆ§ C âˆˆ m â‡’ Line t âˆ§ A âˆˆ t âˆ§ B âˆˆ t â‡’ Â¬(A = E) âˆ§ Â¬(B = C) âˆ§ Â¬(A = B) âˆ§ E âˆ‰ t âˆ§ C âˆ‰ t â‡’ Â¬(C,E same_side t) â‡’ l âˆ¥ m â‡’ âˆ¡ E A B â‰¡ âˆ¡ C B A proof intro_TAC âˆ€A B C E l m, l_line, m_line, t_line, Distinct, Cnsim_tE, para_lm; Â¬Collinear C B A [] by fol Distinct t_line NonCollinearRaa CollinearSymmetry; A âˆ‰ m âˆ§ Angle (âˆ¡ C B A) [notAm] by fol m_line - Collinear_DEF âˆ‰ ANGLE; consider D such that Â¬(A = D) âˆ§ D âˆ‰ t âˆ§ Â¬(C,D same_side t) âˆ§ seg A D â‰¡ seg A E âˆ§ âˆ¡ B A D â‰¡ âˆ¡ C B A [Dexists] by simplify C4OppositeSide - Distinct t_line; consider k such that Line k âˆ§ A âˆˆ k âˆ§ D âˆˆ k [k_line] by fol Distinct I1; k âˆ¥ m [] by fol - m_line t_line Dexists Distinct AngleSymmetry AlternateInteriorAngles; k = l [] by fol m_line notAm l_line k_line - para_lm P; D,E same_side t âˆ§ A âˆ‰ Open (D, E) âˆ§ Collinear A E D [] by fol t_line Distinct Dexists Cnsim_tE AtMost2Sides SameSide_DEF âˆ‰ - k_line l_line Collinear_DEF; ray A D = ray A E [] by fol Distinct - IN_Ray Dexists RayWellDefined IN_DIFF IN_SING; fol - Dexists AngleSymmetry Angle_DEF; qed; `;; let HilbertTriangleSum = theorem `; âˆ€A B C. Â¬Collinear A B C â‡’ âˆƒE F. B âˆˆ Open (E, F) âˆ§ C âˆˆ int_angle A B F âˆ§ âˆ¡ E B A â‰¡ âˆ¡ C A B âˆ§ âˆ¡ C B F â‰¡ âˆ¡ B C A proof intro_TAC âˆ€A B C, ABCncol; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear C A B [Distinct] by fol ABCncol NonCollinearImpliesDistinct CollinearSymmetry; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line] by fol Distinct I1; consider x such that Line x âˆ§ A âˆˆ x âˆ§ B âˆˆ x [x_line] by fol Distinct I1; consider y such that Line y âˆ§ B âˆˆ y âˆ§ C âˆˆ y [y_line] by fol Distinct I1; C âˆ‰ x [notCx] by fol x_line ABCncol Collinear_DEF âˆ‰; Angle (âˆ¡ C A B) [] by fol ABCncol CollinearSymmetry ANGLE; consider E such that Â¬(B = E) âˆ§ E âˆ‰ x âˆ§ Â¬(C,E same_side x) âˆ§ seg B E â‰¡ seg A B âˆ§ âˆ¡ A B E â‰¡ âˆ¡ C A B [Eexists] by simplify C4OppositeSide - Distinct x_line notCx; consider m such that Line m âˆ§ B âˆˆ m âˆ§ E âˆˆ m [m_line] by fol - I1; âˆ¡ E B A â‰¡ âˆ¡ C A B [EBAeqCAB] by fol Eexists AngleSymmetry; m âˆ¥ l [para_lm] by fol m_line l_line x_line Eexists Distinct notCx - AlternateInteriorAngles; m âˆ© l = âˆ… [ml0] by fol - PARALLEL; C âˆ‰ m âˆ§ A âˆ‰ m [notACm] by fol - l_line INTER_COMM DisjointOneNotOther; consider F such that B âˆˆ Open (E, F) [EBF] by fol Eexists B2'; Â¬(B = F) âˆ§ F âˆˆ m [EBF'] by fol - B1' m_line BetweenLinear; Â¬Collinear A B F âˆ§ F âˆ‰ x [ABFncol] by fol EBF' m_line notACm NonCollinearRaa CollinearSymmetry Collinear_DEF x_line âˆ‰; Â¬(E,F same_side x) âˆ§ Â¬(E,F same_side y) [Ensim_yF] by fol EBF x_line y_line SameSide_DEF; C,F same_side x [Csim_xF] by fol x_line notCx Eexists ABFncol Eexists - AtMost2Sides; C,A same_side m [] by fol m_line l_line ml0 DisjointLinesImplySameSide; C âˆˆ int_angle A B F [CintABF] by fol ABFncol x_line m_line EBF' notCx notACm Csim_xF - IN_InteriorAngle; A âˆˆ int_angle C B E [] by fol EBF B1' - InteriorAngleSymmetry InteriorReflectionInterior; A âˆ‰ y âˆ§ A,E same_side y [Asim_yE] by fol y_line m_line - InteriorUse; E âˆ‰ y âˆ§ F âˆ‰ y [notEFy] by fol y_line m_line EBF' Eexists EBF' I1 Collinear_DEF notACm âˆ‰; E,A same_side y [] by fol y_line - Asim_yE SameSideSymmetric; Â¬(A,F same_side y) [Ansim_yF] by fol y_line notEFy Asim_yE - Ensim_yF SameSideTransitive; âˆ¡ F B C â‰¡ âˆ¡ A C B [] by fol m_line EBF' l_line y_line EBF' Distinct notEFy Asim_yE Ansim_yF para_lm ConverseAlternateInteriorAngles; fol EBF CintABF EBAeqCAB - AngleSymmetry; qed; `;; let EuclidPropositionI_13 = theorem `; âˆ€A O B A'. Â¬Collinear A O B âˆ§ O âˆˆ Open (A, A') â‡’ Î¼ (âˆ¡ A O B) + Î¼ (âˆ¡ B O A') = &180 proof intro_TAC âˆ€A O B A', H1 H2; case_split RightAOB | notRightAOB by fol -; suppose Right (âˆ¡ A O B); Right (âˆ¡ B O A') âˆ§ Î¼ (âˆ¡ A O B) = &90 âˆ§ Î¼ (âˆ¡ B O A') = &90 [] by fol H1 H2 - RightImpliesSupplRight AMb; real_arithmetic -; end; suppose Â¬Right (âˆ¡ A O B); Â¬(A = O) âˆ§ Â¬(O = B) [Distinct] by fol H1 NonCollinearImpliesDistinct; consider l such that Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ A' âˆˆ l [l_line] by fol - I1 H2 BetweenLinear; B âˆ‰ l [notBl] by fol - Distinct I1 Collinear_DEF H1 âˆ‰; consider F such that Right (âˆ¡ O A F) âˆ§ Angle (âˆ¡ O A F) [RightOAF] by fol Distinct EuclidPropositionI_11 RightImpliesAngle; âˆƒ! r. Ray r âˆ§ âˆƒE. Â¬(O = E) âˆ§ r = ray O E âˆ§ E âˆ‰ l âˆ§ E,B same_side l âˆ§ âˆ¡ A O E â‰¡ âˆ¡ O A F [] by simplify C4 - Distinct l_line notBl; consider E such that Â¬(O = E) âˆ§ E âˆ‰ l âˆ§ E,B same_side l âˆ§ âˆ¡ A O E â‰¡ âˆ¡ O A F [Eexists] by fol -; Â¬Collinear A O E [AOEncol] by fol Distinct l_line - NonCollinearRaa CollinearSymmetry; Right (âˆ¡ A O E) [RightAOE] by fol - ANGLE RightOAF Eexists CongRightImpliesRight; Right (âˆ¡ E O A') âˆ§ Î¼ (âˆ¡ A O E) = &90 âˆ§ Î¼ (âˆ¡ E O A') = &90 [RightEOA'] by fol AOEncol H2 - RightImpliesSupplRight AMb; Â¬(âˆ¡ A O B â‰¡ âˆ¡ A O E) [] by fol notRightAOB H1 ANGLE RightAOE CongRightImpliesRight; Â¬(âˆ¡ A O B = âˆ¡ A O E) [] by fol H1 AOEncol ANGLE - C5Reflexive; Â¬(ray O B = ray O E) [] by fol - Angle_DEF; B âˆ‰ ray O E âˆ§ O âˆ‰ Open (B, E) [] by fol Distinct - Eexists RayWellDefined IN_DIFF IN_SING âˆ‰ l_line B1' SameSide_DEF; Â¬Collinear O E B [] by fol - Eexists IN_Ray âˆ‰; E âˆˆ int_angle A O B âˆ¨ B âˆˆ int_angle A O E [] by fol Distinct l_line Eexists notBl AngleOrdering - CollinearSymmetry InteriorAngleSymmetry; case_split EintAOB | BintAOE by fol -; suppose E âˆˆ int_angle A O B; B âˆˆ int_angle E O A' [] by fol H2 - InteriorReflectionInterior; Î¼ (âˆ¡ A O B) = Î¼ (âˆ¡ A O E) + Î¼ (âˆ¡ E O B) âˆ§ Î¼ (âˆ¡ E O A') = Î¼ (âˆ¡ E O B) + Î¼ (âˆ¡ B O A') [] by fol EintAOB - AMd; real_arithmetic - RightEOA'; end; suppose B âˆˆ int_angle A O E; E âˆˆ int_angle B O A' [] by fol H2 - InteriorReflectionInterior; Î¼ (âˆ¡ A O E) = Î¼ (âˆ¡ A O B) + Î¼ (âˆ¡ B O E) âˆ§ Î¼ (âˆ¡ B O A') = Î¼ (âˆ¡ B O E) + Î¼ (âˆ¡ E O A') [] by fol BintAOE - AMd; real_arithmetic - RightEOA'; end; end; qed; `;; let TriangleSum = theorem `; âˆ€A B C. Â¬Collinear A B C â‡’ Î¼ (âˆ¡ A B C) + Î¼ (âˆ¡ B C A) + Î¼ (âˆ¡ C A B) = &180 proof intro_TAC âˆ€A B C, ABCncol; Â¬Collinear C A B âˆ§ Â¬Collinear B C A [CABncol] by fol ABCncol CollinearSymmetry; consider E F such that B âˆˆ Open (E, F) âˆ§ C âˆˆ int_angle A B F âˆ§ âˆ¡ E B A â‰¡ âˆ¡ C A B âˆ§ âˆ¡ C B F â‰¡ âˆ¡ B C A [EBF] by fol ABCncol HilbertTriangleSum; Â¬Collinear C B F âˆ§ Â¬Collinear A B F âˆ§ Collinear E B F âˆ§ Â¬(B = E) [CBFncol] by fol - InteriorAngleSymmetry InteriorEZHelp IN_InteriorAngle B1' CollinearSymmetry; Â¬Collinear E B A [EBAncol] by fol CollinearSymmetry - NoncollinearityExtendsToLine; Î¼ (âˆ¡ A B F) = Î¼ (âˆ¡ A B C) + Î¼ (âˆ¡ C B F) [Î¼CintABF] by fol EBF AMd; Î¼ (âˆ¡ E B A) + Î¼ (âˆ¡ A B F) = &180 [suppl180] by fol EBAncol EBF EuclidPropositionI_13; Î¼ (âˆ¡ C A B) = Î¼ (âˆ¡ E B A) âˆ§ Î¼ (âˆ¡ B C A) = Î¼ (âˆ¡ C B F) [] by fol CABncol EBAncol CBFncol ANGLE EBF AMc; real_arithmetic suppl180 Î¼CintABF -; qed; `;; let CircleConvex2_THM = theorem `; âˆ€O A B C. Â¬Collinear A O B â‡’ B âˆˆ Open (A, C) â‡’ seg O A <__ seg O B âˆ¨ seg O A â‰¡ seg O B â‡’ seg O B <__ seg O C proof intro_TAC âˆ€O A B C, H1, H2, H3; Â¬Collinear O B A âˆ§ Â¬Collinear B O A âˆ§ Â¬Collinear O A B âˆ§ Â¬(O = A) âˆ§ Â¬(O = B) [H1'] by fol H1 CollinearSymmetry NonCollinearImpliesDistinct; B âˆˆ Open (C, A) âˆ§ Â¬(C = A) âˆ§ Â¬(C = B) âˆ§ Collinear A B C âˆ§ Collinear B A C [H2'] by fol H2 B1' CollinearSymmetry; Â¬Collinear O B C âˆ§ Â¬Collinear O C B [OBCncol] by fol H1' - NoncollinearityExtendsToLine CollinearSymmetry; Â¬Collinear O A C [OABncol] by fol H1' H2' NoncollinearityExtendsToLine; âˆ¡ O C B <_ang âˆ¡ O B A [OCBlessOBA] by fol OBCncol H2' ExteriorAngle; âˆ¡ O A B <_ang âˆ¡ O B C [OABlessOBC] by fol H1' H2 ExteriorAngle; âˆ¡ O B A <_ang âˆ¡ B A O âˆ¨ âˆ¡ O B A â‰¡ âˆ¡ B A O [] proof assume seg O A â‰¡ seg O B [Cong] by fol H3 H1' EuclidPropositionI_18; seg O B â‰¡ seg O A [] by fol H1' SEGMENT - C2Symmetric; fol H1' - IsoscelesCongBaseAngles AngleSymmetry; qed; âˆ¡ O B A <_ang âˆ¡ O A B âˆ¨ âˆ¡ O B A â‰¡ âˆ¡ O A B [OBAlessOAB] by fol - AngleSymmetry; âˆ¡ O C B <_ang âˆ¡ O B C [] by fol OCBlessOBA - OABlessOBC OBCncol H1' OABncol OBCncol ANGLE - AngleOrderTransitivity AngleTrichotomy2; fol OBCncol - AngleSymmetry EuclidPropositionI_19; qed; `;;