---

Step * 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 ∈ Length
11. q' = c + b ∈ Length
12. X_p'_q'
⊢ Ax ∈ a ≤ b
BY
{ ((Assert c + a ∈ {p:Point| O_X_p}  BY
          (Unfold `geo-add-length` 0 THEN GeneralizeGeoExtends [`z'] THEN D -1 THEN MemTypeCD THEN Auto))
   THEN (Assert c + b ∈ {p:Point| O_X_p}  BY
               (Unfold `geo-add-length` 0 THEN GeneralizeGeoExtends [`z'] THEN D -1 THEN MemTypeCD THEN Auto))
   ) }

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 ∈ Length
11. q' = c + b ∈ Length
12. X_p'_q'
13. c + a ∈ {p:Point| O_X_p} 
14. c + b ∈ {p:Point| O_X_p} 
⊢ 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.  q'  =  c  +  b
12.  X\_p'\_q'
\mvdash{}  Ax  \mmember{}  a  \mleq{}  b


By

---

Latex:
((Assert  c  +  a  \mmember{}  \{p:Point|  O\_X\_p\}    BY
                (Unfold  `geo-add-length`  0
                  THEN  GeneralizeGeoExtends  [`z']
                  THEN  D  -1
                  THEN  MemTypeCD
                  THEN  Auto))
  THEN  (Assert  c  +  b  \mmember{}  \{p:Point|  O\_X\_p\}    BY
                          (Unfold  `geo-add-length`  0
                            THEN  GeneralizeGeoExtends  [`z']
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto))
  )

---

Home Index