---

Step * 1 of Lemma geo-lt-add1-iff2


1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2|
⊢ |a1a2| + |c1c2| < |b1b2| + |c1c2|
BY
{ ((Unfold `geo-lt` -1 THEN ExRepD)
   THEN Unfold `geo-le` -1
   THEN ((Unfold `geo-lt` 0 THEN ExRepD) THEN Unfold `geo-le` 0)
   THEN (InstConcl [⌜a⌝;⌜b⌝]⋅ THEN Auto)
   THEN ExRepD) }

1
1. e : BasicGeometry
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. a : Point
9. b : Point
10. a # b
11. p' : {p:Point| B(OXp)} 
12. q' : {p:Point| B(OXp)} 
13. p' = |a1a2| + |ab| ∈ Length
14. q' = |b1b2| ∈ Length
15. B(Xp'q')
16. a # b
⊢ ↓∃p',q':{p:Point| B(OXp)} . ((p' = |a1a2| + |c1c2| + |ab| ∈ Length) ∧ (q' = |b1b2| + |c1c2| ∈ Length) ∧ B(Xp'q'))

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  |a1a2|  <  |b1b2|
\mvdash{}  |a1a2|  +  |c1c2|  <  |b1b2|  +  |c1c2|


By

---

Latex:
((Unfold  `geo-lt`  -1  THEN  ExRepD)
  THEN  Unfold  `geo-le`  -1
  THEN  ((Unfold  `geo-lt`  0  THEN  ExRepD)  THEN  Unfold  `geo-le`  0)
  THEN  (InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ExRepD)

---

Home Index