---

Step * of Lemma Euclid-Prop23_half-plane

No Annotations
∀e:EuclideanPlane. ∀a,b,x,y,z:Point.  (z # xy ⇒ a # b ⇒ (∃x',b':Point. (out(a bb') ∧ x' leftof ab' ∧ x'ab' ≅a zxy)))
BY
{ (Auto
   THEN (InstLemma `Euclid-Prop20_cycle` [⌜e⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THENA Auto)
   THEN ((InstLemma `Prop23-construction-lemma` [⌜e⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN ExRepD)
   THEN RenameVar `b1' (12)
   THEN (GenConclTerm ⌜CCL(a;c1;b1;c2)⌝⋅
         THENA (Auto THEN ((InstConcl [⌜c1⌝;⌜c2⌝]⋅ THEN EAuto 1) ORELSE (D 1 THEN Unhide THEN Auto)))
         )
   THEN InstConcl [⌜v⌝;⌜b1⌝]⋅
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. z # xy
8. a # b
9. |yz| < |yx| + |xz|
10. |xz| < |yx| + |yz|
11. |yx| < |xz| + |yz|
12. b1 : Point
13. c1 : Point
14. c2 : Point
15. xy ≅ ab1
16. out(a bb1)
17. xz ≅ ac1
18. b1c2 > b1c1
19. yz ≅ b1c2
20. ac1 > ac2
21. v : {u:Point| ac1 ≅ au ∧ b1c2 ≅ b1u ∧ u leftof ab1} 
22. CCL(a;c1;b1;c2) = v ∈ {u:Point| ac1 ≅ au ∧ b1c2 ≅ b1u ∧ u leftof ab1} 
23. out(a bb1)
24. v leftof ab1
⊢ vab1 ≅a zxy

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y,z:Point.
    (z  \#  xy  {}\mRightarrow{}  a  \#  b  {}\mRightarrow{}  (\mexists{}x',b':Point.  (out(a  bb')  \mwedge{}  x'  leftof  ab'  \mwedge{}  x'ab'  \mcong{}\msuba{}  zxy)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-Prop20\_cycle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `Prop23-construction-lemma`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  RenameVar  `b1'  (12)
  THEN  (GenConclTerm  \mkleeneopen{}CCL(a;c1;b1;c2)\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  ((InstConcl  [\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)  ORELSE  (D  1  THEN  Unhide  THEN  Auto)))
              )
  THEN  InstConcl  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index