---

Step * 1 of Lemma geo-add-length_functionality_wrt_le


1. e : BasicGeometry
2. x : Length
3. y : Length
4. x' : Length
5. y' : Length
6. y ≤ y'
7. x ≤ x'
⊢ Ax ∈ x + y ≤ x' + y'
BY
{ ((D 2 THEN (GenConcl ⌜x = a ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto) THEN Fold `member` 0)
   THEN ThinVar `x1'
   THEN (Assert a ≤ x' BY
               (RWO "-1<" 0 THEN Auto))
   THEN ThinVar `x'
   THEN (D 2 THEN (GenConcl ⌜y = b ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto) THEN Fold `member` 0)
   THEN ThinVar `y1'
   THEN (Assert b ≤ y' BY
               (RWO "-1<" 0 THEN Auto))
   THEN ThinVar `y'
   THEN (D 2 THEN (GenConcl ⌜x' = c ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto) THEN Fold `member` 0)
   THEN ThinVar `x1'
   THEN (Assert a ≤ c BY
               (RWO "-1<" 0 THEN Auto))
   THEN ThinVar `x\''
   THEN (D 2 THEN (GenConcl ⌜y' = d ∈ {p:Point| B(OXp)} ⌝⋅ THENA Auto) THEN Fold `member` 0)
   THEN ThinVar `y1'
   THEN (Assert b ≤ d BY
               (RWO "-1<" 0 THEN Auto))
   THEN ThinVar `y\'') }

1
1. e : BasicGeometry
2. a : {p:Point| B(OXp)} 
3. b : {p:Point| B(OXp)} 
4. c : {p:Point| B(OXp)} 
5. a ≤ c
6. d : {p:Point| B(OXp)} 
7. b ≤ d
⊢ Ax ∈ a + b ≤ c + d

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Length
3.  y  :  Length
4.  x'  :  Length
5.  y'  :  Length
6.  y  \mleq{}  y'
7.  x  \mleq{}  x'
\mvdash{}  Ax  \mmember{}  x  +  y  \mleq{}  x'  +  y'


By

---

Latex:
((D  2  THEN  (GenConcl  \mkleeneopen{}x  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Fold  `member`  0)
  THEN  ThinVar  `x1'
  THEN  (Assert  a  \mleq{}  x'  BY
                          (RWO  "-1<"  0  THEN  Auto))
  THEN  ThinVar  `x'
  THEN  (D  2  THEN  (GenConcl  \mkleeneopen{}y  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Fold  `member`  0)
  THEN  ThinVar  `y1'
  THEN  (Assert  b  \mleq{}  y'  BY
                          (RWO  "-1<"  0  THEN  Auto))
  THEN  ThinVar  `y'
  THEN  (D  2  THEN  (GenConcl  \mkleeneopen{}x'  =  c\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Fold  `member`  0)
  THEN  ThinVar  `x1'
  THEN  (Assert  a  \mleq{}  c  BY
                          (RWO  "-1<"  0  THEN  Auto))
  THEN  ThinVar  `x\mbackslash{}''
  THEN  (D  2  THEN  (GenConcl  \mkleeneopen{}y'  =  d\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  Fold  `member`  0)
  THEN  ThinVar  `y1'
  THEN  (Assert  b  \mleq{}  d  BY
                          (RWO  "-1<"  0  THEN  Auto))
  THEN  ThinVar  `y\mbackslash{}'')

---

Home Index