---

Step * 8 1 1 1 1 1 1 of Lemma eu-eq_dist-axiomsA


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. a' : Point
9. c' : Point
10. A : Point
11. B : Point
12. E1 : Point
13. E2 : Point
14. C : Point
15. xy ≥ ab
16. c'-a'-A
17. B(Aa'B)
18. a'B ≅ xy
19. c'E1 ≅ xy
20. c'E2 ≅ cd
21. B(Aa'C)
22. a'C ≅ E1E2
23. B(E1c'E2)
24. a' # B
25. a' # C
26. |a'B| ≤ |a'C| ⇐⇒ B(a'BC)
⊢ B(a'BC)
BY
{ (D -1
   THEN (D -2 THEN Auto)
   THEN (FLemma `geo-add-length-between` [23] THENA Auto)
   THEN ((Subst' |E1c'| + |c'E2| = |xy| + |cd| ∈ Length -1 THENA Auto)
         THEN (Assert |a'C| = |xy| + |cd| ∈ Length BY
                     Auto)
         THEN (RWO "-1" 0 THEN Auto)
         THEN (Assert |a'B| = |xy| ∈ Length BY
                     Auto)
         THEN RWO "-1" 0
         THEN Auto)
   THEN (Assert |a'C| = |xy| + |cd| ∈ Length BY
               Auto)
   THEN (RWO "-1" 0 THEN Auto)
   THEN (Assert |a'B| = |xy| ∈ Length BY
               Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  x  :  Point
7.  y  :  Point
8.  a'  :  Point
9.  c'  :  Point
10.  A  :  Point
11.  B  :  Point
12.  E1  :  Point
13.  E2  :  Point
14.  C  :  Point
15.  xy  \mgeq{}  ab
16.  c'-a'-A
17.  B(Aa'B)
18.  a'B  \mcong{}  xy
19.  c'E1  \mcong{}  xy
20.  c'E2  \mcong{}  cd
21.  B(Aa'C)
22.  a'C  \mcong{}  E1E2
23.  B(E1c'E2)
24.  a'  \#  B
25.  a'  \#  C
26.  |a'B|  \mleq{}  |a'C|  \mLeftarrow{}{}\mRightarrow{}  B(a'BC)
\mvdash{}  B(a'BC)


By

---

Latex:
(D  -1
  THEN  (D  -2  THEN  Auto)
  THEN  (FLemma  `geo-add-length-between`  [23]  THENA  Auto)
  THEN  ((Subst'  |E1c'|  +  |c'E2|  =  |xy|  +  |cd|  -1  THENA  Auto)
              THEN  (Assert  |a'C|  =  |xy|  +  |cd|  BY
                                      Auto)
              THEN  (RWO  "-1"  0  THEN  Auto)
              THEN  (Assert  |a'B|  =  |xy|  BY
                                      Auto)
              THEN  RWO  "-1"  0
              THEN  Auto)
  THEN  (Assert  |a'C|  =  |xy|  +  |cd|  BY
                          Auto)
  THEN  (RWO  "-1"  0  THEN  Auto)
  THEN  (Assert  |a'B|  =  |xy|  BY
                          Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index