---

Step * of Lemma geo-lt-add1_2

∀e:BasicGeometry. ∀p,q,r:{a:Point| O_X_a} .  (X ≠ p ⇒ X ≠ q ⇒ X ≠ r ⇒ p < q ⇒ p + r < q + r)
BY
{ ((Auto THEN ((Unfold `geo-lt` -1 THEN ExRepD) THEN Unfold `geo-lt` 0) THEN InstConcl [⌜a⌝;⌜b⌝]⋅ THEN Auto)
   THEN (((Unfold `geo-le` 11 THEN D 11) THEN Unhide THEN Auto) THEN ExRepD)
   THEN (gProperProlong ⌜X⌝⌜r⌝`p1'⌜⌜X⌝⌝⌜p'⌝⋅
         THENA (Auto
                THEN ((Assert X_p_p' BY Auto) THEN Auto)
                THEN (InstLemma `geo-le-iff-between-points` [⌜e⌝;⌜p⌝;⌜p'⌝]⋅ THEN Auto)
                THEN (D -2 THEN Auto)
                THEN RWO"-5" 0
                THEN Auto)
         )
   THEN (gProperProlong ⌜X⌝⌜r⌝`q1'⌜⌜X⌝⌝⌜q'⌝⋅ THENA Auto)
   THEN skip{(Unfold `geo-le` 0 THEN InstConcl [⌜p1⌝;⌜q1⌝]⋅)}) }

1
1. e : BasicGeometry
2. p : {a:Point| O_X_a} 
3. q : {a:Point| O_X_a} 
4. r : {a:Point| O_X_a} 
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. a : Point
9. b : Point
10. a ≠ b
11. p' : {p:Point| O_X_p} 
12. q' : {p:Point| O_X_p} 
13. p' = p + |ab| ∈ Length
14. q' = q ∈ Length
15. X_p'_q'
16. a ≠ b
17. p1 : Point
18. X-r-p1 ∧ rp1 ≅ Xp'
19. q1 : Point
20. X-r-q1 ∧ rq1 ≅ Xq'
⊢ p + r + |ab| ≤ q + r

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q,r:\{a:Point|  O\_X\_a\}  .    (X  \mneq{}  p  {}\mRightarrow{}  X  \mneq{}  q  {}\mRightarrow{}  X  \mneq{}  r  {}\mRightarrow{}  p  <  q  {}\mRightarrow{}  p  +  r  <  q  +  r)


By

---

Latex:
((Auto
    THEN  ((Unfold  `geo-lt`  -1  THEN  ExRepD)  THEN  Unfold  `geo-lt`  0)
    THEN  InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}
    THEN  Auto)
  THEN  (((Unfold  `geo-le`  11  THEN  D  11)  THEN  Unhide  THEN  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}X\mkleeneclose{}\mkleeneopen{}r\mkleeneclose{}`p1'\mkleeneopen{}\mkleeneopen{}X\mkleeneclose{}\mkleeneclose{}\mkleeneopen{}p'\mkleeneclose{}\mcdot{}
              THENA  (Auto
                            THEN  ((Assert  X\_p\_p'  BY  Auto)  THEN  Auto)
                            THEN  (InstLemma  `geo-le-iff-between-points`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  (D  -2  THEN  Auto)
                            THEN  RWO"-5"  0
                            THEN  Auto)
              )
  THEN  (gProperProlong  \mkleeneopen{}X\mkleeneclose{}\mkleeneopen{}r\mkleeneclose{}`q1'\mkleeneopen{}\mkleeneopen{}X\mkleeneclose{}\mkleeneclose{}\mkleeneopen{}q'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  skip\{(Unfold  `geo-le`  0  THEN  InstConcl  [\mkleeneopen{}p1\mkleeneclose{};\mkleeneopen{}q1\mkleeneclose{}]\mcdot{})\})

---

Home Index