---

Step * 1 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. 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'))
BY
{ ((Assert X # p' BY
          ((D 11 THEN (Unhide THENA Auto))
           THEN (InstLemma `geo-le-sep` [⌜e⌝;⌜a⌝;⌜b⌝;⌜X⌝;⌜p'⌝]⋅ THEN Auto)
           THEN Subst' |Xp'| = |a1a2| + |ab| ∈ Length 0
           THEN Auto))
   THEN (Assert X # q' BY
               Auto)
   ) }

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
17. X # p'
18. X # q'
⊢ ↓∃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.  a  :  Point
9.  b  :  Point
10.  a  \#  b
11.  p'  :  \{p:Point|  B(OXp)\} 
12.  q'  :  \{p:Point|  B(OXp)\} 
13.  p'  =  |a1a2|  +  |ab|
14.  q'  =  |b1b2|
15.  B(Xp'q')
16.  a  \#  b
\mvdash{}  \mdownarrow{}\mexists{}p',q':\{p:Point|  B(OXp)\}  .  ((p'  =  |a1a2|  +  |c1c2|  +  |ab|)  \mwedge{}  (q'  =  |b1b2|  +  |c1c2|)  \mwedge{}  B(Xp'q'))


By

---

Latex:
((Assert  X  \#  p'  BY
                ((D  11  THEN  (Unhide  THENA  Auto))
                  THEN  (InstLemma  `geo-le-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  Subst'  |Xp'|  =  |a1a2|  +  |ab|  0
                  THEN  Auto))
  THEN  (Assert  X  \#  q'  BY
                          Auto)
  )

---

Home Index