(* ----------------------------------------------------------------- *) (* HOL Light Hilbert geometry axiomatic proofs using miz3. *) (* ----------------------------------------------------------------- *) (* 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 their proofs in miz3 and HOL Light. Thanks to BjÃ¸rn Jahren, Miguel Lerma,Takuo Matsuoka, Stephen Wilson for advice on Hilbert's axioms, and especially Benjamin Kordesh, who carefully read 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 valuable tool to help read it, as Hartshorne's proofs are often sketchy and even have gaps. M. Greenberg, Euclidean and non-Euclidean geometries, W. H. Freeman and Co., 1974. R. Hartshorne, Geometry, Euclid and Beyond, Undergraduate Texts in Math., Springer, 2000. Thanks to Mizar folks for their influential language, Freek Wiedijk, who wrote the miz3 port of Mizar to HOL Light, and especially John Harrison, who was extremely helpful and developed the framework for porting my axiomatic proofs to HOL Light. *) verbose := false;; report_timing := false;; horizon := 0;; timeout := 50;; new_type("point",0);; new_type_abbrev("point_set",`:point->bool`);; new_constant("Between",`:point->point->point->bool`);; new_constant("Line",`:point_set->bool`);; new_constant("â‰¡",`:(point->bool)->(point->bool)->bool`);; parse_as_infix("â‰…",(12, "right"));; parse_as_infix("same_side",(12, "right"));; parse_as_infix("â‰¡",(12, "right"));; parse_as_infix("<__",(12, "right"));; parse_as_infix("<_ang",(12, "right"));; parse_as_infix("suppl",(12, "right"));; parse_as_infix("âˆ‰",(11, "right"));; parse_as_infix("âˆ¥",(12, "right"));;let âˆ‰ = new_definition `âˆ€a:A l:A->bool. a âˆ‰ l â‡” Â¬(a âˆˆ l)`;;let Interval_DEF = new_definition `âˆ€ A B. open (A,B) = {X | Between A X B}`;;let Collinear_DEF = new_definition `Collinear A B C â‡” âˆƒ l. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l`;;let SameSide_DEF = new_definition `A,B same_side l â‡” Line l âˆ§ Â¬ âˆƒ X. (X âˆˆ l) âˆ§ X âˆˆ open (A,B)`;;let Ray_DEF = new_definition `âˆ€ A B. ray A B = {X | Â¬(A = B) âˆ§ Collinear A B X âˆ§ A âˆ‰ open (X,B)}`;;let Ordered_DEF = new_definition `ordered A B C D â‡” B âˆˆ open (A,C) âˆ§ B âˆˆ open (A,D) âˆ§ C âˆˆ open (A,D) âˆ§ C âˆˆ open (B,D)`;;let InteriorAngle_DEF = new_definition `âˆ€ A O B. int_angle A O B = {P:point | Â¬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 = new_definition `âˆ€ 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 = new_definition `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 = new_definition `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 = new_definition `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 = new_definition `seg A B = {A, B} UNION open (A,B)`;;let SegmentOrdering_DEF = new_definition `s <__ t â‡” Segment s âˆ§ âˆƒ C D X. t = seg C D âˆ§ X âˆˆ open (C,D) âˆ§ s â‰¡ seg C X`;;let AngleOrdering_DEF = new_definition `Î± <_ang Î² â‡” Angle Î± âˆ§ âˆƒ A O B G. Â¬Collinear A O B âˆ§ Î² = âˆ¡ A O B âˆ§ G âˆˆ int_angle A O B âˆ§ Î± â‰¡ âˆ¡ A O G`;;let TriangleCong_DEF = new_definition `âˆ€ A B C A' B' C' :point. (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 = new_definition `âˆ€ Î± Î². Î± suppl Î² â‡” âˆƒ A O B A'. Â¬Collinear A O B âˆ§ O âˆˆ open (A,A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î² = âˆ¡ B O A'`;;let RightAngle_DEF = new_definition `âˆ€ Î±. Right Î± â‡” âˆƒ Î². Î± suppl Î² âˆ§ Î± â‰¡ Î²`;;let PlaneComplement_DEF = new_definition `âˆ€ Î±:point_set. complement Î± = {P | P âˆ‰ Î±}`;;let Parallelogram_DEF = new_definition `âˆ€ 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`;;(* ---------------------------------------------------------------------------- *) (* Hilbert's geometry axioms, except the parallel axiom P, defined near the end. *) (* ---------------------------------------------------------------------------- *) let I1 = new_axiom `âˆ€ A B. Â¬(A = B) â‡’ âˆƒ! l. Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l`;; let I2 = new_axiom `âˆ€ l. Line l â‡’ âˆƒ A B. A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B)`;; let I3 = new_axiom `âˆƒ A B C. Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear A B C`;; let B1 = new_axiom `âˆ€ A B C. Between A B C â‡’ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Between C B A âˆ§ Collinear A B C`;; let B2 = new_axiom `âˆ€ A B. Â¬(A = B) â‡’ âˆƒ C. Between A B C`;; let B3 = new_axiom `âˆ€ 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 = new_axiom `âˆ€ 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 = new_axiom `âˆ€ s O Z. Segment s âˆ§ Â¬(O = Z) â‡’ âˆƒ! P. P âˆˆ ray O Z â” O âˆ§ seg O P â‰¡ s`;; let C2Reflexive = new_axiom `Segment s â‡’ s â‰¡ s`;; let C2Symmetric = new_axiom `Segment s âˆ§ Segment t âˆ§ s â‰¡ t â‡’ t â‰¡ s`;; let C2Transitive = new_axiom `Segment s âˆ§ Segment t âˆ§ Segment u âˆ§ s â‰¡ t âˆ§ t â‰¡ u â‡’ s â‰¡ u`;; let C3 = new_axiom `âˆ€ 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 = new_axiom `âˆ€ Î± 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 = new_axiom `Angle Î± â‡’ Î± â‰¡ Î±`;; let C5Symmetric = new_axiom `Angle Î± âˆ§ Angle Î² âˆ§ Î± â‰¡ Î² â‡’ Î² â‰¡ Î±`;; let C5Transitive = new_axiom `Angle Î± âˆ§ Angle Î² âˆ§ Angle Î³ âˆ§ Î± â‰¡ Î² âˆ§ Î² â‰¡ Î³ â‡’ Î± â‰¡ Î³`;; let C6 = new_axiom `âˆ€ 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 = thm `; âˆ€ A B X. X âˆˆ open (A,B) â‡” Between A X B by Interval_DEF, SET_RULE; `;; let IN_Ray = thm `; âˆ€ A B X. X âˆˆ ray A B â‡” Â¬(A = B) âˆ§ Collinear A B X âˆ§ A âˆ‰ open (X,B) by Ray_DEF, SET_RULE; `;; let IN_InteriorAngle = thm `; âˆ€ 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 InteriorAngle_DEF, SET_RULE; `;; let IN_InteriorTriangle = thm `; âˆ€ 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 InteriorTriangle_DEF, SET_RULE; `;; let IN_PlaneComplement = thm `; âˆ€ Î±:point_set. âˆ€ P. P âˆˆ complement Î± â‡” P âˆ‰ Î± by PlaneComplement_DEF, SET_RULE; `;; let IN_InteriorCircle = thm `; âˆ€ O R P. P âˆˆ int_circle O R â‡” Â¬(O = R) âˆ§ (P = O âˆ¨ seg O P <__ seg O R) by InteriorCircle_DEF, SET_RULE; `;; let B1' = thm `; âˆ€ A B C. B âˆˆ open (A,C) â‡’ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ B âˆˆ open (C,A) âˆ§ Collinear A B C by IN_Interval, B1; `;; let B2' = thm `; âˆ€ A B. Â¬(A = B) â‡’ âˆƒ C. B âˆˆ open (A,C) by IN_Interval, B2; `;; let B3' = thm `; âˆ€ 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 IN_Interval, B3; `;; let B4' = thm `; âˆ€ 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 IN_Interval, B4; `;; let B4'' = thm `; âˆ€ l:point_set. âˆ€ A B C:point. 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 by B4', SameSide_DEF; `;; let DisjointOneNotOther = thm `; âˆ€ l m:A->bool. (âˆ€ x:A. x âˆˆ m â‡’ x âˆ‰ l) â‡” l âˆ© m = âˆ… by SET_RULE, âˆ‰; `;; let EquivIntersectionHelp = thm `; âˆ€ e x:A. âˆ€ l m:A->bool. (l âˆ© m = {x} âˆ¨ m âˆ© l = {x}) âˆ§ e âˆˆ m â” x â‡’ e âˆ‰ l by SET_RULE, âˆ‰; `;; let CollinearSymmetry = thm `; let A B C be point; assume Collinear A B C [H1]; thus Collinear A C B âˆ§ Collinear B A C âˆ§ Collinear B C A âˆ§ Collinear C A B âˆ§ Collinear C B A proof consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l by H1, Collinear_DEF; qed by -, Collinear_DEF; `;; let ExistsNewPointOnLine = thm `; let P be point; let l be point_set; assume Line l âˆ§ P âˆˆ l [H1]; thus âˆƒ Q. Q âˆˆ l âˆ§ Â¬(P = Q) proof consider A B such that A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B) [l_line] by H1, I2; cases; suppose P = A; qed by -, l_line; suppose Â¬(P = A); qed by -, l_line; end; `;; let ExistsPointOffLine = thm `; let l be point_set; assume Line l [H1]; thus âˆƒ Q:point. Q âˆ‰ l proof consider A B C such that Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear A B C [Distinct] by I3; (A âˆ‰ l âˆ¨ B âˆ‰ l âˆ¨ C âˆ‰ l) âˆ¨ (A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l) by âˆ‰; cases by -; suppose A âˆ‰ l âˆ¨ B âˆ‰ l âˆ¨ C âˆ‰ l; qed by -; suppose (A âˆˆ l) âˆ§ (B âˆˆ l) âˆ§ (C âˆˆ l); Collinear A B C by H1, -, Collinear_DEF; qed by -, Distinct; end; `;; let BetweenLinear = thm `; let A B C be point; let m be point_set; assume Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m [H1]; assume B âˆˆ open (A,C) âˆ¨ C âˆˆ open (B,A) âˆ¨ A âˆˆ open (C,B) [H2]; thus B âˆˆ m proof Â¬(A = C) âˆ§ (Collinear A B C âˆ¨ Collinear B C A âˆ¨ Collinear C A B) [X1] by H2, B1'; consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l [X2] by -, Collinear_DEF; l = m by X1, -, H2, H1, I1; qed by -, X2; `;; let CollinearLinear = thm `; let A B C be point; let m be point_set; assume Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m [H1]; assume Collinear A B C âˆ¨ Collinear B C A âˆ¨ Collinear C A B [H2]; assume Â¬(A = C) [H3]; thus B âˆˆ m proof consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l [X1] by H2, Collinear_DEF; l = m by H3, -, H1, I1; qed by -, X1; `;; let NonCollinearImpliesDistinct = thm `; let A B C be point; assume Â¬Collinear A B C [H1]; thus Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) proof cases; suppose A = B âˆ§ B = C [Case1]; consider Q such that Â¬(Q = A) by I3; qed by -, I1, Case1, Collinear_DEF, H1; suppose (A = B âˆ§ Â¬(A = C)) âˆ¨ (A = C âˆ§ Â¬(A = B)) âˆ¨ (B = C âˆ§ Â¬(A = B)); qed by -, I1, Collinear_DEF, H1; suppose Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C); qed by -; end; `;; let Reverse4Order = thm `; âˆ€ A B C D:point. ordered A B C D â‡’ ordered D C B A by Ordered_DEF, B1'; `;; let OriginInRay = thm `; let O Q be point; assume Â¬(Q = O) [H1]; thus O âˆˆ ray O Q proof O âˆ‰ open (O,Q) [OOQ] by B1', âˆ‰; Collinear O Q O by H1, I1, Collinear_DEF; qed by H1, -, OOQ, IN_Ray; `;; let EndpointInRay = thm `; let O Q be point; assume Â¬(Q = O) [H1]; thus Q âˆˆ ray O Q proof O âˆ‰ open (Q,Q) [notOQQ] by B1', âˆ‰; Collinear O Q Q by H1, I1, Collinear_DEF; qed by H1, -, notOQQ, IN_Ray; `;; let I1Uniqueness = thm `; let X be point; let l m be point_set; assume Line l âˆ§ Line m [H0]; assume Â¬(l = m) [H1]; assume X âˆˆ l âˆ§ X âˆˆ m [H2]; thus l âˆ© m = {X} proof assume Â¬(l âˆ© m = {X}) [H3]; X âˆˆ l âˆ© m by H2, IN_INTER; consider A such that A âˆˆ l âˆ© m âˆ§ Â¬(A = X) [X1] by -, H3, SET_RULE; A âˆˆ l âˆ§ X âˆˆ l âˆ§ A âˆˆ m âˆ§ X âˆˆ m by H0, -, H2, IN_INTER; l = m by H0, -, X1, I1; qed by -, H1; `;; let EquivIntersection = thm `; let A B X be point; let l m be point_set; assume Line l âˆ§ Line m [H0]; assume l âˆ© m = {X} [H1]; assume A âˆˆ m â” X âˆ§ B âˆˆ m â” X [H2]; assume X âˆ‰ open (A,B) [H3]; thus A,B same_side l proof assume Â¬(A,B same_side l) [Con]; A âˆˆ m âˆ§ B âˆˆ m âˆ§ Â¬(A = X) âˆ§ Â¬(B = X) [H2'] by H2, IN_DELETE; Â¬(open (A,B) âˆ© l = âˆ…) [nonempty] by H0, Con, SameSide_DEF, SET_RULE; open (A,B) âŠ‚ m [ABm] by H0, H2', BetweenLinear, SUBSET; open (A,B) âˆ© l âŠ‚ {X} by -, SET_RULE, H1; X âˆˆ open (A,B) âˆ© l by nonempty, -, SET_RULE; qed by -, IN_INTER, H3, âˆ‰; `;; let RayLine = thm `; âˆ€ O P:point. âˆ€ l: point_set. Line l âˆ§ O âˆˆ l âˆ§ P âˆˆ l â‡’ ray O P âŠ‚ l by IN_Ray, CollinearLinear, SUBSET; `;; let RaySameSide = thm `; let l be point_set; let O A P be point; assume Line l âˆ§ O âˆˆ l [l_line]; assume A âˆ‰ l [notAl]; assume P âˆˆ ray O A â” O [PrOA]; thus P âˆ‰ l âˆ§ P,A same_side l proof Â¬(O = A) [notOA] by l_line, notAl, âˆ‰; consider d such that Line d âˆ§ O âˆˆ d âˆ§ A âˆˆ d [d_line] by notOA, I1; Â¬(l = d) by -, notAl, âˆ‰; l âˆ© d = {O} [ldO] by l_line, d_line, -, I1Uniqueness; A âˆˆ d â” O [Ad_O] by d_line, notOA, IN_DELETE; ray O A âŠ‚ d by d_line, RayLine; P âˆˆ d â” O [Pd_O] by PrOA, -, SUBSET, IN_DELETE; P âˆ‰ l [notPl] by ldO, -, EquivIntersectionHelp; O âˆ‰ open (P,A) by PrOA, IN_DELETE, IN_Ray; P,A same_side l by l_line, d_line, ldO, Ad_O, Pd_O, -, EquivIntersection; qed by notPl, -; `;; let IntervalRayEZ = thm `; let A B C be point; assume B âˆˆ open (A,C) [H1]; thus B âˆˆ ray A C â” A âˆ§ C âˆˆ ray A B â” A proof Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Collinear A B C [ABC] by H1, B1'; A âˆ‰ open (B,C) âˆ§ A âˆ‰ open (C,B) by -, H1, B3', B1', âˆ‰; qed by ABC, CollinearSymmetry, -, IN_Ray, IN_DELETE, âˆ‰; `;; let NoncollinearityExtendsToLine = thm `; let A O B X be point; assume Â¬Collinear A O B [H1]; assume Collinear O B X âˆ§ Â¬(X = O) [H2]; thus Â¬Collinear A O X proof Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) [Distinct] by H1, NonCollinearImpliesDistinct; consider b such that Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [b_line] by Distinct, I1; A âˆ‰ b [notAb] by b_line, Collinear_DEF, H1, âˆ‰; X âˆˆ b by H2, b_line, Distinct, I1, Collinear_DEF; qed by b_line, -, H2, I1, Collinear_DEF, notAb, âˆ‰; `;; let SameSideReflexive = thm `; âˆ€ l A. Line l âˆ§ A âˆ‰ l â‡’ A,A same_side l by B1', SameSide_DEF; `;; let SameSideSymmetric = thm `; âˆ€ l A B. Line l âˆ§ A âˆ‰ l âˆ§ B âˆ‰ l â‡’ A,B same_side l â‡’ B,A same_side l by SameSide_DEF, B1'; `;; let SameSideTransitive = thm `; let l be point_set; let A B C be point; assume Line l [l_line]; assume A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l [notABCl]; assume A,B same_side l [Asim_lB]; assume B,C same_side l [Bsim_lC]; thus A,C same_side l proof cases; suppose Â¬Collinear A B C âˆ¨ A = B âˆ¨ A = C âˆ¨ B = C; qed by l_line, -, notABCl, Asim_lB, Bsim_lC, B4'', SameSideReflexive; suppose Collinear A B C âˆ§ Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [Distinct]; consider m such that Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m [m_line] by Distinct, I1; B âˆˆ m [Bm] by -, Distinct, CollinearLinear; cases; suppose m âˆ© l = âˆ…; qed by m_line, l_line, -, BetweenLinear, SET_RULE, SameSide_DEF; suppose Â¬(m âˆ© l = âˆ…); consider X such that X âˆˆ l âˆ§ X âˆˆ m [Xlm] by -, MEMBER_NOT_EMPTY, IN_INTER; Collinear A X B âˆ§ Collinear B A C âˆ§ Collinear A B C [ABXcol] by m_line, Bm, -, Collinear_DEF; consider E such that E âˆˆ l âˆ§ Â¬(E = X) [El_X] by l_line, Xlm, ExistsNewPointOnLine; Â¬Collinear E A X [EAXncol] by l_line, El_X, Xlm, I1, Collinear_DEF, notABCl, âˆ‰; consider B' such that Â¬(B = E) âˆ§ B âˆˆ open (E,B') [EBB'] by notABCl, El_X, âˆ‰, B2'; Â¬(B' = E) âˆ§ Â¬(B' = B) âˆ§ Collinear B E B' [EBB'col] by -, B1', CollinearSymmetry; Â¬Collinear A B B' âˆ§ Â¬Collinear B' B A âˆ§ Â¬Collinear B' A B [ABB'ncol] by EAXncol, ABXcol, Distinct, NoncollinearityExtendsToLine, CollinearSymmetry, -; Â¬Collinear B' B C âˆ§ Â¬Collinear B' A C âˆ§ Â¬Collinear A B' C [AB'Cncol] by ABB'ncol, ABXcol, Distinct, NoncollinearityExtendsToLine, CollinearSymmetry; B' âˆˆ ray E B â” E âˆ§ B âˆˆ ray E B' â” E by EBB', IntervalRayEZ; B' âˆ‰ l âˆ§ B',B same_side l âˆ§ B,B' same_side l [notB'l] by l_line, El_X, notABCl, -, RaySameSide; A,B' same_side l âˆ§ B',C same_side l by l_line, ABB'ncol, notABCl, notB'l, Asim_lB, -, B4'', AB'Cncol, Bsim_lC; qed by l_line, AB'Cncol, notABCl, notB'l, -, B4''; end; end; `;; let ConverseCrossbar = thm `; let O A B G be point; assume Â¬Collinear A O B [H1]; assume G âˆˆ open (A,B) [H2]; thus G âˆˆ int_angle A O B proof Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) [Distinct] by H1, NonCollinearImpliesDistinct; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by -, I1; consider b such that Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [b_line] by Distinct, I1; consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l [l_line] by Distinct, I1; B âˆ‰ a âˆ§ A âˆ‰ b by H1, a_line, Collinear_DEF, âˆ‰, b_line; Â¬(a = l) âˆ§ Â¬(b = l) by -, l_line, âˆ‰; a âˆ© l = {A} âˆ§ b âˆ© l = {B} [alA] by -, a_line, l_line, I1Uniqueness, b_line; Â¬(A = G) âˆ§ Â¬(A = B) âˆ§ Â¬(G = B) [AGB] by H2, B1'; A âˆ‰ open (G,B) âˆ§ B âˆ‰ open (G,A) [notGAB] by H2, B3', B1', âˆ‰; G âˆˆ l [Gl] by l_line, H2, BetweenLinear; G âˆ‰ a âˆ§ G âˆ‰ b [notGa] by alA, Gl, AGB, IN_DELETE, EquivIntersectionHelp; G âˆˆ l â” A âˆ§ B âˆˆ l â” A âˆ§ G âˆˆ l â” B âˆ§ A âˆˆ l â” B by Gl, l_line, AGB, IN_DELETE; G,B same_side a âˆ§ G,A same_side b by a_line, l_line, alA, -, notGAB, EquivIntersection, b_line; qed by H1, a_line, b_line, notGa, -, IN_InteriorAngle; `;; let InteriorUse = thm `; let A O B P be point; let a b be point_set; assume Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [aOAbOB]; assume P âˆˆ int_angle A O B [P_AOB]; thus P âˆ‰ a âˆ§ P âˆ‰ b âˆ§ P,B same_side a âˆ§ P,A same_side b proof 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 P_AOB, IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) [Distinct] by -, NonCollinearImpliesDistinct; Î± = a âˆ§ Î² = b by -, aOAbOB, exists, I1; qed by -, exists; `;; let InteriorEZHelp = thm `; let A O B P be point; assume P âˆˆ int_angle A O B [P_AOB]; thus Â¬(P = A) âˆ§ Â¬(P = O) âˆ§ Â¬(P = B) âˆ§ Â¬Collinear A O P proof 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 P_AOB, IN_InteriorAngle; Â¬(P = A) âˆ§ Â¬(P = O) âˆ§ Â¬(P = B) [PnotAOB] by -, âˆ‰; Â¬(A = O) [notAO] by def_int, NonCollinearImpliesDistinct; Â¬Collinear A O P by def_int, notAO, -, I1, Collinear_DEF, âˆ‰; qed by PnotAOB, -; `;; let InteriorAngleSymmetry = thm `; âˆ€ A O B P: point. P âˆˆ int_angle A O B â‡’ P âˆˆ int_angle B O A by IN_InteriorAngle, CollinearSymmetry; `;; let InteriorWellDefined = thm `; let A O B X P be point; assume P âˆˆ int_angle A O B [H1]; assume X âˆˆ ray O B â” O [H2]; thus P âˆˆ int_angle A O X proof 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 H1, IN_InteriorAngle; Â¬(X = O) âˆ§ Â¬(O = B) âˆ§ Collinear O B X [H2'] by H2, IN_DELETE, IN_Ray; B âˆ‰ a [notBa] by def_int, Collinear_DEF, âˆ‰; Â¬Collinear A O X [AOXnoncol] by def_int, H2', NoncollinearityExtendsToLine; X âˆˆ b [Xb] by def_int, H2', CollinearLinear; X âˆ‰ a âˆ§ B,X same_side a by def_int, notBa, H2, RaySameSide, SameSideSymmetric; P,X same_side a by def_int, -, notBa, SameSideTransitive; qed by AOXnoncol, def_int, Xb, -, IN_InteriorAngle; `;; let WholeRayInterior = thm `; let A O B X P be point; assume X âˆˆ int_angle A O B [XintAOB]; assume P âˆˆ ray O X â” O [PrOX]; thus P âˆˆ int_angle A O B proof 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 XintAOB, IN_InteriorAngle; P âˆ‰ a âˆ§ P,X same_side a âˆ§ P âˆ‰ b âˆ§ P,X same_side b [Psim_abX] by def_int, PrOX, RaySameSide; P,B same_side a âˆ§ P,A same_side b by -, def_int, Collinear_DEF, SameSideTransitive, âˆ‰; qed by def_int, Psim_abX, -, IN_InteriorAngle; `;; let AngleOrdering = thm `; let O A P Q be point; let a be point_set; assume Â¬(O = A) [H1]; assume Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [H2]; assume P âˆ‰ a âˆ§ Q âˆ‰ a [H3]; assume P, Q same_side a [H4]; assume Â¬Collinear P O Q [H5]; thus P âˆˆ int_angle Q O A âˆ¨ Q âˆˆ int_angle P O A proof Â¬(P = O) âˆ§ Â¬(P = Q) âˆ§ Â¬(O = Q) [Distinct] by H5, NonCollinearImpliesDistinct; consider q such that Line q âˆ§ O âˆˆ q âˆ§ Q âˆˆ q [q_line] by Distinct, I1; P âˆ‰ q [notPq] by -, Collinear_DEF, H5, âˆ‰; assume Â¬(P âˆˆ int_angle Q O A) [notPintQOA]; Â¬Collinear Q O A âˆ§ Â¬Collinear P O A [POAncol] by H1, H2, I1, Collinear_DEF, H3, âˆ‰; Â¬(P,A same_side q) by -, H2, q_line, H3, notPq, H4, notPintQOA, IN_InteriorAngle; consider G such that G âˆˆ q âˆ§ G âˆˆ open (P,A) [existG] by q_line, -, SameSide_DEF; G âˆˆ int_angle P O A [G_POA] by POAncol, existG, ConverseCrossbar; G âˆ‰ a âˆ§ G,P same_side a âˆ§ Â¬(G = O) [Gsim_aP] by -, IN_InteriorAngle, H1, H2, I1, âˆ‰; G,Q same_side a by H2, Gsim_aP, H3, H4, SameSideTransitive; O âˆ‰ open (Q,G) [notQOG] by -, SameSide_DEF, H2, B1', âˆ‰; Collinear O G Q by q_line, existG, Collinear_DEF; Q âˆˆ ray O G â” O by Gsim_aP, -, notQOG, IN_Ray, Distinct, IN_DELETE; qed by G_POA, -, WholeRayInterior; `;; let InteriorsDisjointSupplement = thm `; let A O B A' be point; assume Â¬Collinear A O B [H1]; assume O âˆˆ open (A,A') [H2]; thus int_angle B O A' âˆ© int_angle A O B = âˆ… proof âˆ€ D. D âˆˆ int_angle A O B â‡’ D âˆ‰ int_angle B O A' proof let D be point; assume D âˆˆ int_angle A O B [H3]; Â¬(A = O) âˆ§ Â¬(O = B) by H1, NonCollinearImpliesDistinct; consider a b such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b âˆ§ A' âˆˆ a [ab_line] by -, I1, H2, BetweenLinear; Â¬Collinear B O A' by H1, CollinearSymmetry, H2, B1', NoncollinearityExtendsToLine; A âˆ‰ b âˆ§ A' âˆ‰ b [notAb] by ab_line, Collinear_DEF, H1, -, âˆ‰; Â¬(A',A same_side b) [A'nsim_bA] by ab_line, H2, B1', SameSide_DEF ; D âˆ‰ b âˆ§ D,A same_side b [DintAOB] by ab_line, H3, InteriorUse; Â¬(D,A' same_side b) by ab_line, notAb, DintAOB, A'nsim_bA, SameSideSymmetric, SameSideTransitive; qed by ab_line, -, InteriorUse, âˆ‰; qed by -, DisjointOneNotOther; `;; let InteriorReflectionInterior = thm `; let A O B D A' be point; assume O âˆˆ open (A,A') [H1]; assume D âˆˆ int_angle A O B [H2]; thus B âˆˆ int_angle D O A' proof 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 H2, IN_InteriorAngle; Â¬(O = B) âˆ§ Â¬(O = A') âˆ§ B âˆ‰ a [Distinct] by -, NonCollinearImpliesDistinct, H1, B1', Collinear_DEF, âˆ‰; Â¬Collinear D O B [DOB_ncol] by DintAOB, -, I1, Collinear_DEF, âˆ‰; A' âˆˆ a [A'a] by H1, DintAOB, BetweenLinear; D âˆ‰ int_angle B O A' by DintAOB, H1, InteriorsDisjointSupplement, H2, DisjointOneNotOther; qed by Distinct, DintAOB, A'a, DOB_ncol, -, AngleOrdering, âˆ‰; `;; let Crossbar_THM = thm `; let O A B D be point; assume D âˆˆ int_angle A O B [H1]; thus âˆƒ G. G âˆˆ open (A,B) âˆ§ G âˆˆ ray O D â” O proof 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 H1, IN_InteriorAngle; B âˆ‰ a [notBa] by DintAOB, Collinear_DEF, âˆ‰; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) âˆ§ Â¬(D = O) [Distinct] by DintAOB, NonCollinearImpliesDistinct, âˆ‰; consider l such that Line l âˆ§ O âˆˆ l âˆ§ D âˆˆ l [l_line] by -, I1; consider A' such that O âˆˆ open (A,A') [AOA'] by Distinct, B2'; A' âˆˆ a âˆ§ Collinear A O A' âˆ§ Â¬(A' = O) [A'a] by DintAOB, -, BetweenLinear, B1'; Â¬(A,A' same_side l) [Ansim_lA'] by l_line, AOA', SameSide_DEF; B âˆˆ int_angle D O A' by H1, AOA', InteriorReflectionInterior; B,A' same_side l [Bsim_lA'] by l_line, DintAOB, A'a, -, InteriorUse; Â¬Collinear A O D âˆ§ Â¬Collinear B O D [AODncol] by H1, InteriorEZHelp, InteriorAngleSymmetry; Â¬Collinear D O A' by -, CollinearSymmetry, A'a, NoncollinearityExtendsToLine; A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ A' âˆ‰ l by l_line, Collinear_DEF, AODncol, -, âˆ‰; Â¬(A,B same_side l) by l_line, -, Bsim_lA', Ansim_lA', SameSideTransitive; consider G such that G âˆˆ open (A,B) âˆ§ G âˆˆ l [AGB] by l_line, -, SameSide_DEF; Collinear O D G [ODGcol] by -, l_line, Collinear_DEF; G âˆˆ int_angle A O B by DintAOB, AGB, ConverseCrossbar; G âˆ‰ a âˆ§ G,B same_side a âˆ§ Â¬(G = O) [Gsim_aB] by DintAOB, -, InteriorUse, âˆ‰; B,D same_side a by DintAOB, notBa, SameSideSymmetric; G,D same_side a [Gsim_aD] by DintAOB, Gsim_aB, notBa, -, SameSideTransitive; O âˆ‰ open (G,D) by DintAOB, -, SameSide_DEF, âˆ‰; G âˆˆ ray O D â” O by Distinct, ODGcol, -, IN_Ray, Gsim_aB, IN_DELETE; qed by AGB, -; `;; let AlternateConverseCrossbar = thm `; let O A B G be point; assume Collinear A G B âˆ§ G âˆˆ int_angle A O B [H1]; thus G âˆˆ open (A,B) proof 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 H1, IN_InteriorAngle; Â¬(A = B) âˆ§ Â¬(G = A) âˆ§ Â¬(G = B) âˆ§ A âˆ‰ open (G,B) âˆ§ B âˆ‰ open (G,A) by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp, SameSide_DEF, âˆ‰; qed by -, H1, B1', B3', âˆ‰; `;; let InteriorOpposite = thm `; let A O B P be point; let p be point_set; assume P âˆˆ int_angle A O B [PintAOB]; assume Line p âˆ§ O âˆˆ p âˆ§ P âˆˆ p [p_line]; thus Â¬(A,B same_side p) proof consider G such that G âˆˆ open (A,B) âˆ§ G âˆˆ ray O P [Gexists] by PintAOB, Crossbar_THM, IN_DELETE; G âˆˆ p by p_line, RayLine, -, SUBSET; qed by p_line, -, Gexists, SameSide_DEF; `;; let IntervalTransitivity = thm `; let O P Q R be point; let m be point_set; assume Line m âˆ§ O âˆˆ m [H0]; assume P âˆˆ m â” O âˆ§ Q âˆˆ m â” O âˆ§ R âˆˆ m â” O [H2]; assume O âˆ‰ open (P,Q) âˆ§ O âˆ‰ open (Q,R) [H3]; thus O âˆ‰ open (P,R) proof consider E such that E âˆ‰ m âˆ§ Â¬(O = E) [notEm] by H0, ExistsPointOffLine, âˆ‰; consider l such that Line l âˆ§ O âˆˆ l âˆ§ E âˆˆ l [l_line] by -, I1; Â¬(m = l) by notEm, -, âˆ‰; l âˆ© m = {O} [lmO] by l_line, H0, -, l_line, I1Uniqueness; P âˆ‰ l âˆ§ Q âˆ‰ l âˆ§ R âˆ‰ l [notPQRl] by -, H2, EquivIntersectionHelp; P,Q same_side l âˆ§ Q,R same_side l by l_line, H0, lmO, H2, H3, EquivIntersection; P,R same_side l [Psim_lR] by l_line, notPQRl, -, SameSideTransitive; qed by l_line, -, SameSide_DEF, âˆ‰; `;; let RayWellDefinedHalfway = thm `; let O P Q be point; assume Â¬(Q = O) [H1]; assume P âˆˆ ray O Q â” O [H2]; thus ray O P âŠ‚ ray O Q proof consider m such that Line m âˆ§ O âˆˆ m âˆ§ Q âˆˆ m [OQm] by H1, I1; P âˆˆ ray O Q âˆ§ Â¬(P = O) âˆ§ O âˆ‰ open (P,Q) [H2'] by H2, IN_DELETE, IN_Ray; P âˆˆ m âˆ§ P âˆˆ m â” O âˆ§ Q âˆˆ m â” O [PQm_O] by OQm, H2', RayLine, SUBSET, H2', OQm, H1, IN_DELETE; O âˆ‰ open (P,Q) [notPOQ] by H2', IN_Ray; âˆ€ X. X âˆˆ ray O P â‡’ X âˆˆ ray O Q proof let X be point; assume X âˆˆ ray O P; X âˆˆ m âˆ§ O âˆ‰ open (X,P) [XrOP] by OQm, PQm_O, H2', -, RayLine, SUBSET, IN_Ray; Collinear O Q X [OQXcol] by OQm, -, Collinear_DEF; cases; suppose X = O; qed by H1, -, OriginInRay; suppose Â¬(X = O); X âˆˆ m â” O by XrOP, -, IN_DELETE; O âˆ‰ open (X,Q) by OQm, -, PQm_O, XrOP, H2', IntervalTransitivity; qed by H1, OQXcol, -, IN_Ray; end; qed by -, SUBSET; `;; let RayWellDefined = thm `; let O P Q be point; assume Â¬(Q = O) [H1]; assume P âˆˆ ray O Q â” O [H2]; thus ray O P = ray O Q proof ray O P âŠ‚ ray O Q [PsubsetQ] by H1, H2, RayWellDefinedHalfway; Â¬(P = O) âˆ§ Collinear O Q P âˆ§ O âˆ‰ open (P,Q) [H2'] by H2, IN_DELETE, IN_Ray; Q âˆˆ ray O P â” O by H2', B1', âˆ‰, CollinearSymmetry, IN_Ray, H1, IN_DELETE; ray O Q âŠ‚ ray O P [QsubsetP] by H2', -, RayWellDefinedHalfway; qed by PsubsetQ, QsubsetP, SUBSET_ANTISYM; `;; let OppositeRaysIntersect1pointHelp = thm `; let A O B X be point; assume O âˆˆ open (A,B) [H1]; assume X âˆˆ ray O B â” O [H2]; thus X âˆ‰ ray O A âˆ§ O âˆˆ open (X,A) proof Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) âˆ§ Collinear A O B [AOB] by H1, B1'; Â¬(X = O) âˆ§ Collinear O B X âˆ§ O âˆ‰ open (X,B) [H2'] by H2, IN_DELETE, IN_Ray; consider m such that Line m âˆ§ A âˆˆ m âˆ§ B âˆˆ m [m_line] by AOB, I1; O âˆˆ m âˆ§ X âˆˆ m [Om] by m_line, H2', AOB, CollinearLinear; A âˆˆ m â” O âˆ§ X âˆˆ m â” O âˆ§ B âˆˆ m â” O by m_line, -, H2', AOB, IN_DELETE; O âˆˆ open (X,A) by H1, m_line, Om, -, H2', IntervalTransitivity, âˆ‰, B1'; qed by -, IN_Ray, âˆ‰; `;; let OppositeRaysIntersect1point = thm `; let A O B be point; assume O âˆˆ open (A,B) [H1]; thus ray O A âˆ© ray O B = {O} proof Â¬(A = O) âˆ§ Â¬(O = B) by H1, B1'; {O} âŠ‚ ray O A âˆ© ray O B [Osubset_rOA] by -, OriginInRay, IN_INTER, SING_SUBSET; âˆ€ X. Â¬(X = O) âˆ§ X âˆˆ ray O B â‡’ X âˆ‰ ray O A by IN_DELETE, H1, OppositeRaysIntersect1pointHelp; ray O A âˆ© ray O B âŠ‚ {O} by -, IN_INTER, IN_SING, SUBSET, âˆ‰; qed by -, Osubset_rOA, SUBSET_ANTISYM; `;; let IntervalRay = thm `; âˆ€ A B C:point. B âˆˆ open (A,C) â‡’ ray A B = ray A C by B1', IntervalRayEZ, RayWellDefined; `;; let TransitivityBetweennessHelp = thm `; let A B C D be point; assume B âˆˆ open (A,C) âˆ§ C âˆˆ open (B,D) [H1]; thus B âˆˆ open (A,D) proof D âˆˆ ray B C â” B by H1, IntervalRayEZ; qed by H1, -, OppositeRaysIntersect1pointHelp, B1'; `;; let TransitivityBetweenness = thm `; let A B C D be point; assume B âˆˆ open (A,C) âˆ§ C âˆˆ open (B,D) [H1]; thus ordered A B C D proof B âˆˆ open (A,D) [ABD] by H1, TransitivityBetweennessHelp; C âˆˆ open (D,B) âˆ§ B âˆˆ open (C,A) by H1, B1'; C âˆˆ open (D,A) by -, TransitivityBetweennessHelp; qed by H1, ABD, -, B1', Ordered_DEF; `;; let IntervalsAreConvex = thm `; let A B C be point; assume B âˆˆ open (A,C) [H1]; thus open (A,B) âŠ‚ open (A,C) proof âˆ€ X. X âˆˆ open (A,B) â‡’ X âˆˆ open (A,C) proof let X be point; assume X âˆˆ open (A,B) [AXB]; X âˆˆ ray B A â” B by AXB, B1', IntervalRayEZ; B âˆˆ open (X,C) by H1, B1', -, OppositeRaysIntersect1pointHelp; qed by AXB, -, TransitivityBetweennessHelp; qed by -, SUBSET; `;; let TransitivityBetweennessVariant = thm `; let A X B C be point; assume X âˆˆ open (A,B) âˆ§ B âˆˆ open (A,C) [H1]; thus ordered A X B C proof X âˆˆ ray B A â” B by H1, B1', IntervalRayEZ; B âˆˆ open (X,C) by H1, B1', -, OppositeRaysIntersect1pointHelp; qed by H1, -, TransitivityBetweenness; `;; let Interval2sides2aLineHelp = thm `; let A B C X be point; assume B âˆˆ open (A,C) [H1]; thus X âˆ‰ open (A,B) âˆ¨ X âˆ‰ open (B,C) proof assume Â¬(X âˆ‰ open (A,B)); ordered A X B C by -, âˆ‰, H1, TransitivityBetweennessVariant; B âˆˆ open (X,C) by -, Ordered_DEF; X âˆ‰ open (C,B) by -, B1', B3', âˆ‰; qed by -, B1', âˆ‰; `;; let Interval2sides2aLine = thm `; let A B C X be point; assume Collinear A B C [H1]; thus X âˆ‰ open (A,B) âˆ¨ X âˆ‰ open (A,C) âˆ¨ X âˆ‰ open (B,C) proof cases; suppose A = B âˆ¨ A = C âˆ¨ B = C; qed by -, B1', âˆ‰; suppose Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C); B âˆˆ open (A,C) âˆ¨ C âˆˆ open (B,A) âˆ¨ A âˆˆ open (C,B) by -, H1, B3'; qed by -, Interval2sides2aLineHelp, B1', âˆ‰; end; `;; let TwosidesTriangle2aLine = thm `; let A B C Y be point; let l m be point_set; assume Line l âˆ§ Â¬Collinear A B C [H1]; assume A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l [off_l]; assume Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m [m_line]; assume Y âˆˆ l âˆ§ Y âˆˆ m [Ylm]; assume Â¬(A,B same_side l) âˆ§ Â¬(B,C same_side l) [H2]; thus A,C same_side l proof consider X Z such that X âˆˆ l âˆ§ X âˆˆ open (A,B) âˆ§ Z âˆˆ l âˆ§ Z âˆˆ open (C,B) [H2'] by 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 H1, NonCollinearImpliesDistinct, Ylm, off_l, âˆ‰, m_line, IN_DELETE; consider p such that Line p âˆ§ B âˆˆ p âˆ§ A âˆˆ p [p_line] by Distinct, I1; consider q such that Line q âˆ§ B âˆˆ q âˆ§ C âˆˆ q [q_line] by Distinct, I1; X âˆˆ p âˆ§ Z âˆˆ q [Xp] by p_line, H2', BetweenLinear, q_line, H2'; A âˆ‰ q âˆ§ B âˆ‰ m âˆ§ C âˆ‰ p [vertex_off_line] by 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 q_line, p_line, -, H2', B1', IntervalRayEZ, RaySameSide; Â¬(m = p) âˆ§ Â¬(m = q) by m_line, vertex_off_line, âˆ‰; p âˆ© m = {A} âˆ§ q âˆ© m = {C} [pmA] by p_line, m_line, q_line, H1, -, Xp, H2', I1Uniqueness; Y âˆ‰ p âˆ§ Y âˆ‰ q [notYpq] by -, Distinct, EquivIntersectionHelp; X âˆˆ ray A B â” A âˆ§ Z âˆˆ ray C B â” C by H2', IntervalRayEZ, H2', B1'; X âˆ‰ m âˆ§ Z âˆ‰ m âˆ§ X,B same_side m âˆ§ B,Z same_side m [notXZm] by m_line, vertex_off_line, -, RaySameSide, SameSideSymmetric; X,Z same_side m by m_line, -, vertex_off_line, SameSideTransitive; Collinear X Y Z âˆ§ Y âˆ‰ open (X,Z) âˆ§ Â¬(Y = X) âˆ§ Â¬(Y = Z) âˆ§ Â¬(X = Z) by H1, H2', Ylm, Collinear_DEF, m_line, -, SameSide_DEF, notXZm, Xsim_qA, Xp, âˆ‰; Z âˆˆ open (X,Y) âˆ¨ X âˆˆ open (Z,Y) by -, B3', âˆ‰, B1'; cases by -; suppose X âˆˆ open (Z,Y); Â¬(Z,Y same_side p) by p_line, Xp, -, SameSide_DEF; Â¬(C,Y same_side p) by p_line, Xsim_qA, vertex_off_line, notYpq, -, SameSideTransitive; A âˆˆ open (C,Y) by p_line, m_line, pmA, Distinct, -, EquivIntersection, âˆ‰; qed by H1, Ylm, off_l, -, B1', IntervalRayEZ, RaySameSide; suppose Z âˆˆ open (X,Y); Â¬(X,Y same_side q) by q_line, Xp, -, SameSide_DEF; Â¬(A,Y same_side q) by q_line, Xsim_qA, vertex_off_line, notYpq, -, SameSideTransitive; C âˆˆ open (Y,A) by q_line, m_line, pmA, Distinct, -, EquivIntersection, âˆ‰, B1'; qed by H1, Ylm, off_l, -, IntervalRayEZ, RaySameSide; end; `;; let LineUnionOf2Rays = thm `; let A O B be point; let l be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l [H1]; assume O âˆˆ open (A,B) [H2]; thus l = ray O A âˆª ray O B proof Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ O âˆˆ l [Distinct] by H2, B1', H1, BetweenLinear; ray O A âˆª ray O B âŠ‚ l [AOBsub_l] by H1, -, RayLine, UNION_SUBSET; âˆ€ X. X âˆˆ l â‡’ X âˆˆ ray O A âˆ¨ X âˆˆ ray O B proof let X be point; assume X âˆˆ l [Xl]; assume Â¬(X âˆˆ ray O B) [notXrOB]; Collinear O B X âˆ§ Collinear X A B âˆ§ Collinear O A X [XABcol] by Distinct, H1, Xl, Collinear_DEF; O âˆˆ open (X,B) by notXrOB, Distinct, -, IN_Ray, âˆ‰; O âˆ‰ open (X,A) by âˆ‰, B1', XABcol, -, H2, Interval2sides2aLine; qed by Distinct, XABcol, -, IN_Ray; l âŠ‚ ray O A âˆª ray O B by -, IN_UNION, SUBSET; qed by -, AOBsub_l, SUBSET_ANTISYM; `;; let AtMost2Sides = thm `; let A B C be point; let l be point_set; assume Line l [H1]; assume A âˆ‰ l âˆ§ B âˆ‰ l âˆ§ C âˆ‰ l [H2]; thus A,B same_side l âˆ¨ A,C same_side l âˆ¨ B,C same_side l proof cases; suppose A = C; qed by -, H1, H2, SameSideReflexive; suppose Â¬(A = C) [notAC]; consider m such that Line m âˆ§ A âˆˆ m âˆ§ C âˆˆ m [m_line] by notAC, I1; cases; suppose m âˆ© l = âˆ…; A,C same_side l by m_line, H1, -, BetweenLinear, SET_RULE, SameSide_DEF; qed by -; suppose Â¬(m âˆ© l = âˆ…); consider Y such that Y âˆˆ l âˆ§ Y âˆˆ m [Ylm] by -, IN_INTER, MEMBER_NOT_EMPTY; cases; suppose Â¬Collinear A B C; qed by H1, -, H2, m_line, Ylm, TwosidesTriangle2aLine; suppose Collinear A B C [ABCcol]; B âˆˆ m [Bm] by -, m_line, notAC, I1, Collinear_DEF; Â¬(Y = A) âˆ§ Â¬(Y = B) âˆ§ Â¬(Y = C) [YnotABC] by Ylm, H2, âˆ‰; Y âˆ‰ open (A,B) âˆ¨ Y âˆ‰ open (A,C) âˆ¨ Y âˆ‰ open (B,C) by ABCcol, Interval2sides2aLine; A âˆˆ ray Y B â” Y âˆ¨ A âˆˆ ray Y C â” Y âˆ¨ B âˆˆ ray Y C â” Y by YnotABC, m_line, Bm, Ylm, Collinear_DEF, -, IN_Ray, IN_DELETE; qed by H1, Ylm, H2, -, RaySameSide; end; end; end; `;; let FourPointsOrder = thm `; let A B C X be point; let l be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l âˆ§ X âˆˆ l [H1]; assume Â¬(X = A) âˆ§ Â¬(X = B) âˆ§ Â¬(X = C) [H2]; assume B âˆˆ open (A,C) [H3]; thus ordered X A B C âˆ¨ ordered A X B C âˆ¨ ordered A B X C âˆ¨ ordered A B C X proof A âˆˆ open (X,B) âˆ¨ X âˆˆ open (A,B) âˆ¨ X âˆˆ open (B,C) âˆ¨ C âˆˆ open (B,X) proof Â¬(A = B) âˆ§ Â¬(B = C) [ABCdistinct] by H3, B1'; Collinear A B X âˆ§ Collinear A C X âˆ§ Collinear C B X [ACXcol] by H1, Collinear_DEF; A âˆˆ open (X,B) âˆ¨ X âˆˆ open (A,B) âˆ¨ B âˆˆ open (A,X) by H2, ABCdistinct, -, B3', B1'; cases by -; suppose A âˆˆ open (X,B) âˆ¨ X âˆˆ open (A,B); qed by -; suppose B âˆˆ open (A,X); B âˆ‰ open (C,X) by ACXcol, H3, -, Interval2sides2aLine, âˆ‰; qed by H2, ABCdistinct, ACXcol, -, B3', B1', âˆ‰; end; qed by -, H3, B1', TransitivityBetweenness, TransitivityBetweennessVariant, Reverse4Order; `;; let HilbertAxiomRedundantByMoore = thm `; let A B C D be point; let l be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ C âˆˆ l âˆ§ D âˆˆ l [H1]; assume Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬(C = D) [H2]; thus 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 Collinear A B C by H1, Collinear_DEF; B âˆˆ open (A,C) âˆ¨ C âˆˆ open (A,B) âˆ¨ A âˆˆ open (C,B) by H2, -, B3', B1'; qed by -, H1, H2, FourPointsOrder; `;; let InteriorTransitivity = thm `; let A O B F G be point; assume G âˆˆ int_angle A O B [GintAOB]; assume F âˆˆ int_angle A O G [FintAOG]; thus F âˆˆ int_angle A O B proof Â¬Collinear A O B [AOBncol] by GintAOB, IN_InteriorAngle; consider G' such that G' âˆˆ open (A,B) âˆ§ G' âˆˆ ray O G â” O [CrossG] by GintAOB, Crossbar_THM; F âˆˆ int_angle A O G' by FintAOG, -, InteriorWellDefined; consider F' such that F' âˆˆ open (A,G') âˆ§ F' âˆˆ ray O F â” O [CrossF] by -, Crossbar_THM; Â¬(F' = O) âˆ§ Â¬(F = O) âˆ§ Collinear O F F' âˆ§ O âˆ‰ open (F',F) by -, IN_DELETE, IN_Ray; F âˆˆ ray O F' â” O [FrOF'] by -, CollinearSymmetry, B1', âˆ‰, IN_Ray, IN_DELETE; open (A,G') âŠ‚ open (A,B) âˆ§ F' âˆˆ open (A,B) by CrossG, IntervalsAreConvex, CrossF, SUBSET; F' âˆˆ int_angle A O B by AOBncol, -, ConverseCrossbar; qed by -, FrOF', WholeRayInterior; `;; let HalfPlaneConvexNonempty = thm `; let l H be point_set; let A be point; assume Line l âˆ§ A âˆ‰ l [l_line]; assume H = {X | X âˆ‰ l âˆ§ X,A same_side l} [HalfPlane]; thus Â¬(H = âˆ…) âˆ§ H âŠ‚ complement l âˆ§ Convex H proof âˆ€ X. X âˆˆ H â‡” X âˆ‰ l âˆ§ X,A same_side l [Hdef] by HalfPlane, SET_RULE; H âŠ‚ complement l [Hsub] by -, IN_PlaneComplement, SUBSET; A,A same_side l âˆ§ A âˆˆ H by l_line, SameSideReflexive, Hdef; Â¬(H = âˆ…) [Hnonempty] by -, MEMBER_NOT_EMPTY; âˆ€ P Q X. P âˆˆ H âˆ§ Q âˆˆ H âˆ§ X âˆˆ open (P,Q) â‡’ X âˆˆ H proof let P Q X be point; assume P âˆˆ H âˆ§ Q âˆˆ H âˆ§ X âˆˆ open (P,Q) [PXQ]; P âˆ‰ l âˆ§ P,A same_side l âˆ§ Q âˆ‰ l âˆ§ Q,A same_side l [PQinH] by -, Hdef; P,Q same_side l [Psim_lQ] by l_line, -, SameSideSymmetric, SameSideTransitive; X âˆ‰ l [notXl] by -, PXQ, SameSide_DEF, âˆ‰; open (X,P) âŠ‚ open (P,Q) by PXQ, IntervalsAreConvex, B1', SUBSET; X,P same_side l by l_line, -, SUBSET, Psim_lQ, SameSide_DEF; X,A same_side l by l_line, notXl, PQinH, -, Psim_lQ, PQinH, SameSideTransitive; qed by -, notXl, Hdef; Convex H by -, SUBSET, CONVEX; qed by Hnonempty, Hsub, -; `;; let PlaneSeparation = thm `; let l be point_set; assume Line l [l_line]; thus âˆƒ H1 H2:point_set. H1 âˆ© H2 = âˆ… âˆ§ Â¬(H1 = âˆ…) âˆ§ Â¬(H2 = âˆ…) âˆ§ Convex H1 âˆ§ Convex H2 âˆ§ complement l = H1 âˆª H2 âˆ§ âˆ€ P Q. P âˆˆ H1 âˆ§ Q âˆˆ H2 â‡’ Â¬(P,Q same_side l) proof consider A such that A âˆ‰ l [notAl] by l_line, ExistsPointOffLine; consider E such that E âˆˆ l âˆ§ Â¬(A = E) [El] by l_line, I2, -, âˆ‰; consider B such that E âˆˆ open (A,B) âˆ§ Â¬(E = B) âˆ§ Collinear A E B [AEB] by -, B2', B1'; B âˆ‰ l [notBl] by l_line, El, -, I1, Collinear_DEF, notAl, âˆ‰; Â¬(A,B same_side l) [Ansim_lB] by 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]; âˆ€ X. (X âˆˆ H1 â‡” X âˆ‰ l âˆ§ X,A same_side l) âˆ§ (X âˆˆ H2 â‡” X âˆ‰ l âˆ§ X,B same_side l) [H12def] by -, SET_RULE; âˆ€ X. X âˆˆ H1 â‡” X âˆ‰ l âˆ§ X,A same_side l [H1def] by H12sets, SET_RULE; âˆ€ X. X âˆˆ H2 â‡” X âˆ‰ l âˆ§ X,B same_side l [H2def] by H12sets, SET_RULE; H1 âˆ© H2 = âˆ… [H12disjoint] proof assume Â¬(H1 âˆ© H2 = âˆ…); consider V such that V âˆˆ H1 âˆ§ V âˆˆ H2 by -, MEMBER_NOT_EMPTY, IN_INTER; V âˆ‰ l âˆ§ V,A same_side l âˆ§ V âˆ‰ l âˆ§ V,B same_side l by -, H12def; A,B same_side l by l_line, -, notAl, notBl, SameSideSymmetric, SameSideTransitive; qed by -, Ansim_lB; Â¬(H1 = âˆ…) âˆ§ Â¬(H2 = âˆ…) âˆ§ H1 âŠ‚ complement l âˆ§ H2 âŠ‚ complement l âˆ§ Convex H1 âˆ§ Convex H2 [H12convex_nonempty] by l_line, notAl, notBl, H12sets, HalfPlaneConvexNonempty; H1 âˆª H2 âŠ‚ complement l [H12sub] by H12convex_nonempty, UNION_SUBSET; âˆ€ C. C âˆˆ complement l â‡’ C âˆˆ H1 âˆª H2 proof let C be point; assume C âˆˆ complement l; C âˆ‰ l [notCl] by -, IN_PlaneComplement; C,A same_side l âˆ¨ C,B same_side l by l_line, notAl, notBl, -, Ansim_lB, AtMost2Sides; C âˆˆ H1 âˆ¨ C âˆˆ H2 by notCl, -, H12def; qed by -, IN_UNION; complement l âŠ‚ H1 âˆª H2 by -, SUBSET; complement l = H1 âˆª H2 [compl_H1unionH2] by H12sub, -, SUBSET_ANTISYM; âˆ€ P Q. P âˆˆ H1 âˆ§ Q âˆˆ H2 â‡’ Â¬(P,Q same_side l) [opp_sides] proof let P Q be point; assume P âˆˆ H1 âˆ§ Q âˆˆ H2; P âˆ‰ l âˆ§ P,A same_side l âˆ§ Q âˆ‰ l âˆ§ Q,B same_side l [PH1_QH2] by -, H12def, IN; qed by l_line, -, notAl, SameSideSymmetric, notBl, Ansim_lB, SameSideTransitive; qed by H12disjoint, H12convex_nonempty, compl_H1unionH2, opp_sides; `;; let TetralateralSymmetry = thm `; let A B C D be point; assume Tetralateral A B C D [H1]; thus Tetralateral B C D A âˆ§ Tetralateral A B D C proof Â¬Collinear A B D âˆ§ Â¬Collinear B D C âˆ§ Â¬Collinear D C A âˆ§ Â¬Collinear C A B [TetraABCD] by H1, Tetralateral_DEF, CollinearSymmetry; qed by H1, -, Tetralateral_DEF; `;; let EasyEmptyIntersectionsTetralateralHelp = thm `; let A B C D be point; assume Tetralateral A B C D [H1]; thus open (A,B) âˆ© open (B,C) = âˆ… proof âˆ€ X. X âˆˆ open (B,C) â‡’ X âˆ‰ open (A,B) proof let X be point; assume X âˆˆ open (B,C); Â¬Collinear A B C âˆ§ Collinear B X C âˆ§ Â¬(X = B) by H1, Tetralateral_DEF, -, B1'; Â¬Collinear A X B by -, CollinearSymmetry, B1', NoncollinearityExtendsToLine; qed by -, B1', âˆ‰; qed by -, DisjointOneNotOther; `;; let EasyEmptyIntersectionsTetralateral = thm `; let A B C D be point; assume Tetralateral A B C D [H1]; thus 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 Tetralateral B C D A âˆ§ Tetralateral C D A B âˆ§ Tetralateral D A B C by H1, TetralateralSymmetry; qed by H1, -, EasyEmptyIntersectionsTetralateralHelp; `;; let SegmentSameSideOppositeLine = thm `; let A B C D be point; let a c be point_set; assume Quadrilateral A B C D [H1]; assume Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line]; assume Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c [c_line]; thus A,B same_side c âˆ¨ C,D same_side a proof assume Â¬(C,D same_side a); :: prove A,B same_side c consider G such that G âˆˆ a âˆ§ G âˆˆ open (C,D) [CGD] by -, a_line, SameSide_DEF; G âˆˆ c âˆ§ Collinear G B A [Gc] by c_line, -, BetweenLinear, a_line, Collinear_DEF; Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ open (A,B) âˆ© open (C,D) = âˆ… [quadABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF; A âˆ‰ c âˆ§ B âˆ‰ c âˆ§ Â¬(A = G) âˆ§ Â¬(B = G) [Distinct] by -, c_line, Collinear_DEF, âˆ‰, Gc; G âˆ‰ open (A,B) by quadABCD, CGD, DisjointOneNotOther; A âˆˆ ray G B â” G by Distinct, Gc, -, IN_Ray, IN_DELETE; qed by c_line, Gc, Distinct, -, RaySameSide; `;; let ConvexImpliesQuad = thm `; let A B C D be point; assume Tetralateral A B C D [H1]; assume C âˆˆ int_angle D A B âˆ§ D âˆˆ int_angle A B C [H2]; thus Quadrilateral A B C D proof Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬(A = D) [TetraABCD] by H1, Tetralateral_DEF; consider a such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line] by TetraABCD, I1; consider b such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b [b_line] by TetraABCD, I1; consider d such that Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [d_line] by TetraABCD, I1; open (B,C) âŠ‚ b âˆ§ open (A,B) âŠ‚ a [BCbABa] by b_line, a_line, BetweenLinear, SUBSET; D,A same_side b âˆ§ C,D same_side a by H2, a_line, b_line, d_line, InteriorUse; b âˆ© open (D,A) = âˆ… âˆ§ a âˆ© open (C,D) = âˆ… by -, b_line, SameSide_DEF, SET_RULE; open (B,C) âˆ© open (D,A) = âˆ… âˆ§ open (A,B) âˆ© open (C,D) = âˆ… by BCbABa, -, SET_RULE; qed by H1, -, Quadrilateral_DEF; `;; let DiagonalsIntersectImpliesConvexQuad = thm `; let A B C D G be point; assume Â¬Collinear B C D [BCDncol]; assume G âˆˆ open (A,C) âˆ§ G âˆˆ open (B,D) [DiagInt]; thus ConvexQuadrilateral A B C D proof Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬(C = D) âˆ§ Â¬(C = A) âˆ§ Â¬(A = G) âˆ§ Â¬(D = G) âˆ§ Â¬(B = G) [Distinct] by BCDncol, NonCollinearImpliesDistinct, DiagInt, B1'; Collinear A G C âˆ§ Collinear B G D [AGCcol] by DiagInt, B1'; Â¬Collinear C D A [CDAncol] by BCDncol, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine; Â¬Collinear D A B [DABncol] by -, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine; Â¬Collinear A B C [ABCncol] by -, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine; Â¬(A = B) âˆ§ Â¬(A = D) by DABncol, NonCollinearImpliesDistinct; Tetralateral A B C D [TetraABCD] by 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 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 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 -, ArCG, WholeRayInterior; qed by TetraABCD, -, ConvexImpliesQuad, ConvexQuad_DEF; `;; let DoubleNotSimImpliesDiagonalsIntersect = thm `; let A B C D be point; let l m be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line]; assume Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [m_line]; assume Tetralateral A B C D [H1]; assume Â¬(B,D same_side l) [H2]; assume Â¬(A,C same_side m) [H3]; thus (âˆƒ G. G âˆˆ open (A,C) âˆ© open (B,D)) âˆ§ ConvexQuadrilateral A B C D proof Â¬Collinear A B C âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B [TetraABCD] by H1, Tetralateral_DEF; consider G such that G âˆˆ open (A,C) âˆ§ G âˆˆ m [AGC] by H3, m_line, SameSide_DEF; G âˆˆ l [Gl] by l_line, -, BetweenLinear; A âˆ‰ m âˆ§ B âˆ‰ l âˆ§ D âˆ‰ l by TetraABCD, m_line, l_line, Collinear_DEF, âˆ‰; Â¬(l = m) âˆ§ B âˆˆ m â” G âˆ§ D âˆˆ m â” G [BDm_G] by -, l_line, âˆ‰, m_line, Gl, IN_DELETE; l âˆ© m = {G} by l_line, m_line, -, Gl, AGC, I1Uniqueness; G âˆˆ open (B,D) by l_line, m_line, -, BDm_G, H2, EquivIntersection, âˆ‰; qed by AGC, -, IN_INTER, TetraABCD, DiagonalsIntersectImpliesConvexQuad; `;; let ConvexQuadImpliesDiagonalsIntersect = thm `; let A B C D be point; let l m be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line]; assume Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [m_line]; assume ConvexQuadrilateral A B C D [ConvQuadABCD]; thus Â¬(B,D same_side l) âˆ§ Â¬(A,C same_side m) âˆ§ (âˆƒ G. G âˆˆ open (A,C) âˆ© open (B,D)) âˆ§ Â¬Quadrilateral A B D C proof Tetralateral A B C D âˆ§ A âˆˆ int_angle B C D âˆ§ D âˆˆ int_angle A B C [convquadABCD] by ConvQuadABCD, ConvexQuad_DEF, Quadrilateral_DEF; Â¬(B,D same_side l) âˆ§ Â¬(A,C same_side m) [opp_sides] by convquadABCD, l_line, m_line, InteriorOpposite; consider G such that G âˆˆ open (A,C) âˆ© open (B,D) [Gexists] by l_line, m_line, convquadABCD, opp_sides, DoubleNotSimImpliesDiagonalsIntersect; Â¬(open (B,D) âˆ© open (C,A) = âˆ…) by -, IN_INTER, B1', MEMBER_NOT_EMPTY; Â¬Quadrilateral A B D C by -, Quadrilateral_DEF; qed by opp_sides, Gexists, -; `;; let FourChoicesTetralateralHelp = thm `; let A B C D be point; assume Tetralateral A B C D [H1]; assume C âˆˆ int_angle D A B [CintDAB]; thus ConvexQuadrilateral A B C D âˆ¨ C âˆˆ int_triangle D A B proof Â¬(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 H1, Tetralateral_DEF; consider a d such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [ad_line] by TetraABCD, I1; consider l m such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l âˆ§ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [lm_line] by TetraABCD, I1; C âˆ‰ a âˆ§ C âˆ‰ d âˆ§ B âˆ‰ l âˆ§ D âˆ‰ l âˆ§ A âˆ‰ m âˆ§ C âˆ‰ m âˆ§ Â¬Collinear A B D âˆ§ Â¬Collinear B D A [tetra'] by TetraABCD, ad_line, lm_line, Collinear_DEF, âˆ‰, CollinearSymmetry; Â¬(B,D same_side l) [Bsim_lD] by CintDAB, lm_line, InteriorOpposite, -, SameSideSymmetric; cases; suppose Â¬(A,C same_side m); qed by lm_line, H1, Bsim_lD, -, DoubleNotSimImpliesDiagonalsIntersect; suppose A,C same_side m; C,A same_side m [Csim_mA] by lm_line, -, tetra', SameSideSymmetric; C,B same_side d âˆ§ C,D same_side a by ad_line, CintDAB, InteriorUse; C âˆˆ int_angle A B D âˆ§ C âˆˆ int_angle B D A by tetra', ad_line, lm_line, Csim_mA, -, IN_InteriorAngle; C âˆˆ int_triangle D A B by CintDAB, -, IN_InteriorTriangle; qed by -; end; `;; let InteriorTriangleSymmetry = thm `; âˆ€ A B C P. P âˆˆ int_triangle A B C â‡’ P âˆˆ int_triangle B C A by IN_InteriorTriangle; `;; let FourChoicesTetralateral = thm `; let A B C D be point; let a be point_set; assume Tetralateral A B C D [H1]; assume Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line]; assume C,D same_side a [Csim_aD]; thus ConvexQuadrilateral A B C D âˆ¨ ConvexQuadrilateral A B D C âˆ¨ D âˆˆ int_triangle A B C âˆ¨ C âˆˆ int_triangle D A B proof Â¬(A = B) âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear D A B âˆ§ Tetralateral A B D C [TetraABCD] by H1, Tetralateral_DEF, TetralateralSymmetry; Â¬Collinear C A D âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a [notCDa] by TetraABCD, CollinearSymmetry, a_line, Collinear_DEF, âˆ‰; C âˆˆ int_angle D A B âˆ¨ D âˆˆ int_angle C A B by TetraABCD, a_line, -, Csim_aD, AngleOrdering; cases by -; suppose C âˆˆ int_angle D A B; ConvexQuadrilateral A B C D âˆ¨ C âˆˆ int_triangle D A B by H1, -, FourChoicesTetralateralHelp; qed by -; suppose D âˆˆ int_angle C A B; ConvexQuadrilateral A B D C âˆ¨ D âˆˆ int_triangle C A B by TetraABCD, -, FourChoicesTetralateralHelp; qed by -, InteriorTriangleSymmetry; end; `;; let QuadrilateralSymmetry = thm `; âˆ€ A B C D:point. Quadrilateral A B C D â‡’ Quadrilateral B C D A âˆ§ Quadrilateral C D A B âˆ§ Quadrilateral D A B C by Quadrilateral_DEF, INTER_COMM, TetralateralSymmetry, Quadrilateral_DEF; `;; let FiveChoicesQuadrilateral = thm `; let A B C D be point; let l m be point_set; assume Quadrilateral A B C D [H1]; assume Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l âˆ§ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [lm_line]; thus (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 Tetralateral A B C D [H1Tetra] by H1, Quadrilateral_DEF; Â¬(A = B) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(C = D) [Distinct] by H1Tetra, Tetralateral_DEF; consider a c such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a âˆ§ Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c [ac_line] by Distinct, I1; Quadrilateral C D A B âˆ§ Tetralateral C D A B [tetraCDAB] by H1, QuadrilateralSymmetry, Quadrilateral_DEF; Â¬ConvexQuadrilateral A B D C âˆ§ Â¬ConvexQuadrilateral C D B A [notconvquad] by 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 by H1, ac_line, SegmentSameSideOppositeLine; cases by -; suppose C,D same_side a; qed by H1Tetra, ac_line, -, notconvquad, FourChoicesTetralateral; suppose A,B same_side c; ConvexQuadrilateral C D A B âˆ¨ B âˆˆ int_triangle C D A âˆ¨ A âˆˆ int_triangle B C D [X1] by tetraCDAB, ac_line, -, notconvquad, FourChoicesTetralateral; qed by -, QuadrilateralSymmetry, ConvexQuad_DEF; end; Â¬(B,D same_side l) âˆ¨ Â¬(A,C same_side m) by -, lm_line, ConvexQuadImpliesDiagonalsIntersect, IN_InteriorTriangle, InteriorAngleSymmetry, InteriorOpposite; qed by 5choices, -; `;; let IntervalSymmetry = thm `; âˆ€ A B: point. open (A,B) = open (B,A) by B1', EXTENSION; `;; let SegmentSymmetry = thm `; âˆ€ A B: point. seg A B = seg B A by Segment_DEF, IntervalSymmetry, SET_RULE; `;; let C1OppositeRay = thm `; let O P be point; let s be point_set; assume Segment s âˆ§ Â¬(O = P) [H1]; thus âˆƒ Q. P âˆˆ open (O,Q) âˆ§ seg P Q â‰¡ s proof consider Z such that P âˆˆ open (O,Z) âˆ§ Â¬(P = Z) [OPZ] by H1, B2', B1'; consider Q such that Q âˆˆ ray P Z â” P âˆ§ seg P Q â‰¡ s [PQeq] by H1, -, C1; P âˆˆ open (Q,O) by OPZ, -, OppositeRaysIntersect1pointHelp; qed by -, B1', PQeq; `;; let OrderedCongruentSegments = thm `; let A B C D F be point; assume Â¬(A = C) âˆ§ Â¬(D = F) [H1]; assume seg A C â‰¡ seg D F [H2]; assume B âˆˆ open (A,C) [H3]; thus âˆƒ E. E âˆˆ open (D,F) âˆ§ seg A B â‰¡ seg D E proof Segment (seg A B) âˆ§ Segment (seg A C) âˆ§ Segment (seg B C) âˆ§ Segment (seg D F) [segs] by H3, B1', H1, SEGMENT; seg D F â‰¡ seg A C [DFeqAC] by -, H2, C2Symmetric; consider E such that E âˆˆ ray D F â” D âˆ§ seg D E â‰¡ seg A B [DEeqAB] by segs, H1, C1; Â¬(E = D) âˆ§ Collinear D E F âˆ§ D âˆ‰ open (F,E) [ErDF] by -, IN_DELETE, IN_Ray, B1', CollinearSymmetry, âˆ‰; consider F' such that E âˆˆ open (D,F') âˆ§ seg E F' â‰¡ seg B C [DEF'] by segs, -, C1OppositeRay; seg D F' â‰¡ seg A C [DF'eqAC] by DEF', H3, DEeqAB, C3; Segment (seg D F') âˆ§ Segment (seg D E) by DEF', B1', SEGMENT; seg A C â‰¡ seg D F' âˆ§ seg A B â‰¡ seg D E [ABeqDE] by segs, -, DF'eqAC, C2Symmetric, DEeqAB; F' âˆˆ ray D E â” D âˆ§ F âˆˆ ray D E â” D by DEF', IntervalRayEZ, ErDF, IN_Ray, H1, IN_DELETE; F' = F by ErDF, segs, -, DF'eqAC, DFeqAC, C1; qed by -, DEF', ABeqDE; `;; let SegmentSubtraction = thm `; let A B C A' B' C' be point; assume B âˆˆ open (A,C) âˆ§ B' âˆˆ open (A',C') [H1]; assume seg A B â‰¡ seg A' B' [H2]; assume seg A C â‰¡ seg A' C' [H3]; thus seg B C â‰¡ seg B' C' proof Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Collinear A B C âˆ§ Segment (seg A' C') âˆ§ Segment (seg B' C') [Distinct] by H1, B1', SEGMENT; consider Q such that B âˆˆ open (A,Q) âˆ§ seg B Q â‰¡ seg B' C' [defQ] by -, C1OppositeRay; seg A Q â‰¡ seg A' C' [AQ_A'C'] by H1, H2, -, C3; Â¬(A = Q) âˆ§ Collinear A B Q âˆ§ A âˆ‰ open (C,B) âˆ§ A âˆ‰ open (Q,B) by defQ, B1', H1, B3', âˆ‰; C âˆˆ ray A B â” A âˆ§ Q âˆˆ ray A B â” A by Distinct, -, IN_Ray, IN_DELETE; C = Q by Distinct, -, AQ_A'C', H3, C1; qed by defQ, -; `;; let SegmentOrderingUse = thm `; let A B be point; let s be point_set; assume Segment s âˆ§ Â¬(A = B) [H1]; assume s <__ seg A B [H2]; thus âˆƒ G. G âˆˆ open (A,B) âˆ§ s â‰¡ seg A G proof consider A' B' G' such that seg A B = seg A' B' âˆ§ G' âˆˆ open (A',B') âˆ§ s â‰¡ seg A' G' [H2'] by H2, SegmentOrdering_DEF; Â¬(A' = G') âˆ§ Â¬(A' = B') âˆ§ seg A' B' â‰¡ seg A B [A'notB'G'] by -, B1', H1, SEGMENT, C2Reflexive; consider G such that G âˆˆ open (A,B) âˆ§ seg A' G' â‰¡ seg A G [AGB] by A'notB'G', H1, H2', -, OrderedCongruentSegments; s â‰¡ seg A G by H1, A'notB'G', -, B1', SEGMENT, H2', C2Transitive; qed by AGB, -; `;; let SegmentTrichotomy1 = thm `; let s t be point_set; assume s <__ t [H1]; thus Â¬(s â‰¡ t) proof consider A B G such that Segment s âˆ§ t = seg A B âˆ§ G âˆˆ open (A,B) âˆ§ s â‰¡ seg A G [H1'] by H1, SegmentOrdering_DEF; Â¬(A = G) âˆ§ Â¬(A = B) âˆ§ Â¬(G = B) [Distinct] by H1', B1'; seg A B â‰¡ seg A B [ABrefl] by -, SEGMENT, C2Reflexive; G âˆˆ ray A B â” A âˆ§ B âˆˆ ray A B â” A by H1', IntervalRay, EndpointInRay, Distinct, IN_DELETE; Â¬(seg A G â‰¡ seg A B) âˆ§ seg A G â‰¡ s by Distinct, SEGMENT, -, ABrefl, C1, H1', C2Symmetric; qed by Distinct, H1', SEGMENT, -, C2Transitive; `;; let SegmentTrichotomy2 = thm `; let s t u be point_set; assume s <__ t [H1]; assume Segment u âˆ§ t â‰¡ u [H2]; thus s <__ u proof consider A B P such that Segment s âˆ§ t = seg A B âˆ§ P âˆˆ open (A,B) âˆ§ s â‰¡ seg A P [H1'] by H1, SegmentOrdering_DEF; Â¬(A = B) âˆ§ Â¬(A = P) [Distinct] by -, B1'; consider X Y such that u = seg X Y âˆ§ Â¬(X = Y) [uXY] by H2, SEGMENT; consider Q such that Q âˆˆ open (X,Y) âˆ§ seg A P â‰¡ seg X Q [XQY] by Distinct, -, H1', H2, OrderedCongruentSegments; Â¬(X = Q) âˆ§ s â‰¡ seg X Q by -, B1', H1', Distinct, SEGMENT, XQY, C2Transitive; qed by H1', uXY, XQY, -, SegmentOrdering_DEF; `;; let SegmentOrderTransitivity = thm `; let s t u be point_set; assume s <__ t âˆ§ t <__ u [H1]; thus s <__ u proof consider A B G such that u = seg A B âˆ§ G âˆˆ open (A,B) âˆ§ t â‰¡ seg A G [H1'] by H1, SegmentOrdering_DEF; Â¬(A = B) âˆ§ Â¬(A = G) âˆ§ Segment s [Distinct] by H1', B1', H1, SegmentOrdering_DEF; s <__ seg A G by H1, H1', Distinct, SEGMENT, SegmentTrichotomy2; consider F such that F âˆˆ open (A,G) âˆ§ s â‰¡ seg A F [AFG] by Distinct, -, SegmentOrderingUse; F âˆˆ open (A,B) by H1', IntervalsAreConvex, -, SUBSET; qed by Distinct, H1', -, AFG, SegmentOrdering_DEF; `;; let SegmentTrichotomy = thm `; let s t be point_set; assume Segment s âˆ§ Segment t [H1]; thus (s â‰¡ t âˆ¨ s <__ t âˆ¨ t <__ s) âˆ§ Â¬(s â‰¡ t âˆ§ s <__ t) âˆ§ Â¬(s â‰¡ t âˆ§ t <__ s) âˆ§ Â¬(s <__ t âˆ§ t <__ s) proof Â¬(s â‰¡ t âˆ§ s <__ t) [Not12] proof assume s <__ t; qed by -, SegmentTrichotomy1; Â¬(s â‰¡ t âˆ§ t <__ s) [Not13] proof assume t <__ s; Â¬(t â‰¡ s) by -, SegmentTrichotomy1; qed by H1, -, C2Symmetric; Â¬(s <__ t âˆ§ t <__ s) [Not23] proof assume s <__ t âˆ§ t <__ s; s <__ s by H1, -, SegmentOrderTransitivity; qed by -, SegmentTrichotomy1, H1, C2Reflexive; consider O P such that s = seg O P âˆ§ Â¬(O = P) [sOP] by H1, SEGMENT; consider Q such that Q âˆˆ ray O P â” O âˆ§ seg O Q â‰¡ t [QrOP] by H1, -, C1; O âˆ‰ open (Q,P) âˆ§ Collinear O P Q âˆ§ Â¬(O = Q) [notQOP] by -, IN_DELETE, IN_Ray; s â‰¡ seg O P âˆ§ t â‰¡ seg O Q âˆ§ seg O Q â‰¡ t âˆ§ seg O P â‰¡ s [stOPQ] by H1, sOP, -, SEGMENT, QrOP, C2Reflexive, C2Symmetric; cases; suppose Q = P; s â‰¡ t by -, sOP, QrOP; qed by -, Not12, Not13, Not23; suppose Â¬(Q = P); P âˆˆ open (O,Q) âˆ¨ Q âˆˆ open (O,P) by sOP, -, notQOP, B3', B1', âˆ‰; s <__ seg O Q âˆ¨ t <__ seg O P by H1, -, stOPQ, SegmentOrdering_DEF; s <__ t âˆ¨ t <__ s by -, H1, stOPQ, SegmentTrichotomy2; qed by -, Not12, Not13, Not23; end; `;; let C4Uniqueness = thm `; let O A B P be point; let l be point_set; assume Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ Â¬(O = A) [H1]; assume B âˆ‰ l âˆ§ P âˆ‰ l âˆ§ P,B same_side l [H2]; assume âˆ¡ A O P â‰¡ âˆ¡ A O B [H3]; thus ray O B = ray O P proof Â¬(O = B) âˆ§ Â¬(O = P) âˆ§ Ray (ray O B) âˆ§ Ray (ray O P) [Distinct] by H2, H1, âˆ‰, RAY; Â¬Collinear A O B âˆ§ B,B same_side l [Bsim_lB] by H1, H2, I1, Collinear_DEF, âˆ‰, SameSideReflexive; Angle (âˆ¡ A O B) âˆ§ âˆ¡ A O B â‰¡ âˆ¡ A O B by -, ANGLE, C5Reflexive; qed by -, H1, H2, Distinct, Bsim_lB, H3, C4; `;; let AngleSymmetry = thm `; âˆ€ A O B. âˆ¡ A O B = âˆ¡ B O A by Angle_DEF, UNION_COMM; `;; let TriangleCongSymmetry = thm `; let A B C A' B' C' be point; assume A,B,C â‰… A',B',C' [H1]; thus 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 Â¬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 H1, TriangleCong_DEF; seg B A â‰¡ seg B' A' âˆ§ seg C A â‰¡ seg C' A' âˆ§ seg C B â‰¡ seg C' B' [segments] by H1', SegmentSymmetry; âˆ¡ C B A â‰¡ âˆ¡ C' B' A' âˆ§ âˆ¡ A C B â‰¡ âˆ¡ A' C' B' âˆ§ âˆ¡ B A C â‰¡ âˆ¡ B' A' C' by H1', AngleSymmetry; qed by CollinearSymmetry, H1', segments, -, TriangleCong_DEF; `;; let SAS = thm `; let A B C A' B' C' be point; assume Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' [H1]; assume seg B A â‰¡ seg B' A' âˆ§ seg B C â‰¡ seg B' C' [H2]; assume âˆ¡ A B C â‰¡ âˆ¡ A' B' C' [H3]; thus A,B,C â‰… A',B',C' proof Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(A' = C') [Distinct] by H1, NonCollinearImpliesDistinct; :: 134 consider c such that Line c âˆ§ A âˆˆ c âˆ§ B âˆˆ c [c_line] by Distinct, I1; C âˆ‰ c [notCc] by H1, c_line, Collinear_DEF, âˆ‰; âˆ¡ B C A â‰¡ âˆ¡ B' C' A' [BCAeq] by H1, H2, H3, C6; âˆ¡ B A C â‰¡ âˆ¡ B' A' C' [BACeq] by H1, CollinearSymmetry, H2, H3, AngleSymmetry, C6; consider Y such that Y âˆˆ ray A C â” A âˆ§ seg A Y â‰¡ seg A' C' [YrAC] by Distinct, SEGMENT, C1; Y âˆ‰ c âˆ§ Y,C same_side c [Ysim_cC] by c_line, notCc, -, RaySameSide; Â¬Collinear Y A B [YABncol] by c_line, -, Distinct, I1, Collinear_DEF, âˆ‰; ray A Y = ray A C âˆ§ âˆ¡ Y A B = âˆ¡ C A B by Distinct, YrAC, RayWellDefined, Angle_DEF; âˆ¡ Y A B â‰¡ âˆ¡ C' A' B' by BACeq, -, AngleSymmetry; âˆ¡ A B Y â‰¡ âˆ¡ A' B' C' [ABYeq] by YABncol, H1, CollinearSymmetry, H2, SegmentSymmetry, YrAC, -, C6; Angle (âˆ¡ A B C) âˆ§ Angle (âˆ¡ A' B' C') âˆ§ Angle (âˆ¡ A B Y) by H1, CollinearSymmetry, YABncol, ANGLE; âˆ¡ A B Y â‰¡ âˆ¡ A B C [ABYeqABC] by -, ABYeq, -, H3, C5Symmetric, C5Transitive; ray B C = ray B Y âˆ§ Â¬(Y = B) âˆ§ Y âˆˆ ray B C by c_line, Distinct, notCc, Ysim_cC, ABYeqABC, C4Uniqueness, âˆ‰, -, EndpointInRay; Collinear B C Y âˆ§ Collinear A C Y by -, YrAC, IN_DELETE, IN_Ray; C = Y by -, I1, Collinear_DEF, H1; seg A C â‰¡ seg A' C' by -, YrAC; qed by H1, H2, SegmentSymmetry, -, H3, BCAeq, BACeq, AngleSymmetry, TriangleCong_DEF; `;; let ASA = thm `; let A B C A' B' C' be point; assume Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' [H1]; assume seg A C â‰¡ seg A' C' [H2]; assume âˆ¡ C A B â‰¡ âˆ¡ C' A' B' âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B' C' A' [H3]; thus A,B,C â‰… A',B',C' proof Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬(A' = B') âˆ§ Â¬(A' = C') âˆ§ Â¬(B' = C') âˆ§ Segment (seg C' B') [Distinct] by H1, NonCollinearImpliesDistinct, SEGMENT; consider D such that D âˆˆ ray C B â” C âˆ§ seg C D â‰¡ seg C' B' âˆ§ Â¬(D = C) [DrCB] by -, C1, IN_DELETE; Collinear C B D [CBDcol] by -, IN_DELETE, IN_Ray; Â¬Collinear D C A âˆ§ Angle (âˆ¡ C A D) âˆ§ Angle (âˆ¡ C' A' B') âˆ§ Angle (âˆ¡ C A B) [DCAncol] by H1, CollinearSymmetry, -, DrCB, NoncollinearityExtendsToLine, H1, ANGLE; consider b such that Line b âˆ§ A âˆˆ b âˆ§ C âˆˆ b [b_line] by Distinct, I1; B âˆ‰ b âˆ§ Â¬(D = A) [notBb] by H1, -, Collinear_DEF, âˆ‰, DCAncol, NonCollinearImpliesDistinct; D âˆ‰ b âˆ§ D,B same_side b [Dsim_bB] by b_line, -, DrCB, RaySameSide; ray C D = ray C B by Distinct, DrCB, RayWellDefined; âˆ¡ D C A â‰¡ âˆ¡ B' C' A' by H3, -, Angle_DEF; D,C,A â‰… B',C',A' by DCAncol, H1, CollinearSymmetry, DrCB, H2, SegmentSymmetry, -, SAS; âˆ¡ C A D â‰¡ âˆ¡ C' A' B' by -, TriangleCong_DEF; âˆ¡ C A D â‰¡ âˆ¡ C A B by DCAncol, -, H3, C5Symmetric, C5Transitive; ray A B = ray A D âˆ§ D âˆˆ ray A B by b_line, Distinct, notBb, Dsim_bB, -, C4Uniqueness, notBb, EndpointInRay; Collinear A B D by -, IN_Ray; D = B by I1, -, Collinear_DEF, CBDcol, H1; seg C B â‰¡ seg C' B' by -, DrCB; B,C,A â‰… B',C',A' by H1, CollinearSymmetry, -, H2, SegmentSymmetry, H3, SAS; qed by -, TriangleCongSymmetry; `;; let AngleSubtraction = thm `; let A O B A' O' B' G G' be point; assume G âˆˆ int_angle A O B âˆ§ G' âˆˆ int_angle A' O' B' [H1]; assume âˆ¡ A O B â‰¡ âˆ¡ A' O' B' âˆ§ âˆ¡ A O G â‰¡ âˆ¡ A' O' G' [H2]; thus âˆ¡ G O B â‰¡ âˆ¡ G' O' B' proof Â¬Collinear A O B âˆ§ Â¬Collinear A' O' B' [A'O'B'ncol] by H1, IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬(G = O) âˆ§ Â¬(G' = O') âˆ§ Segment (seg O' A') âˆ§ Segment (seg O' B') [Distinct] by -, 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 -, C1; G âˆˆ int_angle X O Y [GintXOY] by 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 -, H1, Crossbar_THM; H âˆˆ int_angle X O Y âˆ§ H' âˆˆ int_angle A' O' B' [HintXOY] by 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 Distinct, XYexists, Hexists, RayWellDefined; âˆ¡ X O Y â‰¡ âˆ¡ A' O' B' âˆ§ âˆ¡ X O H â‰¡ âˆ¡ A' O' H' [H2'] by H2, -, Angle_DEF; Â¬Collinear X O Y by GintXOY, IN_InteriorAngle; X,O,Y â‰… A',O',B' by -, 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 -, TriangleCong_DEF; Â¬Collinear O H X âˆ§ Â¬Collinear O' H' A' âˆ§ Â¬Collinear O Y H âˆ§ Â¬Collinear O' B' H' [OHXncol] by 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 Hexists, B1', IntervalRay; âˆ¡ H X O â‰¡ âˆ¡ H' A' O' by XOYcong, -, Angle_DEF; O,H,X â‰… O',H',A' by OHXncol, XYexists, -, H2', ASA; seg X H â‰¡ seg A' H' by -, TriangleCong_DEF, SegmentSymmetry; seg H Y â‰¡ seg H' B' by Hexists, XOYcong, -, SegmentSubtraction; seg Y O â‰¡ seg B' O' âˆ§ seg Y H â‰¡ seg B' H' [YHeq] by XYexists, -, SegmentSymmetry; âˆ¡ O Y H â‰¡ âˆ¡ O' B' H' by XOYcong, Hrays, Angle_DEF; O,Y,H â‰… O',B',H' by OHXncol, YHeq, -, SAS; âˆ¡ H O Y â‰¡ âˆ¡ H' O' B' by -, TriangleCong_DEF; qed by -, Orays, Angle_DEF; `;; let OrderedCongruentAngles = thm `; let A O B A' O' B' G be point; assume Â¬Collinear A' O' B' [H1]; assume âˆ¡ A O B â‰¡ âˆ¡ A' O' B' [H2]; assume G âˆˆ int_angle A O B [H3]; thus âˆƒ G'. G' âˆˆ int_angle A' O' B' âˆ§ âˆ¡ A O G â‰¡ âˆ¡ A' O' G' proof Â¬Collinear A O B [AOBncol] by H3, IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬(A' = B') âˆ§ Â¬(O = G) âˆ§ Segment (seg O' A') âˆ§ Segment (seg O' B') [Distinct] by 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 -, C1; G âˆˆ int_angle X O Y [GintXOY] by H3, -, InteriorWellDefined, InteriorAngleSymmetry; Â¬Collinear X O Y âˆ§ Â¬(X = Y) [XOYncol] by -, IN_InteriorAngle, NonCollinearImpliesDistinct; consider H such that H âˆˆ open (X,Y) âˆ§ H âˆˆ ray O G â” O [defH] by GintXOY, Crossbar_THM; ray O X = ray O A âˆ§ ray O Y = ray O B âˆ§ ray O H = ray O G [Orays] by Distinct, defXY, -, RayWellDefined; âˆ¡ X O Y â‰¡ âˆ¡ A' O' B' by H2, -, Angle_DEF; X,O,Y â‰… A',O',B' by XOYncol, H1, defXY, -, SAS; seg X Y â‰¡ seg A' B' âˆ§ âˆ¡ O X Y â‰¡ âˆ¡ O' A' B' [YXOcong] by -, TriangleCong_DEF, AngleSymmetry; consider G' such that G' âˆˆ open (A',B') âˆ§ seg X H â‰¡ seg A' G' [A'G'B'] by XOYncol, Distinct, -, defH, OrderedCongruentSegments; G' âˆˆ int_angle A' O' B' [G'intA'O'B'] by H1, -, ConverseCrossbar; ray X H = ray X Y âˆ§ ray A' G' = ray A' B' by defH, A'G'B', IntervalRay; âˆ¡ O X H â‰¡ âˆ¡ O' A' G' [HXOeq] by -, Angle_DEF, YXOcong; H âˆˆ int_angle X O Y by GintXOY, defH, WholeRayInterior; Â¬Collinear O X H âˆ§ Â¬Collinear O' A' G' by -, G'intA'O'B', InteriorEZHelp, CollinearSymmetry; O,X,H â‰… O',A',G' by -, A'G'B', defXY, SegmentSymmetry, HXOeq, SAS; âˆ¡ X O H â‰¡ âˆ¡ A' O' G' by -, TriangleCong_DEF, AngleSymmetry; âˆ¡ A O G â‰¡ âˆ¡ A' O' G' by -, Orays, Angle_DEF; qed by G'intA'O'B', -; `;; let AngleAddition = thm `; let A O B A' O' B' G G' be point; assume G âˆˆ int_angle A O B âˆ§ G' âˆˆ int_angle A' O' B' [H1]; assume âˆ¡ A O G â‰¡ âˆ¡ A' O' G' âˆ§ âˆ¡ G O B â‰¡ âˆ¡ G' O' B' [H2]; thus âˆ¡ A O B â‰¡ âˆ¡ A' O' B' proof Â¬Collinear A O B âˆ§ Â¬Collinear A' O' B' [AOBncol] by H1, IN_InteriorAngle; Â¬(A = O) âˆ§ Â¬(A = B) âˆ§ Â¬(O = B) âˆ§ Â¬(A' = O') âˆ§ Â¬(A' = B') âˆ§ Â¬(O' = B') âˆ§ Â¬(G = O) [Distinct] by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp; consider a b such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a âˆ§ Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [a_line] by Distinct, I1; consider g such that Line g âˆ§ O âˆˆ g âˆ§ G âˆˆ g [g_line] by Distinct, I1; G âˆ‰ a âˆ§ G,B same_side a [H1'] by a_line, H1, InteriorUse; Â¬Collinear A O G âˆ§ Â¬Collinear A' O' G' [AOGncol] by H1, InteriorEZHelp, IN_InteriorAngle; Angle (âˆ¡ A O B) âˆ§ Angle (âˆ¡ A' O' B') âˆ§ Angle (âˆ¡ A O G) âˆ§ Angle (âˆ¡ A' O' G') [angles] by 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 -, Distinct, a_line, H1', C4; consider X such that X âˆ‰ a âˆ§ X,G same_side a âˆ§ âˆ¡ A O X â‰¡ âˆ¡ A' O' B' [Xexists] by -; Â¬Collinear A O X [AOXncol] by -, a_line, Distinct, I1, Collinear_DEF, âˆ‰; âˆ¡ A' O' B' â‰¡ âˆ¡ A O X by -, AOBncol, ANGLE, Xexists, C5Symmetric; consider Y such that Y âˆˆ int_angle A O X âˆ§ âˆ¡ A' O' G' â‰¡ âˆ¡ A O Y [YintAOX] by AOXncol, -, H1, OrderedCongruentAngles; Â¬Collinear A O Y by -, InteriorEZHelp; âˆ¡ A O Y â‰¡ âˆ¡ A O G [AOGeq] by -, angles, -, ANGLE, YintAOX, H2, C5Transitive, C5Symmetric; consider x such that Line x âˆ§ O âˆˆ x âˆ§ X âˆˆ x by Distinct, I1; Y âˆ‰ a âˆ§ Y,X same_side a by a_line, -, YintAOX, InteriorUse; Y âˆ‰ a âˆ§ Y,G same_side a by a_line, -, Xexists, H1', SameSideTransitive; ray O G = ray O Y by a_line, Distinct, H1', -, AOGeq, C4Uniqueness; G âˆˆ ray O Y â” O by Distinct, -, EndpointInRay, IN_DELETE; G âˆˆ int_angle A O X [GintAOX] by YintAOX, -, WholeRayInterior; âˆ¡ G O X â‰¡ âˆ¡ G' O' B' [GOXeq] by -, H1, Xexists, H2, AngleSubtraction; Â¬Collinear G O X âˆ§ Â¬Collinear G O B âˆ§ Â¬Collinear G' O' B' [GOXncol] by GintAOX, H1, InteriorAngleSymmetry, InteriorEZHelp, CollinearSymmetry; Angle (âˆ¡ G O X) âˆ§ Angle (âˆ¡ G O B) âˆ§ Angle (âˆ¡ G' O' B') by -, ANGLE; âˆ¡ G O X â‰¡ âˆ¡ G O B [G'O'Xeq] by angles, -, GOXeq, C5Symmetric, H2, C5Transitive; Â¬(A,X same_side g) âˆ§ Â¬(A,B same_side g) [Ansim_aXB] by g_line, GintAOX, H1, InteriorOpposite; A âˆ‰ g âˆ§ B âˆ‰ g âˆ§ X âˆ‰ g [notABXg] by g_line, AOGncol, GOXncol, Distinct, I1, Collinear_DEF, âˆ‰; X,B same_side g by g_line, -, Ansim_aXB, AtMost2Sides; ray O X = ray O B by g_line, Distinct, notABXg, -, G'O'Xeq, C4Uniqueness; qed by -, Xexists, Angle_DEF; `;; let AngleOrderingUse = thm `; let A O B be point; let Î± be point_set; assume Angle Î± âˆ§ Â¬Collinear A O B [H1]; assume Î± <_ang âˆ¡ A O B [H3]; thus âˆƒ G. G âˆˆ int_angle A O B âˆ§ Î± â‰¡ âˆ¡ A O G proof 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 H3, AngleOrdering_DEF; Angle (âˆ¡ A O B) âˆ§ Angle (âˆ¡ A' O' B') âˆ§ Angle (âˆ¡ A' O' G') [angles] by H1, -, ANGLE, InteriorEZHelp; âˆ¡ A' O' B' â‰¡ âˆ¡ A O B by -, H3', C5Reflexive; consider G such that G âˆˆ int_angle A O B âˆ§ âˆ¡ A' O' G' â‰¡ âˆ¡ A O G [GintAOB] by H1, H3', -, OrderedCongruentAngles; Î± â‰¡ âˆ¡ A O G by H1, angles, -, InteriorEZHelp, ANGLE, H3', GintAOB, C5Transitive; qed by -, GintAOB; `;; let AngleTrichotomy1 = thm `; let Î± Î² be point_set; assume Î± <_ang Î² [H1]; thus Â¬(Î± â‰¡ Î²) proof assume Î± â‰¡ Î² [Con]; 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 H1, AngleOrdering_DEF; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬Collinear A O G [Distinct] by H1', NonCollinearImpliesDistinct, InteriorEZHelp; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by Distinct, I1; consider b such that Line b âˆ§ O âˆˆ b âˆ§ B âˆˆ b [b_line] by Distinct, I1; B âˆ‰ a [notBa] by a_line, H1', Collinear_DEF, âˆ‰; G âˆ‰ a âˆ§ G âˆ‰ b âˆ§ G,B same_side a [GintAOB] by a_line, b_line, H1', InteriorUse; âˆ¡ A O G â‰¡ Î± by H1', Distinct, ANGLE, C5Symmetric; âˆ¡ A O G â‰¡ âˆ¡ A O B by H1', Distinct, ANGLE, -, Con, C5Transitive; ray O B = ray O G by a_line, Distinct, notBa, GintAOB, -, C4Uniqueness; G âˆˆ b by Distinct, -, EndpointInRay, b_line, RayLine, SUBSET; qed by -, GintAOB, âˆ‰; `;; let AngleTrichotomy2 = thm `; let Î± Î² Î³ be point_set; assume Î± <_ang Î² [H1]; assume Angle Î³ [H2]; assume Î² â‰¡ Î³ [H3]; thus Î± <_ang Î³ proof 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 H1, AngleOrdering_DEF; consider A' O' B' such that Î³ = âˆ¡ A' O' B' âˆ§ Â¬Collinear A' O' B' [Î³A'O'B'] by H2, ANGLE; consider G' such that G' âˆˆ int_angle A' O' B' âˆ§ âˆ¡ A O G â‰¡ âˆ¡ A' O' G' [G'intA'O'B'] by Î³A'O'B', H1', H3, OrderedCongruentAngles; Â¬Collinear A O G âˆ§ Â¬Collinear A' O' G' [ncol] by H1', -, InteriorEZHelp; Î± â‰¡ âˆ¡ A' O' G' by H1', ANGLE, -, G'intA'O'B', C5Transitive; qed by H1', -, ncol, Î³A'O'B', G'intA'O'B', -, AngleOrdering_DEF; `;; let AngleOrderTransitivity = thm `; let Î± Î² Î³ be point_set; assume Î± <_ang Î² [H0]; assume Î² <_ang Î³ [H2]; thus Î± <_ang Î³ proof 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 H2, AngleOrdering_DEF; Â¬Collinear A O G [AOGncol] by H2', InteriorEZHelp; Angle Î± âˆ§ Angle (âˆ¡ A O G) âˆ§ Angle Î³ [angles] by H0, AngleOrdering_DEF, H2', -, ANGLE; Î± <_ang âˆ¡ A O G by H0, H2', -, AngleTrichotomy2; consider F such that F âˆˆ int_angle A O G âˆ§ Î± â‰¡ âˆ¡ A O F [FintAOG] by angles, AOGncol, -, AngleOrderingUse; F âˆˆ int_angle A O B by H2', -, InteriorTransitivity; qed by angles, H2', -, FintAOG, AngleOrdering_DEF; `;; let AngleTrichotomy = thm `; let Î± Î² be point_set; assume Angle Î± âˆ§ Angle Î² [H1]; thus (Î± â‰¡ Î² âˆ¨ Î± <_ang Î² âˆ¨ Î² <_ang Î±) âˆ§ Â¬(Î± â‰¡ Î² âˆ§ Î± <_ang Î²) âˆ§ Â¬(Î± â‰¡ Î² âˆ§ Î² <_ang Î±) âˆ§ Â¬(Î± <_ang Î² âˆ§ Î² <_ang Î±) proof Â¬(Î± â‰¡ Î² âˆ§ Î± <_ang Î²) [Not12] by AngleTrichotomy1; Â¬(Î± â‰¡ Î² âˆ§ Î² <_ang Î±) [Not13] by H1, C5Symmetric, AngleTrichotomy1; Â¬(Î± <_ang Î² âˆ§ Î² <_ang Î±) [Not23] by H1, AngleOrderTransitivity, AngleTrichotomy1, C5Reflexive; consider P O A such that Î± = âˆ¡ P O A âˆ§ Â¬Collinear P O A [POA] by H1, ANGLE; Â¬(P = O) âˆ§ Â¬(O = A) [Distinct] by -, NonCollinearImpliesDistinct; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by -, I1; P âˆ‰ a [notPa] by -, 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 H1, Distinct, a_line, -, C4; consider Q such that Â¬(O = Q) âˆ§ Q âˆ‰ a âˆ§ Q,P same_side a âˆ§ âˆ¡ A O Q â‰¡ Î² [Qexists] by -; O âˆ‰ open (Q,P) [notQOP] by a_line, Qexists, SameSide_DEF, âˆ‰; Â¬Collinear A O P [AOPncol] by POA, CollinearSymmetry; Â¬Collinear A O Q [AOQncol] by a_line, Distinct, I1, Collinear_DEF, Qexists, âˆ‰; Angle (âˆ¡ A O P) âˆ§ Angle (âˆ¡ A O Q) by AOPncol, -, ANGLE; Î± â‰¡ âˆ¡ A O P âˆ§ Î² â‰¡ âˆ¡ A O Q âˆ§ âˆ¡ A O P â‰¡ Î± [flip] by H1, -, POA, AngleSymmetry, C5Reflexive, Qexists, C5Symmetric; cases; suppose Collinear Q O P; Collinear O P Q by -, CollinearSymmetry; Q âˆˆ ray O P â” O by Distinct, -, notQOP, IN_Ray, Qexists, IN_DELETE; ray O Q = ray O P by Distinct, -, RayWellDefined; âˆ¡ P O A = âˆ¡ A O Q by -, Angle_DEF, AngleSymmetry; Î± â‰¡ Î² by -, POA, Qexists; qed by -, Not12, Not13, Not23; suppose Â¬Collinear Q O P; P âˆˆ int_angle Q O A âˆ¨ Q âˆˆ int_angle P O A by Distinct, a_line, Qexists, notPa, -, AngleOrdering; P âˆˆ int_angle A O Q âˆ¨ Q âˆˆ int_angle A O P by -, InteriorAngleSymmetry; Î± <_ang âˆ¡ A O Q âˆ¨ Î² <_ang âˆ¡ A O P by H1, AOQncol, AOPncol, -, flip, AngleOrdering_DEF; Î± <_ang Î² âˆ¨ Î² <_ang Î± by H1, -, Qexists, flip, AngleTrichotomy2; qed by -, Not12, Not13, Not23; end; `;; let SupplementExists = thm `; let Î± be point_set; assume Angle Î± [H1]; thus âˆƒ Î±'. Î± suppl Î±' proof consider A O B such that Î± = âˆ¡ A O B âˆ§ Â¬Collinear A O B âˆ§ Â¬(A = O) [def_Î±] by H1, ANGLE, NonCollinearImpliesDistinct; consider A' such that O âˆˆ open (A,A') by -, B2'; âˆ¡ A O B suppl âˆ¡ A' O B [AOBsup] by def_Î±, -, SupplementaryAngles_DEF, AngleSymmetry; qed by -, def_Î±; `;; let SupplementImpliesAngle = thm `; let Î± Î² be point_set; assume Î± suppl Î² [H1]; thus Angle Î± âˆ§ Angle Î² proof consider A O B A' such that Â¬Collinear A O B âˆ§ O âˆˆ open (A,A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î² = âˆ¡ B O A' [H1'] by H1, SupplementaryAngles_DEF; Â¬(O = A') âˆ§ Collinear A O A' [Distinct] by -, NonCollinearImpliesDistinct, B1'; Â¬Collinear B O A' by H1', CollinearSymmetry, -, NoncollinearityExtendsToLine; qed by H1', -, ANGLE; `;; let RightImpliesAngle = thm `; âˆ€ Î±: point_set. Right Î± â‡’ Angle Î± by RightAngle_DEF, SupplementImpliesAngle; `;; let SupplementSymmetry = thm `; let Î± Î² be point_set; assume Î± suppl Î² [H1]; thus Î² suppl Î± proof consider A O B A' such that Â¬Collinear A O B âˆ§ O âˆˆ open (A,A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î² = âˆ¡ B O A' [H1'] by H1, SupplementaryAngles_DEF; Â¬(O = A') âˆ§ Collinear A O A' by -, NonCollinearImpliesDistinct, B1'; Â¬Collinear A' O B [A'OBncol] by H1', CollinearSymmetry, -, NoncollinearityExtendsToLine; O âˆˆ open (A',A) âˆ§ Î² = âˆ¡ A' O B âˆ§ Î± = âˆ¡ B O A by H1', B1', AngleSymmetry; qed by A'OBncol, -, SupplementaryAngles_DEF; `;; let SupplementsCongAnglesCong = thm `; let Î± Î² Î±' Î²' be point_set; assume Î± suppl Î±' âˆ§ Î² suppl Î²' [H1]; assume Î± â‰¡ Î² [H2]; thus Î±' â‰¡ Î²' proof consider A O B A' such that Â¬Collinear A O B âˆ§ O âˆˆ open (A,A') âˆ§ Î± = âˆ¡ A O B âˆ§ Î±' = âˆ¡ B O A' [def_Î±] by H1, SupplementaryAngles_DEF; Â¬(A = O) âˆ§ Â¬(O = B) âˆ§ Â¬(A = A') âˆ§ Â¬(O = A') âˆ§ Collinear A O A' [DistinctÎ±] by -, NonCollinearImpliesDistinct, B1'; Â¬Collinear B A A' âˆ§ Â¬Collinear O A' B [BAA'ncol] by def_Î±, CollinearSymmetry, -, NoncollinearityExtendsToLine; Segment (seg O A) âˆ§ Segment (seg O B) âˆ§ Segment (seg O A') [Osegments] by 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 H1, SupplementaryAngles_DEF; Â¬(C = P) âˆ§ Â¬(P = D) âˆ§ Â¬(P = C') [DistinctÎ²] by def_Î², NonCollinearImpliesDistinct, B1'; consider X such that X âˆˆ ray P C â” P âˆ§ seg P X â‰¡ seg O A [defX] by Osegments, DistinctÎ², C1; consider Y such that Y âˆˆ ray P D â” P âˆ§ seg P Y â‰¡ seg O B âˆ§ Â¬(Y = P) [defY] by Osegments, DistinctÎ², C1, IN_DELETE; consider X' such that X' âˆˆ ray P C' â” P âˆ§ seg P X' â‰¡ seg O A' [defX'] by Osegments, DistinctÎ², C1; P âˆˆ open (X',C) âˆ§ P âˆˆ open (X,X') [XPX'] by 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 defX, defX', IN_DELETE, -, B1', def_Î±, IntervalRay; Collinear P D Y âˆ§ Collinear P C X by defY, defX, IN_DELETE, IN_Ray; Â¬Collinear C P Y âˆ§ Â¬Collinear X P Y [XPYncol] by def_Î², -, defY, NoncollinearityExtendsToLine, CollinearSymmetry, XPX'line; Â¬Collinear Y X X' âˆ§ Â¬Collinear P X' Y [YXX'ncol] by -, 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 DistinctÎ², defX, defY, defX', RayWellDefined; Î² = âˆ¡ X P Y âˆ§ Î²' = âˆ¡ Y P X' âˆ§ âˆ¡ A O B â‰¡ âˆ¡ X P Y [AOBeqXPY] by 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 Osegments, XPX'line, SEGMENT, defX, defY, defX', C2Symmetric, SegmentSymmetry; seg A A' â‰¡ seg X X' [AA'eq] by def_Î±, XPX'line, XPX', -, SegmentSymmetry, C3; A,O,B â‰… X,P,Y by def_Î±, XPYncol, OAeq, AOBeqXPY, SAS; seg A B â‰¡ seg X Y âˆ§ âˆ¡ B A O â‰¡ âˆ¡ Y X P [AOBâ‰…] by -, TriangleCong_DEF, AngleSymmetry; ray A O = ray A A' âˆ§ ray X P = ray X X' âˆ§ âˆ¡ B A A' â‰¡ âˆ¡ Y X X' by def_Î±, XPX', IntervalRay, -, Angle_DEF; B,A,A' â‰… Y,X,X' by BAA'ncol, YXX'ncol, AOBâ‰…, -, AA'eq, -, SAS; seg A' B â‰¡ seg X' Y âˆ§ âˆ¡ A A' B â‰¡ âˆ¡ X X' Y by -, TriangleCong_DEF, SegmentSymmetry; O,A',B â‰… P,X',Y by BAA'ncol, YXX'ncol, OAeq, -, XPX'line, Angle_DEF, SAS; âˆ¡ B O A' â‰¡ âˆ¡ Y P X' by -, TriangleCong_DEF; qed by -, equalPrays, def_Î², Angle_DEF, def_Î±; `;; let SupplementUnique = thm `; âˆ€ Î± Î² Î²': point_set. Î± suppl Î² âˆ§ Î± suppl Î²' â‡’ Î² â‰¡ Î²' by SupplementaryAngles_DEF, ANGLE, C5Reflexive, SupplementsCongAnglesCong; `;; let CongRightImpliesRight = thm `; let Î± Î² be point_set; assume Angle Î± âˆ§ Right Î² [H1]; assume Î± â‰¡ Î² [H2]; thus Right Î± proof consider Î±' Î²' such that Î± suppl Î±' âˆ§ Î² suppl Î²' âˆ§ Î² â‰¡ Î²' [suppl] by H1, SupplementExists, H1, RightAngle_DEF; Î±' â‰¡ Î²' [Î±'eqÎ²'] by suppl, H2, SupplementsCongAnglesCong; Angle Î² âˆ§ Angle Î±' âˆ§ Angle Î²' by suppl, SupplementImpliesAngle; Î± â‰¡ Î±' by H1, -, H2, suppl, Î±'eqÎ²', C5Symmetric, C5Transitive; qed by suppl, -, RightAngle_DEF; `;; let RightAnglesCongruentHelp = thm `; let A O B A' P be point; let a be point_set; assume Â¬Collinear A O B âˆ§ O âˆˆ open (A,A') [H1]; assume Right (âˆ¡ A O B) âˆ§ Right (âˆ¡ A O P) [H2]; thus P âˆ‰ int_angle A O B proof assume Â¬(P âˆ‰ int_angle A O B); P âˆˆ int_angle A O B [PintAOB] by -, âˆ‰; B âˆˆ int_angle P O A' âˆ§ B âˆˆ int_angle A' O P [BintA'OP] by H1, -, InteriorReflectionInterior, InteriorAngleSymmetry ; Â¬Collinear A O P âˆ§ Â¬Collinear P O A' [AOPncol] by PintAOB, InteriorEZHelp, -, IN_InteriorAngle; âˆ¡ A O B suppl âˆ¡ B O A' âˆ§ âˆ¡ A O P suppl âˆ¡ P O A' [AOBsup] by H1, -, SupplementaryAngles_DEF; consider Î±' Î²' such that âˆ¡ A O B suppl Î±' âˆ§ âˆ¡ A O B â‰¡ Î±' âˆ§ âˆ¡ A O P suppl Î²' âˆ§ âˆ¡ A O P â‰¡ Î²' [supplÎ±'] by H2, RightAngle_DEF; Î±' â‰¡ âˆ¡ B O A' âˆ§ Î²' â‰¡ âˆ¡ P O A' [Î±'eqA'OB] by -, AOBsup, SupplementUnique; Angle (âˆ¡ A O B) âˆ§ Angle Î±' âˆ§ Angle (âˆ¡ B O A') âˆ§ Angle (âˆ¡ A O P) âˆ§ Angle Î²' âˆ§ Angle (âˆ¡ P O A') [angles] by AOBsup, supplÎ±', SupplementImpliesAngle, AngleSymmetry; âˆ¡ A O B â‰¡ âˆ¡ B O A' âˆ§ âˆ¡ A O P â‰¡ âˆ¡ P O A' [H2'] by -, supplÎ±', Î±'eqA'OB, C5Transitive; âˆ¡ A O P â‰¡ âˆ¡ A O P âˆ§ âˆ¡ B O A' â‰¡ âˆ¡ B O A' [refl] by angles, C5Reflexive; âˆ¡ A O P <_ang âˆ¡ A O B âˆ§ âˆ¡ B O A' <_ang âˆ¡ P O A' [BOA'lessPOA'] by angles, H1, PintAOB, -, AngleOrdering_DEF, AOPncol, CollinearSymmetry, BintA'OP, AngleSymmetry; âˆ¡ A O P <_ang âˆ¡ B O A' by -, angles, H2', AngleTrichotomy2; âˆ¡ A O P <_ang âˆ¡ P O A' by -, BOA'lessPOA', AngleOrderTransitivity; qed by -, H2', AngleTrichotomy1; `;; let RightAnglesCongruent = thm `; let Î± Î² be point_set; assume Right Î± âˆ§ Right Î² [H1]; thus Î± â‰¡ Î² proof consider Î±' such that Î± suppl Î±' âˆ§ Î± â‰¡ Î±' by 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 -, SupplementaryAngles_DEF; Â¬(A = O) âˆ§ Â¬(O = B) [Distinct] by def_Î±, NonCollinearImpliesDistinct, B1'; consider a such that Line a âˆ§ O âˆˆ a âˆ§ A âˆˆ a [a_line] by Distinct, I1; B âˆ‰ a [notBa] by -, def_Î±, Collinear_DEF, âˆ‰; Angle Î² by H1, RightImpliesAngle; âˆƒ! r. Ray r âˆ§ âˆƒ P. Â¬(O = P) âˆ§ r = ray O P âˆ§ P âˆ‰ a âˆ§ P,B same_side a âˆ§ âˆ¡ A O P â‰¡ Î² by -, Distinct, a_line, notBa, C4; consider P such that Â¬(O = P) âˆ§ P âˆ‰ a âˆ§ P,B same_side a âˆ§ âˆ¡ A O P â‰¡ Î² [defP] by -; O âˆ‰ open (P,B) [notPOB] by a_line, -, SameSide_DEF, âˆ‰; Â¬Collinear A O P [AOPncol] by a_line, Distinct, I1, defP, Collinear_DEF, âˆ‰; Right (âˆ¡ A O P) [AOPright] by -, ANGLE, H1, defP, CongRightImpliesRight; P âˆ‰ int_angle A O B âˆ§ B âˆ‰ int_angle A O P by def_Î±, H1, -, AOPncol, AOPright, RightAnglesCongruentHelp; Collinear P O B by Distinct, a_line, defP, notBa, -, AngleOrdering, InteriorAngleSymmetry, âˆ‰; P âˆˆ ray O B â” O by Distinct, -, CollinearSymmetry, notPOB, IN_Ray, defP, IN_DELETE; ray O P = ray O B âˆ§ âˆ¡ A O P = âˆ¡ A O B by Distinct, -, RayWellDefined, Angle_DEF; qed by -, defP, def_Î±; `;; let OppositeRightAnglesLinear = thm `; let A B O H be point; let h be point_set; assume Â¬Collinear A O H âˆ§ Â¬Collinear H O B [H0]; assume Right (âˆ¡ A O H) âˆ§ Right (âˆ¡ H O B) [H1]; assume Line h âˆ§ O âˆˆ h âˆ§ H âˆˆ h âˆ§ Â¬(A,B same_side h) [H2]; thus O âˆˆ open (A,B) proof Â¬(A = O) âˆ§ Â¬(O = H) âˆ§ Â¬(O = B) [Distinct] by H0, NonCollinearImpliesDistinct; A âˆ‰ h âˆ§ B âˆ‰ h [notABh] by H0, H2, Collinear_DEF, âˆ‰; consider E such that O âˆˆ open (A,E) âˆ§ Â¬(E = O) [AOE] by Distinct, B2', B1'; âˆ¡ A O H suppl âˆ¡ H O E [AOHsupplHOE] by H0, -, SupplementaryAngles_DEF; E âˆ‰ h [notEh] by H2, âˆ‰, AOE, BetweenLinear, notABh; Â¬(A,E same_side h) by H2, AOE, SameSide_DEF; B,E same_side h [Bsim_hE] by H2, notABh, notEh, -, H2, AtMost2Sides; consider Î±' such that âˆ¡ A O H suppl Î±' âˆ§ âˆ¡ A O H â‰¡ Î±' [AOHsupplÎ±'] by H1, RightAngle_DEF; Angle (âˆ¡ H O B) âˆ§ Angle (âˆ¡ A O H) âˆ§ Angle Î±' âˆ§ Angle (âˆ¡ H O E) [angÎ±'] by H1, RightImpliesAngle, -, AOHsupplHOE, SupplementImpliesAngle; âˆ¡ H O B â‰¡ âˆ¡ A O H âˆ§ Î±' â‰¡ âˆ¡ H O E by H1, RightAnglesCongruent, AOHsupplÎ±', AOHsupplHOE, SupplementUnique; âˆ¡ H O B â‰¡ âˆ¡ H O E by angÎ±', -, AOHsupplÎ±', C5Transitive; ray O B = ray O E by H2, Distinct, notABh, notEh, Bsim_hE, -, C4Uniqueness; B âˆˆ ray O E â” O by Distinct, EndpointInRay, -, IN_DELETE; qed by AOE, -, OppositeRaysIntersect1pointHelp, B1'; `;; let RightImpliesSupplRight = thm `; let A O B A' be point; assume Â¬Collinear A O B [H1]; assume O âˆˆ open (A,A') [H2]; assume Right (âˆ¡ A O B) [H3]; thus Right (âˆ¡ B O A') proof âˆ¡ A O B suppl âˆ¡ B O A' âˆ§ Angle (âˆ¡ A O B) âˆ§ Angle (âˆ¡ B O A') [AOBsuppl] by H1, H2, SupplementaryAngles_DEF, SupplementImpliesAngle; consider Î² such that âˆ¡ A O B suppl Î² âˆ§ âˆ¡ A O B â‰¡ Î² [Î²suppl] by H3, RightAngle_DEF; Angle Î² âˆ§ Î² â‰¡ âˆ¡ A O B [angÎ²] by -, SupplementImpliesAngle, C5Symmetric; âˆ¡ B O A' â‰¡ Î² by AOBsuppl, Î²suppl, SupplementUnique; âˆ¡ B O A' â‰¡ âˆ¡ A O B by AOBsuppl, angÎ², -, Î²suppl, C5Transitive; qed by AOBsuppl, H3, -, CongRightImpliesRight; `;; let IsoscelesCongBaseAngles = thm `; let A B C be point; assume Â¬Collinear A B C [H1]; assume seg B A â‰¡ seg B C [H2]; thus âˆ¡ C A B â‰¡ âˆ¡ A C B proof Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear C B A [CBAncol] by H1, NonCollinearImpliesDistinct, CollinearSymmetry; seg B C â‰¡ seg B A âˆ§ âˆ¡ A B C â‰¡ âˆ¡ C B A by -, SEGMENT, H2, C2Symmetric, H1, ANGLE, AngleSymmetry, C5Reflexive; A,B,C â‰… C,B,A by H1, CBAncol, H2, -, SAS; qed by -, TriangleCong_DEF; `;; let C4withC1 = thm `; let Î± l be point_set; let O A Y P Q be point; assume Angle Î± âˆ§ Â¬(O = A) âˆ§ Â¬(P = Q) [H1]; assume Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ Y âˆ‰ l [l_line]; thus âˆƒ N. Â¬(O = N) âˆ§ N âˆ‰ l âˆ§ N,Y same_side l âˆ§ seg O N â‰¡ seg P Q âˆ§ âˆ¡ A O N â‰¡ Î± proof âˆƒ! r. Ray r âˆ§ âˆƒ B. Â¬(O = B) âˆ§ r = ray O B âˆ§ B âˆ‰ l âˆ§ B,Y same_side l âˆ§ âˆ¡ A O B â‰¡ Î± by H1, l_line, C4; consider B such that Â¬(O = B) âˆ§ B âˆ‰ l âˆ§ B,Y same_side l âˆ§ âˆ¡ A O B â‰¡ Î± [Bexists] by -; consider N such that N âˆˆ ray O B â” O âˆ§ seg O N â‰¡ seg P Q [Nexists] by H1, -, SEGMENT, C1; Â¬(O = N) [notON] by -, IN_DELETE; N âˆ‰ l âˆ§ N,B same_side l [notNl] by l_line, Bexists, Nexists, RaySameSide; N,Y same_side l [Nsim_lY] by l_line, -, Bexists, SameSideTransitive; ray O N = ray O B âˆ§ âˆ¡ A O N â‰¡ Î± by Bexists, Nexists, RayWellDefined, Angle_DEF; qed by notON, notNl, Nsim_lY, Nexists, -; `;; let C4OppositeSide = thm `; let Î± l be point_set; let O A Z P Q be point; assume Angle Î± âˆ§ Â¬(O = A) âˆ§ Â¬(P = Q) [H1]; assume Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ Z âˆ‰ l [l_line]; thus âˆƒ N. Â¬(O = N) âˆ§ N âˆ‰ l âˆ§ Â¬(Z,N same_side l) âˆ§ seg O N â‰¡ seg P Q âˆ§ âˆ¡ A O N â‰¡ Î± proof Â¬(Z = O) by l_line, âˆ‰; consider Y such that O âˆˆ open (Z,Y) [ZOY] by -, B2'; Â¬(O = Y) âˆ§ Collinear Z O Y by -, B1'; Y âˆ‰ l [notYl] by l_line, I1, -, Collinear_DEF, âˆ‰; consider N such that Â¬(O = N) âˆ§ N âˆ‰ l âˆ§ N,Y same_side l âˆ§ seg O N â‰¡ seg P Q âˆ§ âˆ¡ A O N â‰¡ Î± [Nexists] by H1, l_line, notYl, C4withC1; Â¬(Z,Y same_side l) by l_line, ZOY, SameSide_DEF; Â¬(Z,N same_side l) by l_line, Nexists, notYl, -, SameSideTransitive; qed by -, Nexists; `;; let SSS = thm `; let A B C A' B' C' be point; assume Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' [H1]; assume seg A B â‰¡ seg A' B' âˆ§ seg A C â‰¡ seg A' C' âˆ§ seg B C â‰¡ seg B' C' [H2]; thus A,B,C â‰… A',B',C' proof Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬(A' = B') âˆ§ Â¬(B' = C') [Distinct] by H1, NonCollinearImpliesDistinct; consider h such that Line h âˆ§ A âˆˆ h âˆ§ C âˆˆ h [h_line] by Distinct, I1; B âˆ‰ h [notBh] by h_line, H1, âˆ‰, Collinear_DEF; Segment (seg A B) âˆ§ Segment (seg C B) âˆ§ Segment (seg A' B') âˆ§ Segment (seg C' B') [segments] by Distinct, -, SEGMENT; Angle (âˆ¡ C' A' B') by 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 -, Distinct, h_line, notBh, C4OppositeSide; Â¬(C = N) by h_line, Nexists, âˆ‰; Segment (seg A N) âˆ§ Segment (seg C N) [segN] by Nexists, -, SEGMENT; Â¬Collinear A N C [ANCncol] by h_line, Distinct, I1, Collinear_DEF, Nexists, âˆ‰; Angle (âˆ¡ A B C) âˆ§ Angle (âˆ¡ A' B' C') âˆ§ Angle (âˆ¡ A N C) [angles] by H1, -, ANGLE; seg A B â‰¡ seg A N [ABeqAN] by segments, segN, Nexists, H2, C2Symmetric, C2Transitive; C,A,N â‰… C',A',B' by ANCncol, H1, CollinearSymmetry, H2, Nexists, SAS; âˆ¡ A N C â‰¡ âˆ¡ A' B' C' âˆ§ seg C N â‰¡ seg C' B' [ANCeq] by -, TriangleCong_DEF; seg C B â‰¡ seg C N [CBeqCN] by segments, segN, -, H2, SegmentSymmetry, C2Symmetric, C2Transitive; consider G such that G âˆˆ h âˆ§ G âˆˆ open (B,N) [BGN] by Nexists, h_line, SameSide_DEF; Â¬(B = N) [notBN] by -, B1'; ray B G = ray B N âˆ§ ray N G = ray N B [Grays] by BGN, B1', IntervalRay; consider v such that Line v âˆ§ B âˆˆ v âˆ§ N âˆˆ v [v_line] by notBN, I1; G âˆˆ v âˆ§ Â¬(h = v) by v_line, BGN, BetweenLinear, notBh, âˆ‰; h âˆ© v = {G} [hvG] by h_line, v_line, -, BGN, I1Uniqueness; Â¬(G = A) â‡’ âˆ¡ A B G â‰¡ âˆ¡ A N G [ABGeqANG] proof assume Â¬(G = A) [notGA]; A âˆ‰ v by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE; Â¬Collinear B A N by v_line, notBN, I1, Collinear_DEF, -, âˆ‰; âˆ¡ N B A â‰¡ âˆ¡ B N A by -, ABeqAN, IsoscelesCongBaseAngles; âˆ¡ G B A â‰¡ âˆ¡ G N A by -, Grays, Angle_DEF, notGA; qed by -, AngleSymmetry; Â¬(G = C) â‡’ âˆ¡ G B C â‰¡ âˆ¡ G N C [GBCeqGNC] proof assume Â¬(G = C) [notGC]; C âˆ‰ v by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE; Â¬Collinear B C N by v_line, notBN, I1, Collinear_DEF, -, âˆ‰; âˆ¡ N B C â‰¡ âˆ¡ B N C by -, CBeqCN, IsoscelesCongBaseAngles, AngleSymmetry; qed by -, Grays, Angle_DEF; âˆ¡ A B C â‰¡ âˆ¡ A N C proof cases; suppose G = A [GA]; Â¬(G = C) by -, Distinct; qed by -, GBCeqGNC, GA; suppose G = C [GC]; Â¬(G = A) by -, Distinct; qed by -, ABGeqANG, GC; suppose Â¬(G = A) âˆ§ Â¬(G = C) [AGCdistinct]; âˆ¡ A B G â‰¡ âˆ¡ A N G âˆ§ âˆ¡ G B C â‰¡ âˆ¡ G N C [Gequivs] by -, ABGeqANG, GBCeqGNC; Â¬Collinear G B C âˆ§ Â¬Collinear G N C âˆ§ Â¬Collinear G B A âˆ§ Â¬Collinear G N A [Gncols] by h_line, BGN, AGCdistinct, I1, Collinear_DEF, notBh, Nexists, âˆ‰; Collinear A G C by h_line, BGN, Collinear_DEF; G âˆˆ open (A,C) âˆ¨ C âˆˆ open (G,A) âˆ¨ A âˆˆ open (C,G) by Distinct, AGCdistinct, -, B3'; cases by -; suppose G âˆˆ open (A,C); G âˆˆ int_angle A B C âˆ§ G âˆˆ int_angle A N C by H1, ANCncol, -, ConverseCrossbar; qed by -, Gequivs, AngleAddition; suppose C âˆˆ open (G,A); C âˆˆ int_angle G B A âˆ§ C âˆˆ int_angle G N A by Gncols, -, B1', ConverseCrossbar; qed by -, Gequivs, AngleSubtraction, AngleSymmetry; suppose A âˆˆ open (C,G); A âˆˆ int_angle G B C âˆ§ A âˆˆ int_angle G N C by Gncols, -, B1', ConverseCrossbar; qed by -, Gequivs, AngleSymmetry, AngleSubtraction; end; end; âˆ¡ A B C â‰¡ âˆ¡ A' B' C' by angles, -, ANCeq, C5Transitive; qed by H1, H2, SegmentSymmetry, -, SAS; `;; let AngleBisector = thm `; let A B C be point; assume Â¬Collinear B A C [H1]; thus âˆƒ F. F âˆˆ int_angle B A C âˆ§ âˆ¡ B A F â‰¡ âˆ¡ F A C proof Â¬(A = B) âˆ§ Â¬(A = C) [Distinct] by H1, NonCollinearImpliesDistinct; consider D such that B âˆˆ open (A,D) [ABD] by Distinct, B2'; Â¬(A = D) âˆ§ Collinear A B D âˆ§ Segment (seg A D) [ABD'] by -, B1', SEGMENT; consider E such that E âˆˆ ray A C â” A âˆ§ seg A E â‰¡ seg A D âˆ§ Â¬(A = E) [ErAC] by -, Distinct, C1, IN_DELETE, IN_Ray; Collinear A C E âˆ§ D âˆˆ ray A B â” A [notAE] by ErAC, IN_DELETE, IN_Ray, ABD, IntervalRayEZ; ray A D = ray A B âˆ§ ray A E = ray A C [equalrays] by Distinct, notAE, ErAC, RayWellDefined; Â¬Collinear D A E âˆ§ Â¬Collinear E A D âˆ§ Â¬Collinear A E D [EADncol] by H1, ABD', notAE, ErAC, CollinearSymmetry, NoncollinearityExtendsToLine; âˆ¡ D E A â‰¡ âˆ¡ E D A [DEAeq] by EADncol, ErAC, IsoscelesCongBaseAngles; Â¬Collinear E D A âˆ§ Angle (âˆ¡ E D A) âˆ§ Â¬Collinear A D E âˆ§ Â¬Collinear D E A [angEDA] by EADncol, CollinearSymmetry, ANGLE; Â¬(D = E) [notDE] by EADncol, NonCollinearImpliesDistinct; consider h such that Line h âˆ§ D âˆˆ h âˆ§ E âˆˆ h [h_line] by -, I1; A âˆ‰ h [notAh] by -, Collinear_DEF, EADncol, âˆ‰; consider F such that Â¬(D = F) âˆ§ F âˆ‰ h âˆ§ Â¬(A,F same_side h) âˆ§ seg D F â‰¡ seg D A âˆ§ âˆ¡ E D F â‰¡ âˆ¡ E D A [Fexists] by angEDA, notDE, ABD', h_line, -, C4OppositeSide; Â¬(A = F) [notAF] by h_line, -, SameSideReflexive; Â¬Collinear E D F âˆ§ Â¬Collinear D E F âˆ§ Â¬Collinear F E D [EDFncol] by h_line, notDE, I1, Collinear_DEF, Fexists, âˆ‰; seg D E â‰¡ seg D E âˆ§ seg F A â‰¡ seg F A [FArefl] by notDE, notAF, SEGMENT, C2Reflexive; E,D,F â‰… E,D,A by EDFncol, angEDA, -, Fexists, SAS; seg F E â‰¡ seg A E âˆ§ âˆ¡ F E D â‰¡ âˆ¡ A E D [FEDâ‰…] by -, TriangleCong_DEF, SegmentSymmetry; âˆ¡ E D A â‰¡ âˆ¡ D E A âˆ§ âˆ¡ E D A â‰¡ âˆ¡ E D F âˆ§ âˆ¡ D E A â‰¡ âˆ¡ D E F [EDAeqEDF] by EDFncol, ANGLE, angEDA, Fexists, FEDâ‰…, DEAeq, C5Symmetric, AngleSymmetry; consider G such that G âˆˆ h âˆ§ G âˆˆ open (A,F) [AGF] by Fexists, h_line, SameSide_DEF; F âˆˆ ray A G â” A [FrAG] by -, IntervalRayEZ; consider v such that Line v âˆ§ A âˆˆ v âˆ§ F âˆˆ v âˆ§ G âˆˆ v [v_line] by notAF, I1, AGF, BetweenLinear; Â¬(v = h) âˆ§ v âˆ© h = {G} [vhG] by -, notAh, âˆ‰, h_line, AGF, I1Uniqueness; D âˆ‰ v [notDv] proof assume Â¬(D âˆ‰ v); D âˆˆ v âˆ§ D = G [DG] by h_line, -, âˆ‰, vhG, IN_INTER, IN_SING; D âˆˆ open (A,F) by DG, AGF; âˆ¡ E D A suppl âˆ¡ E D F [EDAsuppl] by angEDA, -, SupplementaryAngles_DEF, AngleSymmetry; Right (âˆ¡ E D A) by EDAsuppl, EDAeqEDF, RightAngle_DEF; Right (âˆ¡ A E D) [RightAED] by angEDA, ANGLE, -, DEAeq, CongRightImpliesRight, AngleSymmetry; Right (âˆ¡ D E F) by EDFncol, ANGLE, -, FEDâ‰…, CongRightImpliesRight, AngleSymmetry; E âˆˆ open (A,F) by EADncol, EDFncol, RightAED, -, h_line, Fexists, OppositeRightAnglesLinear; E âˆˆ v âˆ§ E = G by v_line, -, BetweenLinear, h_line, vhG, IN_INTER, IN_SING; qed by -, DG, notDE; E âˆ‰ v [notEv] proof assume Â¬(E âˆ‰ v); E âˆˆ v âˆ§ E = G [EG] by h_line, -, âˆ‰, vhG, IN_INTER, IN_SING; E âˆˆ open (A,F) by -, AGF; âˆ¡ D E A suppl âˆ¡ D E F [DEAsuppl] by EADncol, -, SupplementaryAngles_DEF, AngleSymmetry; Right (âˆ¡ D E A) [RightDEA] by DEAsuppl, EDAeqEDF, RightAngle_DEF; Right (âˆ¡ E D A) [RightEDA] by angEDA, RightDEA, EDAeqEDF, CongRightImpliesRight; Right (âˆ¡ E D F) by EDFncol, ANGLE, RightEDA, Fexists, CongRightImpliesRight; D âˆˆ open (A,F) by angEDA, EDFncol, RightEDA, AngleSymmetry, -, h_line, Fexists, OppositeRightAnglesLinear; D âˆˆ v âˆ§ D = G by v_line, -, BetweenLinear, h_line, vhG, IN_INTER, IN_SING; qed by -, EG, notDE; Â¬Collinear F A E âˆ§ Â¬Collinear F A D âˆ§ Â¬(F = E) [FAEncol] by v_line, notAF, I1, Collinear_DEF, notEv, notDv, âˆ‰, NonCollinearImpliesDistinct; seg F E â‰¡ seg A D [FEeqAD] by -, ErAC, ABD', SEGMENT, FEDâ‰…, ErAC, C2Transitive; seg A D â‰¡ seg F D by SegmentSymmetry, ABD', Fexists, SEGMENT, C2Symmetric; seg F E â‰¡ seg F D by FAEncol, ABD', Fexists, SEGMENT, FEeqAD, -, C2Transitive; F,A,E â‰… F,A,D by FAEncol, FArefl, -, ErAC, SSS; âˆ¡ F A E â‰¡ âˆ¡ F A D [FAEeq] by -, TriangleCong_DEF; âˆ¡ D A F â‰¡ âˆ¡ F A E by FAEncol, ANGLE, FAEeq, C5Symmetric, AngleSymmetry; âˆ¡ B A F â‰¡ âˆ¡ F A C [BAFeqFAC] by -, equalrays, Angle_DEF; Â¬(E,D same_side v) proof assume E,D same_side v; ray A D = ray A E by v_line, notAF, notDv, notEv, -, FAEeq, C4Uniqueness; qed by ABD', EndpointInRay, -, IN_Ray, EADncol; consider H such that H âˆˆ v âˆ§ H âˆˆ open (E,D) [EHD] by v_line, -, SameSide_DEF; H = G by -, h_line, BetweenLinear, IN_INTER, vhG, IN_SING; G âˆˆ int_angle E A D [GintEAD] by EADncol, -, EHD, ConverseCrossbar; F âˆˆ int_angle E A D [FintEAD] by GintEAD, FrAG, WholeRayInterior; B âˆˆ ray A D â” A âˆ§ C âˆˆ ray A E â” A by equalrays, Distinct, EndpointInRay, IN_DELETE; F âˆˆ int_angle B A C by FintEAD, -, InteriorWellDefined, InteriorAngleSymmetry; qed by -, BAFeqFAC; `;; let EuclidPropositionI_6 = thm `; let A B C be point; assume Â¬Collinear A B C [H1]; assume âˆ¡ B A C â‰¡ âˆ¡ B C A [H2]; thus seg B A â‰¡ seg B C proof Â¬(A = C) by H1, NonCollinearImpliesDistinct; seg C A â‰¡ seg A C [CAeqAC] by SegmentSymmetry, -, SEGMENT, C2Reflexive; Â¬Collinear B C A âˆ§ Â¬Collinear C B A âˆ§ Â¬Collinear B A C [BCAncol] by H1, CollinearSymmetry; âˆ¡ A C B â‰¡ âˆ¡ C A B by -, ANGLE, H2, C5Symmetric, AngleSymmetry; C,B,A â‰… A,B,C by H1, BCAncol, CAeqAC, H2, -, ASA; qed by -, TriangleCong_DEF; `;; let IsoscelesExists = thm `; let A B be point; assume Â¬(A = B) [H1]; thus âˆƒ D. Â¬Collinear A D B âˆ§ seg D A â‰¡ seg D B proof consider l such that Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l [l_line] by H1, I1; consider C such that C âˆ‰ l [notCl] by -, ExistsPointOffLine; Â¬Collinear C A B âˆ§ Â¬Collinear C B A âˆ§ Â¬Collinear A B C âˆ§ Â¬Collinear A C B âˆ§ Â¬Collinear B A C [CABncol] by 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 -, ANGLE, AngleTrichotomy; cases by -; suppose âˆ¡ C A B â‰¡ âˆ¡ C B A; qed by -, CABncol, EuclidPropositionI_6; suppose âˆ¡ C A B <_ang âˆ¡ C B A; âˆ¡ C A B <_ang âˆ¡ A B C by -, AngleSymmetry; consider E such that E âˆˆ int_angle A B C âˆ§ âˆ¡ C A B â‰¡ âˆ¡ A B E [Eexists] by CABncol, ANGLE, -, AngleOrderingUse; Â¬(B = E) [notBE] by -, InteriorEZHelp; consider D such that D âˆˆ open (A,C) âˆ§ D âˆˆ ray B E â” B [Dexists] by Eexists, Crossbar_THM; D âˆˆ int_angle A B C by Eexists, -, WholeRayInterior; Â¬Collinear A D B [ADBncol] by -, InteriorEZHelp, CollinearSymmetry; ray B D = ray B E âˆ§ ray A D = ray A C by notBE, Dexists, RayWellDefined, IntervalRay; âˆ¡ D A B â‰¡ âˆ¡ A B D by Eexists, -, Angle_DEF; qed by ADBncol, -, AngleSymmetry, EuclidPropositionI_6; :: similar case suppose âˆ¡ C B A <_ang âˆ¡ C A B; âˆ¡ C B A <_ang âˆ¡ B A C by -, AngleSymmetry; consider E such that E âˆˆ int_angle B A C âˆ§ âˆ¡ C B A â‰¡ âˆ¡ B A E [Eexists] by CABncol, ANGLE, -, AngleOrderingUse; Â¬(A = E) [notAE] by -, InteriorEZHelp; consider D such that D âˆˆ open (B,C) âˆ§ D âˆˆ ray A E â” A [Dexists] by Eexists, Crossbar_THM; D âˆˆ int_angle B A C by Eexists, -, WholeRayInterior; Â¬Collinear A D B âˆ§ Â¬Collinear D A B âˆ§ Â¬Collinear D B A [ADBncol] by -, InteriorEZHelp, CollinearSymmetry; ray A D = ray A E âˆ§ ray B D = ray B C by notAE, Dexists, RayWellDefined, IntervalRay; âˆ¡ D B A â‰¡ âˆ¡ B A D by Eexists, -, Angle_DEF; âˆ¡ D A B â‰¡ âˆ¡ D B A by AngleSymmetry, ADBncol, ANGLE, -, C5Symmetric; qed by ADBncol, -, EuclidPropositionI_6; end; `;; let MidpointExists = thm `; let A B be point; assume Â¬(A = B) [H1]; thus âˆƒ M. M âˆˆ open (A,B) âˆ§ seg A M â‰¡ seg M B proof consider D such that Â¬Collinear A D B âˆ§ seg D A â‰¡ seg D B [Dexists] by H1, IsoscelesExists; consider F such that F âˆˆ int_angle A D B âˆ§ âˆ¡ A D F â‰¡ âˆ¡ F D B [Fexists] by -, AngleBisector; Â¬(D = F) [notDF] by -, InteriorEZHelp; consider M such that M âˆˆ open (A,B) âˆ§ M âˆˆ ray D F â” D [Mexists] by Fexists, Crossbar_THM; ray D M = ray D F by notDF, -, RayWellDefined; âˆ¡ A D M â‰¡ âˆ¡ M D B [ADMeqMDB] by Fexists, -, Angle_DEF; M âˆˆ int_angle A D B by Fexists, Mexists, WholeRayInterior; Â¬(D = M) âˆ§ Â¬Collinear A D M âˆ§ Â¬Collinear B D M [ADMncol] by -, InteriorEZHelp, InteriorAngleSymmetry; seg D M â‰¡ seg D M by -, SEGMENT, C2Reflexive; A,D,M â‰… B,D,M by ADMncol, Dexists, -, ADMeqMDB, AngleSymmetry, SAS; qed by Mexists, -, TriangleCong_DEF, SegmentSymmetry; `;; let EuclidPropositionI_7short = thm `; let A B C D be point; let a be point_set; assume Â¬(A = B) âˆ§ Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line]; assume Â¬(C = D) âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a âˆ§ C,D same_side a [Csim_aD]; assume seg A C â‰¡ seg A D [ACeqAD]; thus Â¬(seg B C â‰¡ seg B D) proof Â¬(A = C) âˆ§ Â¬(A = D) [AnotCD] by a_line, Csim_aD, âˆ‰; assume seg B C â‰¡ seg B D; seg C B â‰¡ seg D B âˆ§ seg A B â‰¡ seg A B âˆ§ seg A D â‰¡ seg A D [segeqs] by -, SegmentSymmetry, a_line, AnotCD, SEGMENT, C2Reflexive; Â¬Collinear A C B âˆ§ Â¬Collinear A D B by a_line, I1, Csim_aD, Collinear_DEF, âˆ‰; A,C,B â‰… A,D,B by -, ACeqAD, segeqs, SSS; âˆ¡ B A C â‰¡ âˆ¡ B A D by -, TriangleCong_DEF; ray A D = ray A C by a_line, Csim_aD, -, C4Uniqueness; C âˆˆ ray A D â” A âˆ§ D âˆˆ ray A D â” A by AnotCD, -, EndpointInRay, IN_DELETE; C = D by AnotCD, SEGMENT, -, ACeqAD, segeqs, C1; qed by -, Csim_aD; `;; let EuclidPropositionI_7Help = thm `; let A B C D be point; let a be point_set; assume Â¬(A = B) [notAB]; assume Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line]; assume Â¬(C = D) âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a âˆ§ C,D same_side a [Csim_aD]; assume seg A C â‰¡ seg A D [ACeqAD]; assume C âˆˆ int_triangle D A B âˆ¨ ConvexQuadrilateral A B C D [Int_ConvQuad]; thus Â¬(seg B C â‰¡ seg B D) proof Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) [Distinct] by a_line, Csim_aD, âˆ‰, SameSide_DEF; cases by 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 -, 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 -, Tetralateral_DEF, CollinearSymmetry, ANGLE; âˆ¡ C D A â‰¡ âˆ¡ D C A [CDAeqDCA] by 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 ABint, InteriorAngleSymmetry, angCDB, ANGLE, C5Reflexive; âˆ¡ D C A <_ang âˆ¡ D C B âˆ§ âˆ¡ C D B <_ang âˆ¡ C D A by angCDB, ABint, -, AngleOrdering_DEF; âˆ¡ C D B <_ang âˆ¡ D C B by -, angCDB, CDAeqDCA, AngleTrichotomy2, AngleOrderTransitivity; Â¬(âˆ¡ D C B â‰¡ âˆ¡ C D B) by -, AngleTrichotomy1, angCDB, ANGLE, C5Symmetric; qed by angCDB, -, IsoscelesCongBaseAngles; suppose C âˆˆ int_triangle D A B; C âˆˆ int_angle A D B âˆ§ C âˆˆ int_angle D A B [CintADB] by -, IN_InteriorTriangle, InteriorAngleSymmetry; Â¬Collinear A D C âˆ§ Â¬Collinear B D C [ADCncol] by CintADB, InteriorEZHelp, InteriorAngleSymmetry; Â¬Collinear D A C âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear A C D âˆ§ Â¬Collinear A D C [DACncol] by -, CollinearSymmetry; Â¬Collinear B C D âˆ§ Angle (âˆ¡ D C A) âˆ§ Angle (âˆ¡ C D B) âˆ§ Â¬Collinear D C B [angCDB] by ADCncol, -, CollinearSymmetry, ANGLE; âˆ¡ C D A â‰¡ âˆ¡ D C A [CDAeqDCA] by DACncol, Distinct, ADCncol, SEGMENT, ACeqAD, C2Symmetric, IsoscelesCongBaseAngles; consider E such that D âˆˆ open (A,E) âˆ§ Â¬(D = E) âˆ§ Collinear A D E [ADE] by Distinct, B2', B1'; B âˆˆ int_angle C D E âˆ§ Collinear D A E [BintCDE] by CintADB, -, InteriorReflectionInterior, CollinearSymmetry; Â¬Collinear C D E [CDEncol] by DACncol, -, ADE, NoncollinearityExtendsToLine; consider F such that F âˆˆ open (B,D) âˆ§ F âˆˆ ray A C â” A [Fexists] by CintADB, Crossbar_THM, B1'; F âˆˆ int_angle B C D [FintBCD] by ADCncol, CollinearSymmetry, -, ConverseCrossbar; Â¬Collinear D C F [DCFncol] by Distinct, ADCncol, CollinearSymmetry, Fexists, B1', NoncollinearityExtendsToLine; Collinear A C F âˆ§ F âˆˆ ray D B â” D âˆ§ C âˆˆ int_angle A D F by Fexists, IN_DELETE, IN_Ray, B1', IntervalRayEZ, CintADB, InteriorWellDefined; C âˆˆ open (A,F) by -, AlternateConverseCrossbar; âˆ¡ A D C suppl âˆ¡ C D E âˆ§ âˆ¡ A C D suppl âˆ¡ D C F by ADE, DACncol, -, SupplementaryAngles_DEF; âˆ¡ C D E â‰¡ âˆ¡ D C F [CDEeqDCF] by -, CDAeqDCA, AngleSymmetry, SupplementsCongAnglesCong; âˆ¡ C D B <_ang âˆ¡ C D E by angCDB, CDEncol, BintCDE, C5Reflexive, AngleOrdering_DEF; âˆ¡ C D B <_ang âˆ¡ D C F [CDBlessDCF] by -, DCFncol, ANGLE, CDEeqDCF, AngleTrichotomy2; âˆ¡ D C F <_ang âˆ¡ D C B by DCFncol, ANGLE, angCDB, FintBCD, InteriorAngleSymmetry, C5Reflexive, AngleOrdering_DEF; âˆ¡ C D B <_ang âˆ¡ D C B by CDBlessDCF, -, AngleOrderTransitivity; Â¬(âˆ¡ D C B â‰¡ âˆ¡ C D B) by -, AngleTrichotomy1, angCDB, CollinearSymmetry, ANGLE, C5Symmetric; qed by Distinct, ADCncol, CollinearSymmetry, -, IsoscelesCongBaseAngles; end; `;; let EuclidPropositionI_7 = thm `; let A B C D be point; let a be point_set; assume Â¬(A = B) [notAB]; assume Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line]; assume Â¬(C = D) âˆ§ C âˆ‰ a âˆ§ D âˆ‰ a âˆ§ C,D same_side a [Csim_aD]; assume seg A C â‰¡ seg A D [ACeqAD]; thus Â¬(seg B C â‰¡ seg B D) proof Â¬Collinear A B C âˆ§ Â¬Collinear D A B [ABCncol] by a_line, notAB, I1, Collinear_DEF, Csim_aD, âˆ‰; Â¬(A = C) âˆ§ Â¬(A = D) âˆ§ Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ A âˆ‰ open (C,D) [Distinct] by a_line, Csim_aD, âˆ‰, SameSide_DEF; Â¬Collinear A D C [ADCncol] proof assume Collinear A D C; C âˆˆ ray A D â” A âˆ§ D âˆˆ ray A D â” A by Distinct, -, IN_Ray, EndpointInRay, IN_DELETE; qed by Distinct, SEGMENT, -, ACeqAD, C2Reflexive, C1, Csim_aD; D,C same_side a [Dsim_aC] by a_line, Csim_aD, SameSideSymmetric; seg A D â‰¡ seg A C âˆ§ seg B D â‰¡ seg B D [ADeqAC] by Distinct, SEGMENT, ACeqAD, C2Symmetric, C2Reflexive; Â¬Collinear D A C âˆ§ Â¬Collinear C D A âˆ§ Â¬Collinear A C D âˆ§ Â¬Collinear A D C [DACncol] by ADCncol, CollinearSymmetry; Â¬(seg B D â‰¡ seg B C) â‡’ Â¬(seg B C â‰¡ seg B D) [BswitchDC] by Distinct, SEGMENT, C2Symmetric; cases; suppose Collinear B D C; B âˆ‰ open (C,D) âˆ§ C âˆˆ ray B D â” B âˆ§ D âˆˆ ray B D â” B by a_line, Csim_aD, SameSide_DEF, âˆ‰, Distinct, -, IN_Ray, Distinct, IN_DELETE, EndpointInRay; qed by Distinct, SEGMENT, -, ACeqAD, ADeqAC, C1, Csim_aD; suppose Â¬Collinear B D C [BDCncol]; Tetralateral A B C D by 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 -, a_line, Csim_aD, FourChoicesTetralateral, InteriorTriangleSymmetry; qed by notAB, a_line, Csim_aD, Dsim_aC, ACeqAD, ADeqAC, -, EuclidPropositionI_7Help, BswitchDC; end; `;; let EuclidPropositionI_11 = thm `; let A B be point; assume Â¬(A = B) [notAB]; thus âˆƒ F. Right (âˆ¡ A B F) proof consider C such that B âˆˆ open (A,C) âˆ§ seg B C â‰¡ seg B A [ABC] by notAB, SEGMENT, C1OppositeRay; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Collinear A B C [Distinct] by ABC, B1'; seg B A â‰¡ seg B C [BAeqBC] by -, SEGMENT, ABC, C2Symmetric; consider F such that Â¬Collinear A F C âˆ§ seg F A â‰¡ seg F C [Fexists] by Distinct, IsoscelesExists; Â¬Collinear B F A âˆ§ Â¬Collinear B F C [BFAncol] by -, CollinearSymmetry, Distinct, NoncollinearityExtendsToLine; Â¬Collinear A B F âˆ§ Angle (âˆ¡ A B F) [angABF] by BFAncol, CollinearSymmetry, ANGLE; âˆ¡ A B F suppl âˆ¡ F B C [ABFsuppl] by -, ABC, SupplementaryAngles_DEF; Â¬(B = F) âˆ§ seg B F â‰¡ seg B F by BFAncol, NonCollinearImpliesDistinct, SEGMENT, C2Reflexive; B,F,A â‰… B,F,C by BFAncol, -, BAeqBC, Fexists, SSS; âˆ¡ A B F â‰¡ âˆ¡ F B C by -, TriangleCong_DEF, AngleSymmetry; qed by angABF, ABFsuppl, -, RightAngle_DEF; `;; let DropPerpendicularToLine = thm `; let P be point; let l be point_set; assume Line l âˆ§ P âˆ‰ l [l_line]; thus âˆƒ E Q. E âˆˆ l âˆ§ Q âˆˆ l âˆ§ Right (âˆ¡ P Q E) proof consider A B such that A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B) [ABl] by l_line, I2; Â¬Collinear B A P âˆ§ Â¬Collinear P A B âˆ§ Â¬(A = P) [BAPncol] by l_line, ABl, I1, Collinear_DEF, âˆ‰, CollinearSymmetry, ABl, âˆ‰; Angle (âˆ¡ B A P) âˆ§ Angle (âˆ¡ P A B) [angBAP] by -, 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 angBAP, ABl, BAPncol, l_line, C4OppositeSide; consider Q such that Q âˆˆ l âˆ§ Q âˆˆ open (P,P') âˆ§ Collinear A B Q [Qexists] by l_line, -, SameSide_DEF, ABl, Collinear_DEF; Â¬Collinear B A P' [BAP'ncol] by l_line, ABl, I1, Collinear_DEF, P'exists, âˆ‰; âˆ¡ B A P â‰¡ âˆ¡ B A P' [BAPeqBAP'] by -, ANGLE, angBAP, P'exists, C5Symmetric; âˆƒ E. E âˆˆ l âˆ§ Â¬Collinear P Q E âˆ§ âˆ¡ P Q E â‰¡ âˆ¡ E Q P' proof cases; suppose A = Q [AQ]; qed by ABl, AQ, BAPncol, BAPeqBAP', AngleSymmetry; suppose Â¬(A = Q) [notAQ]; seg A Q â‰¡ seg A Q âˆ§ seg A P â‰¡ seg A P' [APeqAP'] by -, SEGMENT, C2Reflexive, BAPncol, P'exists, C2Symmetric; Â¬Collinear Q A P' âˆ§ Â¬Collinear Q A P [QAP'ncol] by l_line, ABl, Qexists, notAQ, I1, Collinear_DEF, P'exists, âˆ‰; âˆ¡ Q A P â‰¡ âˆ¡ Q A P' proof cases; suppose A âˆˆ open (Q,B); âˆ¡ B A P suppl âˆ¡ P A Q âˆ§ âˆ¡ B A P' suppl âˆ¡ P' A Q by BAPncol, BAP'ncol, -, B1', SupplementaryAngles_DEF; qed by -, BAPeqBAP', SupplementsCongAnglesCong, AngleSymmetry; suppose Â¬(A âˆˆ open (Q,B)); A âˆ‰ open (Q,B) âˆ§ Q âˆˆ ray A B â” A âˆ§ ray A Q = ray A B by -, âˆ‰, ABl, Qexists, IN_Ray, notAQ, IN_DELETE, ABl, RayWellDefined; qed by -, BAPeqBAP', Angle_DEF; end; Q,A,P â‰… Q,A,P' by QAP'ncol, APeqAP', -, SAS; qed by -, TriangleCong_DEF, AngleSymmetry, ABl, QAP'ncol, CollinearSymmetry; end; consider E such that E âˆˆ l âˆ§ Â¬Collinear P Q E âˆ§ âˆ¡ P Q E â‰¡ âˆ¡ E Q P' [Eexists] by -; âˆ¡ P Q E suppl âˆ¡ E Q P' âˆ§ Right (âˆ¡ P Q E) by -, Qexists, SupplementaryAngles_DEF, RightAngle_DEF; qed by Eexists, Qexists, -; `;; let EuclidPropositionI_14 = thm `; let A B C D be point; let l be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ Â¬(A = B) [l_line]; assume C âˆ‰ l âˆ§ D âˆ‰ l âˆ§ Â¬(C,D same_side l) [Cnsim_lD]; assume âˆ¡ C B A suppl âˆ¡ A B D [CBAsupplABD]; thus B âˆˆ open (C,D) proof Â¬(B = C) âˆ§ Â¬(B = D) âˆ§ Â¬Collinear C B A [Distinct] by l_line, Cnsim_lD, âˆ‰, I1, Collinear_DEF; consider E such that B âˆˆ open (C,E) [CBE] by Distinct, B2'; E âˆ‰ l âˆ§ Â¬(C,E same_side l) [Csim_lE] by l_line, âˆ‰, -, BetweenLinear, Cnsim_lD, SameSide_DEF; D,E same_side l [Dsim_lE] by l_line, Cnsim_lD, -, AtMost2Sides; âˆ¡ C B A suppl âˆ¡ A B E by Distinct, CBE, SupplementaryAngles_DEF; âˆ¡ A B D â‰¡ âˆ¡ A B E by CBAsupplABD, -, SupplementUnique; ray B E = ray B D by l_line, Csim_lE, Cnsim_lD, Dsim_lE, -, C4Uniqueness; D âˆˆ ray B E â” B by Distinct, -, EndpointInRay, IN_DELETE; qed by CBE, -, OppositeRaysIntersect1pointHelp, B1'; `;; let VerticalAnglesCong = thm `; :: Euclid's Proposition I.15 let A B O A' B' be point; assume Â¬Collinear A O B [H1]; assume O âˆˆ open (A,A') âˆ§ O âˆˆ open (B,B') [H2]; thus âˆ¡ B O A' â‰¡ âˆ¡ B' O A proof âˆ¡ A O B suppl âˆ¡ B O A' [AOBsupplBOA'] by H1, H2, SupplementaryAngles_DEF; âˆ¡ B O A suppl âˆ¡ A O B' by H1, CollinearSymmetry, H2, SupplementaryAngles_DEF; qed by AOBsupplBOA', -, AngleSymmetry, SupplementUnique; `;; let EuclidPropositionI_16 = thm `; let A B C D be point; assume Â¬Collinear A B C [H1]; assume C âˆˆ open (B,D) [H2]; thus âˆ¡ B A C <_ang âˆ¡ D C A proof Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [Distinct] by H1, NonCollinearImpliesDistinct; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line] by Distinct, I1; consider m such that Line m âˆ§ B âˆˆ m âˆ§ C âˆˆ m [m_line] by Distinct, I1; D âˆˆ m [Dm] by m_line, H2, BetweenLinear; consider E such that E âˆˆ open (A,C) âˆ§ seg A E â‰¡ seg E C [AEC] by Distinct, MidpointExists; Â¬(A = E) âˆ§ Â¬(E = C) âˆ§ Collinear A E C âˆ§ Â¬(B = E) [AECcol] by -, B1', H1; E âˆˆ l [El] by l_line, AEC, BetweenLinear; consider F such that E âˆˆ open (B,F) âˆ§ seg E F â‰¡ seg E B [BEF] by AECcol, SEGMENT, C1OppositeRay; Â¬(B = E) âˆ§ Â¬(B = F) âˆ§ Â¬(E = F) âˆ§ Collinear B E F [BEF'] by BEF, B1'; B âˆ‰ l [notBl] by l_line, Distinct, I1, Collinear_DEF, H1, âˆ‰; Â¬Collinear A E B âˆ§ Â¬Collinear C E B [AEBncol] by l_line, El, AECcol, I1, Collinear_DEF, notBl, âˆ‰; Angle (âˆ¡ B A E) [angBAE] by -, CollinearSymmetry, ANGLE; Â¬Collinear C E F [CEFncol] by AEBncol, BEF', CollinearSymmetry, NoncollinearityExtendsToLine; âˆ¡ B E A â‰¡ âˆ¡ F E C [BEAeqFEC] by AEBncol, AEC, B1', BEF, VerticalAnglesCong; seg E A â‰¡ seg E C âˆ§ seg E B â‰¡ seg E F by AEC, SegmentSymmetry, AECcol, BEF', SEGMENT, BEF, C2Symmetric; A,E,B â‰… C,E,F by AEBncol, CEFncol, -, BEAeqFEC, AngleSymmetry, SAS; âˆ¡ B A E â‰¡ âˆ¡ F C E [BAEeqFCE] by -, TriangleCong_DEF; Â¬Collinear E C D [ECDncol] by AEBncol, H2, B1', CollinearSymmetry, NoncollinearityExtendsToLine; F âˆ‰ l âˆ§ D âˆ‰ l [notFl] by l_line, El, Collinear_DEF, CEFncol, -, âˆ‰; F âˆˆ ray B E â” B âˆ§ E âˆ‰ m by BEF, IntervalRayEZ, m_line, Collinear_DEF, AEBncol, âˆ‰; F âˆ‰ m âˆ§ F,E same_side m [Fsim_mE] by m_line, -, RaySameSide; Â¬(B,F same_side l) âˆ§ Â¬(B,D same_side l) by El, l_line, BEF, H2, SameSide_DEF; F,D same_side l by l_line, notBl, notFl, -, AtMost2Sides; F âˆˆ int_angle E C D by ECDncol, l_line, El, m_line, Dm, notFl, Fsim_mE, -, IN_InteriorAngle; âˆ¡ B A E <_ang âˆ¡ E C D [BAElessECD] by angBAE, ECDncol, -, BAEeqFCE, AngleSymmetry, AngleOrdering_DEF; ray A E = ray A C âˆ§ ray C E = ray C A by AEC, B1', IntervalRay; âˆ¡ B A C <_ang âˆ¡ A C D by BAElessECD, -, Angle_DEF; qed by -, AngleSymmetry; `;; let ExteriorAngle = thm `; let A B C D be point; assume Â¬Collinear A B C [H1]; assume C âˆˆ open (B,D) [H2]; thus âˆ¡ A B C <_ang âˆ¡ A C D proof Â¬(C = D) âˆ§ C âˆˆ open (D,B) âˆ§ Collinear B C D [H2'] by H2, BetweenLinear, B1'; Â¬Collinear B A C âˆ§ Â¬(A = C) [BACncol] by H1, CollinearSymmetry, NonCollinearImpliesDistinct; consider E such that C âˆˆ open (A,E) [ACE] by -, B2'; Â¬(C = E) âˆ§ C âˆˆ open (E,A) âˆ§ Collinear A C E [ACE'] by -, B1'; Â¬Collinear A C D âˆ§ Â¬Collinear D C E [DCEncol] by H1, CollinearSymmetry, H2', -, NoncollinearityExtendsToLine; âˆ¡ A B C <_ang âˆ¡ E C B [ABClessECB] by BACncol, ACE, EuclidPropositionI_16; âˆ¡ E C B â‰¡ âˆ¡ A C D by DCEncol, ACE', H2', VerticalAnglesCong; qed by ABClessECB, DCEncol, ANGLE, -, AngleTrichotomy2; `;; let EuclidPropositionI_17 = thm `; let A B C be point; let Î± Î² Î³ be point_set; assume Â¬Collinear A B C âˆ§ Î± = âˆ¡ A B C âˆ§ Î² = âˆ¡ B C A [H1]; assume Î² suppl Î³ [H2]; thus Î± <_ang Î³ proof Angle Î³ [angÎ³] by H2, SupplementImpliesAngle; Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) [Distinct] by H1, NonCollinearImpliesDistinct; Â¬Collinear B A C âˆ§ Â¬Collinear A C B [BACncol] by H1, CollinearSymmetry; consider D such that C âˆˆ open (A,D) [ACD] by Distinct, B2'; âˆ¡ A B C <_ang âˆ¡ D C B [ABClessDCB] by BACncol, ACD, EuclidPropositionI_16; Î² suppl âˆ¡ B C D by -, H1, AngleSymmetry, BACncol, ACD, SupplementaryAngles_DEF; âˆ¡ B C D â‰¡ Î³ by H2, -, SupplementUnique; qed by ABClessDCB, H1, AngleSymmetry, angÎ³, -, AngleTrichotomy2; `;; let EuclidPropositionI_18 = thm `; let A B C be point; assume Â¬Collinear A B C [H1]; assume seg A C <__ seg A B [H2]; thus âˆ¡ A B C <_ang âˆ¡ B C A proof Â¬(A = B) âˆ§ Â¬(A = C) [Distinct] by H1, NonCollinearImpliesDistinct; consider D such that D âˆˆ open (A,B) âˆ§ seg A C â‰¡ seg A D [ADB] by Distinct, SEGMENT, H2, SegmentOrderingUse; Â¬(D = A) âˆ§ Â¬(D = B) âˆ§ D âˆˆ open (B,A) âˆ§ Collinear A D B âˆ§ ray B D = ray B A [ADB'] by -, B1', IntervalRay; D âˆˆ int_angle A C B [DintACB] by H1, CollinearSymmetry, ADB, ConverseCrossbar; Â¬Collinear D A C âˆ§ Â¬Collinear C B D [DACncol] by H1, CollinearSymmetry, ADB', NoncollinearityExtendsToLine; seg A D â‰¡ seg A C by ADB', Distinct, SEGMENT, ADB, C2Symmetric; âˆ¡ C D A â‰¡ âˆ¡ A C D by DACncol, -, IsoscelesCongBaseAngles, AngleSymmetry; âˆ¡ C D A <_ang âˆ¡ A C B [CDAlessACB] by DACncol, CollinearSymmetry, ANGLE, H1, CollinearSymmetry, DintACB, -, AngleOrdering_DEF; âˆ¡ B D C suppl âˆ¡ C D A by DACncol, CollinearSymmetry, ADB', SupplementaryAngles_DEF; âˆ¡ C B D <_ang âˆ¡ C D A by DACncol, -, EuclidPropositionI_17; âˆ¡ C B D <_ang âˆ¡ A C B by -, CDAlessACB, AngleOrderTransitivity; qed by -, ADB', Angle_DEF, AngleSymmetry; `;; let EuclidPropositionI_19 = thm `; let A B C be point; assume Â¬Collinear A B C [H1]; assume âˆ¡ A B C <_ang âˆ¡ B C A [H2]; thus seg A C <__ seg A B proof Â¬Collinear B A C âˆ§ Â¬Collinear B C A âˆ§ Â¬Collinear A C B [BACncol] by H1, CollinearSymmetry; Â¬(A = B) âˆ§ Â¬(A = C) [Distinct] by H1, NonCollinearImpliesDistinct; assume Â¬(seg A C <__ seg A B); seg A B â‰¡ seg A C âˆ¨ seg A B <__ seg A C by Distinct, SEGMENT, -, SegmentTrichotomy; cases by -; suppose seg A B â‰¡ seg A C; âˆ¡ C B A â‰¡ âˆ¡ B C A by BACncol, -, IsoscelesCongBaseAngles; qed by -, AngleSymmetry, H2, AngleTrichotomy1; suppose seg A B <__ seg A C; âˆ¡ A C B <_ang âˆ¡ C B A by BACncol, -, EuclidPropositionI_18; qed by H1, BACncol, ANGLE, -, AngleSymmetry, H2, AngleTrichotomy; end; `;; let EuclidPropositionI_20 = thm `; let A B C D be point; assume Â¬Collinear A B C [H1]; assume A âˆˆ open (B,D) âˆ§ seg A D â‰¡ seg A C [H2]; thus seg B C <__ seg B D proof Â¬(B = D) âˆ§ Â¬(A = D) âˆ§ A âˆˆ open (D,B) âˆ§ Collinear B A D âˆ§ ray D A = ray D B [BAD'] by H2, B1', IntervalRay; Â¬Collinear C A D [CADncol] by H1, CollinearSymmetry, BAD', NoncollinearityExtendsToLine; Â¬Collinear D C B âˆ§ Â¬Collinear B D C [DCBncol] by H1, CollinearSymmetry, BAD', NoncollinearityExtendsToLine; :: 13 Angle (âˆ¡ C D A) [angCDA] by CADncol, CollinearSymmetry, ANGLE; âˆ¡ C D A â‰¡ âˆ¡ D C A [CDAeqDCA] by CADncol, CollinearSymmetry, H2, IsoscelesCongBaseAngles; A âˆˆ int_angle D C B by DCBncol, BAD', ConverseCrossbar; âˆ¡ C D A <_ang âˆ¡ D C B by angCDA, DCBncol, -, CDAeqDCA, AngleOrdering_DEF; âˆ¡ B D C <_ang âˆ¡ D C B by -, BAD', Angle_DEF, AngleSymmetry; qed by DCBncol, -, EuclidPropositionI_19; `;; let EuclidPropositionI_21 = thm `; let A B C D be point; assume Â¬Collinear A B C [H1]; assume D âˆˆ int_triangle A B C [H2]; thus âˆ¡ A B C <_ang âˆ¡ C D A proof Â¬(B = A) âˆ§ Â¬(B = C) âˆ§ Â¬(A = C) [Distinct] by H1, NonCollinearImpliesDistinct; D âˆˆ int_angle B A C âˆ§ D âˆˆ int_angle C B A [DintTri] by H2, IN_InteriorTriangle, InteriorAngleSymmetry; consider E such that E âˆˆ open (B,C) âˆ§ E âˆˆ ray A D â” A [BEC] by -, Crossbar_THM; Â¬(B = E) âˆ§ Â¬(E = C) âˆ§ Collinear B E C âˆ§ Collinear A D E [BEC'] by -, B1', IN_DELETE, IN_Ray; ray B E = ray B C âˆ§ E âˆˆ ray B C â” B [rBErBC] by BEC, IntervalRay, IntervalRayEZ; D âˆˆ int_angle A B E [DintABE] by DintTri, -, InteriorAngleSymmetry, InteriorWellDefined; D âˆˆ open (A,E) [ADE] by BEC', -, AlternateConverseCrossbar; ray E D = ray E A [rEDrEA] by -, B1', IntervalRay; Â¬Collinear A B E âˆ§ Â¬Collinear B E A âˆ§ Â¬Collinear C B D âˆ§ Â¬(A = D) [ABEncol] by DintABE, IN_InteriorAngle, CollinearSymmetry, DintTri, InteriorEZHelp; Â¬Collinear E D C âˆ§ Â¬Collinear C E D [EDCncol] by -, CollinearSymmetry, BEC', NoncollinearityExtendsToLine; âˆ¡ A B E <_ang âˆ¡ A E C by ABEncol, BEC, ExteriorAngle; âˆ¡ A B C <_ang âˆ¡ C E D [ABClessAEC] by -, rBErBC, rEDrEA, Angle_DEF, AngleSymmetry; âˆ¡ C E D <_ang âˆ¡ C D A by EDCncol, ADE, B1', ExteriorAngle; qed by ABClessAEC, -, AngleOrderTransitivity; `;; let AngleTrichotomy3 = thm `; let Î± Î² Î³ be point_set; assume Î± <_ang Î² âˆ§ Angle Î³ âˆ§ Î³ â‰¡ Î± [H1]; thus Î³ <_ang Î² proof 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 H1, AngleOrdering_DEF; Â¬Collinear A O G by -, InteriorEZHelp; Î³ â‰¡ âˆ¡ A O G by H1, H1', -, ANGLE, C5Transitive; qed by H1, H1', -, AngleOrdering_DEF; `;; let InteriorCircleConvexHelp = thm `; let O A B C be point; assume Â¬Collinear A O C [H1]; assume B âˆˆ open (A,C) [H2]; assume seg O A <__ seg O C âˆ¨ seg O A â‰¡ seg O C [H3]; thus seg O B <__ seg O C proof Â¬Collinear O C A âˆ§ Â¬Collinear C O A âˆ§ Â¬(O = A) âˆ§ Â¬(O = C) [H1'] by H1, CollinearSymmetry, NonCollinearImpliesDistinct; ray A B = ray A C âˆ§ ray C B = ray C A [equal_rays] by H2, IntervalRay, B1'; âˆ¡ O C A <_ang âˆ¡ C A O âˆ¨ âˆ¡ O C A â‰¡ âˆ¡ C A O proof cases by H3; suppose seg O A <__ seg O C; qed by H1', -, EuclidPropositionI_18; suppose seg O A â‰¡ seg O C [seg_eq]; seg O C â‰¡ seg O A by H1', SEGMENT, -, C2Symmetric; qed by H1', -, IsoscelesCongBaseAngles, AngleSymmetry; end; âˆ¡ O C B <_ang âˆ¡ B A O âˆ¨ âˆ¡ O C B â‰¡ âˆ¡ B A O by -, equal_rays, Angle_DEF; âˆ¡ B C O <_ang âˆ¡ O A B âˆ¨ âˆ¡ B C O â‰¡ âˆ¡ O A B [BCOlessOAB] by -, AngleSymmetry; Â¬Collinear O A B âˆ§ Â¬Collinear B C O âˆ§ Â¬Collinear O C B [OABncol] by H1, CollinearSymmetry, H2, B1', NoncollinearityExtendsToLine; âˆ¡ O A B <_ang âˆ¡ O B C by -, H2, ExteriorAngle; âˆ¡ B C O <_ang âˆ¡ O B C by BCOlessOAB, -, AngleOrderTransitivity, OABncol, ANGLE, -, AngleTrichotomy3; qed by OABncol, -, AngleSymmetry, EuclidPropositionI_19; `;; let InteriorCircleConvex = thm `; let O R A B C be point; assume Â¬(O = R) [H1]; assume B âˆˆ open (A,C) [H2]; assume A âˆˆ int_circle O R âˆ§ C âˆˆ int_circle O R [H3]; thus B âˆˆ int_circle O R proof Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ B âˆˆ open (C,A) [H2'] by H2, B1'; (A = O âˆ¨ seg O A <__ seg O R) âˆ§ (C = O âˆ¨ seg O C <__ seg O R) [ACintOR] by H3, H1, IN_InteriorCircle; cases; suppose O = A âˆ¨ O = C; B âˆˆ open (O,C) âˆ¨ B âˆˆ open (O,A) by -, H2, B1'; seg O B <__ seg O A âˆ§ Â¬(O = A) âˆ¨ seg O B <__ seg O C âˆ§ Â¬(O = C) by -, B1', SEGMENT, C2Reflexive, SegmentOrdering_DEF; seg O B <__ seg O R by -, ACintOR, SegmentOrderTransitivity; qed by -, H1, IN_InteriorCircle; suppose Â¬(O = A) âˆ§ Â¬(O = C) [OnotAC]; cases; suppose Â¬Collinear A O C [AOCncol]; seg O A <__ seg O C âˆ¨ seg O A â‰¡ seg O C âˆ¨ seg O C <__ seg O A by OnotAC, SEGMENT, SegmentTrichotomy; seg O B <__ seg O C âˆ¨ seg O B <__ seg O A by AOCncol, H2, -, InteriorCircleConvexHelp, CollinearSymmetry, B1'; qed by OnotAC, ACintOR, -, SegmentOrderTransitivity, H1, IN_InteriorCircle; suppose Collinear A O C [AOCcol]; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l by H2', I1; Collinear B A O âˆ§ Collinear B C O [OABCcol] by -, H2, BetweenLinear, H2', AOCcol, CollinearLinear, Collinear_DEF; B âˆ‰ open (O,A) âˆ§ B âˆ‰ open (O,C) â‡’ B = O proof assume B âˆ‰ open (O,A) âˆ§ B âˆ‰ open (O,C); O âˆˆ ray B A âˆ© ray B C by H2', OABCcol, -, IN_Ray, IN_INTER; qed by -, H2, OppositeRaysIntersect1point, IN_SING; B âˆˆ open (O,A) âˆ¨ B âˆˆ open (O,C) âˆ¨ B = O by -, âˆ‰; seg O B <__ seg O A âˆ¨ seg O B <__ seg O C âˆ¨ B = O by -, B1', SEGMENT, C2Reflexive, SegmentOrdering_DEF; seg O B <__ seg O R âˆ¨ B = O by -, ACintOR, OnotAC, SegmentOrderTransitivity; qed by -, H1, IN_InteriorCircle; end; end; `;; let SegmentTrichotomy3 = thm `; let s t u be point_set; assume s <__ t âˆ§ Segment u âˆ§ u â‰¡ s [H1]; thus u <__ t proof consider C D X such that Segment s âˆ§ t = seg C D âˆ§ X âˆˆ open (C,D) âˆ§ s â‰¡ seg C X âˆ§ Â¬(C = X) [H1'] by H1, SegmentOrdering_DEF, B1'; u â‰¡ seg C X by H1, -, SEGMENT, C2Transitive; qed by H1, H1', -, SegmentOrdering_DEF; `;; let EuclidPropositionI_24Help = thm `; let O A C O' D F be point; assume Â¬Collinear A O C âˆ§ Â¬Collinear D O' F [H1]; assume seg O' D â‰¡ seg O A âˆ§ seg O' F â‰¡ seg O C [H2]; assume âˆ¡ D O' F <_ang âˆ¡ A O C [H3]; assume seg O A <__ seg O C âˆ¨ seg O A â‰¡ seg O C [H4]; thus seg D F <__ seg A C proof consider K such that K âˆˆ int_angle A O C âˆ§ âˆ¡ D O' F â‰¡ âˆ¡ A O K [KintAOC] by H1, ANGLE, H3, AngleOrderingUse; Â¬(O = C) âˆ§ Â¬(D = F) âˆ§ Â¬(O' = F) âˆ§ Â¬(O = K) [Distinct] by H1, NonCollinearImpliesDistinct, -, InteriorEZHelp; consider B such that B âˆˆ ray O K â” O âˆ§ seg O B â‰¡ seg O C [BrOK] by Distinct, SEGMENT, -, C1; ray O B = ray O K by Distinct, -, RayWellDefined; âˆ¡ D O' F â‰¡ âˆ¡ A O B [DO'FeqAOB] by KintAOC, -, Angle_DEF; B âˆˆ int_angle A O C [BintAOC] by KintAOC, BrOK, WholeRayInterior; Â¬(B = O) âˆ§ Â¬Collinear A O B [AOBncol] by -, InteriorEZHelp; seg O C â‰¡ seg O B [OCeqOB] by Distinct, -, SEGMENT, BrOK, C2Symmetric; seg O' F â‰¡ seg O B by Distinct, SEGMENT, AOBncol, H2, -, C2Transitive; D,O',F â‰… A,O,B by H1, AOBncol, H2, -, DO'FeqAOB, SAS; seg D F â‰¡ seg A B [DFeqAB] by -, TriangleCong_DEF; consider G such that G âˆˆ open (A,C) âˆ§ G âˆˆ ray O B â” O âˆ§ Â¬(G = O) [AGC] by BintAOC, Crossbar_THM, B1', IN_DELETE; Segment (seg O G) âˆ§ Â¬(O = B) [notOB] by AGC, SEGMENT, BrOK, IN_DELETE; seg O G <__ seg O C by H1, AGC, H4, InteriorCircleConvexHelp; seg O G <__ seg O B by -, OCeqOB, BrOK, IN_DELETE, SEGMENT, SegmentTrichotomy2; consider G' such that G' âˆˆ open (O,B) âˆ§ seg O G â‰¡ seg O G' [OG'B] by notOB, -, SegmentOrderingUse; Â¬(G' = O) âˆ§ seg O G' â‰¡ seg O G' âˆ§ Segment (seg O G') [notG'O] by -, B1', SEGMENT, C2Reflexive, SEGMENT; G' âˆˆ ray O B â” O by OG'B, IntervalRayEZ; G' = G âˆ§ G âˆˆ open (B,O) by notG'O, notOB, -, AGC, OG'B, C1, B1'; ConvexQuadrilateral B A O C by H1, -, AGC, DiagonalsIntersectImpliesConvexQuad; A âˆˆ int_angle O C B âˆ§ O âˆˆ int_angle C B A âˆ§ Quadrilateral B A O C [OintCBA] by -, ConvexQuad_DEF; A âˆˆ int_angle B C O [AintBCO] by -, InteriorAngleSymmetry; Tetralateral B A O C by OintCBA, Quadrilateral_DEF; Â¬Collinear C B A âˆ§ Â¬Collinear B C O âˆ§ Â¬Collinear C O B âˆ§ Â¬Collinear C B O [BCOncol] by -, Tetralateral_DEF, CollinearSymmetry; âˆ¡ B C O â‰¡ âˆ¡ C B O [BCOeqCBO] by -, OCeqOB, IsoscelesCongBaseAngles; Â¬Collinear B C A âˆ§ Â¬Collinear A C B [ACBncol] by AintBCO, InteriorEZHelp, CollinearSymmetry; âˆ¡ B C A â‰¡ âˆ¡ B C A âˆ§ Angle (âˆ¡ B C A) âˆ§ âˆ¡ C B O â‰¡ âˆ¡ C B O [CBOref] by -, ANGLE, BCOncol, C5Reflexive; âˆ¡ B C A <_ang âˆ¡ B C O by -, BCOncol, ANGLE, AintBCO, AngleOrdering_DEF; âˆ¡ B C A <_ang âˆ¡ C B O [BCAlessCBO] by -, BCOncol, ANGLE, BCOeqCBO, AngleTrichotomy2; âˆ¡ C B O <_ang âˆ¡ C B A by BCOncol, ANGLE, OintCBA, CBOref, AngleOrdering_DEF; âˆ¡ A C B <_ang âˆ¡ C B A by BCAlessCBO, -, AngleOrderTransitivity, AngleSymmetry; seg A B <__ seg A C by ACBncol, -, EuclidPropositionI_19; qed by -, Distinct, SEGMENT, DFeqAB, SegmentTrichotomy3; `;; let EuclidPropositionI_24 = thm `; let O A C O' D F be point; assume Â¬Collinear A O C âˆ§ Â¬Collinear D O' F [H1]; assume seg O' D â‰¡ seg O A âˆ§ seg O' F â‰¡ seg O C [H2]; assume âˆ¡ D O' F <_ang âˆ¡ A O C [H3]; thus seg D F <__ seg A C proof Â¬(O = A) âˆ§ Â¬(O = C) âˆ§ Â¬Collinear C O A âˆ§ Â¬Collinear F O' D [Distinct] by H1, NonCollinearImpliesDistinct, CollinearSymmetry; seg O A â‰¡ seg O C âˆ¨ seg O A <__ seg O C âˆ¨ seg O C <__ seg O A by -, SEGMENT, SegmentTrichotomy; cases by -; suppose seg O A <__ seg O C âˆ¨ seg O A â‰¡ seg O C; qed by H1, H2, H3, -, EuclidPropositionI_24Help; suppose seg O C <__ seg O A [H4]; âˆ¡ F O' D <_ang âˆ¡ C O A by H3, AngleSymmetry; qed by Distinct, H3, AngleSymmetry, H2, H4, EuclidPropositionI_24Help, SegmentSymmetry; end; `;; let EuclidPropositionI_25 = thm `; let O A C O' D F be point; assume Â¬Collinear A O C âˆ§ Â¬Collinear D O' F [H1]; assume seg O' D â‰¡ seg O A âˆ§ seg O' F â‰¡ seg O C [H2]; assume seg D F <__ seg A C [H3]; thus âˆ¡ D O' F <_ang âˆ¡ A O C proof Â¬(O = A) âˆ§ Â¬(O = C) âˆ§ Â¬(A = C) âˆ§ Â¬(D = F) âˆ§ Â¬(O' = D) âˆ§ Â¬(O' = F) [Distinct] by H1, NonCollinearImpliesDistinct; assume Â¬(âˆ¡ D O' F <_ang âˆ¡ A O C); âˆ¡ D O' F â‰¡ âˆ¡ A O C âˆ¨ âˆ¡ A O C <_ang âˆ¡ D O' F by H1, ANGLE, -, AngleTrichotomy; cases by -; suppose âˆ¡ D O' F â‰¡ âˆ¡ A O C; D,O',F â‰… A,O,C by H1, H2, -, SAS; seg D F â‰¡ seg A C by -, TriangleCong_DEF; qed by Distinct, SEGMENT, -, H3, SegmentTrichotomy; suppose âˆ¡ A O C <_ang âˆ¡ D O' F [Con]; seg O A â‰¡ seg O' D âˆ§ seg O C â‰¡ seg O' F [H2'] by Distinct, SEGMENT, H2, C2Symmetric; seg A C <__ seg D F by H1, -, Con, EuclidPropositionI_24; qed by Distinct, SEGMENT, -, H3, SegmentTrichotomy; end; `;; let AAS = thm `; let A B C A' B' C' be point; assume Â¬Collinear A B C âˆ§ Â¬Collinear A' B' C' [H1]; assume âˆ¡ A B C â‰¡ âˆ¡ A' B' C' âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B' C' A' [H2]; assume seg A B â‰¡ seg A' B' [H3]; thus A,B,C â‰… A',B',C' proof Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬(B' = C') [Distinct] by H1, NonCollinearImpliesDistinct; consider G such that G âˆˆ ray B C â” B âˆ§ seg B G â‰¡ seg B' C' [Gexists] by Distinct, SEGMENT, C1; Â¬(G = B) âˆ§ B âˆ‰ open (G,C) âˆ§ Collinear G B C [notGBC] by -, IN_DELETE, IN_Ray, CollinearSymmetry; Â¬Collinear A B G âˆ§ Â¬Collinear B G A [ABGncol] by H1, notGBC, CollinearSymmetry, NoncollinearityExtendsToLine; ray B G = ray B C by Distinct, Gexists, RayWellDefined; âˆ¡ A B G = âˆ¡ A B C by Distinct, -, Angle_DEF; A,B,G â‰… A',B',C' [ABGâ‰…A'B'C'] by H1, ABGncol, H3, SegmentSymmetry, H2, -, Gexists, SAS; âˆ¡ B G A â‰¡ âˆ¡ B' C' A' [BGAeqB'C'A'] by -, TriangleCong_DEF; Â¬Collinear B C A âˆ§ Â¬Collinear B' C' A' [BCAncol] by H1, CollinearSymmetry; âˆ¡ B' C' A' â‰¡ âˆ¡ B C A âˆ§ âˆ¡ B C A â‰¡ âˆ¡ B C A [BCArefl] by -, ANGLE, H2, C5Symmetric, C5Reflexive; âˆ¡ B G A â‰¡ âˆ¡ B C A [BGAeqBCA] by ABGncol, BCAncol, ANGLE, BGAeqB'C'A', -, C5Transitive; cases; suppose G = C; qed by -, ABGâ‰…A'B'C'; suppose Â¬(G = C) [notGC]; Â¬Collinear A C G âˆ§ Â¬Collinear A G C [ACGncol] by H1, notGBC, -, CollinearSymmetry, NoncollinearityExtendsToLine; C âˆˆ open (B,G) âˆ¨ G âˆˆ open (C,B) by notGBC, notGC, Distinct, B3', âˆ‰; cases by -; suppose C âˆˆ open (B,G) ; C âˆˆ open (G,B) âˆ§ ray G C = ray G B [rGCrBG] by -, B1', IntervalRay; âˆ¡ A G C <_ang âˆ¡ A C B by ACGncol, -, ExteriorAngle; âˆ¡ B G A <_ang âˆ¡ B C A by -, rGCrBG, Angle_DEF, AngleSymmetry, AngleSymmetry; qed by ABGncol, BCAncol, ANGLE, -, AngleSymmetry, BGAeqBCA, AngleTrichotomy; suppose G âˆˆ open (C,B) [CGB]; ray C G = ray C B âˆ§ âˆ¡ A C G <_ang âˆ¡ A G B by -, IntervalRay, ACGncol, ExteriorAngle; âˆ¡ A C B <_ang âˆ¡ B G A by -, Angle_DEF, AngleSymmetry; âˆ¡ B C A <_ang âˆ¡ B C A by -, BCAncol, ANGLE, BGAeqBCA, AngleTrichotomy2, AngleSymmetry; qed by -, BCArefl, AngleTrichotomy1; end; end; `;; let ParallelSymmetry = thm `; âˆ€ l k: point_set. l âˆ¥ k â‡’ k âˆ¥ l by PARALLEL, INTER_COMM; `;; let AlternateInteriorAngles = thm `; let A B C E be point; let l m t be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ E âˆˆ l [l_line]; assume Line m âˆ§ B âˆˆ m âˆ§ C âˆˆ m [m_line]; assume Line t âˆ§ A âˆˆ t âˆ§ B âˆˆ t [t_line]; assume Â¬(A = E) âˆ§ Â¬(B = C) âˆ§ Â¬(A = B) âˆ§ E âˆ‰ t âˆ§ C âˆ‰ t [Distinct]; assume Â¬(C,E same_side t) [Cnsim_tE]; assume âˆ¡ E A B â‰¡ âˆ¡ C B A [AltIntAngCong]; thus l âˆ¥ m proof Â¬Collinear E A B âˆ§ Â¬Collinear C B A [EABncol] by t_line, Distinct, I1, Collinear_DEF, âˆ‰; B âˆ‰ l âˆ§ A âˆ‰ m [notAmBl] by l_line, m_line, Collinear_DEF, -, âˆ‰; assume Â¬(l âˆ¥ m); Â¬(l âˆ© m = âˆ…) by -, l_line, m_line, PARALLEL; consider G such that G âˆˆ l âˆ§ G âˆˆ m [Glm] by -, 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 -, notAmBl, âˆ‰, m_line, l_line, Collinear_DEF; Â¬Collinear A G B âˆ§ Â¬Collinear B G A âˆ§ G âˆ‰ t [AGBncol] by EABncol, CollinearSymmetry, -, NoncollinearityExtendsToLine, t_line, Collinear_DEF, âˆ‰; Â¬(E,C same_side t) [Ensim_tC] by t_line, -, Distinct, Cnsim_tE, SameSideSymmetric; C âˆˆ m â” B âˆ§ G âˆˆ m â” B [CGm_B] by m_line, Glm, Distinct, GnotAB, IN_DELETE; E âˆˆ l â” A âˆ§ G âˆˆ l â” A [EGm_A] by l_line, Glm, Distinct, GnotAB, IN_DELETE; Â¬(G,E same_side t) proof assume G,E same_side t [Gsim_tE]; A âˆ‰ open (G,E) [notGAE] by t_line, -, SameSide_DEF, âˆ‰; G âˆˆ ray A E â” A by Distinct, GnotAB, notGAE, IN_Ray, GnotAB, IN_DELETE; ray A G = ray A E [rAGrAE] by Distinct, -, RayWellDefined; Â¬(C,G same_side t) by t_line, AGBncol, Distinct, Gsim_tE, Cnsim_tE, SameSideTransitive; C âˆ‰ ray B G âˆ§ B âˆˆ open (C,G) by t_line, AGBncol, Distinct, -, RaySameSide, âˆ‰, GnotAB, IN_DELETE, IN_Ray; âˆ¡ G A B <_ang âˆ¡ C B A by AGBncol, -, B1', EuclidPropositionI_16; âˆ¡ E A B <_ang âˆ¡ C B A by -, rAGrAE, Angle_DEF; qed by EABncol, ANGLE, AltIntAngCong, -, AngleTrichotomy1; G,C same_side t [Gsim_tC] by t_line, AGBncol, Distinct, -, Cnsim_tE, AtMost2Sides; :: now we make a symmetric argument B âˆ‰ open (G,C) [notGBC] by t_line, -, SameSide_DEF, âˆ‰; G âˆˆ ray B C â” B by Distinct, GnotAB, notGBC, IN_Ray, GnotAB, IN_DELETE; ray B G = ray B C [rBGrBC] by Distinct, -, RayWellDefined; âˆ¡ C B A â‰¡ âˆ¡ E A B [flipAltIntAngCong] by EABncol, ANGLE, AltIntAngCong, C5Symmetric; Â¬(E,G same_side t) by t_line, AGBncol, Distinct, Gsim_tC, Ensim_tC, SameSideTransitive; E âˆ‰ ray A G âˆ§ A âˆˆ open (E,G) by t_line, AGBncol, Distinct, -, RaySameSide, âˆ‰, GnotAB, IN_Ray, IN_DELETE; âˆ¡ G B A <_ang âˆ¡ E A B by AGBncol, -, B1', EuclidPropositionI_16; âˆ¡ C B A <_ang âˆ¡ E A B by -, rBGrBC, Angle_DEF; qed by EABncol, ANGLE, flipAltIntAngCong, -, AngleTrichotomy1; `;; let EuclidPropositionI_28 = thm `; let A B C D E F G H be point; let l m t be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ B âˆˆ l âˆ§ G âˆˆ l [l_line]; assume Line m âˆ§ C âˆˆ m âˆ§ D âˆˆ m âˆ§ H âˆˆ m [m_line]; assume Line t âˆ§ G âˆˆ t âˆ§ H âˆˆ t [t_line]; assume G âˆ‰ m âˆ§ H âˆ‰ l [notGmHl]; assume G âˆˆ open (A,B) âˆ§ H âˆˆ open (C,D) [H1]; assume G âˆˆ open (E,H) âˆ§ H âˆˆ open (F,G) [H2]; assume Â¬(D,A same_side t) [H3]; assume âˆ¡ E G B â‰¡ âˆ¡ G H D âˆ¨ âˆ¡ B G H suppl âˆ¡ G H D [H4]; thus l âˆ¥ m proof Â¬(A = G) âˆ§ Â¬(G = B) âˆ§ Â¬(H = D) âˆ§ Â¬(E = G) âˆ§ Â¬(G = H) âˆ§ Collinear A G B âˆ§ Collinear E G H [Distinct] by H1, H2, B1'; Â¬Collinear H G A âˆ§ Â¬Collinear G H D âˆ§ A âˆ‰ t âˆ§ D âˆ‰ t [HGAncol] by l_line, m_line, Distinct, I1, Collinear_DEF, notGmHl, âˆ‰, t_line, Collinear_DEF; Â¬Collinear B G H âˆ§ Â¬Collinear A G E âˆ§ Â¬Collinear E G B [BGHncol] by -, Distinct, CollinearSymmetry, NoncollinearityExtendsToLine; âˆ¡ A G H â‰¡ âˆ¡ D H G proof cases by H4; suppose âˆ¡ E G B â‰¡ âˆ¡ G H D [EGBeqGHD]; âˆ¡ E G B â‰¡ âˆ¡ H G A by BGHncol, H1, H2, VerticalAnglesCong; âˆ¡ H G A â‰¡ âˆ¡ E G B by BGHncol, HGAncol, ANGLE, -, C5Symmetric; âˆ¡ H G A â‰¡ âˆ¡ G H D by BGHncol, HGAncol, ANGLE, -, EGBeqGHD, C5Transitive; qed by -, AngleSymmetry; suppose âˆ¡ B G H suppl âˆ¡ G H D [BGHeqGHD]; âˆ¡ B G H suppl âˆ¡ H G A by BGHncol, H1, B1', SupplementaryAngles_DEF; qed by -, BGHeqGHD, AngleSymmetry, SupplementUnique, AngleSymmetry; end; qed by l_line, m_line, t_line, Distinct, HGAncol, H3, -, AlternateInteriorAngles; `;; let OppositeSidesCongImpliesParallelogram = thm `; let A B C D be point; assume Quadrilateral A B C D [H1]; assume seg A B â‰¡ seg C D âˆ§ seg B C â‰¡ seg D A [H2]; thus Parallelogram A B C D proof Â¬(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 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 TetraABCD, I1; consider b d such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [bd_line] by TetraABCD, I1; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line] by TetraABCD, I1; consider m such that Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [m_line] by TetraABCD, I1; B âˆ‰ l âˆ§ D âˆ‰ l âˆ§ A âˆ‰ m âˆ§ C âˆ‰ m [notBDlACm] by l_line, m_line, TetraABCD, Collinear_DEF, âˆ‰; seg A C â‰¡ seg C A âˆ§ seg B D â‰¡ seg D B [seg_refl] by TetraABCD, SEGMENT, C2Reflexive, SegmentSymmetry; A,B,C â‰… C,D,A by TetraABCD, H2, -, SSS; âˆ¡ B C A â‰¡ âˆ¡ D A C âˆ§ âˆ¡ C A B â‰¡ âˆ¡ A C D [BCAeqDAC] by -, TriangleCong_DEF; seg C D â‰¡ seg A B [CDeqAB] by TetraABCD, SEGMENT, H2, C2Symmetric; B,C,D â‰… D,A,B by TetraABCD, H2, -, seg_refl, SSS; âˆ¡ C D B â‰¡ âˆ¡ A B D âˆ§ âˆ¡ D B C â‰¡ âˆ¡ B D A [CDBeqABD] by -, TriangleCong_DEF; Â¬(B,D same_side l) âˆ¨ Â¬(A,C same_side m) by H1, l_line, m_line, FiveChoicesQuadrilateral; cases by -; suppose Â¬(B,D same_side l); Â¬(D,B same_side l) by l_line, notBDlACm, -, SameSideSymmetric; a âˆ¥ c âˆ§ b âˆ¥ d by ac_line, l_line, TetraABCD, notBDlACm, -, BCAeqDAC, AngleSymmetry, AlternateInteriorAngles, bd_line, BCAeqDAC; qed by H1, ac_line, bd_line, -, Parallelogram_DEF; suppose Â¬(A,C same_side m); b âˆ¥ d âˆ§ c âˆ¥ a by bd_line, m_line, TetraABCD, notBDlACm, -, CDBeqABD, AngleSymmetry, AlternateInteriorAngles, ac_line, CDBeqABD; qed by H1, ac_line, bd_line, -, ParallelSymmetry, Parallelogram_DEF; end; `;; let OppositeAnglesCongImpliesParallelogramHelp = thm `; let A B C D be point; let a c be point_set; assume Quadrilateral A B C D [H1]; assume âˆ¡ A B C â‰¡ âˆ¡ C D A âˆ§ âˆ¡ D A B â‰¡ âˆ¡ B C D [H2]; assume Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line]; assume Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c [c_line]; thus a âˆ¥ c proof Â¬(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 H1, Quadrilateral_DEF, Tetralateral_DEF; âˆ¡ C D A â‰¡ âˆ¡ A B C âˆ§ âˆ¡ B C D â‰¡ âˆ¡ D A B [H2'] by TetraABCD, ANGLE, H2, C5Symmetric; consider l m such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l âˆ§ Line m âˆ§ B âˆˆ m âˆ§ D âˆˆ m [lm_line] by TetraABCD, I1; consider b d such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b âˆ§ Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [bd_line] by TetraABCD, I1; A âˆ‰ c âˆ§ B âˆ‰ c âˆ§ A âˆ‰ b âˆ§ D âˆ‰ b âˆ§ B âˆ‰ d âˆ§ C âˆ‰ d [point_off_line] by 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; âˆ¡ 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 TetraABCD, -, EuclidPropositionI_21; qed by -, H2', H2, AngleTrichotomy1; ConvexQuadrilateral A B C D by 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 -, ConvexQuad_DEF; B,A same_side c âˆ§ B,C same_side d [Bsim_cA] by c_line, bd_line, -, InteriorUse; A,D same_side b [Asim_bD] by bd_line, c_line, AintBCD, InteriorUse; assume Â¬(a âˆ¥ c); consider G such that G âˆˆ a âˆ§ G âˆˆ c [Gac] by -, a_line, c_line, PARALLEL, MEMBER_NOT_EMPTY, IN_INTER; Collinear A B G âˆ§ Collinear D G C âˆ§ Collinear C G D [ABGcol] by a_line, -, Collinear_DEF, c_line; Â¬(G = A) âˆ§ Â¬(G = B) âˆ§ Â¬(G = C) âˆ§ Â¬(G = D) [GnotABCD] by Gac, ABGcol, TetraABCD, CollinearSymmetry, Collinear_DEF; Â¬Collinear B G C âˆ§ Â¬Collinear A D G [BGCncol] by c_line, Gac, GnotABCD, I1, Collinear_DEF, point_off_line, âˆ‰; Â¬Collinear B C G âˆ§ Â¬Collinear G B C âˆ§ Â¬Collinear G A D âˆ§ Â¬Collinear A G D [BCGncol] by -, CollinearSymmetry; G âˆ‰ b âˆ§ G âˆ‰ d [notGb] by bd_line, Collinear_DEF, BGCncol, âˆ‰; G âˆ‰ open (B,A) [notBGA] by Bsim_cA, Gac, SameSide_DEF, âˆ‰; B âˆ‰ open (A,G) [notABG] proof assume Â¬(B âˆ‰ open (A,G)); B âˆˆ open (A,G) [ABG] by -, âˆ‰; ray A B = ray A G [rABrAG] by -, IntervalRay; Â¬(A,G same_side b) by bd_line, ABG, SameSide_DEF; Â¬(D,G same_side b) by bd_line, point_off_line, notGb, Asim_bD, -, SameSideTransitive; D âˆ‰ ray C G by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, âˆ‰; C âˆˆ open (D,G) [DCG] by GnotABCD, ABGcol, -, IN_Ray, âˆ‰; consider M such that D âˆˆ open (C,M) [CDM] by TetraABCD, B2'; D âˆˆ open (G,M) [GDM] by -, B1', DCG, TransitivityBetweennessHelp; âˆ¡ C D A suppl âˆ¡ A D M âˆ§ âˆ¡ A B C suppl âˆ¡ C B G by TetraABCD, CDM, ABG, SupplementaryAngles_DEF; âˆ¡ M D A â‰¡ âˆ¡ G B C [MDAeqGBC] by -, H2', SupplementsCongAnglesCong, AngleSymmetry; âˆ¡ G A D <_ang âˆ¡ M D A âˆ§ âˆ¡ G B C <_ang âˆ¡ D C B by BCGncol, BGCncol, GDM, DCG, B1', EuclidPropositionI_16; âˆ¡ G A D <_ang âˆ¡ D C B by -, BCGncol, ANGLE, MDAeqGBC, AngleTrichotomy2, AngleOrderTransitivity; âˆ¡ D A B <_ang âˆ¡ B C D by -, rABrAG, Angle_DEF, AngleSymmetry; qed by -, H2, AngleTrichotomy1; A âˆ‰ open (G,B) proof assume Â¬(A âˆ‰ open (G,B)); A âˆˆ open (B,G) [BAG] by -, B1', âˆ‰; ray B A = ray B G [rBArBG] by -, IntervalRay; Â¬(B,G same_side d) by bd_line, BAG, SameSide_DEF; Â¬(C,G same_side d) by bd_line, point_off_line, notGb, Bsim_cA, -, SameSideTransitive; C âˆ‰ ray D G by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, âˆ‰; D âˆˆ open (C,G) [CDG] by GnotABCD, ABGcol, -, IN_Ray, âˆ‰; consider M such that C âˆˆ open (D,M) [DCM] by B2', TetraABCD; C âˆˆ open (G,M) [GCM] by -, B1', CDG, TransitivityBetweennessHelp; âˆ¡ B C D suppl âˆ¡ M C B âˆ§ âˆ¡ D A B suppl âˆ¡ G A D by TetraABCD, CollinearSymmetry, DCM, BAG, SupplementaryAngles_DEF, AngleSymmetry; âˆ¡ M C B â‰¡ âˆ¡ G A D [GADeqMCB] by -, H2', SupplementsCongAnglesCong; âˆ¡ G B C <_ang âˆ¡ M C B âˆ§ âˆ¡ G A D <_ang âˆ¡ C D A by BGCncol, GCM, BCGncol, CDG, B1', EuclidPropositionI_16; âˆ¡ G B C <_ang âˆ¡ C D A by -, BCGncol, ANGLE, GADeqMCB, AngleTrichotomy2, AngleOrderTransitivity; âˆ¡ A B C <_ang âˆ¡ C D A by -, rBArBG, Angle_DEF; qed by -, H2, AngleTrichotomy1; qed by TetraABCD, GnotABCD, ABGcol, notABG, notBGA, -, B3', âˆ‰; `;; let OppositeAnglesCongImpliesParallelogram = thm `; let A B C D be point; assume Quadrilateral A B C D [H1]; assume âˆ¡ A B C â‰¡ âˆ¡ C D A âˆ§ âˆ¡ D A B â‰¡ âˆ¡ B C D [H2]; thus Parallelogram A B C D proof Quadrilateral B C D A [QuadBCDA] by H1, QuadrilateralSymmetry; Â¬(A = B) âˆ§ Â¬(B = C) âˆ§ Â¬(C = D) âˆ§ Â¬(D = A) âˆ§ Â¬Collinear B C D âˆ§ Â¬Collinear D A B [TetraABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF; âˆ¡ B C D â‰¡ âˆ¡ D A B [H2'] by TetraABCD, ANGLE, H2, C5Symmetric; consider a such that Line a âˆ§ A âˆˆ a âˆ§ B âˆˆ a [a_line] by TetraABCD, I1; consider b such that Line b âˆ§ B âˆˆ b âˆ§ C âˆˆ b [b_line] by TetraABCD, I1; consider c such that Line c âˆ§ C âˆˆ c âˆ§ D âˆˆ c [c_line] by TetraABCD, I1; consider d such that Line d âˆ§ D âˆˆ d âˆ§ A âˆˆ d [d_line] by TetraABCD, I1; qed by H1, QuadBCDA, H2, H2', a_line, b_line, c_line, d_line, OppositeAnglesCongImpliesParallelogramHelp, Parallelogram_DEF; `;; let P = new_axiom `âˆ€ P l. Line l âˆ§ P âˆ‰ l â‡’ âˆƒ! m. Line m âˆ§ P âˆˆ m âˆ§ m âˆ¥ l`;; new_constant("Î¼",`:point_set->real`);; let AMa = new_axiom `âˆ€ Î±. Angle Î± â‡’ &0 < Î¼ Î± âˆ§ Î¼ Î± < &180`;; let AMb = new_axiom `âˆ€ Î±. Right Î± â‡’ Î¼ Î± = &90`;; let AMc = new_axiom `âˆ€ Î± Î². Angle Î± âˆ§ Angle Î² âˆ§ Î± â‰¡ Î² â‡’ Î¼ Î± = Î¼ Î²`;; let AMd = new_axiom `âˆ€ A O B P. P âˆˆ int_angle A O B â‡’ Î¼ (âˆ¡ A O B) = Î¼ (âˆ¡ A O P) + Î¼ (âˆ¡ P O B)`;; let ConverseAlternateInteriorAngles = thm `; let A B C E be point; let l m t be point_set; assume Line l âˆ§ A âˆˆ l âˆ§ E âˆˆ l [l_line]; assume Line m âˆ§ B âˆˆ m âˆ§ C âˆˆ m [m_line]; assume Line t âˆ§ A âˆˆ t âˆ§ B âˆˆ t [t_line]; assume Â¬(A = E) âˆ§ Â¬(B = C) âˆ§ Â¬(A = B) âˆ§ E âˆ‰ t âˆ§ C âˆ‰ t [Distinct]; assume Â¬(C,E same_side t) [Cnsim_tE]; assume l âˆ¥ m [para_lm]; thus âˆ¡ E A B â‰¡ âˆ¡ C B A proof Â¬Collinear C B A by t_line, Distinct, I1, Collinear_DEF, âˆ‰, ANGLE; A âˆ‰ m âˆ§ Angle (âˆ¡ C B A) [notAm] by 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 -, Distinct, t_line, C4OppositeSide; consider k such that Line k âˆ§ A âˆˆ k âˆ§ D âˆˆ k [k_line] by Distinct, I1; k âˆ¥ m by -, m_line, t_line, Dexists, Distinct, AngleSymmetry, AlternateInteriorAngles; k = l by m_line, notAm, l_line, k_line, -, para_lm, P; D,E same_side t âˆ§ A âˆ‰ open (D,E) âˆ§ Collinear A E D by t_line, Distinct, Dexists, Cnsim_tE, AtMost2Sides, SameSide_DEF, âˆ‰, -, k_line, l_line, Collinear_DEF; ray A D = ray A E by Distinct, -, IN_Ray, Dexists, IN_DELETE, RayWellDefined; qed by -, Dexists, AngleSymmetry, Angle_DEF; `;; let HilbertTriangleSum = thm `; let A B C be point; assume Â¬Collinear A B C [ABCncol]; thus âˆƒ 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 Â¬(A = B) âˆ§ Â¬(A = C) âˆ§ Â¬(B = C) âˆ§ Â¬Collinear C A B [Distinct] by ABCncol, NonCollinearImpliesDistinct, CollinearSymmetry; consider l such that Line l âˆ§ A âˆˆ l âˆ§ C âˆˆ l [l_line] by Distinct, I1; consider x such that Line x âˆ§ A âˆˆ x âˆ§ B âˆˆ x [x_line] by Distinct, I1; consider y such that Line y âˆ§ B âˆˆ y âˆ§ C âˆˆ y [y_line] by Distinct, I1; C âˆ‰ x [notCx] by x_line, ABCncol, Collinear_DEF, âˆ‰; Angle (âˆ¡ C A B) by 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 -, Distinct, x_line, notCx, C4OppositeSide; consider m such that Line m âˆ§ B âˆˆ m âˆ§ E âˆˆ m [m_line] by -, I1, IN_DELETE; âˆ¡ E B A â‰¡ âˆ¡ C A B [EBAeqCAB] by Eexists, AngleSymmetry; m âˆ¥ l [para_lm] by m_line, l_line, x_line, Eexists, Distinct, notCx, -, AlternateInteriorAngles; m âˆ© l = âˆ… [lm0] by -, PARALLEL; C âˆ‰ m âˆ§ A âˆ‰ m [notACm] by -, l_line, INTER_COMM, DisjointOneNotOther; consider F such that B âˆˆ open (E,F) [EBF] by Eexists, B2'; Â¬(B = F) âˆ§ F âˆˆ m [EBF'] by -, B1', m_line, BetweenLinear; Â¬Collinear A B F âˆ§ F âˆ‰ x [ABFncol] by m_line, -, I1, Collinear_DEF, notACm, âˆ‰, x_line; Â¬(E,F same_side x) âˆ§ Â¬(E,F same_side y) [Ensim_yF] by EBF, x_line, y_line, SameSide_DEF; C,F same_side x [Csim_xF] by x_line, notCx, Eexists, ABFncol, Eexists, -, AtMost2Sides; m âˆ© open(C,A) = âˆ… by l_line, BetweenLinear, SUBSET, SET_RULE, lm0, SUBSET_EMPTY; C,A same_side m by m_line, -, SameSide_DEF, SET_RULE; C âˆˆ int_angle A B F [CintABF] by ABFncol, x_line, m_line, EBF', notCx, notACm, Csim_xF, -, IN_InteriorAngle; A âˆˆ int_angle C B E by EBF, B1', -, InteriorAngleSymmetry, InteriorReflectionInterior; A âˆ‰ y âˆ§ A,E same_side y [Asim_yE] by y_line, m_line, -, InteriorUse; E âˆ‰ y âˆ§ F âˆ‰ y [notEFy] by y_line, m_line, EBF', Eexists, EBF', I1, Collinear_DEF, notACm, âˆ‰; E,A same_side y by y_line, -, Asim_yE, SameSideSymmetric; Â¬(A,F same_side y) [Ansim_yF] by y_line, notEFy, Asim_yE, -, Ensim_yF, SameSideTransitive; âˆ¡ F B C â‰¡ âˆ¡ A C B by m_line, EBF', l_line, y_line, EBF', Distinct, notEFy, Asim_yE, Ansim_yF, para_lm, ConverseAlternateInteriorAngles; qed by EBF, CintABF, EBAeqCAB, -, AngleSymmetry; `;; let EuclidPropositionI_13 = thm `; let A O B A' be point; assume Â¬Collinear A O B [H1]; assume O âˆˆ open (A,A') [H2]; thus Î¼ (âˆ¡ A O B) + Î¼ (âˆ¡ B O A') = &180 proof cases; suppose Right (âˆ¡ A O B); Right (âˆ¡ B O A') âˆ§ Î¼ (âˆ¡ A O B) = &90 âˆ§ Î¼ (âˆ¡ B O A') = &90 by H1, H2, -, RightImpliesSupplRight, AMb; qed by -, REAL_ARITH; suppose Â¬Right (âˆ¡ A O B) [notRightAOB]; Â¬(A = O) âˆ§ Â¬(O = B) [Distinct] by H1, NonCollinearImpliesDistinct; consider l such that Line l âˆ§ O âˆˆ l âˆ§ A âˆˆ l âˆ§ A' âˆˆ l [l_line] by -, I1, H2, BetweenLinear; B âˆ‰ l [notBl] by -, Distinct, I1, Collinear_DEF, H1, âˆ‰; consider F such that Right (âˆ¡ O A F) âˆ§ Angle (âˆ¡ O A F) [RightOAF] by 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 -, Distinct, l_line, notBl, C4; consider E such that Â¬(O = E) âˆ§ E âˆ‰ l âˆ§ E,B same_side l âˆ§ âˆ¡ A O E â‰¡ âˆ¡ O A F [Eexists] by -; Â¬Collinear A O E [AOEncol] by l_line, Distinct, I1, Collinear_DEF, -, âˆ‰; Right (âˆ¡ A O E) [RightAOE] by -, ANGLE, RightOAF, Eexists, CongRightImpliesRight; Right (âˆ¡ E O A') âˆ§ Î¼ (âˆ¡ A O E) = &90 âˆ§ Î¼ (âˆ¡ E O A') = &90 [RightEOA'] by AOEncol, H2, -, RightImpliesSupplRight, AMb; Â¬(âˆ¡ A O B â‰¡ âˆ¡ A O E) by notRightAOB, H1, ANGLE, RightAOE, CongRightImpliesRight; Â¬(âˆ¡ A O B = âˆ¡ A O E) by H1, AOEncol, ANGLE, -, C5Reflexive; Â¬(ray O B = ray O E) by -, Angle_DEF; B âˆ‰ ray O E âˆ§ O âˆ‰ open (B,E) by Distinct, -, Eexists, RayWellDefined, IN_DELETE, âˆ‰, l_line, B1', SameSide_DEF; Â¬Collinear O E B by -, Eexists, IN_Ray, âˆ‰; E âˆˆ int_angle A O B âˆ¨ B âˆˆ int_angle A O E by Distinct, l_line, Eexists, notBl, AngleOrdering, -, CollinearSymmetry, InteriorAngleSymmetry; cases by -; suppose E âˆˆ int_angle A O B [EintAOB]; B âˆˆ int_angle E O A' by H2, -, InteriorReflectionInterior; Î¼ (âˆ¡ A O B) = Î¼ (âˆ¡ A O E) + Î¼ (âˆ¡ E O B) âˆ§ Î¼ (âˆ¡ E O A') = Î¼ (âˆ¡ E O B) + Î¼ (âˆ¡ B O A') by EintAOB, -, AMd; qed by -, RightEOA', REAL_ARITH; suppose B âˆˆ int_angle A O E [BintAOE]; E âˆˆ int_angle B O A' by H2, -, InteriorReflectionInterior; Î¼ (âˆ¡ A O E) = Î¼ (âˆ¡ A O B) + Î¼ (âˆ¡ B O E) âˆ§ Î¼ (âˆ¡ B O A') = Î¼ (âˆ¡ B O E) + Î¼ (âˆ¡ E O A') by BintAOE, -, AMd; qed by -, RightEOA', REAL_ARITH; end; end; `;; let TriangleSum = thm `; let A B C be point; assume Â¬Collinear A B C [ABCncol]; thus Î¼ (âˆ¡ A B C) + Î¼ (âˆ¡ B C A) + Î¼ (âˆ¡ C A B) = &180 proof Â¬Collinear C A B âˆ§ Â¬Collinear B C A [CABncol] by 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 ABCncol, HilbertTriangleSum; Â¬Collinear C B F âˆ§ Â¬Collinear A B F âˆ§ Collinear E B F âˆ§ Â¬(B = E) [CBFncol] by -, InteriorAngleSymmetry, InteriorEZHelp, IN_InteriorAngle, B1', CollinearSymmetry; Â¬Collinear E B A [EBAncol] by CollinearSymmetry, -, NoncollinearityExtendsToLine; Î¼ (âˆ¡ A B F) = Î¼ (âˆ¡ A B C) + Î¼ (âˆ¡ C B F) [Î¼CintABF] by EBF, AMd; Î¼ (âˆ¡ E B A) + Î¼ (âˆ¡ A B F) = &180 [suppl180] by EBAncol, EBF, EuclidPropositionI_13; Î¼ (âˆ¡ C A B) = Î¼ (âˆ¡ E B A) âˆ§ Î¼ (âˆ¡ B C A) = Î¼ (âˆ¡ C B F) by CABncol, EBAncol, CBFncol, ANGLE, EBF, AMc; qed by suppl180, Î¼CintABF, -, REAL_ARITH; `;;let InteriorCircle_DEF = new_definition `âˆ€ O R. int_circle O R = {P | Â¬(O = R) âˆ§ (P = O âˆ¨ seg O P <__ seg O R)} `;;