---

Step * of Lemma Prop23-construction-lemma

∀e:EuclideanPlane. ∀p,q,r,a,a':Point.
  (p # qr ⇒ a ≠ a' ⇒ (∃b,c1,c2:Point. (((pq ≅ ab ∧ out(a a'b)) ∧ pr ≅ ac1 ∧ bc2 > bc1) ∧ qr ≅ bc2 ∧ ac1 > ac2)))
BY
{ ((Auto THEN (InstLemma `Euclid-Prop20_cycle` [⌜e⌝;⌜p⌝;⌜q⌝;⌜r⌝]⋅ THENA Auto))
   THEN (((gProperProlong ⌜a'⌝⌜a⌝`P'⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
         THEN (gProperProlong ⌜P⌝⌜a⌝`b'⌜p⌝⌜q⌝⋅ THENA Auto)
         THEN ExRepD)
   THEN (D 0 With ⌜b⌝  THENA Auto)
   THEN (Assert out(a a'b) BY
               (InstLemma `geo-out-iff-between1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜a'⌝;⌜P⌝]⋅ THEN EAuto 1))) }

1
1. e : EuclideanPlane
2. p : Point
3. q : Point
4. r : Point
5. a : Point
6. a' : Point
7. p # qr
8. a ≠ a'
9. |qr| < |qp| + |pr|
10. |pr| < |qp| + |qr|
11. |qp| < |pr| + |qr|
12. P : Point
13. a'-a-P
14. aP ≅ OX
15. b : Point
16. P-a-b
17. ab ≅ pq
18. out(a a'b)
⊢ ∃c1,c2:Point. (((pq ≅ ab ∧ out(a a'b)) ∧ pr ≅ ac1 ∧ bc2 > bc1) ∧ qr ≅ bc2 ∧ ac1 > ac2)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}p,q,r,a,a':Point.
    (p  \#  qr
    {}\mRightarrow{}  a  \mneq{}  a'
    {}\mRightarrow{}  (\mexists{}b,c1,c2:Point.  (((pq  \mcong{}  ab  \mwedge{}  out(a  a'b))  \mwedge{}  pr  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  qr  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)))


By

---

Latex:
((Auto  THEN  (InstLemma  `Euclid-Prop20\_cycle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (((gProperProlong  \mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`P'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
              THEN  (gProperProlong  \mkleeneopen{}P\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`b'\mkleeneopen{}p\mkleeneclose{}\mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  ExRepD)
  THEN  (D  0  With  \mkleeneopen{}b\mkleeneclose{}    THENA  Auto)
  THEN  (Assert  out(a  a'b)  BY
                          (InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)))

---

Home Index