---

Step * 1 of Lemma dist-lemma-lt


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. b' : Point
10. c' : Point
11. u : {u:Point| c' # u} 
12. B(a'b'c')
13. B(a'uc')
14. ab ≅ a'b'
15. cd ≅ b'c'
16. ef ≅ a'u
17. |ef| ≤ |ab| + |cd|
18. u # c'
⊢ |ef| + |uc'| ≤ |ab| + |cd|
BY
{ (((Assert |ef| = |a'u| ∈ Length BY
           Auto)
    THEN (FLemma `geo-add-length-between` [13] THENA Auto)
    THEN (FLemma `geo-add-length-between` [12] THENA Auto))
   THEN ((Subst' |a'b'| + |b'c'| = |ab| + |cd| ∈ Length -1 THENA Auto) THEN (RWO "19" 0 THENA Auto))
   THEN EAuto  1) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  a'  :  Point
9.  b'  :  Point
10.  c'  :  Point
11.  u  :  \{u:Point|  c'  \#  u\} 
12.  B(a'b'c')
13.  B(a'uc')
14.  ab  \mcong{}  a'b'
15.  cd  \mcong{}  b'c'
16.  ef  \mcong{}  a'u
17.  |ef|  \mleq{}  |ab|  +  |cd|
18.  u  \#  c'
\mvdash{}  |ef|  +  |uc'|  \mleq{}  |ab|  +  |cd|


By

---

Latex:
(((Assert  |ef|  =  |a'u|  BY
                  Auto)
    THEN  (FLemma  `geo-add-length-between`  [13]  THENA  Auto)
    THEN  (FLemma  `geo-add-length-between`  [12]  THENA  Auto))
  THEN  ((Subst'  |a'b'|  +  |b'c'|  =  |ab|  +  |cd|  -1  THENA  Auto)  THEN  (RWO  "19"  0  THENA  Auto))
  THEN  EAuto    1)

---

Home Index