---

Step * 1 1 2 of Lemma Euclid-Prop20


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. d : Point
7. b-a-d
8. adc ≅a acd
9. ad ≅ ac
10. adc < bcd
11. |bc| < |bd|
⊢ |bc| < |ba| + |ac|
BY
{ (D -5
   THEN (Assert |ba| + |ac| = |bd| ∈ Length BY
               ((FLemma `geo-add-length-between` [-6] THEN EAuto 1)
                THEN (Assert |ad| = |ac| ∈ Length BY
                            Auto)
                THEN Auto))
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a  \#  bc
6.  d  :  Point
7.  b-a-d
8.  adc  \mcong{}\msuba{}  acd
9.  ad  \mcong{}  ac
10.  adc  <  bcd
11.  |bc|  <  |bd|
\mvdash{}  |bc|  <  |ba|  +  |ac|


By

---

Latex:
(D  -5
  THEN  (Assert  |ba|  +  |ac|  =  |bd|  BY
                          ((FLemma  `geo-add-length-between`  [-6]  THEN  EAuto  1)
                            THEN  (Assert  |ad|  =  |ac|  BY
                                                    Auto)
                            THEN  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index