---

Step * 1 1 1 1 1 of Lemma geo-add-length-cancel-left-le


1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. c : Point
7. O_X_c
8. p' : {p:Point| O_X_p} 
9. q' : {p:Point| O_X_p} 
10. p' = c + a ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
11. p' ∈ {p:Point| O_X_p} 
12. c + a ∈ {p:Point| O_X_p} 
13. p' ≡ c + a
14. q' = c + b ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
15. q' ∈ {p:Point| O_X_p} 
16. c + b ∈ {p:Point| O_X_p} 
17. q' ≡ c + b
18. c + a ∈ {p:Point| O_X_p} 
19. c + b ∈ {p:Point| O_X_p} 
⊢ X_c + a_c + b ⇒ (Ax ∈ a ≤ b)
BY
{ (Unfold `geo-add-length` 0 THEN GeneralizeGeoExtends [`z';`u']⋅) }

1
1. e : BasicGeometry
2. a : Point
3. O_X_a
4. b : Point
5. O_X_b
6. c : Point
7. O_X_c
8. p' : {p:Point| O_X_p} 
9. q' : {p:Point| O_X_p} 
10. p' = c + a ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
11. p' ∈ {p:Point| O_X_p} 
12. c + a ∈ {p:Point| O_X_p} 
13. p' ≡ c + a
14. q' = c + b ∈ pertype(λx,y. ((x ∈ {p:Point| O_X_p} ) ∧ (y ∈ {p:Point| O_X_p} ) ∧ x ≡ y))
15. q' ∈ {p:Point| O_X_p} 
16. c + b ∈ {p:Point| O_X_p} 
17. q' ≡ c + b
18. c + a ∈ {p:Point| O_X_p} 
19. c + b ∈ {p:Point| O_X_p} 
20. z : {x:Point| O_c_x ∧ cx ≅ Xa} 
21. cz ≅ Xa ∧ O_c_z
22. u : {x:Point| O_c_x ∧ cx ≅ Xb} 
23. cu ≅ Xb ∧ O_c_u
⊢ X_z_u ⇒ (Ax ∈ a ≤ b)

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  O\_X\_a
4.  b  :  Point
5.  O\_X\_b
6.  c  :  Point
7.  O\_X\_c
8.  p'  :  \{p:Point|  O\_X\_p\} 
9.  q'  :  \{p:Point|  O\_X\_p\} 
10.  p'  =  c  +  a
11.  p'  \mmember{}  \{p:Point|  O\_X\_p\} 
12.  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\} 
13.  p'  \mequiv{}  c  +  a
14.  q'  =  c  +  b
15.  q'  \mmember{}  \{p:Point|  O\_X\_p\} 
16.  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\} 
17.  q'  \mequiv{}  c  +  b
18.  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\} 
19.  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\} 
\mvdash{}  X\_c  +  a\_c  +  b  {}\mRightarrow{}  (Ax  \mmember{}  a  \mleq{}  b)


By

---

Latex:
(Unfold  `geo-add-length`  0  THEN  GeneralizeGeoExtends  [`z';`u']\mcdot{})

---

Home Index