---

Step * 1 1 1 2 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
17. X # p'
18. X # q'
19. P : Point
20. B(Xp'P)
21. p'P ≅ c1c2
22. Q : Point
23. B(Xq'Q)
24. q'Q ≅ c1c2
25. P = |a1a2| + |c1c2| + |ab| ∈ Length
⊢ Q = |b1b2| + |c1c2| ∈ Length
BY
{ ((FLemma `geo-add-length-between` [-3] THEN Auto)
   THEN (Subst' |XQ| = Q ∈ Length -1 THEN Auto)
   THEN (Subst' |Xq'| = |b1b2| ∈ Length -1 THEN Auto)
   THEN (Subst' |q'Q| = |c1c2| ∈ Length -1 THEN Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

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
17.  X  \#  p'
18.  X  \#  q'
19.  P  :  Point
20.  B(Xp'P)
21.  p'P  \mcong{}  c1c2
22.  Q  :  Point
23.  B(Xq'Q)
24.  q'Q  \mcong{}  c1c2
25.  P  =  |a1a2|  +  |c1c2|  +  |ab|
\mvdash{}  Q  =  |b1b2|  +  |c1c2|


By

---

Latex:
((FLemma  `geo-add-length-between`  [-3]  THEN  Auto)
  THEN  (Subst'  |XQ|  =  Q  -1  THEN  Auto)
  THEN  (Subst'  |Xq'|  =  |b1b2|  -1  THEN  Auto)
  THEN  (Subst'  |q'Q|  =  |c1c2|  -1  THEN  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index