(* ----------------------------------------------------------------- *)
(* 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 := 150;;

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("cong",(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("NOTIN",(11, "right"));;
parse_as_infix("parallel",(12, "right"));;

let NOTIN = new_definition
  `!a:A l:A->bool. a NOTIN l <=> ~(a IN 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 IN l /\ B IN l /\ C IN l`;;
let SameSide_DEF = new_definition
  `A,B same_side l  <=>
  Line l /\ ~ ? X. (X IN l) /\  X IN open (A,B)`;;
let Ray_DEF = new_definition
  `! A B. ray A B = {X | ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)}`;;
let Ordered_DEF = new_definition
 `ordered A B C D  <=>
  B IN open (A,C) /\ B IN open (A,D) /\ C IN open (A,D) /\ C IN 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 IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
               P NOTIN a /\ P NOTIN 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 IN int_angle A B C  /\
         P IN int_angle B C A  /\
         P IN 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) INTER open (C,D) = {} /\
  open (B,C) INTER open (D,A) = {} `;;
let ConvexQuad_DEF = new_definition
  `ConvexQuadrilateral A B C D  <=>
  Quadrilateral A B C D /\
  A IN int_angle B C D /\ B IN int_angle C D A /\ C IN int_angle D A B /\ D IN int_angle A B C `;;
let Segment_DEF = new_definition
  `seg A B = {A, B} UNION open (A,B)`;;
let SEGMENT = new_definition
  `Segment s  <=>  ? A B. s = seg A B /\ ~(A = B)`;;
let SegmentOrdering_DEF = new_definition
 `s <__ t   <=>
  Segment s /\
  ? C D X. t = seg C D /\ X IN open (C,D) /\ s === seg C X`;;
let Angle_DEF = new_definition
 ` angle A O B = ray O A UNION ray O B `;;
let ANGLE = new_definition
 `Angle alpha  <=>  ? A O B. alpha = angle A O B /\ ~Collinear A O B`;;
let AngleOrdering_DEF = new_definition
 `alpha <_ang beta  <=>
  Angle alpha /\
  ? A O B G. ~Collinear A O B  /\  beta = angle A O B /\
             G IN int_angle A O B  /\  alpha === angle A O G`;;
let RAY = new_definition
 `Ray r  <=>  ? O A. ~(O = A) /\ r = ray O A`;;
let TriangleCong_DEF = new_definition
 `! A B C A' B' C' :point. (A, B, C) cong (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' /\
  angle A B C === angle A' B' C' /\
  angle B C A === angle B' C' A' /\
  angle C A B === angle C' A' B'`;;
let SupplementaryAngles_DEF = new_definition
 `! alpha beta. alpha suppl beta   <=>
  ? A O B A'. ~Collinear A O B  /\  O IN open (A,A')  /\  alpha = angle A O B  /\  beta = angle B O A'`;;
let RightAngle_DEF = new_definition
 `! alpha. Right alpha  <=>  ? beta. alpha suppl beta /\ alpha === beta`;;
let PlaneComplement_DEF = new_definition
 `! alpha:point_set. complement alpha = {P | P NOTIN alpha}`;;
let CONVEX = new_definition
 `Convex alpha  <=>  ! A B. A IN alpha /\ B IN alpha  ==> open (A,B) SUBSET alpha`;;
let PARALLEL = new_definition
 `! l k. l parallel k   <=>
  Line l /\ Line k /\ l INTER k = {}`;;
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 IN a /\ B IN a /\
  Line b /\ B IN b /\ C IN b /\
  Line c  /\ C IN c /\ D IN d /\
  Line d /\ D IN d /\ A IN d /\
  a parallel c  /\  b parallel d`;;
let InteriorCircle_DEF = new_definition
 `! O R.  int_circle O R = {P | ~(O = R) /\ (P = O  \/  seg O P <__ seg O R)}
`;;
(* ---------------------------------------------------------------------------- *) (* Hilbert's geometry axioms, except the parallel axiom P, defined near the end. *) (* ---------------------------------------------------------------------------- *) let I1 = new_axiom `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;; let I2 = new_axiom `! l. Line l ==> ? A B. A IN l /\ B IN 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 NOTIN l /\ B NOTIN l /\ C NOTIN l /\ (? X. X IN l /\ Between A X C) ==> (? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C)`;; let C1 = new_axiom `! s O Z. Segment s /\ ~(O = Z) ==> ?! P. P IN ray O Z DELETE 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 IN open (A,C) /\ B' IN 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 `! alpha O A l Y. Angle alpha /\ ~(O = A) /\ Line l /\ O IN l /\ A IN l /\ Y NOTIN l ==> ?! r. Ray r /\ ? B. ~(O = B) /\ r = ray O B /\ B NOTIN l /\ B,Y same_side l /\ angle A O B === alpha`;; let C5Reflexive = new_axiom `Angle alpha ==> alpha === alpha`;; let C5Symmetric = new_axiom `Angle alpha /\ Angle beta /\ alpha === beta ==> beta === alpha`;; let C5Transitive = new_axiom `Angle alpha /\ Angle beta /\ Angle gamma /\ alpha === beta /\ beta === gamma ==> alpha === gamma`;; 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' /\ angle A B C === angle A' B' C' ==> angle B C A === angle B' C' A'`;; (* ----------------------------------------------------------------- *) (* Theorems. *) (* ----------------------------------------------------------------- *) let IN_Interval = thm `; ! A B X. X IN open (A,B) <=> Between A X B by Interval_DEF, SET_RULE; `;; let IN_Ray = thm `; ! A B X. X IN ray A B <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B) by Ray_DEF, SET_RULE; `;; let IN_InteriorAngle = thm `; ! A O B P. P IN int_angle A O B <=> ~Collinear A O B /\ ? a b. Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\ P NOTIN a /\ P NOTIN 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 IN int_triangle A B C <=> P IN int_angle A B C /\ P IN int_angle B C A /\ P IN int_angle C A B by InteriorTriangle_DEF, SET_RULE; `;; let IN_PlaneComplement = thm `; ! alpha:point_set. ! P. P IN complement alpha <=> P NOTIN alpha by PlaneComplement_DEF, SET_RULE; `;; let IN_InteriorCircle = thm `; ! O R P. P IN 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 IN open (A,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ B IN open (C,A) /\ Collinear A B C by IN_Interval, B1; `;; let B2' = thm `; ! A B. ~(A = B) ==> ? C. B IN open (A,C) by IN_Interval, B2; `;; let B3' = thm `; ! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C ==> (B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B)) /\ ~(B IN open (A,C) /\ C IN open (B,A)) /\ ~(B IN open (A,C) /\ A IN open (C,B)) /\ ~(C IN open (B,A) /\ A IN open (C,B)) by IN_Interval, B3; `;; let B4' = thm `; ! l A B C. Line l /\ ~Collinear A B C /\ A NOTIN l /\ B NOTIN l /\ C NOTIN l /\ (? X. X IN l /\ X IN open (A,C)) ==> (? Y. Y IN l /\ Y IN open (A,B)) \/ (? Y. Y IN l /\ Y IN open (B,C)) by IN_Interval, B4; `;; let B4'' = thm `; ! l:point_set. ! A B C:point. Line l /\ ~Collinear A B C /\ A NOTIN l /\ B NOTIN l /\ C NOTIN 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 IN m ==> x NOTIN l) <=> l INTER m = {} by SET_RULE, NOTIN; `;; let EquivIntersectionHelp = thm `; ! e x:A. ! l m:A->bool. (l INTER m = {x} \/ m INTER l = {x}) /\ e IN m DELETE x ==> e NOTIN l by SET_RULE, NOTIN; `;; 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 IN l /\ B IN l /\ C IN 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 IN l [H1]; thus ? Q. Q IN l /\ ~(P = Q) proof consider A B such that A IN l /\ B IN 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 NOTIN l proof consider A B C such that ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear A B C [Distinct] by I3; (A NOTIN l \/ B NOTIN l \/ C NOTIN l) \/ (A IN l /\ B IN l /\ C IN l) by NOTIN; cases by -; suppose A NOTIN l \/ B NOTIN l \/ C NOTIN l; qed by -; suppose (A IN l) /\ (B IN l) /\ (C IN 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 IN m /\ C IN m [H1]; assume B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B) [H2]; thus B IN 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 IN l /\ B IN l /\ C IN 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 IN m /\ C IN m [H1]; assume Collinear A B C \/ Collinear B C A \/ Collinear C A B [H2]; assume ~(A = C) [H3]; thus B IN m proof consider l such that Line l /\ A IN l /\ B IN l /\ C IN 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 IN ray O Q proof O NOTIN open (O,Q) [OOQ] by B1', NOTIN; 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 IN ray O Q proof O NOTIN open (Q,Q) [notOQQ] by B1', NOTIN; 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 IN l /\ X IN m [H2]; thus l INTER m = {X} proof assume ~(l INTER m = {X}) [H3]; X IN l INTER m by H2, IN_INTER; consider A such that A IN l INTER m /\ ~(A = X) [X1] by -, H3, SET_RULE; A IN l /\ X IN l /\ A IN m /\ X IN 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 INTER m = {X} [H1]; assume A IN m DELETE X /\ B IN m DELETE X [H2]; assume X NOTIN open (A,B) [H3]; thus A,B same_side l proof assume ~(A,B same_side l) [Con]; A IN m /\ B IN m /\ ~(A = X) /\ ~(B = X) [H2'] by H2, IN_DELETE; ~(open (A,B) INTER l = {}) [nonempty] by H0, Con, SameSide_DEF, SET_RULE; open (A,B) SUBSET m [ABm] by H0, H2', BetweenLinear, SUBSET; open (A,B) INTER l SUBSET {X} by -, SET_RULE, H1; X IN open (A,B) INTER l by nonempty, -, SET_RULE; qed by -, IN_INTER, H3, NOTIN; `;; let RayLine = thm `; ! O P:point. ! l: point_set. Line l /\ O IN l /\ P IN l ==> ray O P SUBSET l by IN_Ray, CollinearLinear, SUBSET; `;; let RaySameSide = thm `; let l be point_set; let O A P be point; assume Line l /\ O IN l [l_line]; assume A NOTIN l [notAl]; assume P IN ray O A DELETE O [PrOA]; thus P NOTIN l /\ P,A same_side l proof ~(O = A) [notOA] by l_line, notAl, NOTIN; consider d such that Line d /\ O IN d /\ A IN d [d_line] by notOA, I1; ~(l = d) by -, notAl, NOTIN; l INTER d = {O} [ldO] by l_line, d_line, -, I1Uniqueness; A IN d DELETE O [Ad_O] by d_line, notOA, IN_DELETE; ray O A SUBSET d by d_line, RayLine; P IN d DELETE O [Pd_O] by PrOA, -, SUBSET, IN_DELETE; P NOTIN l [notPl] by ldO, -, EquivIntersectionHelp; O NOTIN 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 IN open (A,C) [H1]; thus B IN ray A C DELETE A /\ C IN ray A B DELETE A proof ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C [ABC] by H1, B1'; A NOTIN open (B,C) /\ A NOTIN open (C,B) by -, H1, B3', B1', NOTIN; qed by ABC, CollinearSymmetry, -, IN_Ray, IN_DELETE, NOTIN; `;; 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 IN b /\ B IN b [b_line] by Distinct, I1; A NOTIN b [notAb] by b_line, Collinear_DEF, H1, NOTIN; X IN b by H2, b_line, Distinct, I1, Collinear_DEF; qed by b_line, -, H2, I1, Collinear_DEF, notAb, NOTIN; `;; let SameSideReflexive = thm `; ! l A. Line l /\ A NOTIN l ==> A,A same_side l by B1', SameSide_DEF; `;; let SameSideSymmetric = thm `; ! l A B. Line l /\ A NOTIN l /\ B NOTIN 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 NOTIN l /\ B NOTIN l /\ C NOTIN 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 IN m /\ C IN m [m_line] by Distinct, I1; B IN m [Bm] by -, Distinct, CollinearLinear; cases; suppose m INTER l = {}; qed by m_line, l_line, -, BetweenLinear, SET_RULE, SameSide_DEF; suppose ~(m INTER l = {}); consider X such that X IN l /\ X IN 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 IN 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, NOTIN; consider B' such that ~(B = E) /\ B IN open (E,B') [EBB'] by notABCl, El_X, NOTIN, 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' IN ray E B DELETE E /\ B IN ray E B' DELETE E by EBB', IntervalRayEZ; B' NOTIN 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 IN open (A,B) [H2]; thus G IN int_angle A O B proof ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct; consider a such that Line a /\ O IN a /\ A IN a [a_line] by -, I1; consider b such that Line b /\ O IN b /\ B IN b [b_line] by Distinct, I1; consider l such that Line l /\ A IN l /\ B IN l [l_line] by Distinct, I1; B NOTIN a /\ A NOTIN b by H1, a_line, Collinear_DEF, NOTIN, b_line; ~(a = l) /\ ~(b = l) by -, l_line, NOTIN; a INTER l = {A} /\ b INTER l = {B} [alA] by -, a_line, l_line, I1Uniqueness, b_line; ~(A = G) /\ ~(A = B) /\ ~(G = B) [AGB] by H2, B1'; A NOTIN open (G,B) /\ B NOTIN open (G,A) [notGAB] by H2, B3', B1', NOTIN; G IN l [Gl] by l_line, H2, BetweenLinear; G NOTIN a /\ G NOTIN b [notGa] by alA, Gl, AGB, IN_DELETE, EquivIntersectionHelp; G IN l DELETE A /\ B IN l DELETE A /\ G IN l DELETE B /\ A IN l DELETE 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 IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b [aOAbOB]; assume P IN int_angle A O B [P_AOB]; thus P NOTIN a /\ P NOTIN b /\ P,B same_side a /\ P,A same_side b proof consider alpha beta such that ~Collinear A O B /\ Line alpha /\ O IN alpha /\ A IN alpha /\ Line beta /\ O IN beta /\B IN beta /\ P NOTIN alpha /\ P NOTIN beta /\ P,B same_side alpha /\ P,A same_side beta [exists] by P_AOB, IN_InteriorAngle; ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by -, NonCollinearImpliesDistinct; alpha = a /\ beta = b by -, aOAbOB, exists, I1; qed by -, exists; `;; let InteriorEZHelp = thm `; let A O B P be point; assume P IN 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 IN a /\ A IN a /\ Line b /\ O IN b /\B IN b /\ P NOTIN a /\ P NOTIN b [def_int] by P_AOB, IN_InteriorAngle; ~(P = A) /\ ~(P = O) /\ ~(P = B) [PnotAOB] by -, NOTIN; ~(A = O) [notAO] by def_int, NonCollinearImpliesDistinct; ~Collinear A O P by def_int, notAO, -, I1, Collinear_DEF, NOTIN; qed by PnotAOB, -; `;; let InteriorAngleSymmetry = thm `; ! A O B P: point. P IN int_angle A O B ==> P IN int_angle B O A by IN_InteriorAngle, CollinearSymmetry; `;; let InteriorWellDefined = thm `; let A O B X P be point; assume P IN int_angle A O B [H1]; assume X IN ray O B DELETE O [H2]; thus P IN int_angle A O X proof consider a b such that ~Collinear A O B /\ Line a /\ O IN a /\ A IN a /\ P NOTIN a /\ Line b /\ O IN b /\ B IN b /\ P NOTIN 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 NOTIN a [notBa] by def_int, Collinear_DEF, NOTIN; ~Collinear A O X [AOXnoncol] by def_int, H2', NoncollinearityExtendsToLine; X IN b [Xb] by def_int, H2', CollinearLinear; X NOTIN 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 IN int_angle A O B [XintAOB]; assume P IN ray O X DELETE O [PrOX]; thus P IN int_angle A O B proof consider a b such that ~Collinear A O B /\ Line a /\ O IN a /\ A IN a /\ X NOTIN a /\ Line b /\ O IN b /\ B IN b /\ X NOTIN b /\ X,B same_side a /\ X,A same_side b [def_int] by XintAOB, IN_InteriorAngle; P NOTIN a /\ P,X same_side a /\ P NOTIN 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, NOTIN; 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 IN a /\ A IN a [H2]; assume P NOTIN a /\ Q NOTIN a [H3]; assume P, Q same_side a [H4]; assume ~Collinear P O Q [H5]; thus P IN int_angle Q O A \/ Q IN int_angle P O A proof ~(P = O) /\ ~(P = Q) /\ ~(O = Q) [Distinct] by H5, NonCollinearImpliesDistinct; consider q such that Line q /\ O IN q /\ Q IN q [q_line] by Distinct, I1; P NOTIN q [notPq] by -, Collinear_DEF, H5, NOTIN; assume ~(P IN int_angle Q O A) [notPintQOA]; ~Collinear Q O A /\ ~Collinear P O A [POAncol] by H1, H2, I1, Collinear_DEF, H3, NOTIN; ~(P,A same_side q) by -, H2, q_line, H3, notPq, H4, notPintQOA, IN_InteriorAngle; consider G such that G IN q /\ G IN open (P,A) [existG] by q_line, -, SameSide_DEF; G IN int_angle P O A [G_POA] by POAncol, existG, ConverseCrossbar; G NOTIN a /\ G,P same_side a /\ ~(G = O) [Gsim_aP] by -, IN_InteriorAngle, H1, H2, I1, NOTIN; G,Q same_side a by H2, Gsim_aP, H3, H4, SameSideTransitive; O NOTIN open (Q,G) [notQOG] by -, SameSide_DEF, H2, B1', NOTIN; Collinear O G Q by q_line, existG, Collinear_DEF; Q IN ray O G DELETE 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 IN open (A,A') [H2]; thus int_angle B O A' INTER int_angle A O B = {} proof ! D. D IN int_angle A O B ==> D NOTIN int_angle B O A' proof let D be point; assume D IN int_angle A O B [H3]; ~(A = O) /\ ~(O = B) by H1, NonCollinearImpliesDistinct; consider a b such that Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\ A' IN a [ab_line] by -, I1, H2, BetweenLinear; ~Collinear B O A' by H1, CollinearSymmetry, H2, B1', NoncollinearityExtendsToLine; A NOTIN b /\ A' NOTIN b [notAb] by ab_line, Collinear_DEF, H1, -, NOTIN; ~(A',A same_side b) [A'nsim_bA] by ab_line, H2, B1', SameSide_DEF ; D NOTIN 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, NOTIN; qed by -, DisjointOneNotOther; `;; let InteriorReflectionInterior = thm `; let A O B D A' be point; assume O IN open (A,A') [H1]; assume D IN int_angle A O B [H2]; thus B IN int_angle D O A' proof consider a b such that ~Collinear A O B /\ Line a /\ O IN a /\ A IN a /\ D NOTIN a /\ Line b /\ O IN b /\ B IN b /\ D NOTIN b /\ D,B same_side a [DintAOB] by H2, IN_InteriorAngle; ~(O = B) /\ ~(O = A') /\ B NOTIN a [Distinct] by -, NonCollinearImpliesDistinct, H1, B1', Collinear_DEF, NOTIN; ~Collinear D O B [DOB_ncol] by DintAOB, -, I1, Collinear_DEF, NOTIN; A' IN a [A'a] by H1, DintAOB, BetweenLinear; D NOTIN int_angle B O A' by DintAOB, H1, InteriorsDisjointSupplement, H2, DisjointOneNotOther; qed by Distinct, DintAOB, A'a, DOB_ncol, -, AngleOrdering, NOTIN; `;; let Crossbar_THM = thm `; let O A B D be point; assume D IN int_angle A O B [H1]; thus ? G. G IN open (A,B) /\ G IN ray O D DELETE O proof consider a b such that ~Collinear A O B /\ Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\ D NOTIN a /\ D NOTIN b /\ D,B same_side a /\ D,A same_side b [DintAOB] by H1, IN_InteriorAngle; B NOTIN a [notBa] by DintAOB, Collinear_DEF, NOTIN; ~(A = O) /\ ~(A = B) /\ ~(O = B) /\ ~(D = O) [Distinct] by DintAOB, NonCollinearImpliesDistinct, NOTIN; consider l such that Line l /\ O IN l /\ D IN l [l_line] by -, I1; consider A' such that O IN open (A,A') [AOA'] by Distinct, B2'; A' IN 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 IN 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 NOTIN l /\ B NOTIN l /\ A' NOTIN l by l_line, Collinear_DEF, AODncol, -, NOTIN; ~(A,B same_side l) by l_line, -, Bsim_lA', Ansim_lA', SameSideTransitive; consider G such that G IN open (A,B) /\ G IN l [AGB] by l_line, -, SameSide_DEF; Collinear O D G [ODGcol] by -, l_line, Collinear_DEF; G IN int_angle A O B by DintAOB, AGB, ConverseCrossbar; G NOTIN a /\ G,B same_side a /\ ~(G = O) [Gsim_aB] by DintAOB, -, InteriorUse, NOTIN; B,D same_side a by DintAOB, notBa, SameSideSymmetric; G,D same_side a [Gsim_aD] by DintAOB, Gsim_aB, notBa, -, SameSideTransitive; O NOTIN open (G,D) by DintAOB, -, SameSide_DEF, NOTIN; G IN ray O D DELETE 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 IN int_angle A O B [H1]; thus G IN open (A,B) proof consider a b such that ~Collinear A O B /\ Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\ G,B same_side a /\ G,A same_side b [GintAOB] by H1, IN_InteriorAngle; ~(A = B) /\ ~(G = A) /\ ~(G = B) /\ A NOTIN open (G,B) /\ B NOTIN open (G,A) by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp, SameSide_DEF, NOTIN; qed by -, H1, B1', B3', NOTIN; `;; let InteriorOpposite = thm `; let A O B P be point; let p be point_set; assume P IN int_angle A O B [PintAOB]; assume Line p /\ O IN p /\ P IN p [p_line]; thus ~(A,B same_side p) proof consider G such that G IN open (A,B) /\ G IN ray O P [Gexists] by PintAOB, Crossbar_THM, IN_DELETE; G IN 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 IN m [H0]; assume P IN m DELETE O /\ Q IN m DELETE O /\ R IN m DELETE O [H2]; assume O NOTIN open (P,Q) /\ O NOTIN open (Q,R) [H3]; thus O NOTIN open (P,R) proof consider E such that E NOTIN m /\ ~(O = E) [notEm] by H0, ExistsPointOffLine, NOTIN; consider l such that Line l /\ O IN l /\ E IN l [l_line] by -, I1; ~(m = l) by notEm, -, NOTIN; l INTER m = {O} [lmO] by l_line, H0, -, l_line, I1Uniqueness; P NOTIN l /\ Q NOTIN l /\ R NOTIN 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, NOTIN; `;; let RayWellDefinedHalfway = thm `; let O P Q be point; assume ~(Q = O) [H1]; assume P IN ray O Q DELETE O [H2]; thus ray O P SUBSET ray O Q proof consider m such that Line m /\ O IN m /\ Q IN m [OQm] by H1, I1; P IN ray O Q /\ ~(P = O) /\ O NOTIN open (P,Q) [H2'] by H2, IN_DELETE, IN_Ray; P IN m /\ P IN m DELETE O /\ Q IN m DELETE O [PQm_O] by OQm, H2', RayLine, SUBSET, H2', OQm, H1, IN_DELETE; O NOTIN open (P,Q) [notPOQ] by H2', IN_Ray; ! X. X IN ray O P ==> X IN ray O Q proof let X be point; assume X IN ray O P; X IN m /\ O NOTIN 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 IN m DELETE O by XrOP, -, IN_DELETE; O NOTIN 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 IN ray O Q DELETE O [H2]; thus ray O P = ray O Q proof ray O P SUBSET ray O Q [PsubsetQ] by H1, H2, RayWellDefinedHalfway; ~(P = O) /\ Collinear O Q P /\ O NOTIN open (P,Q) [H2'] by H2, IN_DELETE, IN_Ray; Q IN ray O P DELETE O by H2', B1', NOTIN, CollinearSymmetry, IN_Ray, H1, IN_DELETE; ray O Q SUBSET 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 IN open (A,B) [H1]; assume X IN ray O B DELETE O [H2]; thus X NOTIN ray O A /\ O IN 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 NOTIN open (X,B) [H2'] by H2, IN_DELETE, IN_Ray; consider m such that Line m /\ A IN m /\ B IN m [m_line] by AOB, I1; O IN m /\ X IN m [Om] by m_line, H2', AOB, CollinearLinear; A IN m DELETE O /\ X IN m DELETE O /\ B IN m DELETE O by m_line, -, H2', AOB, IN_DELETE; O IN open (X,A) by H1, m_line, Om, -, H2', IntervalTransitivity, NOTIN, B1'; qed by -, IN_Ray, NOTIN; `;; let OppositeRaysIntersect1point = thm `; let A O B be point; assume O IN open (A,B) [H1]; thus ray O A INTER ray O B = {O} proof ~(A = O) /\ ~(O = B) by H1, B1'; {O} SUBSET ray O A INTER ray O B [Osubset_rOA] by -, OriginInRay, IN_INTER, SING_SUBSET; ! X. ~(X = O) /\ X IN ray O B ==> X NOTIN ray O A by IN_DELETE, H1, OppositeRaysIntersect1pointHelp; ray O A INTER ray O B SUBSET {O} by -, IN_INTER, IN_SING, SUBSET, NOTIN; qed by -, Osubset_rOA, SUBSET_ANTISYM; `;; let IntervalRay = thm `; ! A B C:point. B IN 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 IN open (A,C) /\ C IN open (B,D) [H1]; thus B IN open (A,D) proof D IN ray B C DELETE B by H1, IntervalRayEZ; qed by H1, -, OppositeRaysIntersect1pointHelp, B1'; `;; let TransitivityBetweenness = thm `; let A B C D be point; assume B IN open (A,C) /\ C IN open (B,D) [H1]; thus ordered A B C D proof B IN open (A,D) [ABD] by H1, TransitivityBetweennessHelp; C IN open (D,B) /\ B IN open (C,A) by H1, B1'; C IN open (D,A) by -, TransitivityBetweennessHelp; qed by H1, ABD, -, B1', Ordered_DEF; `;; let IntervalsAreConvex = thm `; let A B C be point; assume B IN open (A,C) [H1]; thus open (A,B) SUBSET open (A,C) proof ! X. X IN open (A,B) ==> X IN open (A,C) proof let X be point; assume X IN open (A,B) [AXB]; X IN ray B A DELETE B by AXB, B1', IntervalRayEZ; B IN 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 IN open (A,B) /\ B IN open (A,C) [H1]; thus ordered A X B C proof X IN ray B A DELETE B by H1, B1', IntervalRayEZ; B IN open (X,C) by H1, B1', -, OppositeRaysIntersect1pointHelp; qed by H1, -, TransitivityBetweenness; `;; let Interval2sides2aLineHelp = thm `; let A B C X be point; assume B IN open (A,C) [H1]; thus X NOTIN open (A,B) \/ X NOTIN open (B,C) proof assume ~(X NOTIN open (A,B)); ordered A X B C by -, NOTIN, H1, TransitivityBetweennessVariant; B IN open (X,C) by -, Ordered_DEF; X NOTIN open (C,B) by -, B1', B3', NOTIN; qed by -, B1', NOTIN; `;; let Interval2sides2aLine = thm `; let A B C X be point; assume Collinear A B C [H1]; thus X NOTIN open (A,B) \/ X NOTIN open (A,C) \/ X NOTIN open (B,C) proof cases; suppose A = B \/ A = C \/ B = C; qed by -, B1', NOTIN; suppose ~(A = B) /\ ~(A = C) /\ ~(B = C); B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B) by -, H1, B3'; qed by -, Interval2sides2aLineHelp, B1', NOTIN; 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 NOTIN l /\ B NOTIN l /\ C NOTIN l [off_l]; assume Line m /\ A IN m /\ C IN m [m_line]; assume Y IN l /\ Y IN 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 IN l /\ X IN open (A,B) /\ Z IN l /\ Z IN open (C,B) [H2'] by H1, H2, SameSide_DEF, B1'; ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Y IN m DELETE A /\ Y IN m DELETE C /\ C IN m DELETE A /\ A IN m DELETE C [Distinct] by H1, NonCollinearImpliesDistinct, Ylm, off_l, NOTIN, m_line, IN_DELETE; consider p such that Line p /\ B IN p /\ A IN p [p_line] by Distinct, I1; consider q such that Line q /\ B IN q /\ C IN q [q_line] by Distinct, I1; X IN p /\ Z IN q [Xp] by p_line, H2', BetweenLinear, q_line, H2'; A NOTIN q /\ B NOTIN m /\ C NOTIN p [vertex_off_line] by q_line, m_line, p_line, H1, Collinear_DEF, NOTIN; X NOTIN q /\ X,A same_side q /\ Z NOTIN 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, NOTIN; p INTER m = {A} /\ q INTER m = {C} [pmA] by p_line, m_line, q_line, H1, -, Xp, H2', I1Uniqueness; Y NOTIN p /\ Y NOTIN q [notYpq] by -, Distinct, EquivIntersectionHelp; X IN ray A B DELETE A /\ Z IN ray C B DELETE C by H2', IntervalRayEZ, H2', B1'; X NOTIN m /\ Z NOTIN 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 NOTIN open (X,Z) /\ ~(Y = X) /\ ~(Y = Z) /\ ~(X = Z) by H1, H2', Ylm, Collinear_DEF, m_line, -, SameSide_DEF, notXZm, Xsim_qA, Xp, NOTIN; Z IN open (X,Y) \/ X IN open (Z,Y) by -, B3', NOTIN, B1'; cases by -; suppose X IN 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 IN open (C,Y) by p_line, m_line, pmA, Distinct, -, EquivIntersection, NOTIN; qed by H1, Ylm, off_l, -, B1', IntervalRayEZ, RaySameSide; suppose Z IN 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 IN open (Y,A) by q_line, m_line, pmA, Distinct, -, EquivIntersection, NOTIN, 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 IN l /\ B IN l [H1]; assume O IN open (A,B) [H2]; thus l = ray O A UNION ray O B proof ~(A = O) /\ ~(O = B) /\ O IN l [Distinct] by H2, B1', H1, BetweenLinear; ray O A UNION ray O B SUBSET l [AOBsub_l] by H1, -, RayLine, UNION_SUBSET; ! X. X IN l ==> X IN ray O A \/ X IN ray O B proof let X be point; assume X IN l [Xl]; assume ~(X IN ray O B) [notXrOB]; Collinear O B X /\ Collinear X A B /\ Collinear O A X [XABcol] by Distinct, H1, Xl, Collinear_DEF; O IN open (X,B) by notXrOB, Distinct, -, IN_Ray, NOTIN; O NOTIN open (X,A) by NOTIN, B1', XABcol, -, H2, Interval2sides2aLine; qed by Distinct, XABcol, -, IN_Ray; l SUBSET ray O A UNION 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 NOTIN l /\ B NOTIN l /\ C NOTIN 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 IN m /\ C IN m [m_line] by notAC, I1; cases; suppose m INTER l = {}; A,C same_side l by m_line, H1, -, BetweenLinear, SET_RULE, SameSide_DEF; qed by -; suppose ~(m INTER l = {}); consider Y such that Y IN l /\ Y IN 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 IN m [Bm] by -, m_line, notAC, I1, Collinear_DEF; ~(Y = A) /\ ~(Y = B) /\ ~(Y = C) [YnotABC] by Ylm, H2, NOTIN; Y NOTIN open (A,B) \/ Y NOTIN open (A,C) \/ Y NOTIN open (B,C) by ABCcol, Interval2sides2aLine; A IN ray Y B DELETE Y \/ A IN ray Y C DELETE Y \/ B IN ray Y C DELETE 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 IN l /\ B IN l /\ C IN l /\ X IN l [H1]; assume ~(X = A) /\ ~(X = B) /\ ~(X = C) [H2]; assume B IN 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 IN open (X,B) \/ X IN open (A,B) \/ X IN open (B,C) \/ C IN 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 IN open (X,B) \/ X IN open (A,B) \/ B IN open (A,X) by H2, ABCdistinct, -, B3', B1'; cases by -; suppose A IN open (X,B) \/ X IN open (A,B); qed by -; suppose B IN open (A,X); B NOTIN open (C,X) by ACXcol, H3, -, Interval2sides2aLine, NOTIN; qed by H2, ABCdistinct, ACXcol, -, B3', B1', NOTIN; 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 IN l /\ B IN l /\ C IN l /\ D IN 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 IN open (A,C) \/ C IN open (A,B) \/ A IN 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 IN int_angle A O B [GintAOB]; assume F IN int_angle A O G [FintAOG]; thus F IN int_angle A O B proof ~Collinear A O B [AOBncol] by GintAOB, IN_InteriorAngle; consider G' such that G' IN open (A,B) /\ G' IN ray O G DELETE O [CrossG] by GintAOB, Crossbar_THM; F IN int_angle A O G' by FintAOG, -, InteriorWellDefined; consider F' such that F' IN open (A,G') /\ F' IN ray O F DELETE O [CrossF] by -, Crossbar_THM; ~(F' = O) /\ ~(F = O) /\ Collinear O F F' /\ O NOTIN open (F',F) by -, IN_DELETE, IN_Ray; F IN ray O F' DELETE O [FrOF'] by -, CollinearSymmetry, B1', NOTIN, IN_Ray, IN_DELETE; open (A,G') SUBSET open (A,B) /\ F' IN open (A,B) by CrossG, IntervalsAreConvex, CrossF, SUBSET; F' IN 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 NOTIN l [l_line]; assume H = {X | X NOTIN l /\ X,A same_side l} [HalfPlane]; thus ~(H = {}) /\ H SUBSET complement l /\ Convex H proof ! X. X IN H <=> X NOTIN l /\ X,A same_side l [Hdef] by HalfPlane, SET_RULE; H SUBSET complement l [Hsub] by -, IN_PlaneComplement, SUBSET; A,A same_side l /\ A IN H by l_line, SameSideReflexive, Hdef; ~(H = {}) [Hnonempty] by -, MEMBER_NOT_EMPTY; ! P Q X. P IN H /\ Q IN H /\ X IN open (P,Q) ==> X IN H proof let P Q X be point; assume P IN H /\ Q IN H /\ X IN open (P,Q) [PXQ]; P NOTIN l /\ P,A same_side l /\ Q NOTIN l /\ Q,A same_side l [PQinH] by -, Hdef; P,Q same_side l [Psim_lQ] by l_line, -, SameSideSymmetric, SameSideTransitive; X NOTIN l [notXl] by -, PXQ, SameSide_DEF, NOTIN; open (X,P) SUBSET 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 INTER H2 = {} /\ ~(H1 = {}) /\ ~(H2 = {}) /\ Convex H1 /\ Convex H2 /\ complement l = H1 UNION H2 /\ ! P Q. P IN H1 /\ Q IN H2 ==> ~(P,Q same_side l) proof consider A such that A NOTIN l [notAl] by l_line, ExistsPointOffLine; consider E such that E IN l /\ ~(A = E) [El] by l_line, I2, -, NOTIN; consider B such that E IN open (A,B) /\ ~(E = B) /\ Collinear A E B [AEB] by -, B2', B1'; B NOTIN l [notBl] by l_line, El, -, I1, Collinear_DEF, notAl, NOTIN; ~(A,B same_side l) [Ansim_lB] by l_line, El, AEB, SameSide_DEF; consider H1 H2 such that H1 = {X | X NOTIN l /\ X,A same_side l} /\ H2 = {X | X NOTIN l /\ X,B same_side l} [H12sets]; ! X. (X IN H1 <=> X NOTIN l /\ X,A same_side l) /\ (X IN H2 <=> X NOTIN l /\ X,B same_side l) [H12def] by -, SET_RULE; ! X. X IN H1 <=> X NOTIN l /\ X,A same_side l [H1def] by H12sets, SET_RULE; ! X. X IN H2 <=> X NOTIN l /\ X,B same_side l [H2def] by H12sets, SET_RULE; H1 INTER H2 = {} [H12disjoint] proof assume ~(H1 INTER H2 = {}); consider V such that V IN H1 /\ V IN H2 by -, MEMBER_NOT_EMPTY, IN_INTER; V NOTIN l /\ V,A same_side l /\ V NOTIN 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 SUBSET complement l /\ H2 SUBSET complement l /\ Convex H1 /\ Convex H2 [H12convex_nonempty] by l_line, notAl, notBl, H12sets, HalfPlaneConvexNonempty; H1 UNION H2 SUBSET complement l [H12sub] by H12convex_nonempty, UNION_SUBSET; ! C. C IN complement l ==> C IN H1 UNION H2 proof let C be point; assume C IN complement l; C NOTIN l [notCl] by -, IN_PlaneComplement; C,A same_side l \/ C,B same_side l by l_line, notAl, notBl, -, Ansim_lB, AtMost2Sides; C IN H1 \/ C IN H2 by notCl, -, H12def; qed by -, IN_UNION; complement l SUBSET H1 UNION H2 by -, SUBSET; complement l = H1 UNION H2 [compl_H1unionH2] by H12sub, -, SUBSET_ANTISYM; ! P Q. P IN H1 /\ Q IN H2 ==> ~(P,Q same_side l) [opp_sides] proof let P Q be point; assume P IN H1 /\ Q IN H2; P NOTIN l /\ P,A same_side l /\ Q NOTIN 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) INTER open (B,C) = {} proof ! X. X IN open (B,C) ==> X NOTIN open (A,B) proof let X be point; assume X IN 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', NOTIN; qed by -, DisjointOneNotOther; `;; let EasyEmptyIntersectionsTetralateral = thm `; let A B C D be point; assume Tetralateral A B C D [H1]; thus open (A,B) INTER open (B,C) = {} /\ open (B,C) INTER open (C,D) = {} /\ open (C,D) INTER open (D,A) = {} /\ open (D,A) INTER 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 IN a /\ B IN a [a_line]; assume Line c /\ C IN c /\ D IN 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 IN a /\ G IN open (C,D) [CGD] by -, a_line, SameSide_DEF; G IN 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) INTER open (C,D) = {} [quadABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF; A NOTIN c /\ B NOTIN c /\ ~(A = G) /\ ~(B = G) [Distinct] by -, c_line, Collinear_DEF, NOTIN, Gc; G NOTIN open (A,B) by quadABCD, CGD, DisjointOneNotOther; A IN ray G B DELETE 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 IN int_angle D A B /\ D IN 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 IN a /\ B IN a [a_line] by TetraABCD, I1; consider b such that Line b /\ B IN b /\ C IN b [b_line] by TetraABCD, I1; consider d such that Line d /\ D IN d /\ A IN d [d_line] by TetraABCD, I1; open (B,C) SUBSET b /\ open (A,B) SUBSET 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 INTER open (D,A) = {} /\ a INTER open (C,D) = {} by -, b_line, SameSide_DEF, SET_RULE; open (B,C) INTER open (D,A) = {} /\ open (A,B) INTER 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 IN open (A,C) /\ G IN 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 IN ray C G DELETE C /\ B IN ray D G DELETE D /\ C IN ray A G DELETE A /\ D IN ray B G DELETE B [ArCG] by DiagInt, B1', IntervalRayEZ; G IN int_angle B C D /\ G IN int_angle C D A /\ G IN int_angle D A B /\ G IN int_angle A B C by BCDncol, CDAncol, DABncol, ABCncol, DiagInt, B1', ConverseCrossbar; A IN int_angle B C D /\ B IN int_angle C D A /\ C IN int_angle D A B /\ D IN 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 IN l /\ C IN l [l_line]; assume Line m /\ B IN m /\ D IN 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 IN open (A,C) INTER 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 IN open (A,C) /\ G IN m [AGC] by H3, m_line, SameSide_DEF; G IN l [Gl] by l_line, -, BetweenLinear; A NOTIN m /\ B NOTIN l /\ D NOTIN l by TetraABCD, m_line, l_line, Collinear_DEF, NOTIN; ~(l = m) /\ B IN m DELETE G /\ D IN m DELETE G [BDm_G] by -, l_line, NOTIN, m_line, Gl, IN_DELETE; l INTER m = {G} by l_line, m_line, -, Gl, AGC, I1Uniqueness; G IN open (B,D) by l_line, m_line, -, BDm_G, H2, EquivIntersection, NOTIN; 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 IN l /\ C IN l [l_line]; assume Line m /\ B IN m /\ D IN m [m_line]; assume ConvexQuadrilateral A B C D [ConvQuadABCD]; thus ~(B,D same_side l) /\ ~(A,C same_side m) /\ (? G. G IN open (A,C) INTER open (B,D)) /\ ~Quadrilateral A B D C proof Tetralateral A B C D /\ A IN int_angle B C D /\ D IN 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 IN open (A,C) INTER open (B,D) [Gexists] by l_line, m_line, convquadABCD, opp_sides, DoubleNotSimImpliesDiagonalsIntersect; ~(open (B,D) INTER 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 IN int_angle D A B [CintDAB]; thus ConvexQuadrilateral A B C D \/ C IN 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 IN a /\ B IN a /\ Line d /\ D IN d /\ A IN d [ad_line] by TetraABCD, I1; consider l m such that Line l /\ A IN l /\ C IN l /\ Line m /\ B IN m /\ D IN m [lm_line] by TetraABCD, I1; C NOTIN a /\ C NOTIN d /\ B NOTIN l /\ D NOTIN l /\ A NOTIN m /\ C NOTIN m /\ ~Collinear A B D /\ ~Collinear B D A [tetra'] by TetraABCD, ad_line, lm_line, Collinear_DEF, NOTIN, 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 IN int_angle A B D /\ C IN int_angle B D A by tetra', ad_line, lm_line, Csim_mA, -, IN_InteriorAngle; C IN int_triangle D A B by CintDAB, -, IN_InteriorTriangle; qed by -; end; `;; let InteriorTriangleSymmetry = thm `; ! A B C P. P IN int_triangle A B C ==> P IN 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 IN a /\ B IN a [a_line]; assume C,D same_side a [Csim_aD]; thus ConvexQuadrilateral A B C D \/ ConvexQuadrilateral A B D C \/ D IN int_triangle A B C \/ C IN 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 NOTIN a /\ D NOTIN a [notCDa] by TetraABCD, CollinearSymmetry, a_line, Collinear_DEF, NOTIN; C IN int_angle D A B \/ D IN int_angle C A B by TetraABCD, a_line, -, Csim_aD, AngleOrdering; cases by -; suppose C IN int_angle D A B; ConvexQuadrilateral A B C D \/ C IN int_triangle D A B by H1, -, FourChoicesTetralateralHelp; qed by -; suppose D IN int_angle C A B; ConvexQuadrilateral A B D C \/ D IN 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 IN l /\ C IN l /\ Line m /\ B IN m /\ D IN m [lm_line]; thus (ConvexQuadrilateral A B C D \/ A IN int_triangle B C D \/ B IN int_triangle C D A \/ C IN int_triangle D A B \/ D IN 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 IN a /\ B IN a /\ Line c /\ C IN c /\ D IN 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 IN int_triangle B C D \/ B IN int_triangle C D A \/ C IN int_triangle D A B \/ D IN 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 IN int_triangle C D A \/ A IN 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 IN open (O,Q) /\ seg P Q === s proof consider Z such that P IN open (O,Z) /\ ~(P = Z) [OPZ] by H1, B2', B1'; consider Q such that Q IN ray P Z DELETE P /\ seg P Q === s [PQeq] by H1, -, C1; P IN 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 IN open (A,C) [H3]; thus ? E. E IN 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 IN ray D F DELETE D /\ seg D E === seg A B [DEeqAB] by segs, H1, C1; ~(E = D) /\ Collinear D E F /\ D NOTIN open (F,E) [ErDF] by -, IN_DELETE, IN_Ray, B1', CollinearSymmetry, NOTIN; consider F' such that E IN 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' IN ray D E DELETE D /\ F IN ray D E DELETE 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 IN open (A,C) /\ B' IN 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 IN 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 NOTIN open (C,B) /\ A NOTIN open (Q,B) by defQ, B1', H1, B3', NOTIN; C IN ray A B DELETE A /\ Q IN ray A B DELETE 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 IN open (A,B) /\ s === seg A G proof consider A' B' G' such that seg A B = seg A' B' /\ G' IN 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 IN 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 IN 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 IN ray A B DELETE A /\ B IN ray A B DELETE 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 IN 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 IN 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 IN 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 IN open (A,G) /\ s === seg A F [AFG] by Distinct, -, SegmentOrderingUse; F IN 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 IN ray O P DELETE O /\ seg O Q === t [QrOP] by H1, -, C1; O NOTIN 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 IN open (O,Q) \/ Q IN open (O,P) by sOP, -, notQOP, B3', B1', NOTIN; 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 IN l /\ A IN l /\ ~(O = A) [H1]; assume B NOTIN l /\ P NOTIN l /\ P,B same_side l [H2]; assume angle A O P === angle 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, NOTIN, RAY; ~Collinear A O B /\ B,B same_side l [Bsim_lB] by H1, H2, I1, Collinear_DEF, NOTIN, SameSideReflexive; Angle (angle A O B) /\ angle A O B === angle A O B by -, ANGLE, C5Reflexive; qed by -, H1, H2, Distinct, Bsim_lB, H3, C4; `;; let AngleSymmetry = thm `; ! A O B. angle A O B = angle B O A by Angle_DEF, UNION_COMM; `;; let TriangleCongSymmetry = thm `; let A B C A' B' C' be point; assume A,B,C cong A',B',C' [H1]; thus A,C,B cong A',C',B' /\ B,A,C cong B',A',C' /\ B,C,A cong B',C',A' /\ C,A,B cong C',A',B' /\ C,B,A cong 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' /\ angle A B C === angle A' B' C' /\ angle B C A === angle B' C' A' /\ angle C A B === angle 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; angle C B A === angle C' B' A' /\ angle A C B === angle A' C' B' /\ angle B A C === angle 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 angle A B C === angle A' B' C' [H3]; thus A,B,C cong A',B',C' proof ~(A = B) /\ ~(A = C) /\ ~(A' = C') [Distinct] by H1, NonCollinearImpliesDistinct; :: 134 consider c such that Line c /\ A IN c /\ B IN c [c_line] by Distinct, I1; C NOTIN c [notCc] by H1, c_line, Collinear_DEF, NOTIN; angle B C A === angle B' C' A' [BCAeq] by H1, H2, H3, C6; angle B A C === angle B' A' C' [BACeq] by H1, CollinearSymmetry, H2, H3, AngleSymmetry, C6; consider Y such that Y IN ray A C DELETE A /\ seg A Y === seg A' C' [YrAC] by Distinct, SEGMENT, C1; Y NOTIN 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, NOTIN; ray A Y = ray A C /\ angle Y A B = angle C A B by Distinct, YrAC, RayWellDefined, Angle_DEF; angle Y A B === angle C' A' B' by BACeq, -, AngleSymmetry; angle A B Y === angle A' B' C' [ABYeq] by YABncol, H1, CollinearSymmetry, H2, SegmentSymmetry, YrAC, -, C6; Angle (angle A B C) /\ Angle (angle A' B' C') /\ Angle (angle A B Y) by H1, CollinearSymmetry, YABncol, ANGLE; angle A B Y === angle A B C [ABYeqABC] by -, ABYeq, -, H3, C5Symmetric, C5Transitive; ray B C = ray B Y /\ ~(Y = B) /\ Y IN ray B C by c_line, Distinct, notCc, Ysim_cC, ABYeqABC, C4Uniqueness, NOTIN, -, 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 angle C A B === angle C' A' B' /\ angle B C A === angle B' C' A' [H3]; thus A,B,C cong 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 IN ray C B DELETE 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 (angle C A D) /\ Angle (angle C' A' B') /\ Angle (angle C A B) [DCAncol] by H1, CollinearSymmetry, -, DrCB, NoncollinearityExtendsToLine, H1, ANGLE; consider b such that Line b /\ A IN b /\ C IN b [b_line] by Distinct, I1; B NOTIN b /\ ~(D = A) [notBb] by H1, -, Collinear_DEF, NOTIN, DCAncol, NonCollinearImpliesDistinct; D NOTIN b /\ D,B same_side b [Dsim_bB] by b_line, -, DrCB, RaySameSide; ray C D = ray C B by Distinct, DrCB, RayWellDefined; angle D C A === angle B' C' A' by H3, -, Angle_DEF; D,C,A cong B',C',A' by DCAncol, H1, CollinearSymmetry, DrCB, H2, SegmentSymmetry, -, SAS; angle C A D === angle C' A' B' by -, TriangleCong_DEF; angle C A D === angle C A B by DCAncol, -, H3, C5Symmetric, C5Transitive; ray A B = ray A D /\ D IN 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 cong 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 IN int_angle A O B /\ G' IN int_angle A' O' B' [H1]; assume angle A O B === angle A' O' B' /\ angle A O G === angle A' O' G' [H2]; thus angle G O B === angle 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 IN ray O A DELETE O /\ seg O X === seg O' A' /\ Y IN ray O B DELETE O /\ seg O Y === seg O' B' [XYexists] by -, C1; G IN int_angle X O Y [GintXOY] by H1, XYexists, InteriorWellDefined, InteriorAngleSymmetry; consider H H' such that H IN open (X,Y) /\ H IN ray O G DELETE O /\ H' IN open (A',B') /\ H' IN ray O' G' DELETE O' [Hexists] by -, H1, Crossbar_THM; H IN int_angle X O Y /\ H' IN 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; angle X O Y === angle A' O' B' /\ angle X O H === angle A' O' H' [H2'] by H2, -, Angle_DEF; ~Collinear X O Y by GintXOY, IN_InteriorAngle; X,O,Y cong A',O',B' by -, A'O'B'ncol, H2', XYexists, SAS; seg X Y === seg A' B' /\ angle O Y X === angle O' B' A' /\ angle Y X O === angle 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; angle H X O === angle H' A' O' by XOYcong, -, Angle_DEF; O,H,X cong 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; angle O Y H === angle O' B' H' by XOYcong, Hrays, Angle_DEF; O,Y,H cong O',B',H' by OHXncol, YHeq, -, SAS; angle H O Y === angle 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 angle A O B === angle A' O' B' [H2]; assume G IN int_angle A O B [H3]; thus ? G'. G' IN int_angle A' O' B' /\ angle A O G === angle 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 IN ray O A DELETE O /\ seg O X === seg O' A' /\ Y IN ray O B DELETE O /\ seg O Y === seg O' B' [defXY] by -, C1; G IN 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 IN open (X,Y) /\ H IN ray O G DELETE 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; angle X O Y === angle A' O' B' by H2, -, Angle_DEF; X,O,Y cong A',O',B' by XOYncol, H1, defXY, -, SAS; seg X Y === seg A' B' /\ angle O X Y === angle O' A' B' [YXOcong] by -, TriangleCong_DEF, AngleSymmetry; consider G' such that G' IN open (A',B') /\ seg X H === seg A' G' [A'G'B'] by XOYncol, Distinct, -, defH, OrderedCongruentSegments; G' IN 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; angle O X H === angle O' A' G' [HXOeq] by -, Angle_DEF, YXOcong; H IN 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 cong O',A',G' by -, A'G'B', defXY, SegmentSymmetry, HXOeq, SAS; angle X O H === angle A' O' G' by -, TriangleCong_DEF, AngleSymmetry; angle A O G === angle 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 IN int_angle A O B /\ G' IN int_angle A' O' B' [H1]; assume angle A O G === angle A' O' G' /\ angle G O B === angle G' O' B' [H2]; thus angle A O B === angle 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 IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b [a_line] by Distinct, I1; consider g such that Line g /\ O IN g /\ G IN g [g_line] by Distinct, I1; G NOTIN 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 (angle A O B) /\ Angle (angle A' O' B') /\ Angle (angle A O G) /\ Angle (angle A' O' G') [angles] by AOBncol, -, ANGLE; ?! r. Ray r /\ ? X. ~(O = X) /\ r = ray O X /\ X NOTIN a /\ X,G same_side a /\ angle A O X === angle A' O' B' by -, Distinct, a_line, H1', C4; consider X such that X NOTIN a /\ X,G same_side a /\ angle A O X === angle A' O' B' [Xexists] by -; ~Collinear A O X [AOXncol] by -, a_line, Distinct, I1, Collinear_DEF, NOTIN; angle A' O' B' === angle A O X by -, AOBncol, ANGLE, Xexists, C5Symmetric; consider Y such that Y IN int_angle A O X /\ angle A' O' G' === angle A O Y [YintAOX] by AOXncol, -, H1, OrderedCongruentAngles; ~Collinear A O Y by -, InteriorEZHelp; angle A O Y === angle A O G [AOGeq] by -, angles, -, ANGLE, YintAOX, H2, C5Transitive, C5Symmetric; consider x such that Line x /\ O IN x /\ X IN x by Distinct, I1; Y NOTIN a /\ Y,X same_side a by a_line, -, YintAOX, InteriorUse; Y NOTIN 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 IN ray O Y DELETE O by Distinct, -, EndpointInRay, IN_DELETE; G IN int_angle A O X [GintAOX] by YintAOX, -, WholeRayInterior; angle G O X === angle 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 (angle G O X) /\ Angle (angle G O B) /\ Angle (angle G' O' B') by -, ANGLE; angle G O X === angle 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 NOTIN g /\ B NOTIN g /\ X NOTIN g [notABXg] by g_line, AOGncol, GOXncol, Distinct, I1, Collinear_DEF, NOTIN; 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 alpha be point_set; assume Angle alpha /\ ~Collinear A O B [H1]; assume alpha <_ang angle A O B [H3]; thus ? G. G IN int_angle A O B /\ alpha === angle A O G proof consider A' O' B' G' such that ~Collinear A' O' B' /\ angle A O B = angle A' O' B' /\ G' IN int_angle A' O' B' /\ alpha === angle A' O' G' [H3'] by H3, AngleOrdering_DEF; Angle (angle A O B) /\ Angle (angle A' O' B') /\ Angle (angle A' O' G') [angles] by H1, -, ANGLE, InteriorEZHelp; angle A' O' B' === angle A O B by -, H3', C5Reflexive; consider G such that G IN int_angle A O B /\ angle A' O' G' === angle A O G [GintAOB] by H1, H3', -, OrderedCongruentAngles; alpha === angle A O G by H1, angles, -, InteriorEZHelp, ANGLE, H3', GintAOB, C5Transitive; qed by -, GintAOB; `;; let AngleTrichotomy1 = thm `; let alpha beta be point_set; assume alpha <_ang beta [H1]; thus ~(alpha === beta) proof assume alpha === beta [Con]; consider A O B G such that Angle alpha /\ ~Collinear A O B /\ beta = angle A O B /\ G IN int_angle A O B /\ alpha === angle 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 IN a /\ A IN a [a_line] by Distinct, I1; consider b such that Line b /\ O IN b /\ B IN b [b_line] by Distinct, I1; B NOTIN a [notBa] by a_line, H1', Collinear_DEF, NOTIN; G NOTIN a /\ G NOTIN b /\ G,B same_side a [GintAOB] by a_line, b_line, H1', InteriorUse; angle A O G === alpha by H1', Distinct, ANGLE, C5Symmetric; angle A O G === angle A O B by H1', Distinct, ANGLE, -, Con, C5Transitive; ray O B = ray O G by a_line, Distinct, notBa, GintAOB, -, C4Uniqueness; G IN b by Distinct, -, EndpointInRay, b_line, RayLine, SUBSET; qed by -, GintAOB, NOTIN; `;; let AngleTrichotomy2 = thm `; let alpha beta gamma be point_set; assume alpha <_ang beta [H1]; assume Angle gamma [H2]; assume beta === gamma [H3]; thus alpha <_ang gamma proof consider A O B G such that Angle alpha /\ ~Collinear A O B /\ beta = angle A O B /\ G IN int_angle A O B /\ alpha === angle A O G [H1'] by H1, AngleOrdering_DEF; consider A' O' B' such that gamma = angle A' O' B' /\ ~Collinear A' O' B' [gammaA'O'B'] by H2, ANGLE; consider G' such that G' IN int_angle A' O' B' /\ angle A O G === angle A' O' G' [G'intA'O'B'] by gammaA'O'B', H1', H3, OrderedCongruentAngles; ~Collinear A O G /\ ~Collinear A' O' G' [ncol] by H1', -, InteriorEZHelp; alpha === angle A' O' G' by H1', ANGLE, -, G'intA'O'B', C5Transitive; qed by H1', -, ncol, gammaA'O'B', G'intA'O'B', -, AngleOrdering_DEF; `;; let AngleOrderTransitivity = thm `; let alpha beta gamma be point_set; assume alpha <_ang beta [H0]; assume beta <_ang gamma [H2]; thus alpha <_ang gamma proof consider A O B G such that Angle beta /\ ~Collinear A O B /\ gamma = angle A O B /\ G IN int_angle A O B /\ beta === angle A O G [H2'] by H2, AngleOrdering_DEF; ~Collinear A O G [AOGncol] by H2', InteriorEZHelp; Angle alpha /\ Angle (angle A O G) /\ Angle gamma [angles] by H0, AngleOrdering_DEF, H2', -, ANGLE; alpha <_ang angle A O G by H0, H2', -, AngleTrichotomy2; consider F such that F IN int_angle A O G /\ alpha === angle A O F [FintAOG] by angles, AOGncol, -, AngleOrderingUse; F IN int_angle A O B by H2', -, InteriorTransitivity; qed by angles, H2', -, FintAOG, AngleOrdering_DEF; `;; let AngleTrichotomy = thm `; let alpha beta be point_set; assume Angle alpha /\ Angle beta [H1]; thus (alpha === beta \/ alpha <_ang beta \/ beta <_ang alpha) /\ ~(alpha === beta /\ alpha <_ang beta) /\ ~(alpha === beta /\ beta <_ang alpha) /\ ~(alpha <_ang beta /\ beta <_ang alpha) proof ~(alpha === beta /\ alpha <_ang beta) [Not12] by AngleTrichotomy1; ~(alpha === beta /\ beta <_ang alpha) [Not13] by H1, C5Symmetric, AngleTrichotomy1; ~(alpha <_ang beta /\ beta <_ang alpha) [Not23] by H1, AngleOrderTransitivity, AngleTrichotomy1, C5Reflexive; consider P O A such that alpha = angle 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 IN a /\ A IN a [a_line] by -, I1; P NOTIN a [notPa] by -, Distinct, I1, POA, Collinear_DEF, NOTIN; ?! r. Ray r /\ ? Q. ~(O = Q) /\ r = ray O Q /\ Q NOTIN a /\ Q,P same_side a /\ angle A O Q === beta by H1, Distinct, a_line, -, C4; consider Q such that ~(O = Q) /\ Q NOTIN a /\ Q,P same_side a /\ angle A O Q === beta [Qexists] by -; O NOTIN open (Q,P) [notQOP] by a_line, Qexists, SameSide_DEF, NOTIN; ~Collinear A O P [AOPncol] by POA, CollinearSymmetry; ~Collinear A O Q [AOQncol] by a_line, Distinct, I1, Collinear_DEF, Qexists, NOTIN; Angle (angle A O P) /\ Angle (angle A O Q) by AOPncol, -, ANGLE; alpha === angle A O P /\ beta === angle A O Q /\ angle A O P === alpha [flip] by H1, -, POA, AngleSymmetry, C5Reflexive, Qexists, C5Symmetric; cases; suppose Collinear Q O P; Collinear O P Q by -, CollinearSymmetry; Q IN ray O P DELETE O by Distinct, -, notQOP, IN_Ray, Qexists, IN_DELETE; ray O Q = ray O P by Distinct, -, RayWellDefined; angle P O A = angle A O Q by -, Angle_DEF, AngleSymmetry; alpha === beta by -, POA, Qexists; qed by -, Not12, Not13, Not23; suppose ~Collinear Q O P; P IN int_angle Q O A \/ Q IN int_angle P O A by Distinct, a_line, Qexists, notPa, -, AngleOrdering; P IN int_angle A O Q \/ Q IN int_angle A O P by -, InteriorAngleSymmetry; alpha <_ang angle A O Q \/ beta <_ang angle A O P by H1, AOQncol, AOPncol, -, flip, AngleOrdering_DEF; alpha <_ang beta \/ beta <_ang alpha by H1, -, Qexists, flip, AngleTrichotomy2; qed by -, Not12, Not13, Not23; end; `;; let SupplementExists = thm `; let alpha be point_set; assume Angle alpha [H1]; thus ? alpha'. alpha suppl alpha' proof consider A O B such that alpha = angle A O B /\ ~Collinear A O B /\ ~(A = O) [def_alpha] by H1, ANGLE, NonCollinearImpliesDistinct; consider A' such that O IN open (A,A') by -, B2'; angle A O B suppl angle A' O B [AOBsup] by def_alpha, -, SupplementaryAngles_DEF, AngleSymmetry; qed by -, def_alpha; `;; let SupplementImpliesAngle = thm `; let alpha beta be point_set; assume alpha suppl beta [H1]; thus Angle alpha /\ Angle beta proof consider A O B A' such that ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ beta = angle 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 `; ! alpha: point_set. Right alpha ==> Angle alpha by RightAngle_DEF, SupplementImpliesAngle; `;; let SupplementSymmetry = thm `; let alpha beta be point_set; assume alpha suppl beta [H1]; thus beta suppl alpha proof consider A O B A' such that ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ beta = angle 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 IN open (A',A) /\ beta = angle A' O B /\ alpha = angle B O A by H1', B1', AngleSymmetry; qed by A'OBncol, -, SupplementaryAngles_DEF; `;; let SupplementsCongAnglesCong = thm `; let alpha beta alpha' beta' be point_set; assume alpha suppl alpha' /\ beta suppl beta' [H1]; assume alpha === beta [H2]; thus alpha' === beta' proof consider A O B A' such that ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ alpha' = angle B O A' [def_alpha] by H1, SupplementaryAngles_DEF; ~(A = O) /\ ~(O = B) /\ ~(A = A') /\ ~(O = A') /\ Collinear A O A' [Distinctalpha] by -, NonCollinearImpliesDistinct, B1'; ~Collinear B A A' /\ ~Collinear O A' B [BAA'ncol] by def_alpha, CollinearSymmetry, -, NoncollinearityExtendsToLine; Segment (seg O A) /\ Segment (seg O B) /\ Segment (seg O A') [Osegments] by Distinctalpha, SEGMENT; consider C P D C' such that ~Collinear C P D /\ P IN open (C,C') /\ beta = angle C P D /\ beta' = angle D P C' [def_beta] by H1, SupplementaryAngles_DEF; ~(C = P) /\ ~(P = D) /\ ~(P = C') [Distinctbeta] by def_beta, NonCollinearImpliesDistinct, B1'; consider X such that X IN ray P C DELETE P /\ seg P X === seg O A [defX] by Osegments, Distinctbeta, C1; consider Y such that Y IN ray P D DELETE P /\ seg P Y === seg O B /\ ~(Y = P) [defY] by Osegments, Distinctbeta, C1, IN_DELETE; consider X' such that X' IN ray P C' DELETE P /\ seg P X' === seg O A' [defX'] by Osegments, Distinctbeta, C1; P IN open (X',C) /\ P IN open (X,X') [XPX'] by def_beta, -, 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_alpha, 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_beta, -, 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 Distinctbeta, defX, defY, defX', RayWellDefined; beta = angle X P Y /\ beta' = angle Y P X' /\ angle A O B === angle X P Y [AOBeqXPY] by def_beta, -, Angle_DEF, H2, def_alpha; 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_alpha, XPX'line, XPX', -, SegmentSymmetry, C3; A,O,B cong X,P,Y by def_alpha, XPYncol, OAeq, AOBeqXPY, SAS; seg A B === seg X Y /\ angle B A O === angle Y X P [AOBcong] by -, TriangleCong_DEF, AngleSymmetry; ray A O = ray A A' /\ ray X P = ray X X' /\ angle B A A' === angle Y X X' by def_alpha, XPX', IntervalRay, -, Angle_DEF; B,A,A' cong Y,X,X' by BAA'ncol, YXX'ncol, AOBcong, -, AA'eq, -, SAS; seg A' B === seg X' Y /\ angle A A' B === angle X X' Y by -, TriangleCong_DEF, SegmentSymmetry; O,A',B cong P,X',Y by BAA'ncol, YXX'ncol, OAeq, -, XPX'line, Angle_DEF, SAS; angle B O A' === angle Y P X' by -, TriangleCong_DEF; qed by -, equalPrays, def_beta, Angle_DEF, def_alpha; `;; let SupplementUnique = thm `; ! alpha beta beta': point_set. alpha suppl beta /\ alpha suppl beta' ==> beta === beta' by SupplementaryAngles_DEF, ANGLE, C5Reflexive, SupplementsCongAnglesCong; `;; let CongRightImpliesRight = thm `; let alpha beta be point_set; assume Angle alpha /\ Right beta [H1]; assume alpha === beta [H2]; thus Right alpha proof consider alpha' beta' such that alpha suppl alpha' /\ beta suppl beta' /\ beta === beta' [suppl] by H1, SupplementExists, H1, RightAngle_DEF; alpha' === beta' [alpha'eqbeta'] by suppl, H2, SupplementsCongAnglesCong; Angle beta /\ Angle alpha' /\ Angle beta' by suppl, SupplementImpliesAngle; alpha === alpha' by H1, -, H2, suppl, alpha'eqbeta', 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 IN open (A,A') [H1]; assume Right (angle A O B) /\ Right (angle A O P) [H2]; thus P NOTIN int_angle A O B proof assume ~(P NOTIN int_angle A O B); P IN int_angle A O B [PintAOB] by -, NOTIN; B IN int_angle P O A' /\ B IN 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; angle A O B suppl angle B O A' /\ angle A O P suppl angle P O A' [AOBsup] by H1, -, SupplementaryAngles_DEF; consider alpha' beta' such that angle A O B suppl alpha' /\ angle A O B === alpha' /\ angle A O P suppl beta' /\ angle A O P === beta' [supplalpha'] by H2, RightAngle_DEF; alpha' === angle B O A' /\ beta' === angle P O A' [alpha'eqA'OB] by -, AOBsup, SupplementUnique; Angle (angle A O B) /\ Angle alpha' /\ Angle (angle B O A') /\ Angle (angle A O P) /\ Angle beta' /\ Angle (angle P O A') [angles] by AOBsup, supplalpha', SupplementImpliesAngle, AngleSymmetry; angle A O B === angle B O A' /\ angle A O P === angle P O A' [H2'] by -, supplalpha', alpha'eqA'OB, C5Transitive; angle A O P === angle A O P /\ angle B O A' === angle B O A' [refl] by angles, C5Reflexive; angle A O P <_ang angle A O B /\ angle B O A' <_ang angle P O A' [BOA'lessPOA'] by angles, H1, PintAOB, -, AngleOrdering_DEF, AOPncol, CollinearSymmetry, BintA'OP, AngleSymmetry; angle A O P <_ang angle B O A' by -, angles, H2', AngleTrichotomy2; angle A O P <_ang angle P O A' by -, BOA'lessPOA', AngleOrderTransitivity; qed by -, H2', AngleTrichotomy1; `;; let RightAnglesCongruent = thm `; let alpha beta be point_set; assume Right alpha /\ Right beta [H1]; thus alpha === beta proof consider alpha' such that alpha suppl alpha' /\ alpha === alpha' by H1, RightAngle_DEF; consider A O B A' such that ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ alpha' = angle B O A' [def_alpha] by -, SupplementaryAngles_DEF; ~(A = O) /\ ~(O = B) [Distinct] by def_alpha, NonCollinearImpliesDistinct, B1'; consider a such that Line a /\ O IN a /\ A IN a [a_line] by Distinct, I1; B NOTIN a [notBa] by -, def_alpha, Collinear_DEF, NOTIN; Angle beta by H1, RightImpliesAngle; ?! r. Ray r /\ ? P. ~(O = P) /\ r = ray O P /\ P NOTIN a /\ P,B same_side a /\ angle A O P === beta by -, Distinct, a_line, notBa, C4; consider P such that ~(O = P) /\ P NOTIN a /\ P,B same_side a /\ angle A O P === beta [defP] by -; O NOTIN open (P,B) [notPOB] by a_line, -, SameSide_DEF, NOTIN; ~Collinear A O P [AOPncol] by a_line, Distinct, I1, defP, Collinear_DEF, NOTIN; Right (angle A O P) [AOPright] by -, ANGLE, H1, defP, CongRightImpliesRight; P NOTIN int_angle A O B /\ B NOTIN int_angle A O P by def_alpha, H1, -, AOPncol, AOPright, RightAnglesCongruentHelp; Collinear P O B by Distinct, a_line, defP, notBa, -, AngleOrdering, InteriorAngleSymmetry, NOTIN; P IN ray O B DELETE O by Distinct, -, CollinearSymmetry, notPOB, IN_Ray, defP, IN_DELETE; ray O P = ray O B /\ angle A O P = angle A O B by Distinct, -, RayWellDefined, Angle_DEF; qed by -, defP, def_alpha; `;; 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 (angle A O H) /\ Right (angle H O B) [H1]; assume Line h /\ O IN h /\ H IN h /\ ~(A,B same_side h) [H2]; thus O IN open (A,B) proof ~(A = O) /\ ~(O = H) /\ ~(O = B) [Distinct] by H0, NonCollinearImpliesDistinct; A NOTIN h /\ B NOTIN h [notABh] by H0, H2, Collinear_DEF, NOTIN; consider E such that O IN open (A,E) /\ ~(E = O) [AOE] by Distinct, B2', B1'; angle A O H suppl angle H O E [AOHsupplHOE] by H0, -, SupplementaryAngles_DEF; E NOTIN h [notEh] by H2, NOTIN, 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 alpha' such that angle A O H suppl alpha' /\ angle A O H === alpha' [AOHsupplalpha'] by H1, RightAngle_DEF; Angle (angle H O B) /\ Angle (angle A O H) /\ Angle alpha' /\ Angle (angle H O E) [angalpha'] by H1, RightImpliesAngle, -, AOHsupplHOE, SupplementImpliesAngle; angle H O B === angle A O H /\ alpha' === angle H O E by H1, RightAnglesCongruent, AOHsupplalpha', AOHsupplHOE, SupplementUnique; angle H O B === angle H O E by angalpha', -, AOHsupplalpha', C5Transitive; ray O B = ray O E by H2, Distinct, notABh, notEh, Bsim_hE, -, C4Uniqueness; B IN ray O E DELETE 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 IN open (A,A') [H2]; assume Right (angle A O B) [H3]; thus Right (angle B O A') proof angle A O B suppl angle B O A' /\ Angle (angle A O B) /\ Angle (angle B O A') [AOBsuppl] by H1, H2, SupplementaryAngles_DEF, SupplementImpliesAngle; consider beta such that angle A O B suppl beta /\ angle A O B === beta [betasuppl] by H3, RightAngle_DEF; Angle beta /\ beta === angle A O B [angbeta] by -, SupplementImpliesAngle, C5Symmetric; angle B O A' === beta by AOBsuppl, betasuppl, SupplementUnique; angle B O A' === angle A O B by AOBsuppl, angbeta, -, betasuppl, 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 angle C A B === angle A C B proof ~(A = B) /\ ~(B = C) /\ ~Collinear C B A [CBAncol] by H1, NonCollinearImpliesDistinct, CollinearSymmetry; seg B C === seg B A /\ angle A B C === angle C B A by -, SEGMENT, H2, C2Symmetric, H1, ANGLE, AngleSymmetry, C5Reflexive; A,B,C cong C,B,A by H1, CBAncol, H2, -, SAS; qed by -, TriangleCong_DEF; `;; let C4withC1 = thm `; let alpha l be point_set; let O A Y P Q be point; assume Angle alpha /\ ~(O = A) /\ ~(P = Q) [H1]; assume Line l /\ O IN l /\ A IN l /\ Y NOTIN l [l_line]; thus ? N. ~(O = N) /\ N NOTIN l /\ N,Y same_side l /\ seg O N === seg P Q /\ angle A O N === alpha proof ?! r. Ray r /\ ? B. ~(O = B) /\ r = ray O B /\ B NOTIN l /\ B,Y same_side l /\ angle A O B === alpha by H1, l_line, C4; consider B such that ~(O = B) /\ B NOTIN l /\ B,Y same_side l /\ angle A O B === alpha [Bexists] by -; consider N such that N IN ray O B DELETE O /\ seg O N === seg P Q [Nexists] by H1, -, SEGMENT, C1; ~(O = N) [notON] by -, IN_DELETE; N NOTIN 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 /\ angle A O N === alpha by Bexists, Nexists, RayWellDefined, Angle_DEF; qed by notON, notNl, Nsim_lY, Nexists, -; `;; let C4OppositeSide = thm `; let alpha l be point_set; let O A Z P Q be point; assume Angle alpha /\ ~(O = A) /\ ~(P = Q) [H1]; assume Line l /\ O IN l /\ A IN l /\ Z NOTIN l [l_line]; thus ? N. ~(O = N) /\ N NOTIN l /\ ~(Z,N same_side l) /\ seg O N === seg P Q /\ angle A O N === alpha proof ~(Z = O) by l_line, NOTIN; consider Y such that O IN open (Z,Y) [ZOY] by -, B2'; ~(O = Y) /\ Collinear Z O Y by -, B1'; Y NOTIN l [notYl] by l_line, I1, -, Collinear_DEF, NOTIN; consider N such that ~(O = N) /\ N NOTIN l /\ N,Y same_side l /\ seg O N === seg P Q /\ angle A O N === alpha [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 cong 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 IN h /\ C IN h [h_line] by Distinct, I1; B NOTIN h [notBh] by h_line, H1, NOTIN, Collinear_DEF; Segment (seg A B) /\ Segment (seg C B) /\ Segment (seg A' B') /\ Segment (seg C' B') [segments] by Distinct, -, SEGMENT; Angle (angle C' A' B') by H1, CollinearSymmetry, ANGLE; consider N such that ~(A = N) /\ N NOTIN h /\ ~(B,N same_side h) /\ seg A N === seg A' B' /\ angle C A N === angle C' A' B' [Nexists] by -, Distinct, h_line, notBh, C4OppositeSide; ~(C = N) by h_line, Nexists, NOTIN; 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, NOTIN; Angle (angle A B C) /\ Angle (angle A' B' C') /\ Angle (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 cong C',A',B' by ANCncol, H1, CollinearSymmetry, H2, Nexists, SAS; angle A N C === angle 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 IN h /\ G IN 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 IN v /\ N IN v [v_line] by notBN, I1; G IN v /\ ~(h = v) by v_line, BGN, BetweenLinear, notBh, NOTIN; h INTER v = {G} [hvG] by h_line, v_line, -, BGN, I1Uniqueness; ~(G = A) ==> angle A B G === angle A N G [ABGeqANG] proof assume ~(G = A) [notGA]; A NOTIN v by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE; ~Collinear B A N by v_line, notBN, I1, Collinear_DEF, -, NOTIN; angle N B A === angle B N A by -, ABeqAN, IsoscelesCongBaseAngles; angle G B A === angle G N A by -, Grays, Angle_DEF, notGA; qed by -, AngleSymmetry; ~(G = C) ==> angle G B C === angle G N C [GBCeqGNC] proof assume ~(G = C) [notGC]; C NOTIN v by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE; ~Collinear B C N by v_line, notBN, I1, Collinear_DEF, -, NOTIN; angle N B C === angle B N C by -, CBeqCN, IsoscelesCongBaseAngles, AngleSymmetry; qed by -, Grays, Angle_DEF; angle A B C === angle 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]; angle A B G === angle A N G /\ angle G B C === angle 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, NOTIN; Collinear A G C by h_line, BGN, Collinear_DEF; G IN open (A,C) \/ C IN open (G,A) \/ A IN open (C,G) by Distinct, AGCdistinct, -, B3'; cases by -; suppose G IN open (A,C); G IN int_angle A B C /\ G IN int_angle A N C by H1, ANCncol, -, ConverseCrossbar; qed by -, Gequivs, AngleAddition; suppose C IN open (G,A); C IN int_angle G B A /\ C IN int_angle G N A by Gncols, -, B1', ConverseCrossbar; qed by -, Gequivs, AngleSubtraction, AngleSymmetry; suppose A IN open (C,G); A IN int_angle G B C /\ A IN int_angle G N C by Gncols, -, B1', ConverseCrossbar; qed by -, Gequivs, AngleSymmetry, AngleSubtraction; end; end; angle A B C === angle 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 IN int_angle B A C /\ angle B A F === angle F A C proof ~(A = B) /\ ~(A = C) [Distinct] by H1, NonCollinearImpliesDistinct; consider D such that B IN 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 IN ray A C DELETE A /\ seg A E === seg A D /\ ~(A = E) [ErAC] by -, Distinct, C1, IN_DELETE, IN_Ray; Collinear A C E /\ D IN ray A B DELETE 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; angle D E A === angle E D A [DEAeq] by EADncol, ErAC, IsoscelesCongBaseAngles; ~Collinear E D A /\ Angle (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 IN h /\ E IN h [h_line] by -, I1; A NOTIN h [notAh] by -, Collinear_DEF, EADncol, NOTIN; consider F such that ~(D = F) /\ F NOTIN h /\ ~(A,F same_side h) /\ seg D F === seg D A /\ angle E D F === angle 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, NOTIN; seg D E === seg D E /\ seg F A === seg F A [FArefl] by notDE, notAF, SEGMENT, C2Reflexive; E,D,F cong E,D,A by EDFncol, angEDA, -, Fexists, SAS; seg F E === seg A E /\ angle F E D === angle A E D [FEDcong] by -, TriangleCong_DEF, SegmentSymmetry; angle E D A === angle D E A /\ angle E D A === angle E D F /\ angle D E A === angle D E F [EDAeqEDF] by EDFncol, ANGLE, angEDA, Fexists, FEDcong, DEAeq, C5Symmetric, AngleSymmetry; consider G such that G IN h /\ G IN open (A,F) [AGF] by Fexists, h_line, SameSide_DEF; F IN ray A G DELETE A [FrAG] by -, IntervalRayEZ; consider v such that Line v /\ A IN v /\ F IN v /\ G IN v [v_line] by notAF, I1, AGF, BetweenLinear; ~(v = h) /\ v INTER h = {G} [vhG] by -, notAh, NOTIN, h_line, AGF, I1Uniqueness; D NOTIN v [notDv] proof assume ~(D NOTIN v); D IN v /\ D = G [DG] by h_line, -, NOTIN, vhG, IN_INTER, IN_SING; D IN open (A,F) by DG, AGF; angle E D A suppl angle E D F [EDAsuppl] by angEDA, -, SupplementaryAngles_DEF, AngleSymmetry; Right (angle E D A) by EDAsuppl, EDAeqEDF, RightAngle_DEF; Right (angle A E D) [RightAED] by angEDA, ANGLE, -, DEAeq, CongRightImpliesRight, AngleSymmetry; Right (angle D E F) by EDFncol, ANGLE, -, FEDcong, CongRightImpliesRight, AngleSymmetry; E IN open (A,F) by EADncol, EDFncol, RightAED, -, h_line, Fexists, OppositeRightAnglesLinear; E IN v /\ E = G by v_line, -, BetweenLinear, h_line, vhG, IN_INTER, IN_SING; qed by -, DG, notDE; E NOTIN v [notEv] proof assume ~(E NOTIN v); E IN v /\ E = G [EG] by h_line, -, NOTIN, vhG, IN_INTER, IN_SING; E IN open (A,F) by -, AGF; angle D E A suppl angle D E F [DEAsuppl] by EADncol, -, SupplementaryAngles_DEF, AngleSymmetry; Right (angle D E A) [RightDEA] by DEAsuppl, EDAeqEDF, RightAngle_DEF; Right (angle E D A) [RightEDA] by angEDA, RightDEA, EDAeqEDF, CongRightImpliesRight; Right (angle E D F) by EDFncol, ANGLE, RightEDA, Fexists, CongRightImpliesRight; D IN open (A,F) by angEDA, EDFncol, RightEDA, AngleSymmetry, -, h_line, Fexists, OppositeRightAnglesLinear; D IN 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, NOTIN, NonCollinearImpliesDistinct; seg F E === seg A D [FEeqAD] by -, ErAC, ABD', SEGMENT, FEDcong, 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 cong F,A,D by FAEncol, FArefl, -, ErAC, SSS; angle F A E === angle F A D [FAEeq] by -, TriangleCong_DEF; angle D A F === angle F A E by FAEncol, ANGLE, FAEeq, C5Symmetric, AngleSymmetry; angle B A F === angle 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 IN v /\ H IN open (E,D) [EHD] by v_line, -, SameSide_DEF; H = G by -, h_line, BetweenLinear, IN_INTER, vhG, IN_SING; G IN int_angle E A D [GintEAD] by EADncol, -, EHD, ConverseCrossbar; F IN int_angle E A D [FintEAD] by GintEAD, FrAG, WholeRayInterior; B IN ray A D DELETE A /\ C IN ray A E DELETE A by equalrays, Distinct, EndpointInRay, IN_DELETE; F IN 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 angle B A C === angle 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; angle A C B === angle C A B by -, ANGLE, H2, C5Symmetric, AngleSymmetry; C,B,A cong 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 IN l /\ B IN l [l_line] by H1, I1; consider C such that C NOTIN 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, -, NOTIN; angle C A B === angle C B A \/ angle C A B <_ang angle C B A \/ angle C B A <_ang angle C A B by -, ANGLE, AngleTrichotomy; cases by -; suppose angle C A B === angle C B A; qed by -, CABncol, EuclidPropositionI_6; suppose angle C A B <_ang angle C B A; angle C A B <_ang angle A B C by -, AngleSymmetry; consider E such that E IN int_angle A B C /\ angle C A B === angle A B E [Eexists] by CABncol, ANGLE, -, AngleOrderingUse; ~(B = E) [notBE] by -, InteriorEZHelp; consider D such that D IN open (A,C) /\ D IN ray B E DELETE B [Dexists] by Eexists, Crossbar_THM; D IN 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; angle D A B === angle A B D by Eexists, -, Angle_DEF; qed by ADBncol, -, AngleSymmetry, EuclidPropositionI_6; :: similar case suppose angle C B A <_ang angle C A B; angle C B A <_ang angle B A C by -, AngleSymmetry; consider E such that E IN int_angle B A C /\ angle C B A === angle B A E [Eexists] by CABncol, ANGLE, -, AngleOrderingUse; ~(A = E) [notAE] by -, InteriorEZHelp; consider D such that D IN open (B,C) /\ D IN ray A E DELETE A [Dexists] by Eexists, Crossbar_THM; D IN 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; angle D B A === angle B A D by Eexists, -, Angle_DEF; angle D A B === angle 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 IN 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 IN int_angle A D B /\ angle A D F === angle F D B [Fexists] by -, AngleBisector; ~(D = F) [notDF] by -, InteriorEZHelp; consider M such that M IN open (A,B) /\ M IN ray D F DELETE D [Mexists] by Fexists, Crossbar_THM; ray D M = ray D F by notDF, -, RayWellDefined; angle A D M === angle M D B [ADMeqMDB] by Fexists, -, Angle_DEF; M IN 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 cong 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 IN a /\ B IN a [a_line]; assume ~(C = D) /\ C NOTIN a /\ D NOTIN 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, NOTIN; 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, NOTIN; A,C,B cong A,D,B by -, ACeqAD, segeqs, SSS; angle B A C === angle B A D by -, TriangleCong_DEF; ray A D = ray A C by a_line, Csim_aD, -, C4Uniqueness; C IN ray A D DELETE A /\ D IN ray A D DELETE 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 IN a /\ B IN a [a_line]; assume ~(C = D) /\ C NOTIN a /\ D NOTIN a /\ C,D same_side a [Csim_aD]; assume seg A C === seg A D [ACeqAD]; assume C IN 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, NOTIN, SameSide_DEF; cases by Int_ConvQuad; suppose ConvexQuadrilateral A B C D; A IN int_angle B C D /\ B IN 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 (angle D C A) /\ Angle (angle C D B) [angCDB] by -, Tetralateral_DEF, CollinearSymmetry, ANGLE; angle C D A === angle D C A [CDAeqDCA] by angCDB, Distinct, SEGMENT, ACeqAD, C2Symmetric, IsoscelesCongBaseAngles; A IN int_angle D C B /\ angle D C A === angle D C A /\ angle C D B === angle C D B by ABint, InteriorAngleSymmetry, angCDB, ANGLE, C5Reflexive; angle D C A <_ang angle D C B /\ angle C D B <_ang angle C D A by angCDB, ABint, -, AngleOrdering_DEF; angle C D B <_ang angle D C B by -, angCDB, CDAeqDCA, AngleTrichotomy2, AngleOrderTransitivity; ~(angle D C B === angle C D B) by -, AngleTrichotomy1, angCDB, ANGLE, C5Symmetric; qed by angCDB, -, IsoscelesCongBaseAngles; suppose C IN int_triangle D A B; C IN int_angle A D B /\ C IN 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 (angle D C A) /\ Angle (angle C D B) /\ ~Collinear D C B [angCDB] by ADCncol, -, CollinearSymmetry, ANGLE; angle C D A === angle D C A [CDAeqDCA] by DACncol, Distinct, ADCncol, SEGMENT, ACeqAD, C2Symmetric, IsoscelesCongBaseAngles; consider E such that D IN open (A,E) /\ ~(D = E) /\ Collinear A D E [ADE] by Distinct, B2', B1'; B IN 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 IN open (B,D) /\ F IN ray A C DELETE A [Fexists] by CintADB, Crossbar_THM, B1'; F IN 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 IN ray D B DELETE D /\ C IN int_angle A D F by Fexists, IN_DELETE, IN_Ray, B1', IntervalRayEZ, CintADB, InteriorWellDefined; C IN open (A,F) by -, AlternateConverseCrossbar; angle A D C suppl angle C D E /\ angle A C D suppl angle D C F by ADE, DACncol, -, SupplementaryAngles_DEF; angle C D E === angle D C F [CDEeqDCF] by -, CDAeqDCA, AngleSymmetry, SupplementsCongAnglesCong; angle C D B <_ang angle C D E by angCDB, CDEncol, BintCDE, C5Reflexive, AngleOrdering_DEF; angle C D B <_ang angle D C F [CDBlessDCF] by -, DCFncol, ANGLE, CDEeqDCF, AngleTrichotomy2; angle D C F <_ang angle D C B by DCFncol, ANGLE, angCDB, FintBCD, InteriorAngleSymmetry, C5Reflexive, AngleOrdering_DEF; angle C D B <_ang angle D C B by CDBlessDCF, -, AngleOrderTransitivity; ~(angle D C B === angle 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 IN a /\ B IN a [a_line]; assume ~(C = D) /\ C NOTIN a /\ D NOTIN 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, NOTIN; ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ A NOTIN open (C,D) [Distinct] by a_line, Csim_aD, NOTIN, SameSide_DEF; ~Collinear A D C [ADCncol] proof assume Collinear A D C; C IN ray A D DELETE A /\ D IN ray A D DELETE 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 NOTIN open (C,D) /\ C IN ray B D DELETE B /\ D IN ray B D DELETE B by a_line, Csim_aD, SameSide_DEF, NOTIN, 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 IN int_triangle D A B \/ ConvexQuadrilateral A B D C \/ D IN 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 (angle A B F) proof consider C such that B IN 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 (angle A B F) [angABF] by BFAncol, CollinearSymmetry, ANGLE; angle A B F suppl angle F B C [ABFsuppl] by -, ABC, SupplementaryAngles_DEF; ~(B = F) /\ seg B F === seg B F by BFAncol, NonCollinearImpliesDistinct, SEGMENT, C2Reflexive; B,F,A cong B,F,C by BFAncol, -, BAeqBC, Fexists, SSS; angle A B F === angle 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 NOTIN l [l_line]; thus ? E Q. E IN l /\ Q IN l /\ Right (angle P Q E) proof consider A B such that A IN l /\ B IN 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, NOTIN, CollinearSymmetry, ABl, NOTIN; Angle (angle B A P) /\ Angle (angle P A B) [angBAP] by -, ANGLE, AngleSymmetry; consider P' such that ~(A = P') /\ P' NOTIN l /\ ~(P,P' same_side l) /\ seg A P' === seg A P /\ angle B A P' === angle B A P [P'exists] by angBAP, ABl, BAPncol, l_line, C4OppositeSide; consider Q such that Q IN l /\ Q IN 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, NOTIN; angle B A P === angle B A P' [BAPeqBAP'] by -, ANGLE, angBAP, P'exists, C5Symmetric; ? E. E IN l /\ ~Collinear P Q E /\ angle P Q E === angle 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, NOTIN; angle Q A P === angle Q A P' proof cases; suppose A IN open (Q,B); angle B A P suppl angle P A Q /\ angle B A P' suppl angle P' A Q by BAPncol, BAP'ncol, -, B1', SupplementaryAngles_DEF; qed by -, BAPeqBAP', SupplementsCongAnglesCong, AngleSymmetry; suppose ~(A IN open (Q,B)); A NOTIN open (Q,B) /\ Q IN ray A B DELETE A /\ ray A Q = ray A B by -, NOTIN, ABl, Qexists, IN_Ray, notAQ, IN_DELETE, ABl, RayWellDefined; qed by -, BAPeqBAP', Angle_DEF; end; Q,A,P cong Q,A,P' by QAP'ncol, APeqAP', -, SAS; qed by -, TriangleCong_DEF, AngleSymmetry, ABl, QAP'ncol, CollinearSymmetry; end; consider E such that E IN l /\ ~Collinear P Q E /\ angle P Q E === angle E Q P' [Eexists] by -; angle P Q E suppl angle E Q P' /\ Right (angle 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 IN l /\ B IN l /\ ~(A = B) [l_line]; assume C NOTIN l /\ D NOTIN l /\ ~(C,D same_side l) [Cnsim_lD]; assume angle C B A suppl angle A B D [CBAsupplABD]; thus B IN open (C,D) proof ~(B = C) /\ ~(B = D) /\ ~Collinear C B A [Distinct] by l_line, Cnsim_lD, NOTIN, I1, Collinear_DEF; consider E such that B IN open (C,E) [CBE] by Distinct, B2'; E NOTIN l /\ ~(C,E same_side l) [Csim_lE] by l_line, NOTIN, -, BetweenLinear, Cnsim_lD, SameSide_DEF; D,E same_side l [Dsim_lE] by l_line, Cnsim_lD, -, AtMost2Sides; angle C B A suppl angle A B E by Distinct, CBE, SupplementaryAngles_DEF; angle A B D === angle A B E by CBAsupplABD, -, SupplementUnique; ray B E = ray B D by l_line, Csim_lE, Cnsim_lD, Dsim_lE, -, C4Uniqueness; D IN ray B E DELETE 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 IN open (A,A') /\ O IN open (B,B') [H2]; thus angle B O A' === angle B' O A proof angle A O B suppl angle B O A' [AOBsupplBOA'] by H1, H2, SupplementaryAngles_DEF; angle B O A suppl angle 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 IN open (B,D) [H2]; thus angle B A C <_ang angle D C A proof ~(A = B) /\ ~(A = C) /\ ~(B = C) [Distinct] by H1, NonCollinearImpliesDistinct; consider l such that Line l /\ A IN l /\ C IN l [l_line] by Distinct, I1; consider m such that Line m /\ B IN m /\ C IN m [m_line] by Distinct, I1; D IN m [Dm] by m_line, H2, BetweenLinear; consider E such that E IN 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 IN l [El] by l_line, AEC, BetweenLinear; consider F such that E IN 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 NOTIN l [notBl] by l_line, Distinct, I1, Collinear_DEF, H1, NOTIN; ~Collinear A E B /\ ~Collinear C E B [AEBncol] by l_line, El, AECcol, I1, Collinear_DEF, notBl, NOTIN; Angle (angle B A E) [angBAE] by -, CollinearSymmetry, ANGLE; ~Collinear C E F [CEFncol] by AEBncol, BEF', CollinearSymmetry, NoncollinearityExtendsToLine; angle B E A === angle 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 cong C,E,F by AEBncol, CEFncol, -, BEAeqFEC, AngleSymmetry, SAS; angle B A E === angle F C E [BAEeqFCE] by -, TriangleCong_DEF; ~Collinear E C D [ECDncol] by AEBncol, H2, B1', CollinearSymmetry, NoncollinearityExtendsToLine; F NOTIN l /\ D NOTIN l [notFl] by l_line, El, Collinear_DEF, CEFncol, -, NOTIN; F IN ray B E DELETE B /\ E NOTIN m by BEF, IntervalRayEZ, m_line, Collinear_DEF, AEBncol, NOTIN; F NOTIN 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 IN int_angle E C D by ECDncol, l_line, El, m_line, Dm, notFl, Fsim_mE, -, IN_InteriorAngle; angle B A E <_ang angle 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; angle B A C <_ang angle 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 IN open (B,D) [H2]; thus angle A B C <_ang angle A C D proof ~(C = D) /\ C IN 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 IN open (A,E) [ACE] by -, B2'; ~(C = E) /\ C IN open (E,A) /\ Collinear A C E [ACE'] by -, B1'; ~Collinear A C D /\ ~Collinear D C E [DCEncol] by H1, CollinearSymmetry, H2', -, NoncollinearityExtendsToLine; angle A B C <_ang angle E C B [ABClessECB] by BACncol, ACE, EuclidPropositionI_16; angle E C B === angle 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 alpha beta gamma be point_set; assume ~Collinear A B C /\ alpha = angle A B C /\ beta = angle B C A [H1]; assume beta suppl gamma [H2]; thus alpha <_ang gamma proof Angle gamma [anggamma] 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 IN open (A,D) [ACD] by Distinct, B2'; angle A B C <_ang angle D C B [ABClessDCB] by BACncol, ACD, EuclidPropositionI_16; beta suppl angle B C D by -, H1, AngleSymmetry, BACncol, ACD, SupplementaryAngles_DEF; angle B C D === gamma by H2, -, SupplementUnique; qed by ABClessDCB, H1, AngleSymmetry, anggamma, -, 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 angle A B C <_ang angle B C A proof ~(A = B) /\ ~(A = C) [Distinct] by H1, NonCollinearImpliesDistinct; consider D such that D IN open (A,B) /\ seg A C === seg A D [ADB] by Distinct, SEGMENT, H2, SegmentOrderingUse; ~(D = A) /\ ~(D = B) /\ D IN open (B,A) /\ Collinear A D B /\ ray B D = ray B A [ADB'] by -, B1', IntervalRay; D IN 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; angle C D A === angle A C D by DACncol, -, IsoscelesCongBaseAngles, AngleSymmetry; angle C D A <_ang angle A C B [CDAlessACB] by DACncol, CollinearSymmetry, ANGLE, H1, CollinearSymmetry, DintACB, -, AngleOrdering_DEF; angle B D C suppl angle C D A by DACncol, CollinearSymmetry, ADB', SupplementaryAngles_DEF; angle C B D <_ang angle C D A by DACncol, -, EuclidPropositionI_17; angle C B D <_ang angle 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 angle A B C <_ang angle 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; angle C B A === angle B C A by BACncol, -, IsoscelesCongBaseAngles; qed by -, AngleSymmetry, H2, AngleTrichotomy1; suppose seg A B <__ seg A C; angle A C B <_ang angle 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 IN open (B,D) /\ seg A D === seg A C [H2]; thus seg B C <__ seg B D proof ~(B = D) /\ ~(A = D) /\ A IN 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 (angle C D A) [angCDA] by CADncol, CollinearSymmetry, ANGLE; angle C D A === angle D C A [CDAeqDCA] by CADncol, CollinearSymmetry, H2, IsoscelesCongBaseAngles; A IN int_angle D C B by DCBncol, BAD', ConverseCrossbar; angle C D A <_ang angle D C B by angCDA, DCBncol, -, CDAeqDCA, AngleOrdering_DEF; angle B D C <_ang angle 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 IN int_triangle A B C [H2]; thus angle A B C <_ang angle C D A proof ~(B = A) /\ ~(B = C) /\ ~(A = C) [Distinct] by H1, NonCollinearImpliesDistinct; D IN int_angle B A C /\ D IN int_angle C B A [DintTri] by H2, IN_InteriorTriangle, InteriorAngleSymmetry; consider E such that E IN open (B,C) /\ E IN ray A D DELETE 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 IN ray B C DELETE B [rBErBC] by BEC, IntervalRay, IntervalRayEZ; D IN int_angle A B E [DintABE] by DintTri, -, InteriorAngleSymmetry, InteriorWellDefined; D IN 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; angle A B E <_ang angle A E C by ABEncol, BEC, ExteriorAngle; angle A B C <_ang angle C E D [ABClessAEC] by -, rBErBC, rEDrEA, Angle_DEF, AngleSymmetry; angle C E D <_ang angle C D A by EDCncol, ADE, B1', ExteriorAngle; qed by ABClessAEC, -, AngleOrderTransitivity; `;; let AngleTrichotomy3 = thm `; let alpha beta gamma be point_set; assume alpha <_ang beta /\ Angle gamma /\ gamma === alpha [H1]; thus gamma <_ang beta proof consider A O B G such that Angle alpha /\ ~Collinear A O B /\ beta = angle A O B /\ G IN int_angle A O B /\ alpha === angle A O G [H1'] by H1, AngleOrdering_DEF; ~Collinear A O G by -, InteriorEZHelp; gamma === angle 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 IN 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'; angle O C A <_ang angle C A O \/ angle O C A === angle 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; angle O C B <_ang angle B A O \/ angle O C B === angle B A O by -, equal_rays, Angle_DEF; angle B C O <_ang angle O A B \/ angle B C O === angle 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; angle O A B <_ang angle O B C by -, H2, ExteriorAngle; angle B C O <_ang angle 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 IN open (A,C) [H2]; assume A IN int_circle O R /\ C IN int_circle O R [H3]; thus B IN int_circle O R proof ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ B IN 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 IN open (O,C) \/ B IN 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 IN l /\ C IN l by H2', I1; Collinear B A O /\ Collinear B C O [OABCcol] by -, H2, BetweenLinear, H2', AOCcol, CollinearLinear, Collinear_DEF; B NOTIN open (O,A) /\ B NOTIN open (O,C) ==> B = O proof assume B NOTIN open (O,A) /\ B NOTIN open (O,C); O IN ray B A INTER ray B C by H2', OABCcol, -, IN_Ray, IN_INTER; qed by -, H2, OppositeRaysIntersect1point, IN_SING; B IN open (O,A) \/ B IN open (O,C) \/ B = O by -, NOTIN; 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 IN 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 angle D O' F <_ang angle 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 IN int_angle A O C /\ angle D O' F === angle 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 IN ray O K DELETE O /\ seg O B === seg O C [BrOK] by Distinct, SEGMENT, -, C1; ray O B = ray O K by Distinct, -, RayWellDefined; angle D O' F === angle A O B [DO'FeqAOB] by KintAOC, -, Angle_DEF; B IN 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 cong 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 IN open (A,C) /\ G IN ray O B DELETE 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' IN 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' IN ray O B DELETE O by OG'B, IntervalRayEZ; G' = G /\ G IN open (B,O) by notG'O, notOB, -, AGC, OG'B, C1, B1'; ConvexQuadrilateral B A O C by H1, -, AGC, DiagonalsIntersectImpliesConvexQuad; A IN int_angle O C B /\ O IN int_angle C B A /\ Quadrilateral B A O C [OintCBA] by -, ConvexQuad_DEF; A IN 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; angle B C O === angle C B O [BCOeqCBO] by -, OCeqOB, IsoscelesCongBaseAngles; ~Collinear B C A /\ ~Collinear A C B [ACBncol] by AintBCO, InteriorEZHelp, CollinearSymmetry; angle B C A === angle B C A /\ Angle (angle B C A) /\ angle C B O === angle C B O [CBOref] by -, ANGLE, BCOncol, C5Reflexive; angle B C A <_ang angle B C O by -, BCOncol, ANGLE, AintBCO, AngleOrdering_DEF; angle B C A <_ang angle C B O [BCAlessCBO] by -, BCOncol, ANGLE, BCOeqCBO, AngleTrichotomy2; angle C B O <_ang angle C B A by BCOncol, ANGLE, OintCBA, CBOref, AngleOrdering_DEF; angle A C B <_ang angle 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 angle D O' F <_ang angle 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]; angle F O' D <_ang angle 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 angle D O' F <_ang angle A O C proof ~(O = A) /\ ~(O = C) /\ ~(A = C) /\ ~(D = F) /\ ~(O' = D) /\ ~(O' = F) [Distinct] by H1, NonCollinearImpliesDistinct; assume ~(angle D O' F <_ang angle A O C); angle D O' F === angle A O C \/ angle A O C <_ang angle D O' F by H1, ANGLE, -, AngleTrichotomy; cases by -; suppose angle D O' F === angle A O C; D,O',F cong A,O,C by H1, H2, -, SAS; seg D F === seg A C by -, TriangleCong_DEF; qed by Distinct, SEGMENT, -, H3, SegmentTrichotomy; suppose angle A O C <_ang angle 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 angle A B C === angle A' B' C' /\ angle B C A === angle B' C' A' [H2]; assume seg A B === seg A' B' [H3]; thus A,B,C cong A',B',C' proof ~(A = B) /\ ~(B = C) /\ ~(B' = C') [Distinct] by H1, NonCollinearImpliesDistinct; consider G such that G IN ray B C DELETE B /\ seg B G === seg B' C' [Gexists] by Distinct, SEGMENT, C1; ~(G = B) /\ B NOTIN 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; angle A B G = angle A B C by Distinct, -, Angle_DEF; A,B,G cong A',B',C' [ABGcongA'B'C'] by H1, ABGncol, H3, SegmentSymmetry, H2, -, Gexists, SAS; angle B G A === angle B' C' A' [BGAeqB'C'A'] by -, TriangleCong_DEF; ~Collinear B C A /\ ~Collinear B' C' A' [BCAncol] by H1, CollinearSymmetry; angle B' C' A' === angle B C A /\ angle B C A === angle B C A [BCArefl] by -, ANGLE, H2, C5Symmetric, C5Reflexive; angle B G A === angle B C A [BGAeqBCA] by ABGncol, BCAncol, ANGLE, BGAeqB'C'A', -, C5Transitive; cases; suppose G = C; qed by -, ABGcongA'B'C'; suppose ~(G = C) [notGC]; ~Collinear A C G /\ ~Collinear A G C [ACGncol] by H1, notGBC, -, CollinearSymmetry, NoncollinearityExtendsToLine; C IN open (B,G) \/ G IN open (C,B) by notGBC, notGC, Distinct, B3', NOTIN; cases by -; suppose C IN open (B,G) ; C IN open (G,B) /\ ray G C = ray G B [rGCrBG] by -, B1', IntervalRay; angle A G C <_ang angle A C B by ACGncol, -, ExteriorAngle; angle B G A <_ang angle B C A by -, rGCrBG, Angle_DEF, AngleSymmetry, AngleSymmetry; qed by ABGncol, BCAncol, ANGLE, -, AngleSymmetry, BGAeqBCA, AngleTrichotomy; suppose G IN open (C,B) [CGB]; ray C G = ray C B /\ angle A C G <_ang angle A G B by -, IntervalRay, ACGncol, ExteriorAngle; angle A C B <_ang angle B G A by -, Angle_DEF, AngleSymmetry; angle B C A <_ang angle B C A by -, BCAncol, ANGLE, BGAeqBCA, AngleTrichotomy2, AngleSymmetry; qed by -, BCArefl, AngleTrichotomy1; end; end; `;; let ParallelSymmetry = thm `; ! l k: point_set. l parallel k ==> k parallel 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 IN l /\ E IN l [l_line]; assume Line m /\ B IN m /\ C IN m [m_line]; assume Line t /\ A IN t /\ B IN t [t_line]; assume ~(A = E) /\ ~(B = C) /\ ~(A = B) /\ E NOTIN t /\ C NOTIN t [Distinct]; assume ~(C,E same_side t) [Cnsim_tE]; assume angle E A B === angle C B A [AltIntAngCong]; thus l parallel m proof ~Collinear E A B /\ ~Collinear C B A [EABncol] by t_line, Distinct, I1, Collinear_DEF, NOTIN; B NOTIN l /\ A NOTIN m [notAmBl] by l_line, m_line, Collinear_DEF, -, NOTIN; assume ~(l parallel m); ~(l INTER m = {}) by -, l_line, m_line, PARALLEL; consider G such that G IN l /\ G IN 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, NOTIN, m_line, l_line, Collinear_DEF; ~Collinear A G B /\ ~Collinear B G A /\ G NOTIN t [AGBncol] by EABncol, CollinearSymmetry, -, NoncollinearityExtendsToLine, t_line, Collinear_DEF, NOTIN; ~(E,C same_side t) [Ensim_tC] by t_line, -, Distinct, Cnsim_tE, SameSideSymmetric; C IN m DELETE B /\ G IN m DELETE B [CGm_B] by m_line, Glm, Distinct, GnotAB, IN_DELETE; E IN l DELETE A /\ G IN l DELETE 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 NOTIN open (G,E) [notGAE] by t_line, -, SameSide_DEF, NOTIN; G IN ray A E DELETE 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 NOTIN ray B G /\ B IN open (C,G) by t_line, AGBncol, Distinct, -, RaySameSide, NOTIN, GnotAB, IN_DELETE, IN_Ray; angle G A B <_ang angle C B A by AGBncol, -, B1', EuclidPropositionI_16; angle E A B <_ang angle 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 NOTIN open (G,C) [notGBC] by t_line, -, SameSide_DEF, NOTIN; G IN ray B C DELETE B by Distinct, GnotAB, notGBC, IN_Ray, GnotAB, IN_DELETE; ray B G = ray B C [rBGrBC] by Distinct, -, RayWellDefined; angle C B A === angle 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 NOTIN ray A G /\ A IN open (E,G) by t_line, AGBncol, Distinct, -, RaySameSide, NOTIN, GnotAB, IN_Ray, IN_DELETE; angle G B A <_ang angle E A B by AGBncol, -, B1', EuclidPropositionI_16; angle C B A <_ang angle 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 IN l /\ B IN l /\ G IN l [l_line]; assume Line m /\ C IN m /\ D IN m /\ H IN m [m_line]; assume Line t /\ G IN t /\ H IN t [t_line]; assume G NOTIN m /\ H NOTIN l [notGmHl]; assume G IN open (A,B) /\ H IN open (C,D) [H1]; assume G IN open (E,H) /\ H IN open (F,G) [H2]; assume ~(D,A same_side t) [H3]; assume angle E G B === angle G H D \/ angle B G H suppl angle G H D [H4]; thus l parallel 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 NOTIN t /\ D NOTIN t [HGAncol] by l_line, m_line, Distinct, I1, Collinear_DEF, notGmHl, NOTIN, t_line, Collinear_DEF; ~Collinear B G H /\ ~Collinear A G E /\ ~Collinear E G B [BGHncol] by -, Distinct, CollinearSymmetry, NoncollinearityExtendsToLine; angle A G H === angle D H G proof cases by H4; suppose angle E G B === angle G H D [EGBeqGHD]; angle E G B === angle H G A by BGHncol, H1, H2, VerticalAnglesCong; angle H G A === angle E G B by BGHncol, HGAncol, ANGLE, -, C5Symmetric; angle H G A === angle G H D by BGHncol, HGAncol, ANGLE, -, EGBeqGHD, C5Transitive; qed by -, AngleSymmetry; suppose angle B G H suppl angle G H D [BGHeqGHD]; angle B G H suppl angle 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 IN a /\ B IN a /\ Line c /\ C IN c /\ D IN c [ac_line] by TetraABCD, I1; consider b d such that Line b /\ B IN b /\ C IN b /\ Line d /\ D IN d /\ A IN d [bd_line] by TetraABCD, I1; consider l such that Line l /\ A IN l /\ C IN l [l_line] by TetraABCD, I1; consider m such that Line m /\ B IN m /\ D IN m [m_line] by TetraABCD, I1; B NOTIN l /\ D NOTIN l /\ A NOTIN m /\ C NOTIN m [notBDlACm] by l_line, m_line, TetraABCD, Collinear_DEF, NOTIN; seg A C === seg C A /\ seg B D === seg D B [seg_refl] by TetraABCD, SEGMENT, C2Reflexive, SegmentSymmetry; A,B,C cong C,D,A by TetraABCD, H2, -, SSS; angle B C A === angle D A C /\ angle C A B === angle A C D [BCAeqDAC] by -, TriangleCong_DEF; seg C D === seg A B [CDeqAB] by TetraABCD, SEGMENT, H2, C2Symmetric; B,C,D cong D,A,B by TetraABCD, H2, -, seg_refl, SSS; angle C D B === angle A B D /\ angle D B C === angle 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 parallel c /\ b parallel 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 parallel d /\ c parallel 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 angle A B C === angle C D A /\ angle D A B === angle B C D [H2]; assume Line a /\ A IN a /\ B IN a [a_line]; assume Line c /\ C IN c /\ D IN c [c_line]; thus a parallel 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; angle C D A === angle A B C /\ angle B C D === angle D A B [H2'] by TetraABCD, ANGLE, H2, C5Symmetric; consider l m such that Line l /\ A IN l /\ C IN l /\ Line m /\ B IN m /\ D IN m [lm_line] by TetraABCD, I1; consider b d such that Line b /\ B IN b /\ C IN b /\ Line d /\ D IN d /\ A IN d [bd_line] by TetraABCD, I1; A NOTIN c /\ B NOTIN c /\ A NOTIN b /\ D NOTIN b /\ B NOTIN d /\ C NOTIN d [point_off_line] by c_line, bd_line, Collinear_DEF, TetraABCD, NOTIN; ~(A IN int_triangle B C D \/ B IN int_triangle C D A \/ C IN int_triangle D A B \/ D IN int_triangle A B C) proof assume A IN int_triangle B C D \/ B IN int_triangle C D A \/ C IN int_triangle D A B \/ D IN int_triangle A B C; angle B C D <_ang angle D A B \/ angle C D A <_ang angle A B C \/ angle D A B <_ang angle B C D \/ angle A B C <_ang angle C D A by TetraABCD, -, EuclidPropositionI_21; qed by -, H2', H2, AngleTrichotomy1; ConvexQuadrilateral A B C D by H1, lm_line, -, FiveChoicesQuadrilateral; A IN int_angle B C D /\ B IN int_angle C D A /\ C IN int_angle D A B /\ D IN 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 parallel c); consider G such that G IN a /\ G IN 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, NOTIN; ~Collinear B C G /\ ~Collinear G B C /\ ~Collinear G A D /\ ~Collinear A G D [BCGncol] by -, CollinearSymmetry; G NOTIN b /\ G NOTIN d [notGb] by bd_line, Collinear_DEF, BGCncol, NOTIN; G NOTIN open (B,A) [notBGA] by Bsim_cA, Gac, SameSide_DEF, NOTIN; B NOTIN open (A,G) [notABG] proof assume ~(B NOTIN open (A,G)); B IN open (A,G) [ABG] by -, NOTIN; 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 NOTIN ray C G by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, NOTIN; C IN open (D,G) [DCG] by GnotABCD, ABGcol, -, IN_Ray, NOTIN; consider M such that D IN open (C,M) [CDM] by TetraABCD, B2'; D IN open (G,M) [GDM] by -, B1', DCG, TransitivityBetweennessHelp; angle C D A suppl angle A D M /\ angle A B C suppl angle C B G by TetraABCD, CDM, ABG, SupplementaryAngles_DEF; angle M D A === angle G B C [MDAeqGBC] by -, H2', SupplementsCongAnglesCong, AngleSymmetry; angle G A D <_ang angle M D A /\ angle G B C <_ang angle D C B by BCGncol, BGCncol, GDM, DCG, B1', EuclidPropositionI_16; angle G A D <_ang angle D C B by -, BCGncol, ANGLE, MDAeqGBC, AngleTrichotomy2, AngleOrderTransitivity; angle D A B <_ang angle B C D by -, rABrAG, Angle_DEF, AngleSymmetry; qed by -, H2, AngleTrichotomy1; A NOTIN open (G,B) proof assume ~(A NOTIN open (G,B)); A IN open (B,G) [BAG] by -, B1', NOTIN; 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 NOTIN ray D G by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, NOTIN; D IN open (C,G) [CDG] by GnotABCD, ABGcol, -, IN_Ray, NOTIN; consider M such that C IN open (D,M) [DCM] by B2', TetraABCD; C IN open (G,M) [GCM] by -, B1', CDG, TransitivityBetweennessHelp; angle B C D suppl angle M C B /\ angle D A B suppl angle G A D by TetraABCD, CollinearSymmetry, DCM, BAG, SupplementaryAngles_DEF, AngleSymmetry; angle M C B === angle G A D [GADeqMCB] by -, H2', SupplementsCongAnglesCong; angle G B C <_ang angle M C B /\ angle G A D <_ang angle C D A by BGCncol, GCM, BCGncol, CDG, B1', EuclidPropositionI_16; angle G B C <_ang angle C D A by -, BCGncol, ANGLE, GADeqMCB, AngleTrichotomy2, AngleOrderTransitivity; angle A B C <_ang angle C D A by -, rBArBG, Angle_DEF; qed by -, H2, AngleTrichotomy1; qed by TetraABCD, GnotABCD, ABGcol, notABG, notBGA, -, B3', NOTIN; `;; let OppositeAnglesCongImpliesParallelogram = thm `; let A B C D be point; assume Quadrilateral A B C D [H1]; assume angle A B C === angle C D A /\ angle D A B === angle 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; angle B C D === angle D A B [H2'] by TetraABCD, ANGLE, H2, C5Symmetric; consider a such that Line a /\ A IN a /\ B IN a [a_line] by TetraABCD, I1; consider b such that Line b /\ B IN b /\ C IN b [b_line] by TetraABCD, I1; consider c such that Line c /\ C IN c /\ D IN c [c_line] by TetraABCD, I1; consider d such that Line d /\ D IN d /\ A IN 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 NOTIN l ==> ?! m. Line m /\ P IN m /\ m parallel l`;; new_constant("mu",`:point_set->real`);; let AMa = new_axiom `! alpha. Angle alpha ==> &0 < mu alpha /\ mu alpha < &180`;; let AMb = new_axiom `! alpha. Right alpha ==> mu alpha = &90`;; let AMc = new_axiom `! alpha beta. Angle alpha /\ Angle beta /\ alpha === beta ==> mu alpha = mu beta`;; let AMd = new_axiom `! A O B P. P IN int_angle A O B ==> mu (angle A O B) = mu (angle A O P) + mu (angle P O B)`;; let ConverseAlternateInteriorAngles = thm `; let A B C E be point; let l m t be point_set; assume Line l /\ A IN l /\ E IN l [l_line]; assume Line m /\ B IN m /\ C IN m [m_line]; assume Line t /\ A IN t /\ B IN t [t_line]; assume ~(A = E) /\ ~(B = C) /\ ~(A = B) /\ E NOTIN t /\ C NOTIN t [Distinct]; assume ~(C,E same_side t) [Cnsim_tE]; assume l parallel m [para_lm]; thus angle E A B === angle C B A proof ~Collinear C B A by t_line, Distinct, I1, Collinear_DEF, NOTIN, ANGLE; A NOTIN m /\ Angle (angle C B A) [notAm] by m_line, -, Collinear_DEF, NOTIN, ANGLE; consider D such that ~(A = D) /\ D NOTIN t /\ ~(C,D same_side t) /\ seg A D === seg A E /\ angle B A D === angle C B A [Dexists] by -, Distinct, t_line, C4OppositeSide; consider k such that Line k /\ A IN k /\ D IN k [k_line] by Distinct, I1; k parallel 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 NOTIN open (D,E) /\ Collinear A E D by t_line, Distinct, Dexists, Cnsim_tE, AtMost2Sides, SameSide_DEF, NOTIN, -, 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 IN open (E,F) /\ C IN int_angle A B F /\ angle E B A === angle C A B /\ angle C B F === angle 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 IN l /\ C IN l [l_line] by Distinct, I1; consider x such that Line x /\ A IN x /\ B IN x [x_line] by Distinct, I1; consider y such that Line y /\ B IN y /\ C IN y [y_line] by Distinct, I1; C NOTIN x [notCx] by x_line, ABCncol, Collinear_DEF, NOTIN; Angle (angle C A B) by ABCncol, CollinearSymmetry, ANGLE; consider E such that ~(B = E) /\ E NOTIN x /\ ~(C,E same_side x) /\ seg B E === seg A B /\ angle A B E === angle C A B [Eexists] by -, Distinct, x_line, notCx, C4OppositeSide; consider m such that Line m /\ B IN m /\ E IN m [m_line] by -, I1, IN_DELETE; angle E B A === angle C A B [EBAeqCAB] by Eexists, AngleSymmetry; m parallel l [para_lm] by m_line, l_line, x_line, Eexists, Distinct, notCx, -, AlternateInteriorAngles; m INTER l = {} [lm0] by -, PARALLEL; C NOTIN m /\ A NOTIN m [notACm] by -, l_line, INTER_COMM, DisjointOneNotOther; consider F such that B IN open (E,F) [EBF] by Eexists, B2'; ~(B = F) /\ F IN m [EBF'] by -, B1', m_line, BetweenLinear; ~Collinear A B F /\ F NOTIN x [ABFncol] by m_line, -, I1, Collinear_DEF, notACm, NOTIN, 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 INTER 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 IN int_angle A B F [CintABF] by ABFncol, x_line, m_line, EBF', notCx, notACm, Csim_xF, -, IN_InteriorAngle; A IN int_angle C B E by EBF, B1', -, InteriorAngleSymmetry, InteriorReflectionInterior; A NOTIN y /\ A,E same_side y [Asim_yE] by y_line, m_line, -, InteriorUse; E NOTIN y /\ F NOTIN y [notEFy] by y_line, m_line, EBF', Eexists, EBF', I1, Collinear_DEF, notACm, NOTIN; 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; angle F B C === angle 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 IN open (A,A') [H2]; thus mu (angle A O B) + mu (angle B O A') = &180 proof cases; suppose Right (angle A O B); Right (angle B O A') /\ mu (angle A O B) = &90 /\ mu (angle B O A') = &90 by H1, H2, -, RightImpliesSupplRight, AMb; qed by -, REAL_ARITH; suppose ~Right (angle A O B) [notRightAOB]; ~(A = O) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct; consider l such that Line l /\ O IN l /\ A IN l /\ A' IN l [l_line] by -, I1, H2, BetweenLinear; B NOTIN l [notBl] by -, Distinct, I1, Collinear_DEF, H1, NOTIN; consider F such that Right (angle O A F) /\ Angle (angle O A F) [RightOAF] by Distinct, EuclidPropositionI_11, RightImpliesAngle; ?! r. Ray r /\ ? E. ~(O = E) /\ r = ray O E /\ E NOTIN l /\ E,B same_side l /\ angle A O E === angle O A F by -, Distinct, l_line, notBl, C4; consider E such that ~(O = E) /\ E NOTIN l /\ E,B same_side l /\ angle A O E === angle O A F [Eexists] by -; ~Collinear A O E [AOEncol] by l_line, Distinct, I1, Collinear_DEF, -, NOTIN; Right (angle A O E) [RightAOE] by -, ANGLE, RightOAF, Eexists, CongRightImpliesRight; Right (angle E O A') /\ mu (angle A O E) = &90 /\ mu (angle E O A') = &90 [RightEOA'] by AOEncol, H2, -, RightImpliesSupplRight, AMb; ~(angle A O B === angle A O E) by notRightAOB, H1, ANGLE, RightAOE, CongRightImpliesRight; ~(angle A O B = angle A O E) by H1, AOEncol, ANGLE, -, C5Reflexive; ~(ray O B = ray O E) by -, Angle_DEF; B NOTIN ray O E /\ O NOTIN open (B,E) by Distinct, -, Eexists, RayWellDefined, IN_DELETE, NOTIN, l_line, B1', SameSide_DEF; ~Collinear O E B by -, Eexists, IN_Ray, NOTIN; E IN int_angle A O B \/ B IN int_angle A O E by Distinct, l_line, Eexists, notBl, AngleOrdering, -, CollinearSymmetry, InteriorAngleSymmetry; cases by -; suppose E IN int_angle A O B [EintAOB]; B IN int_angle E O A' by H2, -, InteriorReflectionInterior; mu (angle A O B) = mu (angle A O E) + mu (angle E O B) /\ mu (angle E O A') = mu (angle E O B) + mu (angle B O A') by EintAOB, -, AMd; qed by -, RightEOA', REAL_ARITH; suppose B IN int_angle A O E [BintAOE]; E IN int_angle B O A' by H2, -, InteriorReflectionInterior; mu (angle A O E) = mu (angle A O B) + mu (angle B O E) /\ mu (angle B O A') = mu (angle B O E) + mu (angle 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 mu (angle A B C) + mu (angle B C A) + mu (angle C A B) = &180 proof ~Collinear C A B /\ ~Collinear B C A [CABncol] by ABCncol, CollinearSymmetry; consider E F such that B IN open (E,F) /\ C IN int_angle A B F /\ angle E B A === angle C A B /\ angle C B F === angle 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; mu (angle A B F) = mu (angle A B C) + mu (angle C B F) [muCintABF] by EBF, AMd; mu (angle E B A) + mu (angle A B F) = &180 [suppl180] by EBAncol, EBF, EuclidPropositionI_13; mu (angle C A B) = mu (angle E B A) /\ mu (angle B C A) = mu (angle C B F) by CABncol, EBAncol, CBFncol, ANGLE, EBF, AMc; qed by suppl180, muCintABF, -, REAL_ARITH; `;;