1 (* ----------------------------------------------------------------- *)
2 (* HOL Light Hilbert geometry axiomatic proofs using miz3. *)
3 (* ----------------------------------------------------------------- *)
5 (* High school students can learn rigorous axiomatic Geometry proofs,
6 as in http://www.math.northwestern.edu/~richter/hilbert.pdf, using
7 Hilbert's axioms, and code up their proofs in miz3 and HOL Light.
8 Thanks to Bjørn Jahren, Miguel Lerma,Takuo Matsuoka, Stephen
9 Wilson for advice on Hilbert's axioms, and especially Benjamin
10 Kordesh, who carefully read much of the paper and the code.
12 Formal proofs are given for the first 7 sections of the paper, the
13 results cited there from Greenberg's book, and most of Euclid's
14 book I propositions up to Proposition I.29, following Hartshorne,
15 whose book seems the most exciting axiomatic geometry text. A
16 proof assistant is an valuable tool to help read it, as
17 Hartshorne's proofs are often sketchy and even have gaps.
19 M. Greenberg, Euclidean and non-Euclidean geometries, W. H. Freeman and Co., 1974.
20 R. Hartshorne, Geometry, Euclid and Beyond, Undergraduate Texts in Math., Springer, 2000.
22 Thanks to Mizar folks for their influential language, Freek
23 Wiedijk, who wrote the miz3 port of Mizar to HOL Light, and
24 especially John Harrison, who was extremely helpful and developed
25 the framework for porting my axiomatic proofs to HOL Light. *)
28 report_timing := false;;
34 new_type_abbrev("point_set",`:point->bool`);;
35 new_constant("Between",`:point->point->point->bool`);;
36 new_constant("Line",`:point_set->bool`);;
37 new_constant("===",`:(point->bool)->(point->bool)->bool`);;
39 parse_as_infix("cong",(12, "right"));;
40 parse_as_infix("same_side",(12, "right"));;
41 parse_as_infix("===",(12, "right"));;
42 parse_as_infix("<__",(12, "right"));;
43 parse_as_infix("<_ang",(12, "right"));;
44 parse_as_infix("suppl",(12, "right"));;
45 parse_as_infix("NOTIN",(11, "right"));;
46 parse_as_infix("parallel",(12, "right"));;
48 let NOTIN = new_definition
49 `!a:A l:A->bool. a NOTIN l <=> ~(a IN l)`;;
51 let Interval_DEF = new_definition
52 `! A B. open (A,B) = {X | Between A X B}`;;
54 let Collinear_DEF = new_definition
56 ? l. Line l /\ A IN l /\ B IN l /\ C IN l`;;
58 let SameSide_DEF = new_definition
60 Line l /\ ~ ? X. (X IN l) /\ X IN open (A,B)`;;
62 let Ray_DEF = new_definition
63 `! A B. ray A B = {X | ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)}`;;
65 let Ordered_DEF = new_definition
67 B IN open (A,C) /\ B IN open (A,D) /\ C IN open (A,D) /\ C IN open (B,D)`;;
69 let InteriorAngle_DEF = new_definition
70 `! A O B. int_angle A O B =
71 {P:point | ~Collinear A O B /\ ? a b.
72 Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
73 P NOTIN a /\ P NOTIN b /\ P,B same_side a /\ P,A same_side b}`;;
75 let InteriorTriangle_DEF = new_definition
76 `! A B C. int_triangle A B C =
77 {P | P IN int_angle A B C /\
78 P IN int_angle B C A /\
79 P IN int_angle C A B}`;;
81 let Tetralateral_DEF = new_definition
82 `Tetralateral A B C D <=>
83 ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) /\
84 ~Collinear A B C /\ ~Collinear B C D /\ ~Collinear C D A /\ ~Collinear D A B`;;
86 let Quadrilateral_DEF = new_definition
87 `Quadrilateral A B C D <=>
88 Tetralateral A B C D /\
89 open (A,B) INTER open (C,D) = {} /\
90 open (B,C) INTER open (D,A) = {} `;;
92 let ConvexQuad_DEF = new_definition
93 `ConvexQuadrilateral A B C D <=>
94 Quadrilateral A B C D /\
95 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 `;;
97 let Segment_DEF = new_definition
98 `seg A B = {A, B} UNION open (A,B)`;;
100 let SEGMENT = new_definition
101 `Segment s <=> ? A B. s = seg A B /\ ~(A = B)`;;
103 let SegmentOrdering_DEF = new_definition
106 ? C D X. t = seg C D /\ X IN open (C,D) /\ s === seg C X`;;
108 let Angle_DEF = new_definition
109 ` angle A O B = ray O A UNION ray O B `;;
111 let ANGLE = new_definition
112 `Angle alpha <=> ? A O B. alpha = angle A O B /\ ~Collinear A O B`;;
114 let AngleOrdering_DEF = new_definition
115 `alpha <_ang beta <=>
117 ? A O B G. ~Collinear A O B /\ beta = angle A O B /\
118 G IN int_angle A O B /\ alpha === angle A O G`;;
120 let RAY = new_definition
121 `Ray r <=> ? O A. ~(O = A) /\ r = ray O A`;;
123 let TriangleCong_DEF = new_definition
124 `! A B C A' B' C' :point. (A, B, C) cong (A', B', C') <=>
125 ~Collinear A B C /\ ~Collinear A' B' C' /\
126 seg A B === seg A' B' /\ seg A C === seg A' C' /\ seg B C === seg B' C' /\
127 angle A B C === angle A' B' C' /\
128 angle B C A === angle B' C' A' /\
129 angle C A B === angle C' A' B'`;;
131 let SupplementaryAngles_DEF = new_definition
132 `! alpha beta. alpha suppl beta <=>
133 ? A O B A'. ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ beta = angle B O A'`;;
135 let RightAngle_DEF = new_definition
136 `! alpha. Right alpha <=> ? beta. alpha suppl beta /\ alpha === beta`;;
138 let PlaneComplement_DEF = new_definition
139 `! alpha:point_set. complement alpha = {P | P NOTIN alpha}`;;
141 let CONVEX = new_definition
142 `Convex alpha <=> ! A B. A IN alpha /\ B IN alpha ==> open (A,B) SUBSET alpha`;;
144 let PARALLEL = new_definition
145 `! l k. l parallel k <=>
146 Line l /\ Line k /\ l INTER k = {}`;;
148 let Parallelogram_DEF = new_definition
149 `! A B C D. Parallelogram A B C D <=>
150 Quadrilateral A B C D /\ ? a b c d.
151 Line a /\ A IN a /\ B IN a /\
152 Line b /\ B IN b /\ C IN b /\
153 Line c /\ C IN c /\ D IN d /\
154 Line d /\ D IN d /\ A IN d /\
155 a parallel c /\ b parallel d`;;
157 let InteriorCircle_DEF = new_definition
158 `! O R. int_circle O R = {P | ~(O = R) /\ (P = O \/ seg O P <__ seg O R)}
162 (* ---------------------------------------------------------------------------- *)
163 (* Hilbert's geometry axioms, except the parallel axiom P, defined near the end. *)
164 (* ---------------------------------------------------------------------------- *)
168 `! A B. ~(A = B) ==> ?! l. Line l /\ A IN l /\ B IN l`;;
171 `! l. Line l ==> ? A B. A IN l /\ B IN l /\ ~(A = B)`;;
174 `? A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
178 `! A B C. Between A B C ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
179 Between C B A /\ Collinear A B C`;;
182 `! A B. ~(A = B) ==> ? C. Between A B C`;;
185 `! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C
186 ==> (Between A B C \/ Between B C A \/ Between C A B) /\
187 ~(Between A B C /\ Between B C A) /\
188 ~(Between A B C /\ Between C A B) /\
189 ~(Between B C A /\ Between C A B)`;;
192 `! l A B C. Line l /\ ~Collinear A B C /\
193 A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
194 (? X. X IN l /\ Between A X C) ==>
195 (? Y. Y IN l /\ Between A Y B) \/ (? Y. Y IN l /\ Between B Y C)`;;
198 `! s O Z. Segment s /\ ~(O = Z) ==>
199 ?! P. P IN ray O Z DELETE O /\ seg O P === s`;;
201 let C2Reflexive = new_axiom
202 `Segment s ==> s === s`;;
204 let C2Symmetric = new_axiom
205 `Segment s /\ Segment t /\ s === t ==> t === s`;;
207 let C2Transitive = new_axiom
208 `Segment s /\ Segment t /\ Segment u /\
209 s === t /\ t === u ==> s === u`;;
212 `! A B C A' B' C'. B IN open (A,C) /\ B' IN open (A',C') /\
213 seg A B === seg A' B' /\ seg B C === seg B' C' ==>
214 seg A C === seg A' C'`;;
217 `! alpha O A l Y. Angle alpha /\ ~(O = A) /\ Line l /\ O IN l /\ A IN l /\ Y NOTIN l
218 ==> ?! r. Ray r /\ ? B. ~(O = B) /\ r = ray O B /\
219 B NOTIN l /\ B,Y same_side l /\ angle A O B === alpha`;;
221 let C5Reflexive = new_axiom
222 `Angle alpha ==> alpha === alpha`;;
224 let C5Symmetric = new_axiom
225 `Angle alpha /\ Angle beta /\ alpha === beta ==> beta === alpha`;;
227 let C5Transitive = new_axiom
228 `Angle alpha /\ Angle beta /\ Angle gamma /\
229 alpha === beta /\ beta === gamma ==> alpha === gamma`;;
232 `! A B C A' B' C'. ~Collinear A B C /\ ~Collinear A' B' C' /\
233 seg B A === seg B' A' /\ seg B C === seg B' C' /\ angle A B C === angle A' B' C'
234 ==> angle B C A === angle B' C' A'`;;
237 (* ----------------------------------------------------------------- *)
239 (* ----------------------------------------------------------------- *)
242 let IN_Interval = thm `;
243 ! A B X. X IN open (A,B) <=> Between A X B
244 by Interval_DEF, SET_RULE;
248 ! A B X. X IN ray A B <=> ~(A = B) /\ Collinear A B X /\ A NOTIN open (X,B)
249 by Ray_DEF, SET_RULE;
252 let IN_InteriorAngle = thm `;
253 ! A O B P. P IN int_angle A O B <=>
254 ~Collinear A O B /\ ? a b.
255 Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
256 P NOTIN a /\ P NOTIN b /\ P,B same_side a /\ P,A same_side b
257 by InteriorAngle_DEF, SET_RULE;
260 let IN_InteriorTriangle = thm `;
261 ! A B C P. P IN int_triangle A B C <=>
262 P IN int_angle A B C /\ P IN int_angle B C A /\ P IN int_angle C A B
263 by InteriorTriangle_DEF, SET_RULE;
266 let IN_PlaneComplement = thm `;
267 ! alpha:point_set. ! P. P IN complement alpha <=> P NOTIN alpha
268 by PlaneComplement_DEF, SET_RULE;
271 let IN_InteriorCircle = thm `;
272 ! O R P. P IN int_circle O R <=>
273 ~(O = R) /\ (P = O \/ seg O P <__ seg O R)
274 by InteriorCircle_DEF, SET_RULE;
278 ! A B C. B IN open (A,C) ==> ~(A = B) /\ ~(A = C) /\ ~(B = C) /\
279 B IN open (C,A) /\ Collinear A B C
284 ! A B. ~(A = B) ==> ? C. B IN open (A,C)
289 ! A B C. ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C
290 ==> (B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B)) /\
291 ~(B IN open (A,C) /\ C IN open (B,A)) /\
292 ~(B IN open (A,C) /\ A IN open (C,B)) /\
293 ~(C IN open (B,A) /\ A IN open (C,B))
298 ! l A B C. Line l /\ ~Collinear A B C /\
299 A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
300 (? X. X IN l /\ X IN open (A,C)) ==>
301 (? Y. Y IN l /\ Y IN open (A,B)) \/ (? Y. Y IN l /\ Y IN open (B,C))
306 ! l:point_set. ! A B C:point.
307 Line l /\ ~Collinear A B C /\ A NOTIN l /\ B NOTIN l /\ C NOTIN l /\
308 A,B same_side l /\ B,C same_side l ==> A,C same_side l
309 by B4', SameSide_DEF;
312 let DisjointOneNotOther = thm `;
313 ! l m:A->bool. (! x:A. x IN m ==> x NOTIN l) <=> l INTER m = {}
317 let EquivIntersectionHelp = thm `;
318 ! e x:A. ! l m:A->bool.
319 (l INTER m = {x} \/ m INTER l = {x}) /\ e IN m DELETE x ==> e NOTIN l
323 let CollinearSymmetry = thm `;
325 assume Collinear A B C [H1];
326 thus Collinear A C B /\ Collinear B A C /\ Collinear B C A /\
327 Collinear C A B /\ Collinear C B A
331 Line l /\ A IN l /\ B IN l /\ C IN l by H1, Collinear_DEF;
332 qed by -, Collinear_DEF;
335 let ExistsNewPointOnLine = thm `;
338 assume Line l /\ P IN l [H1];
339 thus ? Q. Q IN l /\ ~(P = Q)
342 consider A B such that
343 A IN l /\ B IN l /\ ~(A = B) [l_line] by H1, I2;
352 let ExistsPointOffLine = thm `;
355 thus ? Q:point. Q NOTIN l
358 consider A B C such that
359 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear A B C [Distinct] by I3;
360 (A NOTIN l \/ B NOTIN l \/ C NOTIN l) \/ (A IN l /\ B IN l /\ C IN l) by NOTIN;
362 suppose A NOTIN l \/ B NOTIN l \/ C NOTIN l;
364 suppose (A IN l) /\ (B IN l) /\ (C IN l);
365 Collinear A B C by H1, -, Collinear_DEF;
370 let BetweenLinear = thm `;
373 assume Line m /\ A IN m /\ C IN m [H1];
374 assume B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B) [H2];
379 (Collinear A B C \/ Collinear B C A \/ Collinear C A B) [X1] by H2, B1';
381 Line l /\ A IN l /\ B IN l /\ C IN l [X2] by -, Collinear_DEF;
382 l = m by X1, -, H2, H1, I1;
386 let CollinearLinear = thm `;
389 assume Line m /\ A IN m /\ C IN m [H1];
390 assume Collinear A B C \/ Collinear B C A \/ Collinear C A B [H2];
391 assume ~(A = C) [H3];
396 Line l /\ A IN l /\ B IN l /\ C IN l [X1] by H2, Collinear_DEF;
397 l = m by H3, -, H1, I1;
401 let NonCollinearImpliesDistinct = thm `;
403 assume ~Collinear A B C [H1];
404 thus ~(A = B) /\ ~(A = C) /\ ~(B = C)
408 suppose A = B /\ B = C [Case1];
411 qed by -, I1, Case1, Collinear_DEF, H1;
412 suppose (A = B /\ ~(A = C)) \/ (A = C /\ ~(A = B)) \/ (B = C /\ ~(A = B));
413 qed by -, I1, Collinear_DEF, H1;
414 suppose ~(A = B) /\ ~(A = C) /\ ~(B = C);
419 let Reverse4Order = thm `;
420 ! A B C D:point. ordered A B C D ==> ordered D C B A
424 let OriginInRay = thm `;
426 assume ~(Q = O) [H1];
430 O NOTIN open (O,Q) [OOQ] by B1', NOTIN;
431 Collinear O Q O by H1, I1, Collinear_DEF;
432 qed by H1, -, OOQ, IN_Ray;
435 let EndpointInRay = thm `;
437 assume ~(Q = O) [H1];
441 O NOTIN open (Q,Q) [notOQQ] by B1', NOTIN;
442 Collinear O Q Q by H1, I1, Collinear_DEF;
443 qed by H1, -, notOQQ, IN_Ray;
446 let I1Uniqueness = thm `;
448 let l m be point_set;
449 assume Line l /\ Line m [H0];
450 assume ~(l = m) [H1];
451 assume X IN l /\ X IN m [H2];
455 assume ~(l INTER m = {X}) [H3];
456 X IN l INTER m by H2, IN_INTER;
458 A IN l INTER m /\ ~(A = X) [X1] by -, H3, SET_RULE;
459 A IN l /\ X IN l /\ A IN m /\ X IN m by H0, -, H2, IN_INTER;
460 l = m by H0, -, X1, I1;
464 let EquivIntersection = thm `;
466 let l m be point_set;
467 assume Line l /\ Line m [H0];
468 assume l INTER m = {X} [H1];
469 assume A IN m DELETE X /\ B IN m DELETE X [H2];
470 assume X NOTIN open (A,B) [H3];
474 assume ~(A,B same_side l) [Con];
475 A IN m /\ B IN m /\ ~(A = X) /\ ~(B = X) [H2'] by H2, IN_DELETE;
476 ~(open (A,B) INTER l = {}) [nonempty] by H0, Con, SameSide_DEF, SET_RULE;
477 open (A,B) SUBSET m [ABm] by H0, H2', BetweenLinear, SUBSET;
478 open (A,B) INTER l SUBSET {X} by -, SET_RULE, H1;
479 X IN open (A,B) INTER l by nonempty, -, SET_RULE;
480 qed by -, IN_INTER, H3, NOTIN;
484 ! O P:point. ! l: point_set.
485 Line l /\ O IN l /\ P IN l ==> ray O P SUBSET l
486 by IN_Ray, CollinearLinear, SUBSET;
489 let RaySameSide = thm `;
492 assume Line l /\ O IN l [l_line];
493 assume A NOTIN l [notAl];
494 assume P IN ray O A DELETE O [PrOA];
495 thus P NOTIN l /\ P,A same_side l
498 ~(O = A) [notOA] by l_line, notAl, NOTIN;
500 Line d /\ O IN d /\ A IN d [d_line] by notOA, I1;
501 ~(l = d) by -, notAl, NOTIN;
502 l INTER d = {O} [ldO] by l_line, d_line, -, I1Uniqueness;
503 A IN d DELETE O [Ad_O] by d_line, notOA, IN_DELETE;
504 ray O A SUBSET d by d_line, RayLine;
505 P IN d DELETE O [Pd_O] by PrOA, -, SUBSET, IN_DELETE;
506 P NOTIN l [notPl] by ldO, -, EquivIntersectionHelp;
507 O NOTIN open (P,A) by PrOA, IN_DELETE, IN_Ray;
508 P,A same_side l by l_line, d_line, ldO, Ad_O, Pd_O, -, EquivIntersection;
512 let IntervalRayEZ = thm `;
514 assume B IN open (A,C) [H1];
515 thus B IN ray A C DELETE A /\ C IN ray A B DELETE A
518 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C [ABC] by H1, B1';
519 A NOTIN open (B,C) /\ A NOTIN open (C,B) by -, H1, B3', B1', NOTIN;
520 qed by ABC, CollinearSymmetry, -, IN_Ray, IN_DELETE, NOTIN;
523 let NoncollinearityExtendsToLine = thm `;
524 let A O B X be point;
525 assume ~Collinear A O B [H1];
526 assume Collinear O B X /\ ~(X = O) [H2];
527 thus ~Collinear A O X
530 ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct;
532 Line b /\ O IN b /\ B IN b [b_line] by Distinct, I1;
533 A NOTIN b [notAb] by b_line, Collinear_DEF, H1, NOTIN;
534 X IN b by H2, b_line, Distinct, I1, Collinear_DEF;
535 qed by b_line, -, H2, I1, Collinear_DEF, notAb, NOTIN;
538 let SameSideReflexive = thm `;
539 ! l A. Line l /\ A NOTIN l ==> A,A same_side l
540 by B1', SameSide_DEF;
543 let SameSideSymmetric = thm `;
544 ! l A B. Line l /\ A NOTIN l /\ B NOTIN l ==>
545 A,B same_side l ==> B,A same_side l
546 by SameSide_DEF, B1';
549 let SameSideTransitive = thm `;
552 assume Line l [l_line];
553 assume A NOTIN l /\ B NOTIN l /\ C NOTIN l [notABCl];
554 assume A,B same_side l [Asim_lB];
555 assume B,C same_side l [Bsim_lC];
560 suppose ~Collinear A B C \/ A = B \/ A = C \/ B = C;
561 qed by l_line, -, notABCl, Asim_lB, Bsim_lC, B4'', SameSideReflexive;
562 suppose Collinear A B C /\ ~(A = B) /\ ~(A = C) /\ ~(B = C) [Distinct];
564 Line m /\ A IN m /\ C IN m [m_line] by Distinct, I1;
565 B IN m [Bm] by -, Distinct, CollinearLinear;
567 suppose m INTER l = {};
568 qed by m_line, l_line, -, BetweenLinear, SET_RULE, SameSide_DEF;
569 suppose ~(m INTER l = {});
571 X IN l /\ X IN m [Xlm] by -, MEMBER_NOT_EMPTY, IN_INTER;
572 Collinear A X B /\ Collinear B A C /\ Collinear A B C [ABXcol] by m_line, Bm, -, Collinear_DEF;
574 E IN l /\ ~(E = X) [El_X] by l_line, Xlm, ExistsNewPointOnLine;
575 ~Collinear E A X [EAXncol] by l_line, El_X, Xlm, I1, Collinear_DEF, notABCl, NOTIN;
576 consider B' such that
577 ~(B = E) /\ B IN open (E,B') [EBB'] by notABCl, El_X, NOTIN, B2';
578 ~(B' = E) /\ ~(B' = B) /\ Collinear B E B' [EBB'col] by -, B1', CollinearSymmetry;
579 ~Collinear A B B' /\ ~Collinear B' B A /\ ~Collinear B' A B [ABB'ncol] by EAXncol, ABXcol, Distinct, NoncollinearityExtendsToLine, CollinearSymmetry, -;
580 ~Collinear B' B C /\ ~Collinear B' A C /\ ~Collinear A B' C [AB'Cncol] by ABB'ncol, ABXcol, Distinct, NoncollinearityExtendsToLine, CollinearSymmetry;
581 B' IN ray E B DELETE E /\ B IN ray E B' DELETE E by EBB', IntervalRayEZ;
582 B' NOTIN l /\ B',B same_side l /\ B,B' same_side l [notB'l] by l_line, El_X, notABCl, -, RaySameSide;
583 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;
584 qed by l_line, AB'Cncol, notABCl, notB'l, -, B4'';
589 let ConverseCrossbar = thm `;
590 let O A B G be point;
591 assume ~Collinear A O B [H1];
592 assume G IN open (A,B) [H2];
593 thus G IN int_angle A O B
596 ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct;
598 Line a /\ O IN a /\ A IN a [a_line] by -, I1;
600 Line b /\ O IN b /\ B IN b [b_line] by Distinct, I1;
602 Line l /\ A IN l /\ B IN l [l_line] by Distinct, I1;
603 B NOTIN a /\ A NOTIN b by H1, a_line, Collinear_DEF, NOTIN, b_line;
604 ~(a = l) /\ ~(b = l) by -, l_line, NOTIN;
605 a INTER l = {A} /\ b INTER l = {B} [alA] by -, a_line, l_line, I1Uniqueness, b_line;
606 ~(A = G) /\ ~(A = B) /\ ~(G = B) [AGB] by H2, B1';
607 A NOTIN open (G,B) /\ B NOTIN open (G,A) [notGAB] by H2, B3', B1', NOTIN;
608 G IN l [Gl] by l_line, H2, BetweenLinear;
609 G NOTIN a /\ G NOTIN b [notGa] by alA, Gl, AGB, IN_DELETE, EquivIntersectionHelp;
610 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;
611 G,B same_side a /\ G,A same_side b by a_line, l_line, alA, -, notGAB, EquivIntersection, b_line;
612 qed by H1, a_line, b_line, notGa, -, IN_InteriorAngle;
615 let InteriorUse = thm `;
616 let A O B P be point;
617 let a b be point_set;
618 assume Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b [aOAbOB];
619 assume P IN int_angle A O B [P_AOB];
620 thus P NOTIN a /\ P NOTIN b /\ P,B same_side a /\ P,A same_side b
623 consider alpha beta such that ~Collinear A O B /\
624 Line alpha /\ O IN alpha /\ A IN alpha /\
625 Line beta /\ O IN beta /\B IN beta /\
626 P NOTIN alpha /\ P NOTIN beta /\
627 P,B same_side alpha /\ P,A same_side beta [exists] by P_AOB, IN_InteriorAngle;
628 ~(A = O) /\ ~(A = B) /\ ~(O = B) [Distinct] by -, NonCollinearImpliesDistinct;
629 alpha = a /\ beta = b by -, aOAbOB, exists, I1;
633 let InteriorEZHelp = thm `;
634 let A O B P be point;
635 assume P IN int_angle A O B [P_AOB];
636 thus ~(P = A) /\ ~(P = O) /\ ~(P = B) /\ ~Collinear A O P
639 consider a b such that
641 Line a /\ O IN a /\ A IN a /\
642 Line b /\ O IN b /\B IN b /\
643 P NOTIN a /\ P NOTIN b [def_int] by P_AOB, IN_InteriorAngle;
644 ~(P = A) /\ ~(P = O) /\ ~(P = B) [PnotAOB] by -, NOTIN;
645 ~(A = O) [notAO] by def_int, NonCollinearImpliesDistinct;
646 ~Collinear A O P by def_int, notAO, -, I1, Collinear_DEF, NOTIN;
650 let InteriorAngleSymmetry = thm `;
651 ! A O B P: point. P IN int_angle A O B ==> P IN int_angle B O A
652 by IN_InteriorAngle, CollinearSymmetry;
655 let InteriorWellDefined = thm `;
656 let A O B X P be point;
657 assume P IN int_angle A O B [H1];
658 assume X IN ray O B DELETE O [H2];
659 thus P IN int_angle A O X
662 consider a b such that
664 Line a /\ O IN a /\ A IN a /\ P NOTIN a /\ Line b /\ O IN b /\ B IN b /\ P NOTIN b /\
665 P,B same_side a /\ P,A same_side b [def_int] by H1, IN_InteriorAngle;
666 ~(X = O) /\ ~(O = B) /\ Collinear O B X [H2'] by H2, IN_DELETE, IN_Ray;
667 B NOTIN a [notBa] by def_int, Collinear_DEF, NOTIN;
668 ~Collinear A O X [AOXnoncol] by def_int, H2', NoncollinearityExtendsToLine;
669 X IN b [Xb] by def_int, H2', CollinearLinear;
670 X NOTIN a /\ B,X same_side a by def_int, notBa, H2, RaySameSide, SameSideSymmetric;
671 P,X same_side a by def_int, -, notBa, SameSideTransitive;
672 qed by AOXnoncol, def_int, Xb, -, IN_InteriorAngle;
675 let WholeRayInterior = thm `;
676 let A O B X P be point;
677 assume X IN int_angle A O B [XintAOB];
678 assume P IN ray O X DELETE O [PrOX];
679 thus P IN int_angle A O B
682 consider a b such that
684 Line a /\ O IN a /\ A IN a /\ X NOTIN a /\ Line b /\ O IN b /\ B IN b /\ X NOTIN b /\
685 X,B same_side a /\ X,A same_side b [def_int] by XintAOB, IN_InteriorAngle;
686 P NOTIN a /\ P,X same_side a /\ P NOTIN b /\ P,X same_side b [Psim_abX] by def_int, PrOX, RaySameSide;
687 P,B same_side a /\ P,A same_side b by -, def_int, Collinear_DEF, SameSideTransitive, NOTIN;
688 qed by def_int, Psim_abX, -, IN_InteriorAngle;
691 let AngleOrdering = thm `;
692 let O A P Q be point;
694 assume ~(O = A) [H1];
695 assume Line a /\ O IN a /\ A IN a [H2];
696 assume P NOTIN a /\ Q NOTIN a [H3];
697 assume P, Q same_side a [H4];
698 assume ~Collinear P O Q [H5];
699 thus P IN int_angle Q O A \/ Q IN int_angle P O A
702 ~(P = O) /\ ~(P = Q) /\ ~(O = Q) [Distinct] by H5, NonCollinearImpliesDistinct;
704 Line q /\ O IN q /\ Q IN q [q_line] by Distinct, I1;
705 P NOTIN q [notPq] by -, Collinear_DEF, H5, NOTIN;
706 assume ~(P IN int_angle Q O A) [notPintQOA];
707 ~Collinear Q O A /\ ~Collinear P O A [POAncol] by H1, H2, I1, Collinear_DEF, H3, NOTIN;
708 ~(P,A same_side q) by -, H2, q_line, H3, notPq, H4, notPintQOA, IN_InteriorAngle;
710 G IN q /\ G IN open (P,A) [existG] by q_line, -, SameSide_DEF;
711 G IN int_angle P O A [G_POA] by POAncol, existG, ConverseCrossbar;
712 G NOTIN a /\ G,P same_side a /\ ~(G = O) [Gsim_aP] by -, IN_InteriorAngle, H1, H2, I1, NOTIN;
713 G,Q same_side a by H2, Gsim_aP, H3, H4, SameSideTransitive;
714 O NOTIN open (Q,G) [notQOG] by -, SameSide_DEF, H2, B1', NOTIN;
715 Collinear O G Q by q_line, existG, Collinear_DEF;
716 Q IN ray O G DELETE O by Gsim_aP, -, notQOG, IN_Ray, Distinct, IN_DELETE;
717 qed by G_POA, -, WholeRayInterior;
720 let InteriorsDisjointSupplement = thm `;
721 let A O B A' be point;
722 assume ~Collinear A O B [H1];
723 assume O IN open (A,A') [H2];
724 thus int_angle B O A' INTER int_angle A O B = {}
727 ! D. D IN int_angle A O B ==> D NOTIN int_angle B O A'
730 assume D IN int_angle A O B [H3];
731 ~(A = O) /\ ~(O = B) by H1, NonCollinearImpliesDistinct;
732 consider a b such that
733 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;
734 ~Collinear B O A' by H1, CollinearSymmetry, H2, B1', NoncollinearityExtendsToLine;
735 A NOTIN b /\ A' NOTIN b [notAb] by ab_line, Collinear_DEF, H1, -, NOTIN;
736 ~(A',A same_side b) [A'nsim_bA] by ab_line, H2, B1', SameSide_DEF ;
737 D NOTIN b /\ D,A same_side b [DintAOB] by ab_line, H3, InteriorUse;
738 ~(D,A' same_side b) by ab_line, notAb, DintAOB, A'nsim_bA, SameSideSymmetric, SameSideTransitive;
739 qed by ab_line, -, InteriorUse, NOTIN;
740 qed by -, DisjointOneNotOther;
743 let InteriorReflectionInterior = thm `;
744 let A O B D A' be point;
745 assume O IN open (A,A') [H1];
746 assume D IN int_angle A O B [H2];
747 thus B IN int_angle D O A'
750 consider a b such that
751 ~Collinear A O B /\ Line a /\ O IN a /\ A IN a /\ D NOTIN a /\
752 Line b /\ O IN b /\ B IN b /\ D NOTIN b /\ D,B same_side a [DintAOB] by H2, IN_InteriorAngle;
753 ~(O = B) /\ ~(O = A') /\ B NOTIN a [Distinct] by -, NonCollinearImpliesDistinct, H1, B1', Collinear_DEF, NOTIN;
754 ~Collinear D O B [DOB_ncol] by DintAOB, -, I1, Collinear_DEF, NOTIN;
755 A' IN a [A'a] by H1, DintAOB, BetweenLinear;
756 D NOTIN int_angle B O A' by DintAOB, H1, InteriorsDisjointSupplement, H2, DisjointOneNotOther;
757 qed by Distinct, DintAOB, A'a, DOB_ncol, -, AngleOrdering, NOTIN;
760 let Crossbar_THM = thm `;
761 let O A B D be point;
762 assume D IN int_angle A O B [H1];
763 thus ? G. G IN open (A,B) /\ G IN ray O D DELETE O
766 consider a b such that
768 Line a /\ O IN a /\ A IN a /\
769 Line b /\ O IN b /\ B IN b /\
770 D NOTIN a /\ D NOTIN b /\ D,B same_side a /\ D,A same_side b [DintAOB] by H1, IN_InteriorAngle;
771 B NOTIN a [notBa] by DintAOB, Collinear_DEF, NOTIN;
772 ~(A = O) /\ ~(A = B) /\ ~(O = B) /\ ~(D = O) [Distinct] by DintAOB, NonCollinearImpliesDistinct, NOTIN;
774 Line l /\ O IN l /\ D IN l [l_line] by -, I1;
775 consider A' such that
776 O IN open (A,A') [AOA'] by Distinct, B2';
777 A' IN a /\ Collinear A O A' /\ ~(A' = O) [A'a] by DintAOB, -, BetweenLinear, B1';
778 ~(A,A' same_side l) [Ansim_lA'] by l_line, AOA', SameSide_DEF;
779 B IN int_angle D O A' by H1, AOA', InteriorReflectionInterior;
780 B,A' same_side l [Bsim_lA'] by l_line, DintAOB, A'a, -, InteriorUse;
781 ~Collinear A O D /\ ~Collinear B O D [AODncol] by H1, InteriorEZHelp, InteriorAngleSymmetry;
782 ~Collinear D O A' by -, CollinearSymmetry, A'a, NoncollinearityExtendsToLine;
783 A NOTIN l /\ B NOTIN l /\ A' NOTIN l by l_line, Collinear_DEF, AODncol, -, NOTIN;
784 ~(A,B same_side l) by l_line, -, Bsim_lA', Ansim_lA', SameSideTransitive;
786 G IN open (A,B) /\ G IN l [AGB] by l_line, -, SameSide_DEF;
787 Collinear O D G [ODGcol] by -, l_line, Collinear_DEF;
788 G IN int_angle A O B by DintAOB, AGB, ConverseCrossbar;
789 G NOTIN a /\ G,B same_side a /\ ~(G = O) [Gsim_aB] by DintAOB, -, InteriorUse, NOTIN;
790 B,D same_side a by DintAOB, notBa, SameSideSymmetric;
791 G,D same_side a [Gsim_aD] by DintAOB, Gsim_aB, notBa, -, SameSideTransitive;
792 O NOTIN open (G,D) by DintAOB, -, SameSide_DEF, NOTIN;
793 G IN ray O D DELETE O by Distinct, ODGcol, -, IN_Ray, Gsim_aB, IN_DELETE;
797 let AlternateConverseCrossbar = thm `;
798 let O A B G be point;
799 assume Collinear A G B /\ G IN int_angle A O B [H1];
803 consider a b such that
804 ~Collinear A O B /\ Line a /\ O IN a /\ A IN a /\ Line b /\ O IN b /\ B IN b /\
805 G,B same_side a /\ G,A same_side b [GintAOB] by H1, IN_InteriorAngle;
806 ~(A = B) /\ ~(G = A) /\ ~(G = B) /\ A NOTIN open (G,B) /\ B NOTIN open (G,A) by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp, SameSide_DEF, NOTIN;
807 qed by -, H1, B1', B3', NOTIN;
810 let InteriorOpposite = thm `;
811 let A O B P be point;
813 assume P IN int_angle A O B [PintAOB];
814 assume Line p /\ O IN p /\ P IN p [p_line];
815 thus ~(A,B same_side p)
819 G IN open (A,B) /\ G IN ray O P [Gexists] by PintAOB, Crossbar_THM, IN_DELETE;
820 G IN p by p_line, RayLine, -, SUBSET;
821 qed by p_line, -, Gexists, SameSide_DEF;
824 let IntervalTransitivity = thm `;
825 let O P Q R be point;
827 assume Line m /\ O IN m [H0];
828 assume P IN m DELETE O /\ Q IN m DELETE O /\ R IN m DELETE O [H2];
829 assume O NOTIN open (P,Q) /\ O NOTIN open (Q,R) [H3];
830 thus O NOTIN open (P,R)
834 E NOTIN m /\ ~(O = E) [notEm] by H0, ExistsPointOffLine, NOTIN;
836 Line l /\ O IN l /\ E IN l [l_line] by -, I1;
837 ~(m = l) by notEm, -, NOTIN;
838 l INTER m = {O} [lmO] by l_line, H0, -, l_line, I1Uniqueness;
839 P NOTIN l /\ Q NOTIN l /\ R NOTIN l [notPQRl] by -, H2, EquivIntersectionHelp;
840 P,Q same_side l /\ Q,R same_side l by l_line, H0, lmO, H2, H3, EquivIntersection;
841 P,R same_side l [Psim_lR] by l_line, notPQRl, -, SameSideTransitive;
842 qed by l_line, -, SameSide_DEF, NOTIN;
845 let RayWellDefinedHalfway = thm `;
847 assume ~(Q = O) [H1];
848 assume P IN ray O Q DELETE O [H2];
849 thus ray O P SUBSET ray O Q
853 Line m /\ O IN m /\ Q IN m [OQm] by H1, I1;
854 P IN ray O Q /\ ~(P = O) /\ O NOTIN open (P,Q) [H2'] by H2, IN_DELETE, IN_Ray;
855 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;
856 O NOTIN open (P,Q) [notPOQ] by H2', IN_Ray;
857 ! X. X IN ray O P ==> X IN ray O Q
861 X IN m /\ O NOTIN open (X,P) [XrOP] by OQm, PQm_O, H2', -, RayLine, SUBSET, IN_Ray;
862 Collinear O Q X [OQXcol] by OQm, -, Collinear_DEF;
865 qed by H1, -, OriginInRay;
867 X IN m DELETE O by XrOP, -, IN_DELETE;
868 O NOTIN open (X,Q) by OQm, -, PQm_O, XrOP, H2', IntervalTransitivity;
869 qed by H1, OQXcol, -, IN_Ray;
874 let RayWellDefined = thm `;
876 assume ~(Q = O) [H1];
877 assume P IN ray O Q DELETE O [H2];
878 thus ray O P = ray O Q
881 ray O P SUBSET ray O Q [PsubsetQ] by H1, H2, RayWellDefinedHalfway;
882 ~(P = O) /\ Collinear O Q P /\ O NOTIN open (P,Q) [H2'] by H2, IN_DELETE, IN_Ray;
883 Q IN ray O P DELETE O by H2', B1', NOTIN, CollinearSymmetry, IN_Ray, H1, IN_DELETE;
884 ray O Q SUBSET ray O P [QsubsetP] by H2', -, RayWellDefinedHalfway;
885 qed by PsubsetQ, QsubsetP, SUBSET_ANTISYM;
888 let OppositeRaysIntersect1pointHelp = thm `;
889 let A O B X be point;
890 assume O IN open (A,B) [H1];
891 assume X IN ray O B DELETE O [H2];
892 thus X NOTIN ray O A /\ O IN open (X,A)
895 ~(A = O) /\ ~(A = B) /\ ~(O = B) /\ Collinear A O B [AOB] by H1, B1';
896 ~(X = O) /\ Collinear O B X /\ O NOTIN open (X,B) [H2'] by H2, IN_DELETE, IN_Ray;
898 Line m /\ A IN m /\ B IN m [m_line] by AOB, I1;
899 O IN m /\ X IN m [Om] by m_line, H2', AOB, CollinearLinear;
900 A IN m DELETE O /\ X IN m DELETE O /\ B IN m DELETE O by m_line, -, H2', AOB, IN_DELETE;
901 O IN open (X,A) by H1, m_line, Om, -, H2', IntervalTransitivity, NOTIN, B1';
902 qed by -, IN_Ray, NOTIN;
905 let OppositeRaysIntersect1point = thm `;
907 assume O IN open (A,B) [H1];
908 thus ray O A INTER ray O B = {O}
911 ~(A = O) /\ ~(O = B) by H1, B1';
912 {O} SUBSET ray O A INTER ray O B [Osubset_rOA] by -, OriginInRay, IN_INTER, SING_SUBSET;
913 ! X. ~(X = O) /\ X IN ray O B ==> X NOTIN ray O A
914 by IN_DELETE, H1, OppositeRaysIntersect1pointHelp;
915 ray O A INTER ray O B SUBSET {O} by -, IN_INTER, IN_SING, SUBSET, NOTIN;
916 qed by -, Osubset_rOA, SUBSET_ANTISYM;
919 let IntervalRay = thm `;
920 ! A B C:point. B IN open (A,C) ==> ray A B = ray A C
921 by B1', IntervalRayEZ, RayWellDefined;
924 let TransitivityBetweennessHelp = thm `;
925 let A B C D be point;
926 assume B IN open (A,C) /\ C IN open (B,D) [H1];
930 D IN ray B C DELETE B by H1, IntervalRayEZ;
931 qed by H1, -, OppositeRaysIntersect1pointHelp, B1';
934 let TransitivityBetweenness = thm `;
935 let A B C D be point;
936 assume B IN open (A,C) /\ C IN open (B,D) [H1];
940 B IN open (A,D) [ABD] by H1, TransitivityBetweennessHelp;
941 C IN open (D,B) /\ B IN open (C,A) by H1, B1';
942 C IN open (D,A) by -, TransitivityBetweennessHelp;
943 qed by H1, ABD, -, B1', Ordered_DEF;
946 let IntervalsAreConvex = thm `;
948 assume B IN open (A,C) [H1];
949 thus open (A,B) SUBSET open (A,C)
952 ! X. X IN open (A,B) ==> X IN open (A,C)
955 assume X IN open (A,B) [AXB];
956 X IN ray B A DELETE B by AXB, B1', IntervalRayEZ;
957 B IN open (X,C) by H1, B1', -, OppositeRaysIntersect1pointHelp;
958 qed by AXB, -, TransitivityBetweennessHelp;
962 let TransitivityBetweennessVariant = thm `;
963 let A X B C be point;
964 assume X IN open (A,B) /\ B IN open (A,C) [H1];
968 X IN ray B A DELETE B by H1, B1', IntervalRayEZ;
969 B IN open (X,C) by H1, B1', -, OppositeRaysIntersect1pointHelp;
970 qed by H1, -, TransitivityBetweenness;
973 let Interval2sides2aLineHelp = thm `;
974 let A B C X be point;
975 assume B IN open (A,C) [H1];
976 thus X NOTIN open (A,B) \/ X NOTIN open (B,C)
979 assume ~(X NOTIN open (A,B));
980 ordered A X B C by -, NOTIN, H1, TransitivityBetweennessVariant;
981 B IN open (X,C) by -, Ordered_DEF;
982 X NOTIN open (C,B) by -, B1', B3', NOTIN;
983 qed by -, B1', NOTIN;
986 let Interval2sides2aLine = thm `;
987 let A B C X be point;
988 assume Collinear A B C [H1];
989 thus X NOTIN open (A,B) \/ X NOTIN open (A,C) \/ X NOTIN open (B,C)
993 suppose A = B \/ A = C \/ B = C;
994 qed by -, B1', NOTIN;
995 suppose ~(A = B) /\ ~(A = C) /\ ~(B = C);
996 B IN open (A,C) \/ C IN open (B,A) \/ A IN open (C,B) by -, H1, B3';
997 qed by -, Interval2sides2aLineHelp, B1', NOTIN;
1001 let TwosidesTriangle2aLine = thm `;
1002 let A B C Y be point;
1003 let l m be point_set;
1004 assume Line l /\ ~Collinear A B C [H1];
1005 assume A NOTIN l /\ B NOTIN l /\ C NOTIN l [off_l];
1006 assume Line m /\ A IN m /\ C IN m [m_line];
1007 assume Y IN l /\ Y IN m [Ylm];
1008 assume ~(A,B same_side l) /\ ~(B,C same_side l) [H2];
1009 thus A,C same_side l
1012 consider X Z such that
1013 X IN l /\ X IN open (A,B) /\ Z IN l /\ Z IN open (C,B) [H2'] by H1, H2, SameSide_DEF, B1';
1014 ~(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;
1015 consider p such that
1016 Line p /\ B IN p /\ A IN p [p_line] by Distinct, I1;
1017 consider q such that
1018 Line q /\ B IN q /\ C IN q [q_line] by Distinct, I1;
1019 X IN p /\ Z IN q [Xp] by p_line, H2', BetweenLinear, q_line, H2';
1020 A NOTIN q /\ B NOTIN m /\ C NOTIN p [vertex_off_line] by q_line, m_line, p_line, H1, Collinear_DEF, NOTIN;
1021 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;
1022 ~(m = p) /\ ~(m = q) by m_line, vertex_off_line, NOTIN;
1023 p INTER m = {A} /\ q INTER m = {C} [pmA] by p_line, m_line, q_line, H1, -, Xp, H2', I1Uniqueness;
1024 Y NOTIN p /\ Y NOTIN q [notYpq] by -, Distinct, EquivIntersectionHelp;
1025 X IN ray A B DELETE A /\ Z IN ray C B DELETE C by H2', IntervalRayEZ, H2', B1';
1026 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;
1027 X,Z same_side m by m_line, -, vertex_off_line, SameSideTransitive;
1028 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;
1029 Z IN open (X,Y) \/ X IN open (Z,Y) by -, B3', NOTIN, B1';
1031 suppose X IN open (Z,Y);
1032 ~(Z,Y same_side p) by p_line, Xp, -, SameSide_DEF;
1033 ~(C,Y same_side p) by p_line, Xsim_qA, vertex_off_line, notYpq, -, SameSideTransitive;
1034 A IN open (C,Y) by p_line, m_line, pmA, Distinct, -, EquivIntersection, NOTIN;
1035 qed by H1, Ylm, off_l, -, B1', IntervalRayEZ, RaySameSide;
1036 suppose Z IN open (X,Y);
1037 ~(X,Y same_side q) by q_line, Xp, -, SameSide_DEF;
1038 ~(A,Y same_side q) by q_line, Xsim_qA, vertex_off_line, notYpq, -, SameSideTransitive;
1039 C IN open (Y,A) by q_line, m_line, pmA, Distinct, -, EquivIntersection, NOTIN, B1';
1040 qed by H1, Ylm, off_l, -, IntervalRayEZ, RaySameSide;
1044 let LineUnionOf2Rays = thm `;
1047 assume Line l /\ A IN l /\ B IN l [H1];
1048 assume O IN open (A,B) [H2];
1049 thus l = ray O A UNION ray O B
1052 ~(A = O) /\ ~(O = B) /\ O IN l [Distinct] by H2, B1', H1, BetweenLinear;
1053 ray O A UNION ray O B SUBSET l [AOBsub_l] by H1, -, RayLine, UNION_SUBSET;
1054 ! X. X IN l ==> X IN ray O A \/ X IN ray O B
1058 assume ~(X IN ray O B) [notXrOB];
1059 Collinear O B X /\ Collinear X A B /\ Collinear O A X [XABcol] by Distinct, H1, Xl, Collinear_DEF;
1060 O IN open (X,B) by notXrOB, Distinct, -, IN_Ray, NOTIN;
1061 O NOTIN open (X,A) by NOTIN, B1', XABcol, -, H2, Interval2sides2aLine;
1062 qed by Distinct, XABcol, -, IN_Ray;
1063 l SUBSET ray O A UNION ray O B by -, IN_UNION, SUBSET;
1064 qed by -, AOBsub_l, SUBSET_ANTISYM;
1067 let AtMost2Sides = thm `;
1071 assume A NOTIN l /\ B NOTIN l /\ C NOTIN l [H2];
1072 thus A,B same_side l \/ A,C same_side l \/ B,C same_side l
1077 qed by -, H1, H2, SameSideReflexive;
1078 suppose ~(A = C) [notAC];
1079 consider m such that
1080 Line m /\ A IN m /\ C IN m [m_line] by notAC, I1;
1082 suppose m INTER l = {};
1083 A,C same_side l by m_line, H1, -, BetweenLinear, SET_RULE, SameSide_DEF;
1085 suppose ~(m INTER l = {});
1086 consider Y such that
1087 Y IN l /\ Y IN m [Ylm] by -, IN_INTER, MEMBER_NOT_EMPTY;
1089 suppose ~Collinear A B C;
1090 qed by H1, -, H2, m_line, Ylm, TwosidesTriangle2aLine;
1091 suppose Collinear A B C [ABCcol];
1092 B IN m [Bm] by -, m_line, notAC, I1, Collinear_DEF;
1093 ~(Y = A) /\ ~(Y = B) /\ ~(Y = C) [YnotABC] by Ylm, H2, NOTIN;
1094 Y NOTIN open (A,B) \/ Y NOTIN open (A,C) \/ Y NOTIN open (B,C) by ABCcol, Interval2sides2aLine;
1095 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;
1096 qed by H1, Ylm, H2, -, RaySameSide;
1102 let FourPointsOrder = thm `;
1103 let A B C X be point;
1105 assume Line l /\ A IN l /\ B IN l /\ C IN l /\ X IN l [H1];
1106 assume ~(X = A) /\ ~(X = B) /\ ~(X = C) [H2];
1107 assume B IN open (A,C) [H3];
1108 thus ordered X A B C \/ ordered A X B C \/
1109 ordered A B X C \/ ordered A B C X
1112 A IN open (X,B) \/ X IN open (A,B) \/ X IN open (B,C) \/ C IN open (B,X)
1114 ~(A = B) /\ ~(B = C) [ABCdistinct] by H3, B1';
1115 Collinear A B X /\ Collinear A C X /\ Collinear C B X [ACXcol] by H1, Collinear_DEF;
1116 A IN open (X,B) \/ X IN open (A,B) \/ B IN open (A,X) by H2, ABCdistinct, -, B3', B1';
1118 suppose A IN open (X,B) \/ X IN open (A,B);
1120 suppose B IN open (A,X);
1121 B NOTIN open (C,X) by ACXcol, H3, -, Interval2sides2aLine, NOTIN;
1122 qed by H2, ABCdistinct, ACXcol, -, B3', B1', NOTIN;
1124 qed by -, H3, B1', TransitivityBetweenness, TransitivityBetweennessVariant, Reverse4Order;
1127 let HilbertAxiomRedundantByMoore = thm `;
1128 let A B C D be point;
1130 assume Line l /\ A IN l /\ B IN l /\ C IN l /\ D IN l [H1];
1131 assume ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) [H2];
1132 thus ordered D A B C \/ ordered A D B C \/ ordered A B D C \/ ordered A B C D \/
1133 ordered D A C B \/ ordered A D C B \/ ordered A C D B \/ ordered A C B D \/
1134 ordered D C A B \/ ordered C D A B \/ ordered C A D B \/ ordered C A B D
1137 Collinear A B C by H1, Collinear_DEF;
1138 B IN open (A,C) \/ C IN open (A,B) \/ A IN open (C,B) by H2, -, B3', B1';
1139 qed by -, H1, H2, FourPointsOrder;
1142 let InteriorTransitivity = thm `;
1143 let A O B F G be point;
1144 assume G IN int_angle A O B [GintAOB];
1145 assume F IN int_angle A O G [FintAOG];
1146 thus F IN int_angle A O B
1149 ~Collinear A O B [AOBncol] by GintAOB, IN_InteriorAngle;
1150 consider G' such that
1151 G' IN open (A,B) /\ G' IN ray O G DELETE O [CrossG] by GintAOB, Crossbar_THM;
1152 F IN int_angle A O G' by FintAOG, -, InteriorWellDefined;
1153 consider F' such that
1154 F' IN open (A,G') /\ F' IN ray O F DELETE O [CrossF] by -, Crossbar_THM;
1155 ~(F' = O) /\ ~(F = O) /\ Collinear O F F' /\ O NOTIN open (F',F) by -, IN_DELETE, IN_Ray;
1156 F IN ray O F' DELETE O [FrOF'] by -, CollinearSymmetry, B1', NOTIN, IN_Ray, IN_DELETE;
1157 open (A,G') SUBSET open (A,B) /\ F' IN open (A,B) by CrossG, IntervalsAreConvex, CrossF, SUBSET;
1158 F' IN int_angle A O B by AOBncol, -, ConverseCrossbar;
1159 qed by -, FrOF', WholeRayInterior;
1162 let HalfPlaneConvexNonempty = thm `;
1163 let l H be point_set;
1165 assume Line l /\ A NOTIN l [l_line];
1166 assume H = {X | X NOTIN l /\ X,A same_side l} [HalfPlane];
1167 thus ~(H = {}) /\ H SUBSET complement l /\ Convex H
1170 ! X. X IN H <=> X NOTIN l /\ X,A same_side l [Hdef] by HalfPlane, SET_RULE;
1171 H SUBSET complement l [Hsub] by -, IN_PlaneComplement, SUBSET;
1172 A,A same_side l /\ A IN H by l_line, SameSideReflexive, Hdef;
1173 ~(H = {}) [Hnonempty] by -, MEMBER_NOT_EMPTY;
1174 ! P Q X. P IN H /\ Q IN H /\ X IN open (P,Q) ==> X IN H
1177 assume P IN H /\ Q IN H /\ X IN open (P,Q) [PXQ];
1178 P NOTIN l /\ P,A same_side l /\ Q NOTIN l /\ Q,A same_side l [PQinH] by -, Hdef;
1179 P,Q same_side l [Psim_lQ] by l_line, -, SameSideSymmetric, SameSideTransitive;
1180 X NOTIN l [notXl] by -, PXQ, SameSide_DEF, NOTIN;
1181 open (X,P) SUBSET open (P,Q) by PXQ, IntervalsAreConvex, B1', SUBSET;
1182 X,P same_side l by l_line, -, SUBSET, Psim_lQ, SameSide_DEF;
1183 X,A same_side l by l_line, notXl, PQinH, -, Psim_lQ, PQinH, SameSideTransitive;
1184 qed by -, notXl, Hdef;
1185 Convex H by -, SUBSET, CONVEX;
1186 qed by Hnonempty, Hsub, -;
1189 let PlaneSeparation = thm `;
1191 assume Line l [l_line];
1192 thus ? H1 H2:point_set. H1 INTER H2 = {} /\ ~(H1 = {}) /\ ~(H2 = {}) /\
1193 Convex H1 /\ Convex H2 /\ complement l = H1 UNION H2 /\
1194 ! P Q. P IN H1 /\ Q IN H2 ==> ~(P,Q same_side l)
1197 consider A such that
1198 A NOTIN l [notAl] by l_line, ExistsPointOffLine;
1199 consider E such that
1200 E IN l /\ ~(A = E) [El] by l_line, I2, -, NOTIN;
1201 consider B such that
1202 E IN open (A,B) /\ ~(E = B) /\ Collinear A E B [AEB] by -, B2', B1';
1203 B NOTIN l [notBl] by l_line, El, -, I1, Collinear_DEF, notAl, NOTIN;
1204 ~(A,B same_side l) [Ansim_lB] by l_line, El, AEB, SameSide_DEF;
1205 consider H1 H2 such that
1206 H1 = {X | X NOTIN l /\ X,A same_side l} /\ H2 = {X | X NOTIN l /\ X,B same_side l} [H12sets];
1207 ! 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;
1208 ! X. X IN H1 <=> X NOTIN l /\ X,A same_side l [H1def] by H12sets, SET_RULE;
1209 ! X. X IN H2 <=> X NOTIN l /\ X,B same_side l [H2def] by H12sets, SET_RULE;
1210 H1 INTER H2 = {} [H12disjoint]
1212 assume ~(H1 INTER H2 = {});
1213 consider V such that
1214 V IN H1 /\ V IN H2 by -, MEMBER_NOT_EMPTY, IN_INTER;
1215 V NOTIN l /\ V,A same_side l /\ V NOTIN l /\ V,B same_side l by -, H12def;
1216 A,B same_side l by l_line, -, notAl, notBl, SameSideSymmetric, SameSideTransitive;
1218 ~(H1 = {}) /\ ~(H2 = {}) /\ H1 SUBSET complement l /\ H2 SUBSET complement l /\ Convex H1 /\ Convex H2 [H12convex_nonempty] by l_line, notAl, notBl, H12sets, HalfPlaneConvexNonempty;
1219 H1 UNION H2 SUBSET complement l [H12sub] by H12convex_nonempty, UNION_SUBSET;
1220 ! C. C IN complement l ==> C IN H1 UNION H2
1223 assume C IN complement l;
1224 C NOTIN l [notCl] by -, IN_PlaneComplement;
1225 C,A same_side l \/ C,B same_side l by l_line, notAl, notBl, -, Ansim_lB, AtMost2Sides;
1226 C IN H1 \/ C IN H2 by notCl, -, H12def;
1228 complement l SUBSET H1 UNION H2 by -, SUBSET;
1229 complement l = H1 UNION H2 [compl_H1unionH2] by H12sub, -, SUBSET_ANTISYM;
1230 ! P Q. P IN H1 /\ Q IN H2 ==> ~(P,Q same_side l) [opp_sides]
1233 assume P IN H1 /\ Q IN H2;
1234 P NOTIN l /\ P,A same_side l /\ Q NOTIN l /\ Q,B same_side l [PH1_QH2] by -, H12def, IN;
1235 qed by l_line, -, notAl, SameSideSymmetric, notBl, Ansim_lB, SameSideTransitive;
1236 qed by H12disjoint, H12convex_nonempty, compl_H1unionH2, opp_sides;
1239 let TetralateralSymmetry = thm `;
1240 let A B C D be point;
1241 assume Tetralateral A B C D [H1];
1242 thus Tetralateral B C D A /\ Tetralateral A B D C
1245 ~Collinear A B D /\ ~Collinear B D C /\ ~Collinear D C A /\ ~Collinear C A B [TetraABCD] by H1, Tetralateral_DEF, CollinearSymmetry;
1246 qed by H1, -, Tetralateral_DEF;
1249 let EasyEmptyIntersectionsTetralateralHelp = thm `;
1250 let A B C D be point;
1251 assume Tetralateral A B C D [H1];
1252 thus open (A,B) INTER open (B,C) = {}
1255 ! X. X IN open (B,C) ==> X NOTIN open (A,B)
1258 assume X IN open (B,C);
1259 ~Collinear A B C /\ Collinear B X C /\ ~(X = B) by H1, Tetralateral_DEF, -, B1';
1260 ~Collinear A X B by -, CollinearSymmetry, B1', NoncollinearityExtendsToLine;
1261 qed by -, B1', NOTIN;
1262 qed by -, DisjointOneNotOther;
1265 let EasyEmptyIntersectionsTetralateral = thm `;
1266 let A B C D be point;
1267 assume Tetralateral A B C D [H1];
1268 thus open (A,B) INTER open (B,C) = {} /\ open (B,C) INTER open (C,D) = {} /\
1269 open (C,D) INTER open (D,A) = {} /\ open (D,A) INTER open (A,B) = {}
1272 Tetralateral B C D A /\ Tetralateral C D A B /\ Tetralateral D A B C by H1, TetralateralSymmetry;
1273 qed by H1, -, EasyEmptyIntersectionsTetralateralHelp;
1276 let SegmentSameSideOppositeLine = thm `;
1277 let A B C D be point;
1278 let a c be point_set;
1279 assume Quadrilateral A B C D [H1];
1280 assume Line a /\ A IN a /\ B IN a [a_line];
1281 assume Line c /\ C IN c /\ D IN c [c_line];
1282 thus A,B same_side c \/ C,D same_side a
1285 assume ~(C,D same_side a); :: prove A,B same_side c
1286 consider G such that
1287 G IN a /\ G IN open (C,D) [CGD] by -, a_line, SameSide_DEF;
1288 G IN c /\ Collinear G B A [Gc] by c_line, -, BetweenLinear, a_line, Collinear_DEF;
1289 ~Collinear B C D /\ ~Collinear C D A /\ open (A,B) INTER open (C,D) = {} [quadABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
1290 A NOTIN c /\ B NOTIN c /\ ~(A = G) /\ ~(B = G) [Distinct] by -, c_line, Collinear_DEF, NOTIN, Gc;
1291 G NOTIN open (A,B) by quadABCD, CGD, DisjointOneNotOther;
1292 A IN ray G B DELETE G by Distinct, Gc, -, IN_Ray, IN_DELETE;
1293 qed by c_line, Gc, Distinct, -, RaySameSide;
1296 let ConvexImpliesQuad = thm `;
1297 let A B C D be point;
1298 assume Tetralateral A B C D [H1];
1299 assume C IN int_angle D A B /\ D IN int_angle A B C [H2];
1300 thus Quadrilateral A B C D
1303 ~(A = B) /\ ~(B = C) /\ ~(A = D) [TetraABCD] by H1, Tetralateral_DEF;
1304 consider a such that
1305 Line a /\ A IN a /\ B IN a [a_line] by TetraABCD, I1;
1306 consider b such that
1307 Line b /\ B IN b /\ C IN b [b_line] by TetraABCD, I1;
1308 consider d such that
1309 Line d /\ D IN d /\ A IN d [d_line] by TetraABCD, I1;
1310 open (B,C) SUBSET b /\ open (A,B) SUBSET a [BCbABa] by b_line, a_line, BetweenLinear, SUBSET;
1311 D,A same_side b /\ C,D same_side a by H2, a_line, b_line, d_line, InteriorUse;
1312 b INTER open (D,A) = {} /\ a INTER open (C,D) = {} by -, b_line, SameSide_DEF, SET_RULE;
1313 open (B,C) INTER open (D,A) = {} /\ open (A,B) INTER open (C,D) = {} by BCbABa, -, SET_RULE;
1314 qed by H1, -, Quadrilateral_DEF;
1317 let DiagonalsIntersectImpliesConvexQuad = thm `;
1318 let A B C D G be point;
1319 assume ~Collinear B C D [BCDncol];
1320 assume G IN open (A,C) /\ G IN open (B,D) [DiagInt];
1321 thus ConvexQuadrilateral A B C D
1324 ~(B = C) /\ ~(B = D) /\ ~(C = D) /\ ~(C = A) /\ ~(A = G) /\ ~(D = G) /\ ~(B = G) [Distinct] by BCDncol, NonCollinearImpliesDistinct, DiagInt, B1';
1325 Collinear A G C /\ Collinear B G D [AGCcol] by DiagInt, B1';
1326 ~Collinear C D A [CDAncol] by BCDncol, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine;
1327 ~Collinear D A B [DABncol] by -, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine;
1328 ~Collinear A B C [ABCncol] by -, CollinearSymmetry, Distinct, AGCcol, NoncollinearityExtendsToLine;
1329 ~(A = B) /\ ~(A = D) by DABncol, NonCollinearImpliesDistinct;
1330 Tetralateral A B C D [TetraABCD] by Distinct, -, BCDncol, CDAncol, DABncol, ABCncol, Tetralateral_DEF;
1331 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;
1332 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;
1333 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;
1334 qed by TetraABCD, -, ConvexImpliesQuad, ConvexQuad_DEF;
1337 let DoubleNotSimImpliesDiagonalsIntersect = thm `;
1338 let A B C D be point;
1339 let l m be point_set;
1340 assume Line l /\ A IN l /\ C IN l [l_line];
1341 assume Line m /\ B IN m /\ D IN m [m_line];
1342 assume Tetralateral A B C D [H1];
1343 assume ~(B,D same_side l) [H2];
1344 assume ~(A,C same_side m) [H3];
1345 thus (? G. G IN open (A,C) INTER open (B,D)) /\ ConvexQuadrilateral A B C D
1348 ~Collinear A B C /\ ~Collinear B C D /\ ~Collinear C D A /\ ~Collinear D A B [TetraABCD] by H1, Tetralateral_DEF;
1349 consider G such that
1350 G IN open (A,C) /\ G IN m [AGC] by H3, m_line, SameSide_DEF;
1351 G IN l [Gl] by l_line, -, BetweenLinear;
1352 A NOTIN m /\ B NOTIN l /\ D NOTIN l by TetraABCD, m_line, l_line, Collinear_DEF, NOTIN;
1353 ~(l = m) /\ B IN m DELETE G /\ D IN m DELETE G [BDm_G] by -, l_line, NOTIN, m_line, Gl, IN_DELETE;
1354 l INTER m = {G} by l_line, m_line, -, Gl, AGC, I1Uniqueness;
1355 G IN open (B,D) by l_line, m_line, -, BDm_G, H2, EquivIntersection, NOTIN;
1356 qed by AGC, -, IN_INTER, TetraABCD, DiagonalsIntersectImpliesConvexQuad;
1359 let ConvexQuadImpliesDiagonalsIntersect = thm `;
1360 let A B C D be point;
1361 let l m be point_set;
1362 assume Line l /\ A IN l /\ C IN l [l_line];
1363 assume Line m /\ B IN m /\ D IN m [m_line];
1364 assume ConvexQuadrilateral A B C D [ConvQuadABCD];
1365 thus ~(B,D same_side l) /\ ~(A,C same_side m) /\
1366 (? G. G IN open (A,C) INTER open (B,D)) /\ ~Quadrilateral A B D C
1369 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;
1370 ~(B,D same_side l) /\ ~(A,C same_side m) [opp_sides] by convquadABCD, l_line, m_line, InteriorOpposite;
1371 consider G such that
1372 G IN open (A,C) INTER open (B,D) [Gexists] by l_line, m_line, convquadABCD, opp_sides, DoubleNotSimImpliesDiagonalsIntersect;
1373 ~(open (B,D) INTER open (C,A) = {}) by -, IN_INTER, B1', MEMBER_NOT_EMPTY;
1374 ~Quadrilateral A B D C by -, Quadrilateral_DEF;
1375 qed by opp_sides, Gexists, -;
1378 let FourChoicesTetralateralHelp = thm `;
1379 let A B C D be point;
1380 assume Tetralateral A B C D [H1];
1381 assume C IN int_angle D A B [CintDAB];
1382 thus ConvexQuadrilateral A B C D \/ C IN int_triangle D A B
1385 ~(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;
1386 consider a d such that
1387 Line a /\ A IN a /\ B IN a /\
1388 Line d /\ D IN d /\ A IN d [ad_line] by TetraABCD, I1;
1389 consider l m such that
1390 Line l /\ A IN l /\ C IN l /\
1391 Line m /\ B IN m /\ D IN m [lm_line] by TetraABCD, I1;
1392 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;
1393 ~(B,D same_side l) [Bsim_lD] by CintDAB, lm_line, InteriorOpposite, -, SameSideSymmetric;
1395 suppose ~(A,C same_side m);
1396 qed by lm_line, H1, Bsim_lD, -, DoubleNotSimImpliesDiagonalsIntersect;
1397 suppose A,C same_side m;
1398 C,A same_side m [Csim_mA] by lm_line, -, tetra', SameSideSymmetric;
1399 C,B same_side d /\ C,D same_side a by ad_line, CintDAB, InteriorUse;
1400 C IN int_angle A B D /\ C IN int_angle B D A by tetra', ad_line, lm_line, Csim_mA, -, IN_InteriorAngle;
1401 C IN int_triangle D A B by CintDAB, -, IN_InteriorTriangle;
1406 let InteriorTriangleSymmetry = thm `;
1407 ! A B C P. P IN int_triangle A B C ==> P IN int_triangle B C A
1408 by IN_InteriorTriangle;
1411 let FourChoicesTetralateral = thm `;
1412 let A B C D be point;
1414 assume Tetralateral A B C D [H1];
1415 assume Line a /\ A IN a /\ B IN a [a_line];
1416 assume C,D same_side a [Csim_aD];
1417 thus ConvexQuadrilateral A B C D \/ ConvexQuadrilateral A B D C \/
1418 D IN int_triangle A B C \/ C IN int_triangle D A B
1421 ~(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;
1422 ~Collinear C A D /\ C NOTIN a /\ D NOTIN a [notCDa] by TetraABCD, CollinearSymmetry, a_line, Collinear_DEF, NOTIN;
1423 C IN int_angle D A B \/ D IN int_angle C A B by TetraABCD, a_line, -, Csim_aD, AngleOrdering;
1425 suppose C IN int_angle D A B;
1426 ConvexQuadrilateral A B C D \/ C IN int_triangle D A B by H1, -, FourChoicesTetralateralHelp;
1428 suppose D IN int_angle C A B;
1429 ConvexQuadrilateral A B D C \/ D IN int_triangle C A B by TetraABCD, -, FourChoicesTetralateralHelp;
1430 qed by -, InteriorTriangleSymmetry;
1434 let QuadrilateralSymmetry = thm `;
1435 ! A B C D:point. Quadrilateral A B C D ==>
1436 Quadrilateral B C D A /\ Quadrilateral C D A B /\ Quadrilateral D A B C
1437 by Quadrilateral_DEF, INTER_COMM, TetralateralSymmetry, Quadrilateral_DEF;
1440 let FiveChoicesQuadrilateral = thm `;
1441 let A B C D be point;
1442 let l m be point_set;
1443 assume Quadrilateral A B C D [H1];
1444 assume Line l /\ A IN l /\ C IN l /\ Line m /\ B IN m /\ D IN m [lm_line];
1445 thus (ConvexQuadrilateral A B C D \/ A IN int_triangle B C D \/
1446 B IN int_triangle C D A \/ C IN int_triangle D A B \/ D IN int_triangle A B C) /\
1447 (~(B,D same_side l) \/ ~(A,C same_side m))
1450 Tetralateral A B C D [H1Tetra] by H1, Quadrilateral_DEF;
1451 ~(A = B) /\ ~(A = D) /\ ~(B = C) /\ ~(C = D) [Distinct] by H1Tetra, Tetralateral_DEF;
1452 consider a c such that
1453 Line a /\ A IN a /\ B IN a /\
1454 Line c /\ C IN c /\ D IN c [ac_line] by Distinct, I1;
1455 Quadrilateral C D A B /\ Tetralateral C D A B [tetraCDAB] by H1, QuadrilateralSymmetry, Quadrilateral_DEF;
1456 ~ConvexQuadrilateral A B D C /\ ~ConvexQuadrilateral C D B A [notconvquad] by Distinct, I1, H1, -, ConvexQuadImpliesDiagonalsIntersect;
1457 ConvexQuadrilateral A B C D \/ A IN int_triangle B C D \/
1458 B IN int_triangle C D A \/ C IN int_triangle D A B \/ D IN int_triangle A B C [5choices]
1460 A,B same_side c \/ C,D same_side a by H1, ac_line, SegmentSameSideOppositeLine;
1462 suppose C,D same_side a;
1463 qed by H1Tetra, ac_line, -, notconvquad, FourChoicesTetralateral;
1464 suppose A,B same_side c;
1465 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;
1466 qed by -, QuadrilateralSymmetry, ConvexQuad_DEF;
1468 ~(B,D same_side l) \/ ~(A,C same_side m) by -, lm_line, ConvexQuadImpliesDiagonalsIntersect, IN_InteriorTriangle, InteriorAngleSymmetry, InteriorOpposite;
1472 let IntervalSymmetry = thm `;
1473 ! A B: point. open (A,B) = open (B,A)
1477 let SegmentSymmetry = thm `;
1478 ! A B: point. seg A B = seg B A
1479 by Segment_DEF, IntervalSymmetry, SET_RULE;
1482 let C1OppositeRay = thm `;
1485 assume Segment s /\ ~(O = P) [H1];
1486 thus ? Q. P IN open (O,Q) /\ seg P Q === s
1489 consider Z such that
1490 P IN open (O,Z) /\ ~(P = Z) [OPZ] by H1, B2', B1';
1491 consider Q such that
1492 Q IN ray P Z DELETE P /\ seg P Q === s [PQeq] by H1, -, C1;
1493 P IN open (Q,O) by OPZ, -, OppositeRaysIntersect1pointHelp;
1494 qed by -, B1', PQeq;
1497 let OrderedCongruentSegments = thm `;
1498 let A B C D F be point;
1499 assume ~(A = C) /\ ~(D = F) [H1];
1500 assume seg A C === seg D F [H2];
1501 assume B IN open (A,C) [H3];
1502 thus ? E. E IN open (D,F) /\ seg A B === seg D E
1505 Segment (seg A B) /\ Segment (seg A C) /\ Segment (seg B C) /\ Segment (seg D F) [segs] by H3, B1', H1, SEGMENT;
1506 seg D F === seg A C [DFeqAC] by -, H2, C2Symmetric;
1507 consider E such that
1508 E IN ray D F DELETE D /\ seg D E === seg A B [DEeqAB] by segs, H1, C1;
1509 ~(E = D) /\ Collinear D E F /\ D NOTIN open (F,E) [ErDF] by -, IN_DELETE, IN_Ray, B1', CollinearSymmetry, NOTIN;
1510 consider F' such that
1511 E IN open (D,F') /\ seg E F' === seg B C [DEF'] by segs, -, C1OppositeRay;
1512 seg D F' === seg A C [DF'eqAC] by DEF', H3, DEeqAB, C3;
1513 Segment (seg D F') /\ Segment (seg D E) by DEF', B1', SEGMENT;
1514 seg A C === seg D F' /\ seg A B === seg D E [ABeqDE] by segs, -, DF'eqAC, C2Symmetric, DEeqAB;
1515 F' IN ray D E DELETE D /\ F IN ray D E DELETE D by DEF', IntervalRayEZ, ErDF, IN_Ray, H1, IN_DELETE;
1516 F' = F by ErDF, segs, -, DF'eqAC, DFeqAC, C1;
1517 qed by -, DEF', ABeqDE;
1520 let SegmentSubtraction = thm `;
1521 let A B C A' B' C' be point;
1522 assume B IN open (A,C) /\ B' IN open (A',C') [H1];
1523 assume seg A B === seg A' B' [H2];
1524 assume seg A C === seg A' C' [H3];
1525 thus seg B C === seg B' C'
1528 ~(A = B) /\ ~(A = C) /\ Collinear A B C /\ Segment (seg A' C') /\ Segment (seg B' C') [Distinct] by H1, B1', SEGMENT;
1529 consider Q such that
1530 B IN open (A,Q) /\ seg B Q === seg B' C' [defQ] by -, C1OppositeRay;
1531 seg A Q === seg A' C' [AQ_A'C'] by H1, H2, -, C3;
1532 ~(A = Q) /\ Collinear A B Q /\ A NOTIN open (C,B) /\ A NOTIN open (Q,B) by defQ, B1', H1, B3', NOTIN;
1533 C IN ray A B DELETE A /\ Q IN ray A B DELETE A by Distinct, -, IN_Ray, IN_DELETE;
1534 C = Q by Distinct, -, AQ_A'C', H3, C1;
1538 let SegmentOrderingUse = thm `;
1541 assume Segment s /\ ~(A = B) [H1];
1542 assume s <__ seg A B [H2];
1543 thus ? G. G IN open (A,B) /\ s === seg A G
1546 consider A' B' G' such that
1547 seg A B = seg A' B' /\ G' IN open (A',B') /\ s === seg A' G' [H2'] by H2, SegmentOrdering_DEF;
1548 ~(A' = G') /\ ~(A' = B') /\ seg A' B' === seg A B [A'notB'G'] by -, B1', H1, SEGMENT, C2Reflexive;
1549 consider G such that
1550 G IN open (A,B) /\ seg A' G' === seg A G [AGB] by A'notB'G', H1, H2', -, OrderedCongruentSegments;
1551 s === seg A G by H1, A'notB'G', -, B1', SEGMENT, H2', C2Transitive;
1555 let SegmentTrichotomy1 = thm `;
1556 let s t be point_set;
1557 assume s <__ t [H1];
1561 consider A B G such that
1562 Segment s /\ t = seg A B /\ G IN open (A,B) /\ s === seg A G [H1'] by H1, SegmentOrdering_DEF;
1563 ~(A = G) /\ ~(A = B) /\ ~(G = B) [Distinct] by H1', B1';
1564 seg A B === seg A B [ABrefl] by -, SEGMENT, C2Reflexive;
1565 G IN ray A B DELETE A /\ B IN ray A B DELETE A by H1', IntervalRay, EndpointInRay, Distinct, IN_DELETE;
1566 ~(seg A G === seg A B) /\ seg A G === s by Distinct, SEGMENT, -, ABrefl, C1, H1', C2Symmetric;
1567 qed by Distinct, H1', SEGMENT, -, C2Transitive;
1570 let SegmentTrichotomy2 = thm `;
1571 let s t u be point_set;
1572 assume s <__ t [H1];
1573 assume Segment u /\ t === u [H2];
1577 consider A B P such that
1578 Segment s /\ t = seg A B /\ P IN open (A,B) /\ s === seg A P [H1'] by H1, SegmentOrdering_DEF;
1579 ~(A = B) /\ ~(A = P) [Distinct] by -, B1';
1580 consider X Y such that
1581 u = seg X Y /\ ~(X = Y) [uXY] by H2, SEGMENT;
1582 consider Q such that
1583 Q IN open (X,Y) /\ seg A P === seg X Q [XQY] by Distinct, -, H1', H2, OrderedCongruentSegments;
1584 ~(X = Q) /\ s === seg X Q by -, B1', H1', Distinct, SEGMENT, XQY, C2Transitive;
1585 qed by H1', uXY, XQY, -, SegmentOrdering_DEF;
1588 let SegmentOrderTransitivity = thm `;
1589 let s t u be point_set;
1590 assume s <__ t /\ t <__ u [H1];
1594 consider A B G such that
1595 u = seg A B /\ G IN open (A,B) /\ t === seg A G [H1'] by H1, SegmentOrdering_DEF;
1596 ~(A = B) /\ ~(A = G) /\ Segment s [Distinct] by H1', B1', H1, SegmentOrdering_DEF;
1597 s <__ seg A G by H1, H1', Distinct, SEGMENT, SegmentTrichotomy2;
1598 consider F such that
1599 F IN open (A,G) /\ s === seg A F [AFG] by Distinct, -, SegmentOrderingUse;
1600 F IN open (A,B) by H1', IntervalsAreConvex, -, SUBSET;
1601 qed by Distinct, H1', -, AFG, SegmentOrdering_DEF;
1604 let SegmentTrichotomy = thm `;
1605 let s t be point_set;
1606 assume Segment s /\ Segment t [H1];
1607 thus (s === t \/ s <__ t \/ t <__ s) /\ ~(s === t /\ s <__ t) /\
1608 ~(s === t /\ t <__ s) /\ ~(s <__ t /\ t <__ s)
1611 ~(s === t /\ s <__ t) [Not12]
1614 qed by -, SegmentTrichotomy1;
1615 ~(s === t /\ t <__ s) [Not13]
1618 ~(t === s) by -, SegmentTrichotomy1;
1619 qed by H1, -, C2Symmetric;
1620 ~(s <__ t /\ t <__ s) [Not23]
1622 assume s <__ t /\ t <__ s;
1623 s <__ s by H1, -, SegmentOrderTransitivity;
1624 qed by -, SegmentTrichotomy1, H1, C2Reflexive;
1625 consider O P such that
1626 s = seg O P /\ ~(O = P) [sOP] by H1, SEGMENT;
1627 consider Q such that
1628 Q IN ray O P DELETE O /\ seg O Q === t [QrOP] by H1, -, C1;
1629 O NOTIN open (Q,P) /\ Collinear O P Q /\ ~(O = Q) [notQOP] by -, IN_DELETE, IN_Ray;
1630 s === seg O P /\ t === seg O Q /\ seg O Q === t /\ seg O P === s [stOPQ] by H1, sOP, -, SEGMENT, QrOP, C2Reflexive, C2Symmetric;
1633 s === t by -, sOP, QrOP;
1634 qed by -, Not12, Not13, Not23;
1636 P IN open (O,Q) \/ Q IN open (O,P) by sOP, -, notQOP, B3', B1', NOTIN;
1637 s <__ seg O Q \/ t <__ seg O P by H1, -, stOPQ, SegmentOrdering_DEF;
1638 s <__ t \/ t <__ s by -, H1, stOPQ, SegmentTrichotomy2;
1639 qed by -, Not12, Not13, Not23;
1643 let C4Uniqueness = thm `;
1644 let O A B P be point;
1646 assume Line l /\ O IN l /\ A IN l /\ ~(O = A) [H1];
1647 assume B NOTIN l /\ P NOTIN l /\ P,B same_side l [H2];
1648 assume angle A O P === angle A O B [H3];
1649 thus ray O B = ray O P
1652 ~(O = B) /\ ~(O = P) /\ Ray (ray O B) /\ Ray (ray O P) [Distinct] by H2, H1, NOTIN, RAY;
1653 ~Collinear A O B /\ B,B same_side l [Bsim_lB] by H1, H2, I1, Collinear_DEF, NOTIN, SameSideReflexive;
1654 Angle (angle A O B) /\ angle A O B === angle A O B by -, ANGLE, C5Reflexive;
1655 qed by -, H1, H2, Distinct, Bsim_lB, H3, C4;
1658 let AngleSymmetry = thm `;
1659 ! A O B. angle A O B = angle B O A
1660 by Angle_DEF, UNION_COMM;
1663 let TriangleCongSymmetry = thm `;
1664 let A B C A' B' C' be point;
1665 assume A,B,C cong A',B',C' [H1];
1666 thus A,C,B cong A',C',B' /\ B,A,C cong B',A',C' /\
1667 B,C,A cong B',C',A' /\ C,A,B cong C',A',B' /\ C,B,A cong C',B',A'
1670 ~Collinear A B C /\ ~Collinear A' B' C' /\
1671 seg A B === seg A' B' /\ seg A C === seg A' C' /\ seg B C === seg B' C' /\
1672 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;
1673 seg B A === seg B' A' /\ seg C A === seg C' A' /\ seg C B === seg C' B' [segments] by H1', SegmentSymmetry;
1674 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;
1675 qed by CollinearSymmetry, H1', segments, -, TriangleCong_DEF;
1679 let A B C A' B' C' be point;
1680 assume ~Collinear A B C /\ ~Collinear A' B' C' [H1];
1681 assume seg B A === seg B' A' /\ seg B C === seg B' C' [H2];
1682 assume angle A B C === angle A' B' C' [H3];
1683 thus A,B,C cong A',B',C'
1686 ~(A = B) /\ ~(A = C) /\ ~(A' = C') [Distinct] by H1, NonCollinearImpliesDistinct; :: 134
1687 consider c such that
1688 Line c /\ A IN c /\ B IN c [c_line] by Distinct, I1;
1689 C NOTIN c [notCc] by H1, c_line, Collinear_DEF, NOTIN;
1690 angle B C A === angle B' C' A' [BCAeq] by H1, H2, H3, C6;
1691 angle B A C === angle B' A' C' [BACeq] by H1, CollinearSymmetry, H2, H3, AngleSymmetry, C6;
1692 consider Y such that
1693 Y IN ray A C DELETE A /\ seg A Y === seg A' C' [YrAC] by Distinct, SEGMENT, C1;
1694 Y NOTIN c /\ Y,C same_side c [Ysim_cC] by c_line, notCc, -, RaySameSide;
1695 ~Collinear Y A B [YABncol] by c_line, -, Distinct, I1, Collinear_DEF, NOTIN;
1696 ray A Y = ray A C /\ angle Y A B = angle C A B by Distinct, YrAC, RayWellDefined, Angle_DEF;
1697 angle Y A B === angle C' A' B' by BACeq, -, AngleSymmetry;
1698 angle A B Y === angle A' B' C' [ABYeq] by YABncol, H1, CollinearSymmetry, H2, SegmentSymmetry, YrAC, -, C6;
1699 Angle (angle A B C) /\ Angle (angle A' B' C') /\ Angle (angle A B Y) by H1, CollinearSymmetry, YABncol, ANGLE;
1700 angle A B Y === angle A B C [ABYeqABC] by -, ABYeq, -, H3, C5Symmetric, C5Transitive;
1701 ray B C = ray B Y /\ ~(Y = B) /\ Y IN ray B C by c_line, Distinct, notCc, Ysim_cC, ABYeqABC, C4Uniqueness, NOTIN, -, EndpointInRay;
1702 Collinear B C Y /\ Collinear A C Y by -, YrAC, IN_DELETE, IN_Ray;
1703 C = Y by -, I1, Collinear_DEF, H1;
1704 seg A C === seg A' C' by -, YrAC;
1705 qed by H1, H2, SegmentSymmetry, -, H3, BCAeq, BACeq, AngleSymmetry, TriangleCong_DEF;
1709 let A B C A' B' C' be point;
1710 assume ~Collinear A B C /\ ~Collinear A' B' C' [H1];
1711 assume seg A C === seg A' C' [H2];
1712 assume angle C A B === angle C' A' B' /\ angle B C A === angle B' C' A' [H3];
1713 thus A,B,C cong A',B',C'
1716 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~(A' = B') /\ ~(A' = C') /\ ~(B' = C') /\ Segment (seg C' B') [Distinct] by H1, NonCollinearImpliesDistinct, SEGMENT;
1717 consider D such that
1718 D IN ray C B DELETE C /\ seg C D === seg C' B' /\ ~(D = C) [DrCB] by -, C1, IN_DELETE;
1719 Collinear C B D [CBDcol] by -, IN_DELETE, IN_Ray;
1720 ~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;
1721 consider b such that
1722 Line b /\ A IN b /\ C IN b [b_line] by Distinct, I1;
1723 B NOTIN b /\ ~(D = A) [notBb] by H1, -, Collinear_DEF, NOTIN, DCAncol, NonCollinearImpliesDistinct;
1724 D NOTIN b /\ D,B same_side b [Dsim_bB] by b_line, -, DrCB, RaySameSide;
1725 ray C D = ray C B by Distinct, DrCB, RayWellDefined;
1726 angle D C A === angle B' C' A' by H3, -, Angle_DEF;
1727 D,C,A cong B',C',A' by DCAncol, H1, CollinearSymmetry, DrCB, H2, SegmentSymmetry, -, SAS;
1728 angle C A D === angle C' A' B' by -, TriangleCong_DEF;
1729 angle C A D === angle C A B by DCAncol, -, H3, C5Symmetric, C5Transitive;
1730 ray A B = ray A D /\ D IN ray A B by b_line, Distinct, notBb, Dsim_bB, -, C4Uniqueness, notBb, EndpointInRay;
1731 Collinear A B D by -, IN_Ray;
1732 D = B by I1, -, Collinear_DEF, CBDcol, H1;
1733 seg C B === seg C' B' by -, DrCB;
1734 B,C,A cong B',C',A' by H1, CollinearSymmetry, -, H2, SegmentSymmetry, H3, SAS;
1735 qed by -, TriangleCongSymmetry;
1738 let AngleSubtraction = thm `;
1739 let A O B A' O' B' G G' be point;
1740 assume G IN int_angle A O B /\ G' IN int_angle A' O' B' [H1];
1741 assume angle A O B === angle A' O' B' /\ angle A O G === angle A' O' G' [H2];
1742 thus angle G O B === angle G' O' B'
1745 ~Collinear A O B /\ ~Collinear A' O' B' [A'O'B'ncol] by H1, IN_InteriorAngle;
1746 ~(A = O) /\ ~(O = B) /\ ~(G = O) /\ ~(G' = O') /\ Segment (seg O' A') /\ Segment (seg O' B') [Distinct] by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp, SEGMENT;
1747 consider X Y such that
1748 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;
1749 G IN int_angle X O Y [GintXOY] by H1, XYexists, InteriorWellDefined, InteriorAngleSymmetry;
1750 consider H H' such that
1751 H IN open (X,Y) /\ H IN ray O G DELETE O /\
1752 H' IN open (A',B') /\ H' IN ray O' G' DELETE O' [Hexists] by -, H1, Crossbar_THM;
1753 H IN int_angle X O Y /\ H' IN int_angle A' O' B' [HintXOY] by GintXOY, H1, -, WholeRayInterior;
1754 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;
1755 angle X O Y === angle A' O' B' /\ angle X O H === angle A' O' H' [H2'] by H2, -, Angle_DEF;
1756 ~Collinear X O Y by GintXOY, IN_InteriorAngle;
1757 X,O,Y cong A',O',B' by -, A'O'B'ncol, H2', XYexists, SAS;
1758 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;
1759 ~Collinear O H X /\ ~Collinear O' H' A' /\ ~Collinear O Y H /\ ~Collinear O' B' H' [OHXncol] by HintXOY, InteriorEZHelp, InteriorAngleSymmetry, CollinearSymmetry;
1760 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;
1761 angle H X O === angle H' A' O' by XOYcong, -, Angle_DEF;
1762 O,H,X cong O',H',A' by OHXncol, XYexists, -, H2', ASA;
1763 seg X H === seg A' H' by -, TriangleCong_DEF, SegmentSymmetry;
1764 seg H Y === seg H' B' by Hexists, XOYcong, -, SegmentSubtraction;
1765 seg Y O === seg B' O' /\ seg Y H === seg B' H' [YHeq] by XYexists, -, SegmentSymmetry;
1766 angle O Y H === angle O' B' H' by XOYcong, Hrays, Angle_DEF;
1767 O,Y,H cong O',B',H' by OHXncol, YHeq, -, SAS;
1768 angle H O Y === angle H' O' B' by -, TriangleCong_DEF;
1769 qed by -, Orays, Angle_DEF;
1772 let OrderedCongruentAngles = thm `;
1773 let A O B A' O' B' G be point;
1774 assume ~Collinear A' O' B' [H1];
1775 assume angle A O B === angle A' O' B' [H2];
1776 assume G IN int_angle A O B [H3];
1777 thus ? G'. G' IN int_angle A' O' B' /\ angle A O G === angle A' O' G'
1780 ~Collinear A O B [AOBncol] by H3, IN_InteriorAngle;
1781 ~(A = O) /\ ~(O = B) /\ ~(A' = B') /\ ~(O = G) /\ Segment (seg O' A') /\ Segment (seg O' B') [Distinct] by AOBncol, H1, NonCollinearImpliesDistinct, H3, InteriorEZHelp, SEGMENT;
1782 consider X Y such that
1783 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;
1784 G IN int_angle X O Y [GintXOY] by H3, -, InteriorWellDefined, InteriorAngleSymmetry;
1785 ~Collinear X O Y /\ ~(X = Y) [XOYncol] by -, IN_InteriorAngle, NonCollinearImpliesDistinct;
1786 consider H such that
1787 H IN open (X,Y) /\ H IN ray O G DELETE O [defH] by GintXOY, Crossbar_THM;
1788 ray O X = ray O A /\ ray O Y = ray O B /\ ray O H = ray O G [Orays] by Distinct, defXY, -, RayWellDefined;
1789 angle X O Y === angle A' O' B' by H2, -, Angle_DEF;
1790 X,O,Y cong A',O',B' by XOYncol, H1, defXY, -, SAS;
1791 seg X Y === seg A' B' /\ angle O X Y === angle O' A' B' [YXOcong] by -, TriangleCong_DEF, AngleSymmetry;
1792 consider G' such that
1793 G' IN open (A',B') /\ seg X H === seg A' G' [A'G'B'] by XOYncol, Distinct, -, defH, OrderedCongruentSegments;
1794 G' IN int_angle A' O' B' [G'intA'O'B'] by H1, -, ConverseCrossbar;
1795 ray X H = ray X Y /\ ray A' G' = ray A' B' by defH, A'G'B', IntervalRay;
1796 angle O X H === angle O' A' G' [HXOeq] by -, Angle_DEF, YXOcong;
1797 H IN int_angle X O Y by GintXOY, defH, WholeRayInterior;
1798 ~Collinear O X H /\ ~Collinear O' A' G' by -, G'intA'O'B', InteriorEZHelp, CollinearSymmetry;
1799 O,X,H cong O',A',G' by -, A'G'B', defXY, SegmentSymmetry, HXOeq, SAS;
1800 angle X O H === angle A' O' G' by -, TriangleCong_DEF, AngleSymmetry;
1801 angle A O G === angle A' O' G' by -, Orays, Angle_DEF;
1802 qed by G'intA'O'B', -;
1805 let AngleAddition = thm `;
1806 let A O B A' O' B' G G' be point;
1807 assume G IN int_angle A O B /\ G' IN int_angle A' O' B' [H1];
1808 assume angle A O G === angle A' O' G' /\ angle G O B === angle G' O' B' [H2];
1809 thus angle A O B === angle A' O' B'
1812 ~Collinear A O B /\ ~Collinear A' O' B' [AOBncol] by H1, IN_InteriorAngle;
1813 ~(A = O) /\ ~(A = B) /\ ~(O = B) /\ ~(A' = O') /\ ~(A' = B') /\ ~(O' = B') /\ ~(G = O) [Distinct] by -, NonCollinearImpliesDistinct, H1, InteriorEZHelp;
1814 consider a b such that
1815 Line a /\ O IN a /\ A IN a /\
1816 Line b /\ O IN b /\ B IN b [a_line] by Distinct, I1;
1817 consider g such that
1818 Line g /\ O IN g /\ G IN g [g_line] by Distinct, I1;
1819 G NOTIN a /\ G,B same_side a [H1'] by a_line, H1, InteriorUse;
1820 ~Collinear A O G /\ ~Collinear A' O' G' [AOGncol] by H1, InteriorEZHelp, IN_InteriorAngle;
1821 Angle (angle A O B) /\ Angle (angle A' O' B') /\ Angle (angle A O G) /\ Angle (angle A' O' G') [angles] by AOBncol, -, ANGLE;
1822 ?! 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;
1823 consider X such that
1824 X NOTIN a /\ X,G same_side a /\ angle A O X === angle A' O' B' [Xexists] by -;
1825 ~Collinear A O X [AOXncol] by -, a_line, Distinct, I1, Collinear_DEF, NOTIN;
1826 angle A' O' B' === angle A O X by -, AOBncol, ANGLE, Xexists, C5Symmetric;
1827 consider Y such that
1828 Y IN int_angle A O X /\ angle A' O' G' === angle A O Y [YintAOX] by AOXncol, -, H1, OrderedCongruentAngles;
1829 ~Collinear A O Y by -, InteriorEZHelp;
1830 angle A O Y === angle A O G [AOGeq] by -, angles, -, ANGLE, YintAOX, H2, C5Transitive, C5Symmetric;
1831 consider x such that
1832 Line x /\ O IN x /\ X IN x by Distinct, I1;
1833 Y NOTIN a /\ Y,X same_side a by a_line, -, YintAOX, InteriorUse;
1834 Y NOTIN a /\ Y,G same_side a by a_line, -, Xexists, H1', SameSideTransitive;
1835 ray O G = ray O Y by a_line, Distinct, H1', -, AOGeq, C4Uniqueness;
1836 G IN ray O Y DELETE O by Distinct, -, EndpointInRay, IN_DELETE;
1837 G IN int_angle A O X [GintAOX] by YintAOX, -, WholeRayInterior;
1838 angle G O X === angle G' O' B' [GOXeq] by -, H1, Xexists, H2, AngleSubtraction;
1839 ~Collinear G O X /\ ~Collinear G O B /\ ~Collinear G' O' B' [GOXncol] by GintAOX, H1, InteriorAngleSymmetry, InteriorEZHelp, CollinearSymmetry;
1840 Angle (angle G O X) /\ Angle (angle G O B) /\ Angle (angle G' O' B') by -, ANGLE;
1841 angle G O X === angle G O B [G'O'Xeq] by angles, -, GOXeq, C5Symmetric, H2, C5Transitive;
1842 ~(A,X same_side g) /\ ~(A,B same_side g) [Ansim_aXB] by g_line, GintAOX, H1, InteriorOpposite;
1843 A NOTIN g /\ B NOTIN g /\ X NOTIN g [notABXg] by g_line, AOGncol, GOXncol, Distinct, I1, Collinear_DEF, NOTIN;
1844 X,B same_side g by g_line, -, Ansim_aXB, AtMost2Sides;
1845 ray O X = ray O B by g_line, Distinct, notABXg, -, G'O'Xeq, C4Uniqueness;
1846 qed by -, Xexists, Angle_DEF;
1849 let AngleOrderingUse = thm `;
1851 let alpha be point_set;
1852 assume Angle alpha /\ ~Collinear A O B [H1];
1853 assume alpha <_ang angle A O B [H3];
1854 thus ? G. G IN int_angle A O B /\ alpha === angle A O G
1857 consider A' O' B' G' such that
1858 ~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;
1859 Angle (angle A O B) /\ Angle (angle A' O' B') /\ Angle (angle A' O' G') [angles] by H1, -, ANGLE, InteriorEZHelp;
1860 angle A' O' B' === angle A O B by -, H3', C5Reflexive;
1861 consider G such that
1862 G IN int_angle A O B /\ angle A' O' G' === angle A O G [GintAOB] by H1, H3', -, OrderedCongruentAngles;
1863 alpha === angle A O G by H1, angles, -, InteriorEZHelp, ANGLE, H3', GintAOB, C5Transitive;
1867 let AngleTrichotomy1 = thm `;
1868 let alpha beta be point_set;
1869 assume alpha <_ang beta [H1];
1870 thus ~(alpha === beta)
1873 assume alpha === beta [Con];
1874 consider A O B G such that
1875 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;
1876 ~(A = O) /\ ~(O = B) /\ ~Collinear A O G [Distinct] by H1', NonCollinearImpliesDistinct, InteriorEZHelp;
1877 consider a such that
1878 Line a /\ O IN a /\ A IN a [a_line] by Distinct, I1;
1879 consider b such that
1880 Line b /\ O IN b /\ B IN b [b_line] by Distinct, I1;
1881 B NOTIN a [notBa] by a_line, H1', Collinear_DEF, NOTIN;
1882 G NOTIN a /\ G NOTIN b /\ G,B same_side a [GintAOB] by a_line, b_line, H1', InteriorUse;
1883 angle A O G === alpha by H1', Distinct, ANGLE, C5Symmetric;
1884 angle A O G === angle A O B by H1', Distinct, ANGLE, -, Con, C5Transitive;
1885 ray O B = ray O G by a_line, Distinct, notBa, GintAOB, -, C4Uniqueness;
1886 G IN b by Distinct, -, EndpointInRay, b_line, RayLine, SUBSET;
1887 qed by -, GintAOB, NOTIN;
1890 let AngleTrichotomy2 = thm `;
1891 let alpha beta gamma be point_set;
1892 assume alpha <_ang beta [H1];
1893 assume Angle gamma [H2];
1894 assume beta === gamma [H3];
1895 thus alpha <_ang gamma
1898 consider A O B G such that
1899 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;
1900 consider A' O' B' such that
1901 gamma = angle A' O' B' /\ ~Collinear A' O' B' [gammaA'O'B'] by H2, ANGLE;
1902 consider G' such that
1903 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;
1904 ~Collinear A O G /\ ~Collinear A' O' G' [ncol] by H1', -, InteriorEZHelp;
1905 alpha === angle A' O' G' by H1', ANGLE, -, G'intA'O'B', C5Transitive;
1906 qed by H1', -, ncol, gammaA'O'B', G'intA'O'B', -, AngleOrdering_DEF;
1909 let AngleOrderTransitivity = thm `;
1910 let alpha beta gamma be point_set;
1911 assume alpha <_ang beta [H0];
1912 assume beta <_ang gamma [H2];
1913 thus alpha <_ang gamma
1916 consider A O B G such that
1917 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;
1918 ~Collinear A O G [AOGncol] by H2', InteriorEZHelp;
1919 Angle alpha /\ Angle (angle A O G) /\ Angle gamma [angles] by H0, AngleOrdering_DEF, H2', -, ANGLE;
1920 alpha <_ang angle A O G by H0, H2', -, AngleTrichotomy2;
1921 consider F such that
1922 F IN int_angle A O G /\ alpha === angle A O F [FintAOG] by angles, AOGncol, -, AngleOrderingUse;
1923 F IN int_angle A O B by H2', -, InteriorTransitivity;
1924 qed by angles, H2', -, FintAOG, AngleOrdering_DEF;
1927 let AngleTrichotomy = thm `;
1928 let alpha beta be point_set;
1929 assume Angle alpha /\ Angle beta [H1];
1930 thus (alpha === beta \/ alpha <_ang beta \/ beta <_ang alpha) /\
1931 ~(alpha === beta /\ alpha <_ang beta) /\
1932 ~(alpha === beta /\ beta <_ang alpha) /\
1933 ~(alpha <_ang beta /\ beta <_ang alpha)
1936 ~(alpha === beta /\ alpha <_ang beta) [Not12] by AngleTrichotomy1;
1937 ~(alpha === beta /\ beta <_ang alpha) [Not13] by H1, C5Symmetric, AngleTrichotomy1;
1938 ~(alpha <_ang beta /\ beta <_ang alpha) [Not23] by H1, AngleOrderTransitivity, AngleTrichotomy1, C5Reflexive;
1939 consider P O A such that
1940 alpha = angle P O A /\ ~Collinear P O A [POA] by H1, ANGLE;
1941 ~(P = O) /\ ~(O = A) [Distinct] by -, NonCollinearImpliesDistinct;
1942 consider a such that
1943 Line a /\ O IN a /\ A IN a [a_line] by -, I1;
1944 P NOTIN a [notPa] by -, Distinct, I1, POA, Collinear_DEF, NOTIN;
1945 ?! 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;
1946 consider Q such that
1947 ~(O = Q) /\ Q NOTIN a /\ Q,P same_side a /\ angle A O Q === beta [Qexists] by -;
1948 O NOTIN open (Q,P) [notQOP] by a_line, Qexists, SameSide_DEF, NOTIN;
1949 ~Collinear A O P [AOPncol] by POA, CollinearSymmetry;
1950 ~Collinear A O Q [AOQncol] by a_line, Distinct, I1, Collinear_DEF, Qexists, NOTIN;
1951 Angle (angle A O P) /\ Angle (angle A O Q) by AOPncol, -, ANGLE;
1952 alpha === angle A O P /\ beta === angle A O Q /\ angle A O P === alpha [flip] by H1, -, POA, AngleSymmetry, C5Reflexive, Qexists, C5Symmetric;
1954 suppose Collinear Q O P;
1955 Collinear O P Q by -, CollinearSymmetry;
1956 Q IN ray O P DELETE O by Distinct, -, notQOP, IN_Ray, Qexists, IN_DELETE;
1957 ray O Q = ray O P by Distinct, -, RayWellDefined;
1958 angle P O A = angle A O Q by -, Angle_DEF, AngleSymmetry;
1959 alpha === beta by -, POA, Qexists;
1960 qed by -, Not12, Not13, Not23;
1961 suppose ~Collinear Q O P;
1962 P IN int_angle Q O A \/ Q IN int_angle P O A by Distinct, a_line, Qexists, notPa, -, AngleOrdering;
1963 P IN int_angle A O Q \/ Q IN int_angle A O P by -, InteriorAngleSymmetry;
1964 alpha <_ang angle A O Q \/ beta <_ang angle A O P by H1, AOQncol, AOPncol, -, flip, AngleOrdering_DEF;
1965 alpha <_ang beta \/ beta <_ang alpha by H1, -, Qexists, flip, AngleTrichotomy2;
1966 qed by -, Not12, Not13, Not23;
1970 let SupplementExists = thm `;
1971 let alpha be point_set;
1972 assume Angle alpha [H1];
1973 thus ? alpha'. alpha suppl alpha'
1976 consider A O B such that
1977 alpha = angle A O B /\ ~Collinear A O B /\ ~(A = O) [def_alpha] by H1, ANGLE, NonCollinearImpliesDistinct;
1978 consider A' such that
1979 O IN open (A,A') by -, B2';
1980 angle A O B suppl angle A' O B [AOBsup] by def_alpha, -, SupplementaryAngles_DEF, AngleSymmetry;
1981 qed by -, def_alpha;
1984 let SupplementImpliesAngle = thm `;
1985 let alpha beta be point_set;
1986 assume alpha suppl beta [H1];
1987 thus Angle alpha /\ Angle beta
1990 consider A O B A' such that
1991 ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ beta = angle B O A' [H1'] by H1, SupplementaryAngles_DEF;
1992 ~(O = A') /\ Collinear A O A' [Distinct] by -, NonCollinearImpliesDistinct, B1';
1993 ~Collinear B O A' by H1', CollinearSymmetry, -, NoncollinearityExtendsToLine;
1994 qed by H1', -, ANGLE;
1997 let RightImpliesAngle = thm `;
1998 ! alpha: point_set. Right alpha ==> Angle alpha
1999 by RightAngle_DEF, SupplementImpliesAngle;
2002 let SupplementSymmetry = thm `;
2003 let alpha beta be point_set;
2004 assume alpha suppl beta [H1];
2005 thus beta suppl alpha
2008 consider A O B A' such that
2009 ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ beta = angle B O A' [H1'] by H1, SupplementaryAngles_DEF;
2010 ~(O = A') /\ Collinear A O A' by -, NonCollinearImpliesDistinct, B1';
2011 ~Collinear A' O B [A'OBncol] by H1', CollinearSymmetry, -, NoncollinearityExtendsToLine;
2012 O IN open (A',A) /\ beta = angle A' O B /\ alpha = angle B O A by H1', B1', AngleSymmetry;
2013 qed by A'OBncol, -, SupplementaryAngles_DEF;
2016 let SupplementsCongAnglesCong = thm `;
2017 let alpha beta alpha' beta' be point_set;
2018 assume alpha suppl alpha' /\ beta suppl beta' [H1];
2019 assume alpha === beta [H2];
2020 thus alpha' === beta'
2023 consider A O B A' such that
2024 ~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;
2025 ~(A = O) /\ ~(O = B) /\ ~(A = A') /\ ~(O = A') /\ Collinear A O A' [Distinctalpha] by -, NonCollinearImpliesDistinct, B1';
2026 ~Collinear B A A' /\ ~Collinear O A' B [BAA'ncol] by def_alpha, CollinearSymmetry, -, NoncollinearityExtendsToLine;
2027 Segment (seg O A) /\ Segment (seg O B) /\ Segment (seg O A') [Osegments] by Distinctalpha, SEGMENT;
2028 consider C P D C' such that
2029 ~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;
2030 ~(C = P) /\ ~(P = D) /\ ~(P = C') [Distinctbeta] by def_beta, NonCollinearImpliesDistinct, B1';
2031 consider X such that
2032 X IN ray P C DELETE P /\ seg P X === seg O A [defX] by Osegments, Distinctbeta, C1;
2033 consider Y such that
2034 Y IN ray P D DELETE P /\ seg P Y === seg O B /\ ~(Y = P) [defY] by Osegments, Distinctbeta, C1, IN_DELETE;
2035 consider X' such that
2036 X' IN ray P C' DELETE P /\ seg P X' === seg O A' [defX'] by Osegments, Distinctbeta, C1;
2037 P IN open (X',C) /\ P IN open (X,X') [XPX'] by def_beta, -, OppositeRaysIntersect1pointHelp, defX;
2038 ~(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;
2039 Collinear P D Y /\ Collinear P C X by defY, defX, IN_DELETE, IN_Ray;
2040 ~Collinear C P Y /\ ~Collinear X P Y [XPYncol] by def_beta, -, defY, NoncollinearityExtendsToLine, CollinearSymmetry, XPX'line;
2041 ~Collinear Y X X' /\ ~Collinear P X' Y [YXX'ncol] by -, CollinearSymmetry, XPX', XPX'line, NoncollinearityExtendsToLine;
2042 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;
2043 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;
2044 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;
2045 seg A A' === seg X X' [AA'eq] by def_alpha, XPX'line, XPX', -, SegmentSymmetry, C3;
2046 A,O,B cong X,P,Y by def_alpha, XPYncol, OAeq, AOBeqXPY, SAS;
2047 seg A B === seg X Y /\ angle B A O === angle Y X P [AOBcong] by -, TriangleCong_DEF, AngleSymmetry;
2048 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;
2049 B,A,A' cong Y,X,X' by BAA'ncol, YXX'ncol, AOBcong, -, AA'eq, -, SAS;
2050 seg A' B === seg X' Y /\ angle A A' B === angle X X' Y by -, TriangleCong_DEF, SegmentSymmetry;
2051 O,A',B cong P,X',Y by BAA'ncol, YXX'ncol, OAeq, -, XPX'line, Angle_DEF, SAS;
2052 angle B O A' === angle Y P X' by -, TriangleCong_DEF;
2053 qed by -, equalPrays, def_beta, Angle_DEF, def_alpha;
2056 let SupplementUnique = thm `;
2057 ! alpha beta beta': point_set. alpha suppl beta /\ alpha suppl beta' ==> beta === beta'
2058 by SupplementaryAngles_DEF, ANGLE, C5Reflexive, SupplementsCongAnglesCong;
2061 let CongRightImpliesRight = thm `;
2062 let alpha beta be point_set;
2063 assume Angle alpha /\ Right beta [H1];
2064 assume alpha === beta [H2];
2068 consider alpha' beta' such that
2069 alpha suppl alpha' /\ beta suppl beta' /\ beta === beta' [suppl] by H1, SupplementExists, H1, RightAngle_DEF;
2070 alpha' === beta' [alpha'eqbeta'] by suppl, H2, SupplementsCongAnglesCong;
2071 Angle beta /\ Angle alpha' /\ Angle beta' by suppl, SupplementImpliesAngle;
2072 alpha === alpha' by H1, -, H2, suppl, alpha'eqbeta', C5Symmetric, C5Transitive;
2073 qed by suppl, -, RightAngle_DEF;
2076 let RightAnglesCongruentHelp = thm `;
2077 let A O B A' P be point;
2079 assume ~Collinear A O B /\ O IN open (A,A') [H1];
2080 assume Right (angle A O B) /\ Right (angle A O P) [H2];
2081 thus P NOTIN int_angle A O B
2084 assume ~(P NOTIN int_angle A O B);
2085 P IN int_angle A O B [PintAOB] by -, NOTIN;
2086 B IN int_angle P O A' /\ B IN int_angle A' O P [BintA'OP] by H1, -, InteriorReflectionInterior, InteriorAngleSymmetry ;
2087 ~Collinear A O P /\ ~Collinear P O A' [AOPncol] by PintAOB, InteriorEZHelp, -, IN_InteriorAngle;
2088 angle A O B suppl angle B O A' /\ angle A O P suppl angle P O A' [AOBsup] by H1, -, SupplementaryAngles_DEF;
2089 consider alpha' beta' such that
2090 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;
2091 alpha' === angle B O A' /\ beta' === angle P O A' [alpha'eqA'OB] by -, AOBsup, SupplementUnique;
2092 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;
2093 angle A O B === angle B O A' /\ angle A O P === angle P O A' [H2'] by -, supplalpha', alpha'eqA'OB, C5Transitive;
2094 angle A O P === angle A O P /\ angle B O A' === angle B O A' [refl] by angles, C5Reflexive;
2095 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;
2096 angle A O P <_ang angle B O A' by -, angles, H2', AngleTrichotomy2;
2097 angle A O P <_ang angle P O A' by -, BOA'lessPOA', AngleOrderTransitivity;
2098 qed by -, H2', AngleTrichotomy1;
2101 let RightAnglesCongruent = thm `;
2102 let alpha beta be point_set;
2103 assume Right alpha /\ Right beta [H1];
2107 consider alpha' such that
2108 alpha suppl alpha' /\ alpha === alpha' by H1, RightAngle_DEF;
2109 consider A O B A' such that
2110 ~Collinear A O B /\ O IN open (A,A') /\ alpha = angle A O B /\ alpha' = angle B O A' [def_alpha] by -, SupplementaryAngles_DEF;
2111 ~(A = O) /\ ~(O = B) [Distinct] by def_alpha, NonCollinearImpliesDistinct, B1';
2112 consider a such that
2113 Line a /\ O IN a /\ A IN a [a_line] by Distinct, I1;
2114 B NOTIN a [notBa] by -, def_alpha, Collinear_DEF, NOTIN;
2115 Angle beta by H1, RightImpliesAngle;
2116 ?! 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;
2117 consider P such that
2118 ~(O = P) /\ P NOTIN a /\ P,B same_side a /\ angle A O P === beta [defP] by -;
2119 O NOTIN open (P,B) [notPOB] by a_line, -, SameSide_DEF, NOTIN;
2120 ~Collinear A O P [AOPncol] by a_line, Distinct, I1, defP, Collinear_DEF, NOTIN;
2121 Right (angle A O P) [AOPright] by -, ANGLE, H1, defP, CongRightImpliesRight;
2122 P NOTIN int_angle A O B /\ B NOTIN int_angle A O P by def_alpha, H1, -, AOPncol, AOPright, RightAnglesCongruentHelp;
2123 Collinear P O B by Distinct, a_line, defP, notBa, -, AngleOrdering, InteriorAngleSymmetry, NOTIN;
2124 P IN ray O B DELETE O by Distinct, -, CollinearSymmetry, notPOB, IN_Ray, defP, IN_DELETE;
2125 ray O P = ray O B /\ angle A O P = angle A O B by Distinct, -, RayWellDefined, Angle_DEF;
2126 qed by -, defP, def_alpha;
2129 let OppositeRightAnglesLinear = thm `;
2130 let A B O H be point;
2132 assume ~Collinear A O H /\ ~Collinear H O B [H0];
2133 assume Right (angle A O H) /\ Right (angle H O B) [H1];
2134 assume Line h /\ O IN h /\ H IN h /\ ~(A,B same_side h) [H2];
2135 thus O IN open (A,B)
2138 ~(A = O) /\ ~(O = H) /\ ~(O = B) [Distinct] by H0, NonCollinearImpliesDistinct;
2139 A NOTIN h /\ B NOTIN h [notABh] by H0, H2, Collinear_DEF, NOTIN;
2140 consider E such that
2141 O IN open (A,E) /\ ~(E = O) [AOE] by Distinct, B2', B1';
2142 angle A O H suppl angle H O E [AOHsupplHOE] by H0, -, SupplementaryAngles_DEF;
2143 E NOTIN h [notEh] by H2, NOTIN, AOE, BetweenLinear, notABh;
2144 ~(A,E same_side h) by H2, AOE, SameSide_DEF;
2145 B,E same_side h [Bsim_hE] by H2, notABh, notEh, -, H2, AtMost2Sides;
2146 consider alpha' such that
2147 angle A O H suppl alpha' /\ angle A O H === alpha' [AOHsupplalpha'] by H1, RightAngle_DEF;
2148 Angle (angle H O B) /\ Angle (angle A O H) /\ Angle alpha' /\ Angle (angle H O E) [angalpha'] by H1, RightImpliesAngle, -, AOHsupplHOE, SupplementImpliesAngle;
2149 angle H O B === angle A O H /\ alpha' === angle H O E by H1, RightAnglesCongruent, AOHsupplalpha', AOHsupplHOE, SupplementUnique;
2150 angle H O B === angle H O E by angalpha', -, AOHsupplalpha', C5Transitive;
2151 ray O B = ray O E by H2, Distinct, notABh, notEh, Bsim_hE, -, C4Uniqueness;
2152 B IN ray O E DELETE O by Distinct, EndpointInRay, -, IN_DELETE;
2153 qed by AOE, -, OppositeRaysIntersect1pointHelp, B1';
2156 let RightImpliesSupplRight = thm `;
2157 let A O B A' be point;
2158 assume ~Collinear A O B [H1];
2159 assume O IN open (A,A') [H2];
2160 assume Right (angle A O B) [H3];
2161 thus Right (angle B O A')
2164 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;
2165 consider beta such that
2166 angle A O B suppl beta /\ angle A O B === beta [betasuppl] by H3, RightAngle_DEF;
2167 Angle beta /\ beta === angle A O B [angbeta] by -, SupplementImpliesAngle, C5Symmetric;
2168 angle B O A' === beta by AOBsuppl, betasuppl, SupplementUnique;
2169 angle B O A' === angle A O B by AOBsuppl, angbeta, -, betasuppl, C5Transitive;
2170 qed by AOBsuppl, H3, -, CongRightImpliesRight;
2173 let IsoscelesCongBaseAngles = thm `;
2175 assume ~Collinear A B C [H1];
2176 assume seg B A === seg B C [H2];
2177 thus angle C A B === angle A C B
2180 ~(A = B) /\ ~(B = C) /\ ~Collinear C B A [CBAncol] by H1, NonCollinearImpliesDistinct, CollinearSymmetry;
2181 seg B C === seg B A /\ angle A B C === angle C B A by -, SEGMENT, H2, C2Symmetric, H1, ANGLE, AngleSymmetry, C5Reflexive;
2182 A,B,C cong C,B,A by H1, CBAncol, H2, -, SAS;
2183 qed by -, TriangleCong_DEF;
2186 let C4withC1 = thm `;
2187 let alpha l be point_set;
2188 let O A Y P Q be point;
2189 assume Angle alpha /\ ~(O = A) /\ ~(P = Q) [H1];
2190 assume Line l /\ O IN l /\ A IN l /\ Y NOTIN l [l_line];
2191 thus ? N. ~(O = N) /\ N NOTIN l /\ N,Y same_side l /\ seg O N === seg P Q /\ angle A O N === alpha
2194 ?! 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;
2195 consider B such that
2196 ~(O = B) /\ B NOTIN l /\ B,Y same_side l /\ angle A O B === alpha [Bexists] by -;
2197 consider N such that
2198 N IN ray O B DELETE O /\ seg O N === seg P Q [Nexists] by H1, -, SEGMENT, C1;
2199 ~(O = N) [notON] by -, IN_DELETE;
2200 N NOTIN l /\ N,B same_side l [notNl] by l_line, Bexists, Nexists, RaySameSide;
2201 N,Y same_side l [Nsim_lY] by l_line, -, Bexists, SameSideTransitive;
2202 ray O N = ray O B /\ angle A O N === alpha by Bexists, Nexists, RayWellDefined, Angle_DEF;
2203 qed by notON, notNl, Nsim_lY, Nexists, -;
2206 let C4OppositeSide = thm `;
2207 let alpha l be point_set;
2208 let O A Z P Q be point;
2209 assume Angle alpha /\ ~(O = A) /\ ~(P = Q) [H1];
2210 assume Line l /\ O IN l /\ A IN l /\ Z NOTIN l [l_line];
2211 thus ? N. ~(O = N) /\ N NOTIN l /\ ~(Z,N same_side l) /\ seg O N === seg P Q /\ angle A O N === alpha
2214 ~(Z = O) by l_line, NOTIN;
2215 consider Y such that
2216 O IN open (Z,Y) [ZOY] by -, B2';
2217 ~(O = Y) /\ Collinear Z O Y by -, B1';
2218 Y NOTIN l [notYl] by l_line, I1, -, Collinear_DEF, NOTIN;
2219 consider N such that
2220 ~(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;
2221 ~(Z,Y same_side l) by l_line, ZOY, SameSide_DEF;
2222 ~(Z,N same_side l) by l_line, Nexists, notYl, -, SameSideTransitive;
2227 let A B C A' B' C' be point;
2228 assume ~Collinear A B C /\ ~Collinear A' B' C' [H1];
2229 assume seg A B === seg A' B' /\ seg A C === seg A' C' /\ seg B C === seg B' C' [H2];
2230 thus A,B,C cong A',B',C'
2233 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~(A' = B') /\ ~(B' = C') [Distinct] by H1, NonCollinearImpliesDistinct;
2234 consider h such that
2235 Line h /\ A IN h /\ C IN h [h_line] by Distinct, I1;
2236 B NOTIN h [notBh] by h_line, H1, NOTIN, Collinear_DEF;
2237 Segment (seg A B) /\ Segment (seg C B) /\ Segment (seg A' B') /\ Segment (seg C' B') [segments] by Distinct, -, SEGMENT;
2238 Angle (angle C' A' B') by H1, CollinearSymmetry, ANGLE;
2239 consider N such that
2240 ~(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;
2241 ~(C = N) by h_line, Nexists, NOTIN;
2242 Segment (seg A N) /\ Segment (seg C N) [segN] by Nexists, -, SEGMENT;
2243 ~Collinear A N C [ANCncol] by h_line, Distinct, I1, Collinear_DEF, Nexists, NOTIN;
2244 Angle (angle A B C) /\ Angle (angle A' B' C') /\ Angle (angle A N C) [angles] by H1, -, ANGLE;
2245 seg A B === seg A N [ABeqAN] by segments, segN, Nexists, H2, C2Symmetric, C2Transitive;
2246 C,A,N cong C',A',B' by ANCncol, H1, CollinearSymmetry, H2, Nexists, SAS;
2247 angle A N C === angle A' B' C' /\ seg C N === seg C' B' [ANCeq] by -, TriangleCong_DEF;
2248 seg C B === seg C N [CBeqCN] by segments, segN, -, H2, SegmentSymmetry, C2Symmetric, C2Transitive;
2249 consider G such that
2250 G IN h /\ G IN open (B,N) [BGN] by Nexists, h_line, SameSide_DEF;
2251 ~(B = N) [notBN] by -, B1';
2252 ray B G = ray B N /\ ray N G = ray N B [Grays] by BGN, B1', IntervalRay;
2253 consider v such that
2254 Line v /\ B IN v /\ N IN v [v_line] by notBN, I1;
2255 G IN v /\ ~(h = v) by v_line, BGN, BetweenLinear, notBh, NOTIN;
2256 h INTER v = {G} [hvG] by h_line, v_line, -, BGN, I1Uniqueness;
2257 ~(G = A) ==> angle A B G === angle A N G [ABGeqANG]
2259 assume ~(G = A) [notGA];
2260 A NOTIN v by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE;
2261 ~Collinear B A N by v_line, notBN, I1, Collinear_DEF, -, NOTIN;
2262 angle N B A === angle B N A by -, ABeqAN, IsoscelesCongBaseAngles;
2263 angle G B A === angle G N A by -, Grays, Angle_DEF, notGA;
2264 qed by -, AngleSymmetry;
2265 ~(G = C) ==> angle G B C === angle G N C [GBCeqGNC]
2267 assume ~(G = C) [notGC];
2268 C NOTIN v by hvG, h_line, -, EquivIntersectionHelp, IN_DELETE;
2269 ~Collinear B C N by v_line, notBN, I1, Collinear_DEF, -, NOTIN;
2270 angle N B C === angle B N C by -, CBeqCN, IsoscelesCongBaseAngles, AngleSymmetry;
2271 qed by -, Grays, Angle_DEF;
2272 angle A B C === angle A N C
2276 ~(G = C) by -, Distinct;
2277 qed by -, GBCeqGNC, GA;
2279 ~(G = A) by -, Distinct;
2280 qed by -, ABGeqANG, GC;
2281 suppose ~(G = A) /\ ~(G = C) [AGCdistinct];
2282 angle A B G === angle A N G /\ angle G B C === angle G N C [Gequivs] by -, ABGeqANG, GBCeqGNC;
2283 ~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;
2284 Collinear A G C by h_line, BGN, Collinear_DEF;
2285 G IN open (A,C) \/ C IN open (G,A) \/ A IN open (C,G) by Distinct, AGCdistinct, -, B3';
2287 suppose G IN open (A,C);
2288 G IN int_angle A B C /\ G IN int_angle A N C by H1, ANCncol, -, ConverseCrossbar;
2289 qed by -, Gequivs, AngleAddition;
2290 suppose C IN open (G,A);
2291 C IN int_angle G B A /\ C IN int_angle G N A by Gncols, -, B1', ConverseCrossbar;
2292 qed by -, Gequivs, AngleSubtraction, AngleSymmetry;
2293 suppose A IN open (C,G);
2294 A IN int_angle G B C /\ A IN int_angle G N C by Gncols, -, B1', ConverseCrossbar;
2295 qed by -, Gequivs, AngleSymmetry, AngleSubtraction;
2298 angle A B C === angle A' B' C' by angles, -, ANCeq, C5Transitive;
2299 qed by H1, H2, SegmentSymmetry, -, SAS;
2302 let AngleBisector = thm `;
2304 assume ~Collinear B A C [H1];
2305 thus ? F. F IN int_angle B A C /\ angle B A F === angle F A C
2308 ~(A = B) /\ ~(A = C) [Distinct] by H1, NonCollinearImpliesDistinct;
2309 consider D such that
2310 B IN open (A,D) [ABD] by Distinct, B2';
2311 ~(A = D) /\ Collinear A B D /\ Segment (seg A D) [ABD'] by -, B1', SEGMENT;
2312 consider E such that
2313 E IN ray A C DELETE A /\ seg A E === seg A D /\ ~(A = E) [ErAC] by -, Distinct, C1, IN_DELETE, IN_Ray;
2314 Collinear A C E /\ D IN ray A B DELETE A [notAE] by ErAC, IN_DELETE, IN_Ray, ABD, IntervalRayEZ;
2315 ray A D = ray A B /\ ray A E = ray A C [equalrays] by Distinct, notAE, ErAC, RayWellDefined;
2316 ~Collinear D A E /\ ~Collinear E A D /\ ~Collinear A E D [EADncol] by H1, ABD', notAE, ErAC, CollinearSymmetry, NoncollinearityExtendsToLine;
2317 angle D E A === angle E D A [DEAeq] by EADncol, ErAC, IsoscelesCongBaseAngles;
2318 ~Collinear E D A /\ Angle (angle E D A) /\ ~Collinear A D E /\ ~Collinear D E A [angEDA] by EADncol, CollinearSymmetry, ANGLE;
2319 ~(D = E) [notDE] by EADncol, NonCollinearImpliesDistinct;
2320 consider h such that
2321 Line h /\ D IN h /\ E IN h [h_line] by -, I1;
2322 A NOTIN h [notAh] by -, Collinear_DEF, EADncol, NOTIN;
2323 consider F such that
2324 ~(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;
2325 ~(A = F) [notAF] by h_line, -, SameSideReflexive;
2326 ~Collinear E D F /\ ~Collinear D E F /\ ~Collinear F E D [EDFncol] by h_line, notDE, I1, Collinear_DEF, Fexists, NOTIN;
2327 seg D E === seg D E /\ seg F A === seg F A [FArefl] by notDE, notAF, SEGMENT, C2Reflexive;
2328 E,D,F cong E,D,A by EDFncol, angEDA, -, Fexists, SAS;
2329 seg F E === seg A E /\ angle F E D === angle A E D [FEDcong] by -, TriangleCong_DEF, SegmentSymmetry;
2330 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;
2331 consider G such that
2332 G IN h /\ G IN open (A,F) [AGF] by Fexists, h_line, SameSide_DEF;
2333 F IN ray A G DELETE A [FrAG] by -, IntervalRayEZ;
2334 consider v such that
2335 Line v /\ A IN v /\ F IN v /\ G IN v [v_line] by notAF, I1, AGF, BetweenLinear;
2336 ~(v = h) /\ v INTER h = {G} [vhG] by -, notAh, NOTIN, h_line, AGF, I1Uniqueness;
2339 assume ~(D NOTIN v);
2340 D IN v /\ D = G [DG] by h_line, -, NOTIN, vhG, IN_INTER, IN_SING;
2341 D IN open (A,F) by DG, AGF;
2342 angle E D A suppl angle E D F [EDAsuppl] by angEDA, -, SupplementaryAngles_DEF, AngleSymmetry;
2343 Right (angle E D A) by EDAsuppl, EDAeqEDF, RightAngle_DEF;
2344 Right (angle A E D) [RightAED] by angEDA, ANGLE, -, DEAeq, CongRightImpliesRight, AngleSymmetry;
2345 Right (angle D E F) by EDFncol, ANGLE, -, FEDcong, CongRightImpliesRight, AngleSymmetry;
2346 E IN open (A,F) by EADncol, EDFncol, RightAED, -, h_line, Fexists, OppositeRightAnglesLinear;
2347 E IN v /\ E = G by v_line, -, BetweenLinear, h_line, vhG, IN_INTER, IN_SING;
2348 qed by -, DG, notDE;
2351 assume ~(E NOTIN v);
2352 E IN v /\ E = G [EG] by h_line, -, NOTIN, vhG, IN_INTER, IN_SING;
2353 E IN open (A,F) by -, AGF;
2354 angle D E A suppl angle D E F [DEAsuppl] by EADncol, -, SupplementaryAngles_DEF, AngleSymmetry;
2355 Right (angle D E A) [RightDEA] by DEAsuppl, EDAeqEDF, RightAngle_DEF;
2356 Right (angle E D A) [RightEDA] by angEDA, RightDEA, EDAeqEDF, CongRightImpliesRight;
2357 Right (angle E D F) by EDFncol, ANGLE, RightEDA, Fexists, CongRightImpliesRight;
2358 D IN open (A,F) by angEDA, EDFncol, RightEDA, AngleSymmetry, -, h_line, Fexists, OppositeRightAnglesLinear;
2359 D IN v /\ D = G by v_line, -, BetweenLinear, h_line, vhG, IN_INTER, IN_SING;
2360 qed by -, EG, notDE;
2361 ~Collinear F A E /\ ~Collinear F A D /\ ~(F = E) [FAEncol] by v_line, notAF, I1, Collinear_DEF, notEv, notDv, NOTIN, NonCollinearImpliesDistinct;
2362 seg F E === seg A D [FEeqAD] by -, ErAC, ABD', SEGMENT, FEDcong, ErAC, C2Transitive;
2363 seg A D === seg F D by SegmentSymmetry, ABD', Fexists, SEGMENT, C2Symmetric;
2364 seg F E === seg F D by FAEncol, ABD', Fexists, SEGMENT, FEeqAD, -, C2Transitive;
2365 F,A,E cong F,A,D by FAEncol, FArefl, -, ErAC, SSS;
2366 angle F A E === angle F A D [FAEeq] by -, TriangleCong_DEF;
2367 angle D A F === angle F A E by FAEncol, ANGLE, FAEeq, C5Symmetric, AngleSymmetry;
2368 angle B A F === angle F A C [BAFeqFAC] by -, equalrays, Angle_DEF;
2371 assume E,D same_side v;
2372 ray A D = ray A E by v_line, notAF, notDv, notEv, -, FAEeq, C4Uniqueness;
2373 qed by ABD', EndpointInRay, -, IN_Ray, EADncol;
2374 consider H such that
2375 H IN v /\ H IN open (E,D) [EHD] by v_line, -, SameSide_DEF;
2376 H = G by -, h_line, BetweenLinear, IN_INTER, vhG, IN_SING;
2377 G IN int_angle E A D [GintEAD] by EADncol, -, EHD, ConverseCrossbar;
2378 F IN int_angle E A D [FintEAD] by GintEAD, FrAG, WholeRayInterior;
2379 B IN ray A D DELETE A /\ C IN ray A E DELETE A by equalrays, Distinct, EndpointInRay, IN_DELETE;
2380 F IN int_angle B A C by FintEAD, -, InteriorWellDefined, InteriorAngleSymmetry;
2384 let EuclidPropositionI_6 = thm `;
2386 assume ~Collinear A B C [H1];
2387 assume angle B A C === angle B C A [H2];
2388 thus seg B A === seg B C
2391 ~(A = C) by H1, NonCollinearImpliesDistinct;
2392 seg C A === seg A C [CAeqAC] by SegmentSymmetry, -, SEGMENT, C2Reflexive;
2393 ~Collinear B C A /\ ~Collinear C B A /\ ~Collinear B A C [BCAncol] by H1, CollinearSymmetry;
2394 angle A C B === angle C A B by -, ANGLE, H2, C5Symmetric, AngleSymmetry;
2395 C,B,A cong A,B,C by H1, BCAncol, CAeqAC, H2, -, ASA;
2396 qed by -, TriangleCong_DEF;
2399 let IsoscelesExists = thm `;
2401 assume ~(A = B) [H1];
2402 thus ? D. ~Collinear A D B /\ seg D A === seg D B
2405 consider l such that
2406 Line l /\ A IN l /\ B IN l [l_line] by H1, I1;
2407 consider C such that
2408 C NOTIN l [notCl] by -, ExistsPointOffLine;
2409 ~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;
2410 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;
2412 suppose angle C A B === angle C B A;
2413 qed by -, CABncol, EuclidPropositionI_6;
2414 suppose angle C A B <_ang angle C B A;
2415 angle C A B <_ang angle A B C by -, AngleSymmetry;
2416 consider E such that
2417 E IN int_angle A B C /\ angle C A B === angle A B E [Eexists] by CABncol, ANGLE, -, AngleOrderingUse;
2418 ~(B = E) [notBE] by -, InteriorEZHelp;
2419 consider D such that
2420 D IN open (A,C) /\ D IN ray B E DELETE B [Dexists] by Eexists, Crossbar_THM;
2421 D IN int_angle A B C by Eexists, -, WholeRayInterior;
2422 ~Collinear A D B [ADBncol] by -, InteriorEZHelp, CollinearSymmetry;
2423 ray B D = ray B E /\ ray A D = ray A C by notBE, Dexists, RayWellDefined, IntervalRay;
2424 angle D A B === angle A B D by Eexists, -, Angle_DEF;
2425 qed by ADBncol, -, AngleSymmetry, EuclidPropositionI_6;
2427 suppose angle C B A <_ang angle C A B;
2428 angle C B A <_ang angle B A C by -, AngleSymmetry;
2429 consider E such that
2430 E IN int_angle B A C /\ angle C B A === angle B A E [Eexists] by CABncol, ANGLE, -, AngleOrderingUse;
2431 ~(A = E) [notAE] by -, InteriorEZHelp;
2432 consider D such that
2433 D IN open (B,C) /\ D IN ray A E DELETE A [Dexists] by Eexists, Crossbar_THM;
2434 D IN int_angle B A C by Eexists, -, WholeRayInterior;
2435 ~Collinear A D B /\ ~Collinear D A B /\ ~Collinear D B A [ADBncol] by -, InteriorEZHelp, CollinearSymmetry;
2436 ray A D = ray A E /\ ray B D = ray B C by notAE, Dexists, RayWellDefined, IntervalRay;
2437 angle D B A === angle B A D by Eexists, -, Angle_DEF;
2438 angle D A B === angle D B A by AngleSymmetry, ADBncol, ANGLE, -, C5Symmetric;
2439 qed by ADBncol, -, EuclidPropositionI_6;
2443 let MidpointExists = thm `;
2445 assume ~(A = B) [H1];
2446 thus ? M. M IN open (A,B) /\ seg A M === seg M B
2449 consider D such that
2450 ~Collinear A D B /\ seg D A === seg D B [Dexists] by H1, IsoscelesExists;
2451 consider F such that
2452 F IN int_angle A D B /\ angle A D F === angle F D B [Fexists] by -, AngleBisector;
2453 ~(D = F) [notDF] by -, InteriorEZHelp;
2454 consider M such that
2455 M IN open (A,B) /\ M IN ray D F DELETE D [Mexists] by Fexists, Crossbar_THM;
2456 ray D M = ray D F by notDF, -, RayWellDefined;
2457 angle A D M === angle M D B [ADMeqMDB] by Fexists, -, Angle_DEF;
2458 M IN int_angle A D B by Fexists, Mexists, WholeRayInterior;
2459 ~(D = M) /\ ~Collinear A D M /\ ~Collinear B D M [ADMncol] by -, InteriorEZHelp, InteriorAngleSymmetry;
2460 seg D M === seg D M by -, SEGMENT, C2Reflexive;
2461 A,D,M cong B,D,M by ADMncol, Dexists, -, ADMeqMDB, AngleSymmetry, SAS;
2462 qed by Mexists, -, TriangleCong_DEF, SegmentSymmetry;
2465 let EuclidPropositionI_7short = thm `;
2466 let A B C D be point;
2468 assume ~(A = B) /\ Line a /\ A IN a /\ B IN a [a_line];
2469 assume ~(C = D) /\ C NOTIN a /\ D NOTIN a /\ C,D same_side a [Csim_aD];
2470 assume seg A C === seg A D [ACeqAD];
2471 thus ~(seg B C === seg B D)
2474 ~(A = C) /\ ~(A = D) [AnotCD] by a_line, Csim_aD, NOTIN;
2475 assume seg B C === seg B D;
2476 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;
2477 ~Collinear A C B /\ ~Collinear A D B by a_line, I1, Csim_aD, Collinear_DEF, NOTIN;
2478 A,C,B cong A,D,B by -, ACeqAD, segeqs, SSS;
2479 angle B A C === angle B A D by -, TriangleCong_DEF;
2480 ray A D = ray A C by a_line, Csim_aD, -, C4Uniqueness;
2481 C IN ray A D DELETE A /\ D IN ray A D DELETE A by AnotCD, -, EndpointInRay, IN_DELETE;
2482 C = D by AnotCD, SEGMENT, -, ACeqAD, segeqs, C1;
2486 let EuclidPropositionI_7Help = thm `;
2487 let A B C D be point;
2489 assume ~(A = B) [notAB];
2490 assume Line a /\ A IN a /\ B IN a [a_line];
2491 assume ~(C = D) /\ C NOTIN a /\ D NOTIN a /\ C,D same_side a [Csim_aD];
2492 assume seg A C === seg A D [ACeqAD];
2493 assume C IN int_triangle D A B \/ ConvexQuadrilateral A B C D [Int_ConvQuad];
2494 thus ~(seg B C === seg B D)
2497 ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) [Distinct] by a_line, Csim_aD, NOTIN, SameSide_DEF;
2498 cases by Int_ConvQuad;
2499 suppose ConvexQuadrilateral A B C D;
2500 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;
2501 ~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;
2502 angle C D A === angle D C A [CDAeqDCA] by angCDB, Distinct, SEGMENT, ACeqAD, C2Symmetric, IsoscelesCongBaseAngles;
2503 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;
2504 angle D C A <_ang angle D C B /\ angle C D B <_ang angle C D A by angCDB, ABint, -, AngleOrdering_DEF;
2505 angle C D B <_ang angle D C B by -, angCDB, CDAeqDCA, AngleTrichotomy2, AngleOrderTransitivity;
2506 ~(angle D C B === angle C D B) by -, AngleTrichotomy1, angCDB, ANGLE, C5Symmetric;
2507 qed by angCDB, -, IsoscelesCongBaseAngles;
2508 suppose C IN int_triangle D A B;
2509 C IN int_angle A D B /\ C IN int_angle D A B [CintADB] by -, IN_InteriorTriangle, InteriorAngleSymmetry;
2510 ~Collinear A D C /\ ~Collinear B D C [ADCncol] by CintADB, InteriorEZHelp, InteriorAngleSymmetry;
2511 ~Collinear D A C /\ ~Collinear C D A /\ ~Collinear A C D /\ ~Collinear A D C [DACncol] by -, CollinearSymmetry;
2512 ~Collinear B C D /\ Angle (angle D C A) /\ Angle (angle C D B) /\ ~Collinear D C B [angCDB] by ADCncol, -, CollinearSymmetry, ANGLE;
2513 angle C D A === angle D C A [CDAeqDCA] by DACncol, Distinct, ADCncol, SEGMENT, ACeqAD, C2Symmetric, IsoscelesCongBaseAngles;
2514 consider E such that
2515 D IN open (A,E) /\ ~(D = E) /\ Collinear A D E [ADE] by Distinct, B2', B1';
2516 B IN int_angle C D E /\ Collinear D A E [BintCDE] by CintADB, -, InteriorReflectionInterior, CollinearSymmetry;
2517 ~Collinear C D E [CDEncol] by DACncol, -, ADE, NoncollinearityExtendsToLine;
2518 consider F such that
2519 F IN open (B,D) /\ F IN ray A C DELETE A [Fexists] by CintADB, Crossbar_THM, B1';
2520 F IN int_angle B C D [FintBCD] by ADCncol, CollinearSymmetry, -, ConverseCrossbar;
2521 ~Collinear D C F [DCFncol] by Distinct, ADCncol, CollinearSymmetry, Fexists, B1', NoncollinearityExtendsToLine;
2522 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;
2523 C IN open (A,F) by -, AlternateConverseCrossbar;
2524 angle A D C suppl angle C D E /\ angle A C D suppl angle D C F by ADE, DACncol, -, SupplementaryAngles_DEF;
2525 angle C D E === angle D C F [CDEeqDCF] by -, CDAeqDCA, AngleSymmetry, SupplementsCongAnglesCong;
2526 angle C D B <_ang angle C D E by angCDB, CDEncol, BintCDE, C5Reflexive, AngleOrdering_DEF;
2527 angle C D B <_ang angle D C F [CDBlessDCF] by -, DCFncol, ANGLE, CDEeqDCF, AngleTrichotomy2;
2528 angle D C F <_ang angle D C B by DCFncol, ANGLE, angCDB, FintBCD, InteriorAngleSymmetry, C5Reflexive, AngleOrdering_DEF;
2529 angle C D B <_ang angle D C B by CDBlessDCF, -, AngleOrderTransitivity;
2530 ~(angle D C B === angle C D B) by -, AngleTrichotomy1, angCDB, CollinearSymmetry, ANGLE, C5Symmetric;
2531 qed by Distinct, ADCncol, CollinearSymmetry, -, IsoscelesCongBaseAngles;
2535 let EuclidPropositionI_7 = thm `;
2536 let A B C D be point;
2538 assume ~(A = B) [notAB];
2539 assume Line a /\ A IN a /\ B IN a [a_line];
2540 assume ~(C = D) /\ C NOTIN a /\ D NOTIN a /\ C,D same_side a [Csim_aD];
2541 assume seg A C === seg A D [ACeqAD];
2542 thus ~(seg B C === seg B D)
2545 ~Collinear A B C /\ ~Collinear D A B [ABCncol] by a_line, notAB, I1, Collinear_DEF, Csim_aD, NOTIN;
2546 ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ A NOTIN open (C,D) [Distinct] by a_line, Csim_aD, NOTIN, SameSide_DEF;
2547 ~Collinear A D C [ADCncol]
2549 assume Collinear A D C;
2550 C IN ray A D DELETE A /\ D IN ray A D DELETE A by Distinct, -, IN_Ray, EndpointInRay, IN_DELETE;
2551 qed by Distinct, SEGMENT, -, ACeqAD, C2Reflexive, C1, Csim_aD;
2552 D,C same_side a [Dsim_aC] by a_line, Csim_aD, SameSideSymmetric;
2553 seg A D === seg A C /\ seg B D === seg B D [ADeqAC] by Distinct, SEGMENT, ACeqAD, C2Symmetric, C2Reflexive;
2554 ~Collinear D A C /\ ~Collinear C D A /\ ~Collinear A C D /\ ~Collinear A D C [DACncol] by ADCncol, CollinearSymmetry;
2555 ~(seg B D === seg B C) ==> ~(seg B C === seg B D) [BswitchDC] by Distinct, SEGMENT, C2Symmetric;
2557 suppose Collinear B D C;
2558 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;
2559 qed by Distinct, SEGMENT, -, ACeqAD, ADeqAC, C1, Csim_aD;
2560 suppose ~Collinear B D C [BDCncol];
2561 Tetralateral A B C D by notAB, Distinct, Csim_aD, ABCncol, -, CollinearSymmetry, DACncol, Tetralateral_DEF;
2562 ConvexQuadrilateral A B C D \/ C IN int_triangle D A B \/
2563 ConvexQuadrilateral A B D C \/ D IN int_triangle C A B by -, a_line, Csim_aD, FourChoicesTetralateral, InteriorTriangleSymmetry;
2564 qed by notAB, a_line, Csim_aD, Dsim_aC, ACeqAD, ADeqAC, -, EuclidPropositionI_7Help, BswitchDC;
2568 let EuclidPropositionI_11 = thm `;
2570 assume ~(A = B) [notAB];
2571 thus ? F. Right (angle A B F)
2574 consider C such that
2575 B IN open (A,C) /\ seg B C === seg B A [ABC] by notAB, SEGMENT, C1OppositeRay;
2576 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ Collinear A B C [Distinct] by ABC, B1';
2577 seg B A === seg B C [BAeqBC] by -, SEGMENT, ABC, C2Symmetric;
2578 consider F such that
2579 ~Collinear A F C /\ seg F A === seg F C [Fexists] by Distinct, IsoscelesExists;
2580 ~Collinear B F A /\ ~Collinear B F C [BFAncol] by -, CollinearSymmetry, Distinct, NoncollinearityExtendsToLine;
2581 ~Collinear A B F /\ Angle (angle A B F) [angABF] by BFAncol, CollinearSymmetry, ANGLE;
2582 angle A B F suppl angle F B C [ABFsuppl] by -, ABC, SupplementaryAngles_DEF;
2583 ~(B = F) /\ seg B F === seg B F by BFAncol, NonCollinearImpliesDistinct, SEGMENT, C2Reflexive;
2584 B,F,A cong B,F,C by BFAncol, -, BAeqBC, Fexists, SSS;
2585 angle A B F === angle F B C by -, TriangleCong_DEF, AngleSymmetry;
2586 qed by angABF, ABFsuppl, -, RightAngle_DEF;
2589 let DropPerpendicularToLine = thm `;
2592 assume Line l /\ P NOTIN l [l_line];
2593 thus ? E Q. E IN l /\ Q IN l /\ Right (angle P Q E)
2596 consider A B such that
2597 A IN l /\ B IN l /\ ~(A = B) [ABl] by l_line, I2;
2598 ~Collinear B A P /\ ~Collinear P A B /\ ~(A = P) [BAPncol] by l_line, ABl, I1, Collinear_DEF, NOTIN, CollinearSymmetry, ABl, NOTIN;
2599 Angle (angle B A P) /\ Angle (angle P A B) [angBAP] by -, ANGLE, AngleSymmetry;
2600 consider P' such that
2601 ~(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;
2602 consider Q such that
2603 Q IN l /\ Q IN open (P,P') /\ Collinear A B Q [Qexists] by l_line, -, SameSide_DEF, ABl, Collinear_DEF;
2604 ~Collinear B A P' [BAP'ncol] by l_line, ABl, I1, Collinear_DEF, P'exists, NOTIN;
2605 angle B A P === angle B A P' [BAPeqBAP'] by -, ANGLE, angBAP, P'exists, C5Symmetric;
2606 ? E. E IN l /\ ~Collinear P Q E /\ angle P Q E === angle E Q P'
2610 qed by ABl, AQ, BAPncol, BAPeqBAP', AngleSymmetry;
2611 suppose ~(A = Q) [notAQ];
2612 seg A Q === seg A Q /\ seg A P === seg A P' [APeqAP'] by -, SEGMENT, C2Reflexive, BAPncol, P'exists, C2Symmetric;
2613 ~Collinear Q A P' /\ ~Collinear Q A P [QAP'ncol] by l_line, ABl, Qexists, notAQ, I1, Collinear_DEF, P'exists, NOTIN;
2614 angle Q A P === angle Q A P'
2617 suppose A IN open (Q,B);
2618 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;
2619 qed by -, BAPeqBAP', SupplementsCongAnglesCong, AngleSymmetry;
2620 suppose ~(A IN open (Q,B));
2621 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;
2622 qed by -, BAPeqBAP', Angle_DEF;
2624 Q,A,P cong Q,A,P' by QAP'ncol, APeqAP', -, SAS;
2625 qed by -, TriangleCong_DEF, AngleSymmetry, ABl, QAP'ncol, CollinearSymmetry;
2627 consider E such that
2628 E IN l /\ ~Collinear P Q E /\ angle P Q E === angle E Q P' [Eexists] by -;
2629 angle P Q E suppl angle E Q P' /\ Right (angle P Q E) by -, Qexists, SupplementaryAngles_DEF, RightAngle_DEF;
2630 qed by Eexists, Qexists, -;
2633 let EuclidPropositionI_14 = thm `;
2634 let A B C D be point;
2636 assume Line l /\ A IN l /\ B IN l /\ ~(A = B) [l_line];
2637 assume C NOTIN l /\ D NOTIN l /\ ~(C,D same_side l) [Cnsim_lD];
2638 assume angle C B A suppl angle A B D [CBAsupplABD];
2639 thus B IN open (C,D)
2642 ~(B = C) /\ ~(B = D) /\ ~Collinear C B A [Distinct] by l_line, Cnsim_lD, NOTIN, I1, Collinear_DEF;
2643 consider E such that
2644 B IN open (C,E) [CBE] by Distinct, B2';
2645 E NOTIN l /\ ~(C,E same_side l) [Csim_lE] by l_line, NOTIN, -, BetweenLinear, Cnsim_lD, SameSide_DEF;
2646 D,E same_side l [Dsim_lE] by l_line, Cnsim_lD, -, AtMost2Sides;
2647 angle C B A suppl angle A B E by Distinct, CBE, SupplementaryAngles_DEF;
2648 angle A B D === angle A B E by CBAsupplABD, -, SupplementUnique;
2649 ray B E = ray B D by l_line, Csim_lE, Cnsim_lD, Dsim_lE, -, C4Uniqueness;
2650 D IN ray B E DELETE B by Distinct, -, EndpointInRay, IN_DELETE;
2651 qed by CBE, -, OppositeRaysIntersect1pointHelp, B1';
2654 let VerticalAnglesCong = thm `; :: Euclid's Proposition I.15
2655 let A B O A' B' be point;
2656 assume ~Collinear A O B [H1];
2657 assume O IN open (A,A') /\ O IN open (B,B') [H2];
2658 thus angle B O A' === angle B' O A
2661 angle A O B suppl angle B O A' [AOBsupplBOA'] by H1, H2, SupplementaryAngles_DEF;
2662 angle B O A suppl angle A O B' by H1, CollinearSymmetry, H2, SupplementaryAngles_DEF;
2663 qed by AOBsupplBOA', -, AngleSymmetry, SupplementUnique;
2666 let EuclidPropositionI_16 = thm `;
2667 let A B C D be point;
2668 assume ~Collinear A B C [H1];
2669 assume C IN open (B,D) [H2];
2670 thus angle B A C <_ang angle D C A
2673 ~(A = B) /\ ~(A = C) /\ ~(B = C) [Distinct] by H1, NonCollinearImpliesDistinct;
2674 consider l such that
2675 Line l /\ A IN l /\ C IN l [l_line] by Distinct, I1;
2676 consider m such that
2677 Line m /\ B IN m /\ C IN m [m_line] by Distinct, I1;
2678 D IN m [Dm] by m_line, H2, BetweenLinear;
2679 consider E such that
2680 E IN open (A,C) /\ seg A E === seg E C [AEC] by Distinct, MidpointExists;
2681 ~(A = E) /\ ~(E = C) /\ Collinear A E C /\ ~(B = E) [AECcol] by -, B1', H1;
2682 E IN l [El] by l_line, AEC, BetweenLinear;
2683 consider F such that
2684 E IN open (B,F) /\ seg E F === seg E B [BEF] by AECcol, SEGMENT, C1OppositeRay;
2685 ~(B = E) /\ ~(B = F) /\ ~(E = F) /\ Collinear B E F [BEF'] by BEF, B1';
2686 B NOTIN l [notBl] by l_line, Distinct, I1, Collinear_DEF, H1, NOTIN;
2687 ~Collinear A E B /\ ~Collinear C E B [AEBncol] by l_line, El, AECcol, I1, Collinear_DEF, notBl, NOTIN;
2688 Angle (angle B A E) [angBAE] by -, CollinearSymmetry, ANGLE;
2689 ~Collinear C E F [CEFncol] by AEBncol, BEF', CollinearSymmetry, NoncollinearityExtendsToLine;
2690 angle B E A === angle F E C [BEAeqFEC] by AEBncol, AEC, B1', BEF, VerticalAnglesCong;
2691 seg E A === seg E C /\ seg E B === seg E F by AEC, SegmentSymmetry, AECcol, BEF', SEGMENT, BEF, C2Symmetric;
2692 A,E,B cong C,E,F by AEBncol, CEFncol, -, BEAeqFEC, AngleSymmetry, SAS;
2693 angle B A E === angle F C E [BAEeqFCE] by -, TriangleCong_DEF;
2694 ~Collinear E C D [ECDncol] by AEBncol, H2, B1', CollinearSymmetry, NoncollinearityExtendsToLine;
2695 F NOTIN l /\ D NOTIN l [notFl] by l_line, El, Collinear_DEF, CEFncol, -, NOTIN;
2696 F IN ray B E DELETE B /\ E NOTIN m by BEF, IntervalRayEZ, m_line, Collinear_DEF, AEBncol, NOTIN;
2697 F NOTIN m /\ F,E same_side m [Fsim_mE] by m_line, -, RaySameSide;
2698 ~(B,F same_side l) /\ ~(B,D same_side l) by El, l_line, BEF, H2, SameSide_DEF;
2699 F,D same_side l by l_line, notBl, notFl, -, AtMost2Sides;
2700 F IN int_angle E C D by ECDncol, l_line, El, m_line, Dm, notFl, Fsim_mE, -, IN_InteriorAngle;
2701 angle B A E <_ang angle E C D [BAElessECD] by angBAE, ECDncol, -, BAEeqFCE, AngleSymmetry, AngleOrdering_DEF;
2702 ray A E = ray A C /\ ray C E = ray C A by AEC, B1', IntervalRay;
2703 angle B A C <_ang angle A C D by BAElessECD, -, Angle_DEF;
2704 qed by -, AngleSymmetry;
2707 let ExteriorAngle = thm `;
2708 let A B C D be point;
2709 assume ~Collinear A B C [H1];
2710 assume C IN open (B,D) [H2];
2711 thus angle A B C <_ang angle A C D
2714 ~(C = D) /\ C IN open (D,B) /\ Collinear B C D [H2'] by H2, BetweenLinear, B1';
2715 ~Collinear B A C /\ ~(A = C) [BACncol] by H1, CollinearSymmetry, NonCollinearImpliesDistinct;
2716 consider E such that
2717 C IN open (A,E) [ACE] by -, B2';
2718 ~(C = E) /\ C IN open (E,A) /\ Collinear A C E [ACE'] by -, B1';
2719 ~Collinear A C D /\ ~Collinear D C E [DCEncol] by H1, CollinearSymmetry, H2', -, NoncollinearityExtendsToLine;
2720 angle A B C <_ang angle E C B [ABClessECB] by BACncol, ACE, EuclidPropositionI_16;
2721 angle E C B === angle A C D by DCEncol, ACE', H2', VerticalAnglesCong;
2722 qed by ABClessECB, DCEncol, ANGLE, -, AngleTrichotomy2;
2725 let EuclidPropositionI_17 = thm `;
2727 let alpha beta gamma be point_set;
2728 assume ~Collinear A B C /\ alpha = angle A B C /\ beta = angle B C A [H1];
2729 assume beta suppl gamma [H2];
2730 thus alpha <_ang gamma
2733 Angle gamma [anggamma] by H2, SupplementImpliesAngle;
2734 ~(A = B) /\ ~(A = C) /\ ~(B = C) [Distinct] by H1, NonCollinearImpliesDistinct;
2735 ~Collinear B A C /\ ~Collinear A C B [BACncol] by H1, CollinearSymmetry;
2736 consider D such that
2737 C IN open (A,D) [ACD] by Distinct, B2';
2738 angle A B C <_ang angle D C B [ABClessDCB] by BACncol, ACD, EuclidPropositionI_16;
2739 beta suppl angle B C D by -, H1, AngleSymmetry, BACncol, ACD, SupplementaryAngles_DEF;
2740 angle B C D === gamma by H2, -, SupplementUnique;
2741 qed by ABClessDCB, H1, AngleSymmetry, anggamma, -, AngleTrichotomy2;
2744 let EuclidPropositionI_18 = thm `;
2746 assume ~Collinear A B C [H1];
2747 assume seg A C <__ seg A B [H2];
2748 thus angle A B C <_ang angle B C A
2751 ~(A = B) /\ ~(A = C) [Distinct] by H1, NonCollinearImpliesDistinct;
2752 consider D such that
2753 D IN open (A,B) /\ seg A C === seg A D [ADB] by Distinct, SEGMENT, H2, SegmentOrderingUse;
2754 ~(D = A) /\ ~(D = B) /\ D IN open (B,A) /\ Collinear A D B /\ ray B D = ray B A [ADB'] by -, B1', IntervalRay;
2755 D IN int_angle A C B [DintACB] by H1, CollinearSymmetry, ADB, ConverseCrossbar;
2756 ~Collinear D A C /\ ~Collinear C B D [DACncol] by H1, CollinearSymmetry, ADB', NoncollinearityExtendsToLine;
2757 seg A D === seg A C by ADB', Distinct, SEGMENT, ADB, C2Symmetric;
2758 angle C D A === angle A C D by DACncol, -, IsoscelesCongBaseAngles, AngleSymmetry;
2759 angle C D A <_ang angle A C B [CDAlessACB] by DACncol, CollinearSymmetry, ANGLE, H1, CollinearSymmetry, DintACB, -, AngleOrdering_DEF;
2760 angle B D C suppl angle C D A by DACncol, CollinearSymmetry, ADB', SupplementaryAngles_DEF;
2761 angle C B D <_ang angle C D A by DACncol, -, EuclidPropositionI_17;
2762 angle C B D <_ang angle A C B by -, CDAlessACB, AngleOrderTransitivity;
2763 qed by -, ADB', Angle_DEF, AngleSymmetry;
2766 let EuclidPropositionI_19 = thm `;
2768 assume ~Collinear A B C [H1];
2769 assume angle A B C <_ang angle B C A [H2];
2770 thus seg A C <__ seg A B
2773 ~Collinear B A C /\ ~Collinear B C A /\ ~Collinear A C B [BACncol] by H1, CollinearSymmetry;
2774 ~(A = B) /\ ~(A = C) [Distinct] by H1, NonCollinearImpliesDistinct;
2775 assume ~(seg A C <__ seg A B);
2776 seg A B === seg A C \/ seg A B <__ seg A C by Distinct, SEGMENT, -, SegmentTrichotomy;
2778 suppose seg A B === seg A C;
2779 angle C B A === angle B C A by BACncol, -, IsoscelesCongBaseAngles;
2780 qed by -, AngleSymmetry, H2, AngleTrichotomy1;
2781 suppose seg A B <__ seg A C;
2782 angle A C B <_ang angle C B A by BACncol, -, EuclidPropositionI_18;
2783 qed by H1, BACncol, ANGLE, -, AngleSymmetry, H2, AngleTrichotomy;
2787 let EuclidPropositionI_20 = thm `;
2788 let A B C D be point;
2789 assume ~Collinear A B C [H1];
2790 assume A IN open (B,D) /\ seg A D === seg A C [H2];
2791 thus seg B C <__ seg B D
2794 ~(B = D) /\ ~(A = D) /\ A IN open (D,B) /\ Collinear B A D /\ ray D A = ray D B [BAD'] by H2, B1', IntervalRay;
2795 ~Collinear C A D [CADncol] by H1, CollinearSymmetry, BAD', NoncollinearityExtendsToLine;
2796 ~Collinear D C B /\ ~Collinear B D C [DCBncol] by H1, CollinearSymmetry, BAD', NoncollinearityExtendsToLine; :: 13
2797 Angle (angle C D A) [angCDA] by CADncol, CollinearSymmetry, ANGLE;
2798 angle C D A === angle D C A [CDAeqDCA] by CADncol, CollinearSymmetry, H2, IsoscelesCongBaseAngles;
2799 A IN int_angle D C B by DCBncol, BAD', ConverseCrossbar;
2800 angle C D A <_ang angle D C B by angCDA, DCBncol, -, CDAeqDCA, AngleOrdering_DEF;
2801 angle B D C <_ang angle D C B by -, BAD', Angle_DEF, AngleSymmetry;
2802 qed by DCBncol, -, EuclidPropositionI_19;
2805 let EuclidPropositionI_21 = thm `;
2806 let A B C D be point;
2807 assume ~Collinear A B C [H1];
2808 assume D IN int_triangle A B C [H2];
2809 thus angle A B C <_ang angle C D A
2812 ~(B = A) /\ ~(B = C) /\ ~(A = C) [Distinct] by H1, NonCollinearImpliesDistinct;
2813 D IN int_angle B A C /\ D IN int_angle C B A [DintTri] by H2, IN_InteriorTriangle, InteriorAngleSymmetry;
2814 consider E such that
2815 E IN open (B,C) /\ E IN ray A D DELETE A [BEC] by -, Crossbar_THM;
2816 ~(B = E) /\ ~(E = C) /\ Collinear B E C /\ Collinear A D E [BEC'] by -, B1', IN_DELETE, IN_Ray;
2817 ray B E = ray B C /\ E IN ray B C DELETE B [rBErBC] by BEC, IntervalRay, IntervalRayEZ;
2818 D IN int_angle A B E [DintABE] by DintTri, -, InteriorAngleSymmetry, InteriorWellDefined;
2819 D IN open (A,E) [ADE] by BEC', -, AlternateConverseCrossbar;
2820 ray E D = ray E A [rEDrEA] by -, B1', IntervalRay;
2821 ~Collinear A B E /\ ~Collinear B E A /\ ~Collinear C B D /\ ~(A = D) [ABEncol] by DintABE, IN_InteriorAngle, CollinearSymmetry, DintTri, InteriorEZHelp;
2822 ~Collinear E D C /\ ~Collinear C E D [EDCncol] by -, CollinearSymmetry, BEC', NoncollinearityExtendsToLine;
2823 angle A B E <_ang angle A E C by ABEncol, BEC, ExteriorAngle;
2824 angle A B C <_ang angle C E D [ABClessAEC] by -, rBErBC, rEDrEA, Angle_DEF, AngleSymmetry;
2825 angle C E D <_ang angle C D A by EDCncol, ADE, B1', ExteriorAngle;
2826 qed by ABClessAEC, -, AngleOrderTransitivity;
2829 let AngleTrichotomy3 = thm `;
2830 let alpha beta gamma be point_set;
2831 assume alpha <_ang beta /\ Angle gamma /\ gamma === alpha [H1];
2832 thus gamma <_ang beta
2835 consider A O B G such that
2836 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;
2837 ~Collinear A O G by -, InteriorEZHelp;
2838 gamma === angle A O G by H1, H1', -, ANGLE, C5Transitive;
2839 qed by H1, H1', -, AngleOrdering_DEF;
2842 let InteriorCircleConvexHelp = thm `;
2843 let O A B C be point;
2844 assume ~Collinear A O C [H1];
2845 assume B IN open (A,C) [H2];
2846 assume seg O A <__ seg O C \/ seg O A === seg O C [H3];
2847 thus seg O B <__ seg O C
2850 ~Collinear O C A /\ ~Collinear C O A /\ ~(O = A) /\ ~(O = C) [H1'] by H1, CollinearSymmetry, NonCollinearImpliesDistinct;
2851 ray A B = ray A C /\ ray C B = ray C A [equal_rays] by H2, IntervalRay, B1';
2852 angle O C A <_ang angle C A O \/ angle O C A === angle C A O
2855 suppose seg O A <__ seg O C;
2856 qed by H1', -, EuclidPropositionI_18;
2857 suppose seg O A === seg O C [seg_eq];
2858 seg O C === seg O A by H1', SEGMENT, -, C2Symmetric;
2859 qed by H1', -, IsoscelesCongBaseAngles, AngleSymmetry;
2861 angle O C B <_ang angle B A O \/ angle O C B === angle B A O by -, equal_rays, Angle_DEF;
2862 angle B C O <_ang angle O A B \/ angle B C O === angle O A B [BCOlessOAB] by -, AngleSymmetry;
2863 ~Collinear O A B /\ ~Collinear B C O /\ ~Collinear O C B [OABncol] by H1, CollinearSymmetry, H2, B1', NoncollinearityExtendsToLine;
2864 angle O A B <_ang angle O B C by -, H2, ExteriorAngle;
2865 angle B C O <_ang angle O B C by BCOlessOAB, -, AngleOrderTransitivity, OABncol, ANGLE, -, AngleTrichotomy3;
2866 qed by OABncol, -, AngleSymmetry, EuclidPropositionI_19;
2869 let InteriorCircleConvex = thm `;
2870 let O R A B C be point;
2871 assume ~(O = R) [H1];
2872 assume B IN open (A,C) [H2];
2873 assume A IN int_circle O R /\ C IN int_circle O R [H3];
2874 thus B IN int_circle O R
2877 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ B IN open (C,A) [H2'] by H2, B1';
2878 (A = O \/ seg O A <__ seg O R) /\ (C = O \/ seg O C <__ seg O R) [ACintOR] by H3, H1, IN_InteriorCircle;
2880 suppose O = A \/ O = C;
2881 B IN open (O,C) \/ B IN open (O,A) by -, H2, B1';
2882 seg O B <__ seg O A /\ ~(O = A) \/ seg O B <__ seg O C /\ ~(O = C) by -, B1', SEGMENT, C2Reflexive, SegmentOrdering_DEF;
2883 seg O B <__ seg O R by -, ACintOR, SegmentOrderTransitivity;
2884 qed by -, H1, IN_InteriorCircle;
2885 suppose ~(O = A) /\ ~(O = C) [OnotAC];
2887 suppose ~Collinear A O C [AOCncol];
2888 seg O A <__ seg O C \/ seg O A === seg O C \/ seg O C <__ seg O A by OnotAC, SEGMENT, SegmentTrichotomy;
2889 seg O B <__ seg O C \/ seg O B <__ seg O A by AOCncol, H2, -, InteriorCircleConvexHelp, CollinearSymmetry, B1';
2890 qed by OnotAC, ACintOR, -, SegmentOrderTransitivity, H1, IN_InteriorCircle;
2891 suppose Collinear A O C [AOCcol];
2892 consider l such that
2893 Line l /\ A IN l /\ C IN l by H2', I1;
2894 Collinear B A O /\ Collinear B C O [OABCcol] by -, H2, BetweenLinear, H2', AOCcol, CollinearLinear, Collinear_DEF;
2895 B NOTIN open (O,A) /\ B NOTIN open (O,C) ==> B = O
2897 assume B NOTIN open (O,A) /\ B NOTIN open (O,C);
2898 O IN ray B A INTER ray B C by H2', OABCcol, -, IN_Ray, IN_INTER;
2899 qed by -, H2, OppositeRaysIntersect1point, IN_SING;
2900 B IN open (O,A) \/ B IN open (O,C) \/ B = O by -, NOTIN;
2901 seg O B <__ seg O A \/ seg O B <__ seg O C \/ B = O by -, B1', SEGMENT, C2Reflexive, SegmentOrdering_DEF;
2902 seg O B <__ seg O R \/ B = O by -, ACintOR, OnotAC, SegmentOrderTransitivity;
2903 qed by -, H1, IN_InteriorCircle;
2908 let SegmentTrichotomy3 = thm `;
2909 let s t u be point_set;
2910 assume s <__ t /\ Segment u /\ u === s [H1];
2914 consider C D X such that
2915 Segment s /\ t = seg C D /\ X IN open (C,D) /\ s === seg C X /\ ~(C = X) [H1'] by H1, SegmentOrdering_DEF, B1';
2916 u === seg C X by H1, -, SEGMENT, C2Transitive;
2917 qed by H1, H1', -, SegmentOrdering_DEF;
2920 let EuclidPropositionI_24Help = thm `;
2921 let O A C O' D F be point;
2922 assume ~Collinear A O C /\ ~Collinear D O' F [H1];
2923 assume seg O' D === seg O A /\ seg O' F === seg O C [H2];
2924 assume angle D O' F <_ang angle A O C [H3];
2925 assume seg O A <__ seg O C \/ seg O A === seg O C [H4];
2926 thus seg D F <__ seg A C
2929 consider K such that
2930 K IN int_angle A O C /\ angle D O' F === angle A O K [KintAOC] by H1, ANGLE, H3, AngleOrderingUse;
2931 ~(O = C) /\ ~(D = F) /\ ~(O' = F) /\ ~(O = K) [Distinct] by H1, NonCollinearImpliesDistinct, -, InteriorEZHelp;
2932 consider B such that
2933 B IN ray O K DELETE O /\ seg O B === seg O C [BrOK] by Distinct, SEGMENT, -, C1;
2934 ray O B = ray O K by Distinct, -, RayWellDefined;
2935 angle D O' F === angle A O B [DO'FeqAOB] by KintAOC, -, Angle_DEF;
2936 B IN int_angle A O C [BintAOC] by KintAOC, BrOK, WholeRayInterior;
2937 ~(B = O) /\ ~Collinear A O B [AOBncol] by -, InteriorEZHelp;
2938 seg O C === seg O B [OCeqOB] by Distinct, -, SEGMENT, BrOK, C2Symmetric;
2939 seg O' F === seg O B by Distinct, SEGMENT, AOBncol, H2, -, C2Transitive;
2940 D,O',F cong A,O,B by H1, AOBncol, H2, -, DO'FeqAOB, SAS;
2941 seg D F === seg A B [DFeqAB] by -, TriangleCong_DEF;
2942 consider G such that
2943 G IN open (A,C) /\ G IN ray O B DELETE O /\ ~(G = O) [AGC] by BintAOC, Crossbar_THM, B1', IN_DELETE;
2944 Segment (seg O G) /\ ~(O = B) [notOB] by AGC, SEGMENT, BrOK, IN_DELETE;
2945 seg O G <__ seg O C by H1, AGC, H4, InteriorCircleConvexHelp;
2946 seg O G <__ seg O B by -, OCeqOB, BrOK, IN_DELETE, SEGMENT, SegmentTrichotomy2;
2947 consider G' such that
2948 G' IN open (O,B) /\ seg O G === seg O G' [OG'B] by notOB, -, SegmentOrderingUse;
2949 ~(G' = O) /\ seg O G' === seg O G' /\ Segment (seg O G') [notG'O] by -, B1', SEGMENT, C2Reflexive, SEGMENT;
2950 G' IN ray O B DELETE O by OG'B, IntervalRayEZ;
2951 G' = G /\ G IN open (B,O) by notG'O, notOB, -, AGC, OG'B, C1, B1';
2952 ConvexQuadrilateral B A O C by H1, -, AGC, DiagonalsIntersectImpliesConvexQuad;
2953 A IN int_angle O C B /\ O IN int_angle C B A /\ Quadrilateral B A O C [OintCBA] by -, ConvexQuad_DEF;
2954 A IN int_angle B C O [AintBCO] by -, InteriorAngleSymmetry;
2955 Tetralateral B A O C by OintCBA, Quadrilateral_DEF;
2956 ~Collinear C B A /\ ~Collinear B C O /\ ~Collinear C O B /\ ~Collinear C B O [BCOncol] by -, Tetralateral_DEF, CollinearSymmetry;
2957 angle B C O === angle C B O [BCOeqCBO] by -, OCeqOB, IsoscelesCongBaseAngles;
2958 ~Collinear B C A /\ ~Collinear A C B [ACBncol] by AintBCO, InteriorEZHelp, CollinearSymmetry;
2959 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;
2960 angle B C A <_ang angle B C O by -, BCOncol, ANGLE, AintBCO, AngleOrdering_DEF;
2961 angle B C A <_ang angle C B O [BCAlessCBO] by -, BCOncol, ANGLE, BCOeqCBO, AngleTrichotomy2;
2962 angle C B O <_ang angle C B A by BCOncol, ANGLE, OintCBA, CBOref, AngleOrdering_DEF;
2963 angle A C B <_ang angle C B A by BCAlessCBO, -, AngleOrderTransitivity, AngleSymmetry;
2964 seg A B <__ seg A C by ACBncol, -, EuclidPropositionI_19;
2965 qed by -, Distinct, SEGMENT, DFeqAB, SegmentTrichotomy3;
2968 let EuclidPropositionI_24 = thm `;
2969 let O A C O' D F be point;
2970 assume ~Collinear A O C /\ ~Collinear D O' F [H1];
2971 assume seg O' D === seg O A /\ seg O' F === seg O C [H2];
2972 assume angle D O' F <_ang angle A O C [H3];
2973 thus seg D F <__ seg A C
2976 ~(O = A) /\ ~(O = C) /\ ~Collinear C O A /\ ~Collinear F O' D [Distinct] by H1, NonCollinearImpliesDistinct, CollinearSymmetry;
2977 seg O A === seg O C \/ seg O A <__ seg O C \/ seg O C <__ seg O A by -, SEGMENT, SegmentTrichotomy;
2979 suppose seg O A <__ seg O C \/ seg O A === seg O C;
2980 qed by H1, H2, H3, -, EuclidPropositionI_24Help;
2981 suppose seg O C <__ seg O A [H4];
2982 angle F O' D <_ang angle C O A by H3, AngleSymmetry;
2983 qed by Distinct, H3, AngleSymmetry, H2, H4, EuclidPropositionI_24Help, SegmentSymmetry;
2987 let EuclidPropositionI_25 = thm `;
2988 let O A C O' D F be point;
2989 assume ~Collinear A O C /\ ~Collinear D O' F [H1];
2990 assume seg O' D === seg O A /\ seg O' F === seg O C [H2];
2991 assume seg D F <__ seg A C [H3];
2992 thus angle D O' F <_ang angle A O C
2995 ~(O = A) /\ ~(O = C) /\ ~(A = C) /\ ~(D = F) /\ ~(O' = D) /\ ~(O' = F) [Distinct] by H1, NonCollinearImpliesDistinct;
2996 assume ~(angle D O' F <_ang angle A O C);
2997 angle D O' F === angle A O C \/ angle A O C <_ang angle D O' F by H1, ANGLE, -, AngleTrichotomy;
2999 suppose angle D O' F === angle A O C;
3000 D,O',F cong A,O,C by H1, H2, -, SAS;
3001 seg D F === seg A C by -, TriangleCong_DEF;
3002 qed by Distinct, SEGMENT, -, H3, SegmentTrichotomy;
3003 suppose angle A O C <_ang angle D O' F [Con];
3004 seg O A === seg O' D /\ seg O C === seg O' F [H2'] by Distinct, SEGMENT, H2, C2Symmetric;
3005 seg A C <__ seg D F by H1, -, Con, EuclidPropositionI_24;
3006 qed by Distinct, SEGMENT, -, H3, SegmentTrichotomy;
3011 let A B C A' B' C' be point;
3012 assume ~Collinear A B C /\ ~Collinear A' B' C' [H1];
3013 assume angle A B C === angle A' B' C' /\ angle B C A === angle B' C' A' [H2];
3014 assume seg A B === seg A' B' [H3];
3015 thus A,B,C cong A',B',C'
3018 ~(A = B) /\ ~(B = C) /\ ~(B' = C') [Distinct] by H1, NonCollinearImpliesDistinct;
3019 consider G such that
3020 G IN ray B C DELETE B /\ seg B G === seg B' C' [Gexists] by Distinct, SEGMENT, C1;
3021 ~(G = B) /\ B NOTIN open (G,C) /\ Collinear G B C [notGBC] by -, IN_DELETE, IN_Ray, CollinearSymmetry;
3022 ~Collinear A B G /\ ~Collinear B G A [ABGncol] by H1, notGBC, CollinearSymmetry, NoncollinearityExtendsToLine;
3023 ray B G = ray B C by Distinct, Gexists, RayWellDefined;
3024 angle A B G = angle A B C by Distinct, -, Angle_DEF;
3025 A,B,G cong A',B',C' [ABGcongA'B'C'] by H1, ABGncol, H3, SegmentSymmetry, H2, -, Gexists, SAS;
3026 angle B G A === angle B' C' A' [BGAeqB'C'A'] by -, TriangleCong_DEF;
3027 ~Collinear B C A /\ ~Collinear B' C' A' [BCAncol] by H1, CollinearSymmetry;
3028 angle B' C' A' === angle B C A /\ angle B C A === angle B C A [BCArefl] by -, ANGLE, H2, C5Symmetric, C5Reflexive;
3029 angle B G A === angle B C A [BGAeqBCA] by ABGncol, BCAncol, ANGLE, BGAeqB'C'A', -, C5Transitive;
3032 qed by -, ABGcongA'B'C';
3033 suppose ~(G = C) [notGC];
3034 ~Collinear A C G /\ ~Collinear A G C [ACGncol] by H1, notGBC, -, CollinearSymmetry, NoncollinearityExtendsToLine;
3035 C IN open (B,G) \/ G IN open (C,B) by notGBC, notGC, Distinct, B3', NOTIN;
3037 suppose C IN open (B,G) ;
3038 C IN open (G,B) /\ ray G C = ray G B [rGCrBG] by -, B1', IntervalRay;
3039 angle A G C <_ang angle A C B by ACGncol, -, ExteriorAngle;
3040 angle B G A <_ang angle B C A by -, rGCrBG, Angle_DEF, AngleSymmetry, AngleSymmetry;
3041 qed by ABGncol, BCAncol, ANGLE, -, AngleSymmetry, BGAeqBCA, AngleTrichotomy;
3042 suppose G IN open (C,B) [CGB];
3043 ray C G = ray C B /\ angle A C G <_ang angle A G B by -, IntervalRay, ACGncol, ExteriorAngle;
3044 angle A C B <_ang angle B G A by -, Angle_DEF, AngleSymmetry;
3045 angle B C A <_ang angle B C A by -, BCAncol, ANGLE, BGAeqBCA, AngleTrichotomy2, AngleSymmetry;
3046 qed by -, BCArefl, AngleTrichotomy1;
3051 let ParallelSymmetry = thm `;
3052 ! l k: point_set. l parallel k ==> k parallel l
3053 by PARALLEL, INTER_COMM;
3056 let AlternateInteriorAngles = thm `;
3057 let A B C E be point;
3058 let l m t be point_set;
3059 assume Line l /\ A IN l /\ E IN l [l_line];
3060 assume Line m /\ B IN m /\ C IN m [m_line];
3061 assume Line t /\ A IN t /\ B IN t [t_line];
3062 assume ~(A = E) /\ ~(B = C) /\ ~(A = B) /\ E NOTIN t /\ C NOTIN t [Distinct];
3063 assume ~(C,E same_side t) [Cnsim_tE];
3064 assume angle E A B === angle C B A [AltIntAngCong];
3068 ~Collinear E A B /\ ~Collinear C B A [EABncol] by t_line, Distinct, I1, Collinear_DEF, NOTIN;
3069 B NOTIN l /\ A NOTIN m [notAmBl] by l_line, m_line, Collinear_DEF, -, NOTIN;
3070 assume ~(l parallel m);
3071 ~(l INTER m = {}) by -, l_line, m_line, PARALLEL;
3072 consider G such that
3073 G IN l /\ G IN m [Glm] by -, MEMBER_NOT_EMPTY, IN_INTER;
3074 ~(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;
3075 ~Collinear A G B /\ ~Collinear B G A /\ G NOTIN t [AGBncol] by EABncol, CollinearSymmetry, -, NoncollinearityExtendsToLine, t_line, Collinear_DEF, NOTIN;
3076 ~(E,C same_side t) [Ensim_tC] by t_line, -, Distinct, Cnsim_tE, SameSideSymmetric;
3077 C IN m DELETE B /\ G IN m DELETE B [CGm_B] by m_line, Glm, Distinct, GnotAB, IN_DELETE;
3078 E IN l DELETE A /\ G IN l DELETE A [EGm_A] by l_line, Glm, Distinct, GnotAB, IN_DELETE;
3081 assume G,E same_side t [Gsim_tE];
3082 A NOTIN open (G,E) [notGAE] by t_line, -, SameSide_DEF, NOTIN;
3083 G IN ray A E DELETE A by Distinct, GnotAB, notGAE, IN_Ray, GnotAB, IN_DELETE;
3084 ray A G = ray A E [rAGrAE] by Distinct, -, RayWellDefined;
3085 ~(C,G same_side t) by t_line, AGBncol, Distinct, Gsim_tE, Cnsim_tE, SameSideTransitive;
3086 C NOTIN ray B G /\ B IN open (C,G) by t_line, AGBncol, Distinct, -, RaySameSide, NOTIN, GnotAB, IN_DELETE, IN_Ray;
3087 angle G A B <_ang angle C B A by AGBncol, -, B1', EuclidPropositionI_16;
3088 angle E A B <_ang angle C B A by -, rAGrAE, Angle_DEF;
3089 qed by EABncol, ANGLE, AltIntAngCong, -, AngleTrichotomy1;
3090 G,C same_side t [Gsim_tC] by t_line, AGBncol, Distinct, -, Cnsim_tE, AtMost2Sides;
3091 :: now we make a symmetric argument
3092 B NOTIN open (G,C) [notGBC] by t_line, -, SameSide_DEF, NOTIN;
3093 G IN ray B C DELETE B by Distinct, GnotAB, notGBC, IN_Ray, GnotAB, IN_DELETE;
3094 ray B G = ray B C [rBGrBC] by Distinct, -, RayWellDefined;
3095 angle C B A === angle E A B [flipAltIntAngCong] by EABncol, ANGLE, AltIntAngCong, C5Symmetric;
3096 ~(E,G same_side t) by t_line, AGBncol, Distinct, Gsim_tC, Ensim_tC, SameSideTransitive;
3097 E NOTIN ray A G /\ A IN open (E,G) by t_line, AGBncol, Distinct, -, RaySameSide, NOTIN, GnotAB, IN_Ray, IN_DELETE;
3098 angle G B A <_ang angle E A B by AGBncol, -, B1', EuclidPropositionI_16;
3099 angle C B A <_ang angle E A B by -, rBGrBC, Angle_DEF;
3100 qed by EABncol, ANGLE, flipAltIntAngCong, -, AngleTrichotomy1;
3103 let EuclidPropositionI_28 = thm `;
3104 let A B C D E F G H be point;
3105 let l m t be point_set;
3106 assume Line l /\ A IN l /\ B IN l /\ G IN l [l_line];
3107 assume Line m /\ C IN m /\ D IN m /\ H IN m [m_line];
3108 assume Line t /\ G IN t /\ H IN t [t_line];
3109 assume G NOTIN m /\ H NOTIN l [notGmHl];
3110 assume G IN open (A,B) /\ H IN open (C,D) [H1];
3111 assume G IN open (E,H) /\ H IN open (F,G) [H2];
3112 assume ~(D,A same_side t) [H3];
3113 assume angle E G B === angle G H D \/ angle B G H suppl angle G H D [H4];
3117 ~(A = G) /\ ~(G = B) /\ ~(H = D) /\ ~(E = G) /\ ~(G = H) /\ Collinear A G B /\ Collinear E G H [Distinct] by H1, H2, B1';
3118 ~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;
3119 ~Collinear B G H /\ ~Collinear A G E /\ ~Collinear E G B [BGHncol] by -, Distinct, CollinearSymmetry, NoncollinearityExtendsToLine;
3120 angle A G H === angle D H G
3123 suppose angle E G B === angle G H D [EGBeqGHD];
3124 angle E G B === angle H G A by BGHncol, H1, H2, VerticalAnglesCong;
3125 angle H G A === angle E G B by BGHncol, HGAncol, ANGLE, -, C5Symmetric;
3126 angle H G A === angle G H D by BGHncol, HGAncol, ANGLE, -, EGBeqGHD, C5Transitive;
3127 qed by -, AngleSymmetry;
3128 suppose angle B G H suppl angle G H D [BGHeqGHD];
3129 angle B G H suppl angle H G A by BGHncol, H1, B1', SupplementaryAngles_DEF;
3130 qed by -, BGHeqGHD, AngleSymmetry, SupplementUnique, AngleSymmetry;
3132 qed by l_line, m_line, t_line, Distinct, HGAncol, H3, -, AlternateInteriorAngles;
3135 let OppositeSidesCongImpliesParallelogram = thm `;
3136 let A B C D be point;
3137 assume Quadrilateral A B C D [H1];
3138 assume seg A B === seg C D /\ seg B C === seg D A [H2];
3139 thus Parallelogram A B C D
3142 ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) /\
3143 ~Collinear A B C /\ ~Collinear B C D /\ ~Collinear C D A /\ ~Collinear D A B [TetraABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
3144 consider a c such that
3145 Line a /\ A IN a /\ B IN a /\
3146 Line c /\ C IN c /\ D IN c [ac_line] by TetraABCD, I1;
3147 consider b d such that
3148 Line b /\ B IN b /\ C IN b /\
3149 Line d /\ D IN d /\ A IN d [bd_line] by TetraABCD, I1;
3150 consider l such that
3151 Line l /\ A IN l /\ C IN l [l_line] by TetraABCD, I1;
3152 consider m such that
3153 Line m /\ B IN m /\ D IN m [m_line] by TetraABCD, I1;
3154 B NOTIN l /\ D NOTIN l /\ A NOTIN m /\ C NOTIN m [notBDlACm] by l_line, m_line, TetraABCD, Collinear_DEF, NOTIN;
3155 seg A C === seg C A /\ seg B D === seg D B [seg_refl] by TetraABCD, SEGMENT, C2Reflexive, SegmentSymmetry;
3156 A,B,C cong C,D,A by TetraABCD, H2, -, SSS;
3157 angle B C A === angle D A C /\ angle C A B === angle A C D [BCAeqDAC] by -, TriangleCong_DEF;
3158 seg C D === seg A B [CDeqAB] by TetraABCD, SEGMENT, H2, C2Symmetric;
3159 B,C,D cong D,A,B by TetraABCD, H2, -, seg_refl, SSS;
3160 angle C D B === angle A B D /\ angle D B C === angle B D A [CDBeqABD] by -, TriangleCong_DEF;
3161 ~(B,D same_side l) \/ ~(A,C same_side m) by H1, l_line, m_line, FiveChoicesQuadrilateral;
3163 suppose ~(B,D same_side l);
3164 ~(D,B same_side l) by l_line, notBDlACm, -, SameSideSymmetric;
3165 a parallel c /\ b parallel d by ac_line, l_line, TetraABCD, notBDlACm, -, BCAeqDAC, AngleSymmetry, AlternateInteriorAngles, bd_line, BCAeqDAC;
3166 qed by H1, ac_line, bd_line, -, Parallelogram_DEF;
3167 suppose ~(A,C same_side m);
3168 b parallel d /\ c parallel a by bd_line, m_line, TetraABCD, notBDlACm, -, CDBeqABD, AngleSymmetry, AlternateInteriorAngles, ac_line, CDBeqABD;
3169 qed by H1, ac_line, bd_line, -, ParallelSymmetry, Parallelogram_DEF;
3173 let OppositeAnglesCongImpliesParallelogramHelp = thm `;
3174 let A B C D be point;
3175 let a c be point_set;
3176 assume Quadrilateral A B C D [H1];
3177 assume angle A B C === angle C D A /\ angle D A B === angle B C D [H2];
3178 assume Line a /\ A IN a /\ B IN a [a_line];
3179 assume Line c /\ C IN c /\ D IN c [c_line];
3183 ~(A = B) /\ ~(A = C) /\ ~(A = D) /\ ~(B = C) /\ ~(B = D) /\ ~(C = D) /\
3184 ~Collinear A B C /\ ~Collinear B C D /\ ~Collinear C D A /\ ~Collinear D A B [TetraABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
3185 angle C D A === angle A B C /\ angle B C D === angle D A B [H2'] by TetraABCD, ANGLE, H2, C5Symmetric;
3186 consider l m such that
3187 Line l /\ A IN l /\ C IN l /\
3188 Line m /\ B IN m /\ D IN m [lm_line] by TetraABCD, I1;
3189 consider b d such that
3190 Line b /\ B IN b /\ C IN b /\ Line d /\ D IN d /\ A IN d [bd_line] by TetraABCD, I1;
3191 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;
3192 ~(A IN int_triangle B C D \/ B IN int_triangle C D A \/
3193 C IN int_triangle D A B \/ D IN int_triangle A B C)
3195 assume A IN int_triangle B C D \/ B IN int_triangle C D A \/
3196 C IN int_triangle D A B \/ D IN int_triangle A B C;
3197 angle B C D <_ang angle D A B \/ angle C D A <_ang angle A B C \/
3198 angle D A B <_ang angle B C D \/ angle A B C <_ang angle C D A by TetraABCD, -, EuclidPropositionI_21;
3199 qed by -, H2', H2, AngleTrichotomy1;
3200 ConvexQuadrilateral A B C D by H1, lm_line, -, FiveChoicesQuadrilateral;
3201 A IN int_angle B C D /\ B IN int_angle C D A /\
3202 C IN int_angle D A B /\ D IN int_angle A B C [AintBCD] by -, ConvexQuad_DEF;
3203 B,A same_side c /\ B,C same_side d [Bsim_cA] by c_line, bd_line, -, InteriorUse;
3204 A,D same_side b [Asim_bD] by bd_line, c_line, AintBCD, InteriorUse;
3205 assume ~(a parallel c);
3206 consider G such that
3207 G IN a /\ G IN c [Gac] by -, a_line, c_line, PARALLEL, MEMBER_NOT_EMPTY, IN_INTER;
3208 Collinear A B G /\ Collinear D G C /\ Collinear C G D [ABGcol] by a_line, -, Collinear_DEF, c_line;
3209 ~(G = A) /\ ~(G = B) /\ ~(G = C) /\ ~(G = D) [GnotABCD] by Gac, ABGcol, TetraABCD, CollinearSymmetry, Collinear_DEF;
3210 ~Collinear B G C /\ ~Collinear A D G [BGCncol] by c_line, Gac, GnotABCD, I1, Collinear_DEF, point_off_line, NOTIN;
3211 ~Collinear B C G /\ ~Collinear G B C /\ ~Collinear G A D /\ ~Collinear A G D [BCGncol] by -, CollinearSymmetry;
3212 G NOTIN b /\ G NOTIN d [notGb] by bd_line, Collinear_DEF, BGCncol, NOTIN;
3213 G NOTIN open (B,A) [notBGA] by Bsim_cA, Gac, SameSide_DEF, NOTIN;
3214 B NOTIN open (A,G) [notABG]
3216 assume ~(B NOTIN open (A,G));
3217 B IN open (A,G) [ABG] by -, NOTIN;
3218 ray A B = ray A G [rABrAG] by -, IntervalRay;
3219 ~(A,G same_side b) by bd_line, ABG, SameSide_DEF;
3220 ~(D,G same_side b) by bd_line, point_off_line, notGb, Asim_bD, -, SameSideTransitive;
3221 D NOTIN ray C G by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, NOTIN;
3222 C IN open (D,G) [DCG] by GnotABCD, ABGcol, -, IN_Ray, NOTIN;
3223 consider M such that
3224 D IN open (C,M) [CDM] by TetraABCD, B2';
3225 D IN open (G,M) [GDM] by -, B1', DCG, TransitivityBetweennessHelp;
3226 angle C D A suppl angle A D M /\ angle A B C suppl angle C B G by TetraABCD, CDM, ABG, SupplementaryAngles_DEF;
3227 angle M D A === angle G B C [MDAeqGBC] by -, H2', SupplementsCongAnglesCong, AngleSymmetry;
3228 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;
3229 angle G A D <_ang angle D C B by -, BCGncol, ANGLE, MDAeqGBC, AngleTrichotomy2, AngleOrderTransitivity;
3230 angle D A B <_ang angle B C D by -, rABrAG, Angle_DEF, AngleSymmetry;
3231 qed by -, H2, AngleTrichotomy1;
3234 assume ~(A NOTIN open (G,B));
3235 A IN open (B,G) [BAG] by -, B1', NOTIN;
3236 ray B A = ray B G [rBArBG] by -, IntervalRay;
3237 ~(B,G same_side d) by bd_line, BAG, SameSide_DEF;
3238 ~(C,G same_side d) by bd_line, point_off_line, notGb, Bsim_cA, -, SameSideTransitive;
3239 C NOTIN ray D G by bd_line, notGb, -, RaySameSide, TetraABCD, IN_DELETE, NOTIN;
3240 D IN open (C,G) [CDG] by GnotABCD, ABGcol, -, IN_Ray, NOTIN;
3241 consider M such that
3242 C IN open (D,M) [DCM] by B2', TetraABCD;
3243 C IN open (G,M) [GCM] by -, B1', CDG, TransitivityBetweennessHelp;
3244 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;
3245 angle M C B === angle G A D [GADeqMCB] by -, H2', SupplementsCongAnglesCong;
3246 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;
3247 angle G B C <_ang angle C D A by -, BCGncol, ANGLE, GADeqMCB, AngleTrichotomy2, AngleOrderTransitivity;
3248 angle A B C <_ang angle C D A by -, rBArBG, Angle_DEF;
3249 qed by -, H2, AngleTrichotomy1;
3250 qed by TetraABCD, GnotABCD, ABGcol, notABG, notBGA, -, B3', NOTIN;
3253 let OppositeAnglesCongImpliesParallelogram = thm `;
3254 let A B C D be point;
3255 assume Quadrilateral A B C D [H1];
3256 assume angle A B C === angle C D A /\ angle D A B === angle B C D [H2];
3257 thus Parallelogram A B C D
3260 Quadrilateral B C D A [QuadBCDA] by H1, QuadrilateralSymmetry;
3261 ~(A = B) /\ ~(B = C) /\ ~(C = D) /\ ~(D = A) /\ ~Collinear B C D /\ ~Collinear D A B [TetraABCD] by H1, Quadrilateral_DEF, Tetralateral_DEF;
3262 angle B C D === angle D A B [H2'] by TetraABCD, ANGLE, H2, C5Symmetric;
3263 consider a such that
3264 Line a /\ A IN a /\ B IN a [a_line] by TetraABCD, I1;
3265 consider b such that
3266 Line b /\ B IN b /\ C IN b [b_line] by TetraABCD, I1;
3267 consider c such that
3268 Line c /\ C IN c /\ D IN c [c_line] by TetraABCD, I1;
3269 consider d such that
3270 Line d /\ D IN d /\ A IN d [d_line] by TetraABCD, I1;
3271 qed by H1, QuadBCDA, H2, H2', a_line, b_line, c_line, d_line, OppositeAnglesCongImpliesParallelogramHelp, Parallelogram_DEF;
3276 `! P l. Line l /\ P NOTIN l ==> ?! m. Line m /\ P IN m /\ m parallel l`;;
3278 new_constant("mu",`:point_set->real`);;
3281 `! alpha. Angle alpha ==> &0 < mu alpha /\ mu alpha < &180`;;
3284 `! alpha. Right alpha ==> mu alpha = &90`;;
3287 `! alpha beta. Angle alpha /\ Angle beta /\ alpha === beta ==> mu alpha = mu beta`;;
3290 `! 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)`;;
3293 let ConverseAlternateInteriorAngles = thm `;
3294 let A B C E be point;
3295 let l m t be point_set;
3296 assume Line l /\ A IN l /\ E IN l [l_line];
3297 assume Line m /\ B IN m /\ C IN m [m_line];
3298 assume Line t /\ A IN t /\ B IN t [t_line];
3299 assume ~(A = E) /\ ~(B = C) /\ ~(A = B) /\ E NOTIN t /\ C NOTIN t [Distinct];
3300 assume ~(C,E same_side t) [Cnsim_tE];
3301 assume l parallel m [para_lm];
3302 thus angle E A B === angle C B A
3305 ~Collinear C B A by t_line, Distinct, I1, Collinear_DEF, NOTIN, ANGLE;
3306 A NOTIN m /\ Angle (angle C B A) [notAm] by m_line, -, Collinear_DEF, NOTIN, ANGLE;
3307 consider D such that
3308 ~(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;
3309 consider k such that
3310 Line k /\ A IN k /\ D IN k [k_line] by Distinct, I1;
3311 k parallel m by -, m_line, t_line, Dexists, Distinct, AngleSymmetry, AlternateInteriorAngles;
3312 k = l by m_line, notAm, l_line, k_line, -, para_lm, P;
3313 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;
3314 ray A D = ray A E by Distinct, -, IN_Ray, Dexists, IN_DELETE, RayWellDefined;
3315 qed by -, Dexists, AngleSymmetry, Angle_DEF;
3318 let HilbertTriangleSum = thm `;
3320 assume ~Collinear A B C [ABCncol];
3321 thus ? E F. B IN open (E,F) /\ C IN int_angle A B F /\
3322 angle E B A === angle C A B /\ angle C B F === angle B C A
3325 ~(A = B) /\ ~(A = C) /\ ~(B = C) /\ ~Collinear C A B [Distinct] by ABCncol, NonCollinearImpliesDistinct, CollinearSymmetry;
3326 consider l such that
3327 Line l /\ A IN l /\ C IN l [l_line] by Distinct, I1;
3328 consider x such that
3329 Line x /\ A IN x /\ B IN x [x_line] by Distinct, I1;
3330 consider y such that
3331 Line y /\ B IN y /\ C IN y [y_line] by Distinct, I1;
3332 C NOTIN x [notCx] by x_line, ABCncol, Collinear_DEF, NOTIN;
3333 Angle (angle C A B) by ABCncol, CollinearSymmetry, ANGLE;
3334 consider E such that
3335 ~(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;
3336 consider m such that
3337 Line m /\ B IN m /\ E IN m [m_line] by -, I1, IN_DELETE;
3338 angle E B A === angle C A B [EBAeqCAB] by Eexists, AngleSymmetry;
3339 m parallel l [para_lm] by m_line, l_line, x_line, Eexists, Distinct, notCx, -, AlternateInteriorAngles;
3340 m INTER l = {} [lm0] by -, PARALLEL;
3341 C NOTIN m /\ A NOTIN m [notACm] by -, l_line, INTER_COMM, DisjointOneNotOther;
3342 consider F such that
3343 B IN open (E,F) [EBF] by Eexists, B2';
3344 ~(B = F) /\ F IN m [EBF'] by -, B1', m_line, BetweenLinear;
3345 ~Collinear A B F /\ F NOTIN x [ABFncol] by m_line, -, I1, Collinear_DEF, notACm, NOTIN, x_line;
3346 ~(E,F same_side x) /\ ~(E,F same_side y) [Ensim_yF] by EBF, x_line, y_line, SameSide_DEF;
3347 C,F same_side x [Csim_xF] by x_line, notCx, Eexists, ABFncol, Eexists, -, AtMost2Sides;
3348 m INTER open(C,A) = {} by l_line, BetweenLinear, SUBSET, SET_RULE, lm0, SUBSET_EMPTY;
3349 C,A same_side m by m_line, -, SameSide_DEF, SET_RULE;
3350 C IN int_angle A B F [CintABF] by ABFncol, x_line, m_line, EBF', notCx, notACm, Csim_xF, -, IN_InteriorAngle;
3351 A IN int_angle C B E by EBF, B1', -, InteriorAngleSymmetry, InteriorReflectionInterior;
3352 A NOTIN y /\ A,E same_side y [Asim_yE] by y_line, m_line, -, InteriorUse;
3353 E NOTIN y /\ F NOTIN y [notEFy] by y_line, m_line, EBF', Eexists, EBF', I1, Collinear_DEF, notACm, NOTIN;
3354 E,A same_side y by y_line, -, Asim_yE, SameSideSymmetric;
3355 ~(A,F same_side y) [Ansim_yF] by y_line, notEFy, Asim_yE, -, Ensim_yF, SameSideTransitive;
3356 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;
3357 qed by EBF, CintABF, EBAeqCAB, -, AngleSymmetry;
3360 let EuclidPropositionI_13 = thm `;
3361 let A O B A' be point;
3362 assume ~Collinear A O B [H1];
3363 assume O IN open (A,A') [H2];
3364 thus mu (angle A O B) + mu (angle B O A') = &180
3368 suppose Right (angle A O B);
3369 Right (angle B O A') /\ mu (angle A O B) = &90 /\ mu (angle B O A') = &90 by H1, H2, -, RightImpliesSupplRight, AMb;
3370 qed by -, REAL_ARITH;
3371 suppose ~Right (angle A O B) [notRightAOB];
3372 ~(A = O) /\ ~(O = B) [Distinct] by H1, NonCollinearImpliesDistinct;
3373 consider l such that
3374 Line l /\ O IN l /\ A IN l /\ A' IN l [l_line] by -, I1, H2, BetweenLinear;
3375 B NOTIN l [notBl] by -, Distinct, I1, Collinear_DEF, H1, NOTIN;
3376 consider F such that
3377 Right (angle O A F) /\ Angle (angle O A F) [RightOAF] by Distinct, EuclidPropositionI_11, RightImpliesAngle;
3378 ?! 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;
3379 consider E such that
3380 ~(O = E) /\ E NOTIN l /\ E,B same_side l /\ angle A O E === angle O A F [Eexists] by -;
3381 ~Collinear A O E [AOEncol] by l_line, Distinct, I1, Collinear_DEF, -, NOTIN;
3382 Right (angle A O E) [RightAOE] by -, ANGLE, RightOAF, Eexists, CongRightImpliesRight;
3383 Right (angle E O A') /\ mu (angle A O E) = &90 /\ mu (angle E O A') = &90 [RightEOA'] by AOEncol, H2, -, RightImpliesSupplRight, AMb;
3384 ~(angle A O B === angle A O E) by notRightAOB, H1, ANGLE, RightAOE, CongRightImpliesRight;
3385 ~(angle A O B = angle A O E) by H1, AOEncol, ANGLE, -, C5Reflexive;
3386 ~(ray O B = ray O E) by -, Angle_DEF;
3387 B NOTIN ray O E /\ O NOTIN open (B,E) by Distinct, -, Eexists, RayWellDefined, IN_DELETE, NOTIN, l_line, B1', SameSide_DEF;
3388 ~Collinear O E B by -, Eexists, IN_Ray, NOTIN;
3389 E IN int_angle A O B \/ B IN int_angle A O E by Distinct, l_line, Eexists, notBl, AngleOrdering, -, CollinearSymmetry, InteriorAngleSymmetry;
3391 suppose E IN int_angle A O B [EintAOB];
3392 B IN int_angle E O A' by H2, -, InteriorReflectionInterior;
3393 mu (angle A O B) = mu (angle A O E) + mu (angle E O B) /\
3394 mu (angle E O A') = mu (angle E O B) + mu (angle B O A') by EintAOB, -, AMd;
3395 qed by -, RightEOA', REAL_ARITH;
3396 suppose B IN int_angle A O E [BintAOE];
3397 E IN int_angle B O A' by H2, -, InteriorReflectionInterior;
3398 mu (angle A O E) = mu (angle A O B) + mu (angle B O E) /\
3399 mu (angle B O A') = mu (angle B O E) + mu (angle E O A') by BintAOE, -, AMd;
3400 qed by -, RightEOA', REAL_ARITH;
3405 let TriangleSum = thm `;
3407 assume ~Collinear A B C [ABCncol];
3408 thus mu (angle A B C) + mu (angle B C A) + mu (angle C A B) = &180
3411 ~Collinear C A B /\ ~Collinear B C A [CABncol] by ABCncol, CollinearSymmetry;
3412 consider E F such that
3413 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;
3414 ~Collinear C B F /\ ~Collinear A B F /\ Collinear E B F /\ ~(B = E) [CBFncol] by -, InteriorAngleSymmetry, InteriorEZHelp, IN_InteriorAngle, B1', CollinearSymmetry;
3415 ~Collinear E B A [EBAncol] by CollinearSymmetry, -, NoncollinearityExtendsToLine;
3416 mu (angle A B F) = mu (angle A B C) + mu (angle C B F) [muCintABF] by EBF, AMd;
3417 mu (angle E B A) + mu (angle A B F) = &180 [suppl180] by EBAncol, EBF, EuclidPropositionI_13;
3418 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;
3419 qed by suppl180, muCintABF, -, REAL_ARITH;