---

Step * 1 1 2 1 2 2 1 1 of Lemma Euclid-Prop22

.....antecedent..... 
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2| + |c1c2|
9. |b1b2| < |a1a2| + |c1c2|
10. |c1c2| < |a1a2| + |b1b2|
11. a1 # a2
12. b1 # b2
13. c1 # c2
14. f : Point
15. O-X-f
16. Xf ≅ a1a2
17. g : Point
18. X-f-g
19. fg ≅ b1b2
20. h : Point
21. f-g-h
22. gh ≅ c1c2
23. x' : Point
24. X-f-x'
25. Xf ≅ fx'
26. f-x'-h
27. h' : Point
28. h-g-h'
29. gh ≅ gh'
30. X-h'-h
31. out(X h'x')
32. |Xh'| < |Xx'| ⇒ |Xh'| + |h'g| < |Xx'| + |h'g|
⊢ |Xh'| + |h'g| < |Xx'| + |h'g|
BY
{ (((Assert B(Xh'g) BY
           Auto)
    THEN (FLemma `geo-add-length-between` [-1] THENA Auto)
    THEN D 18
    THEN (FLemma `geo-add-length-between` [18] THENA Auto))
   THEN (Subst' |Xh'| + |h'g| = |Xg| ∈ Length 0 THENA Auto)
   THEN (Subst' |Xg| = |Xf| + |fg| ∈ Length 0 THENA Auto)
   THEN (Subst' |Xf| + |fg| = |a1a2| + |b1b2| ∈ Length 0 THENA Auto)
   THEN (D 25 THEN (FLemma `geo-add-length-between` [25] THENA Auto))
   THEN (Subst' |Xx'| = |Xf| + |fx'| ∈ Length 0 THENA Auto)
   THEN (Subst' |Xf| + |fx'| = |a1a2| + |a1a2| ∈ Length 0 THENA Auto)
   THEN (Subst' |h'g| = |c1c2| ∈ Length 0 THENA Auto)) }

1
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2| + |c1c2|
9. |b1b2| < |a1a2| + |c1c2|
10. |c1c2| < |a1a2| + |b1b2|
11. a1 # a2
12. b1 # b2
13. c1 # c2
14. f : Point
15. O-X-f
16. Xf ≅ a1a2
17. g : Point
18. B(Xfg)
19. X # f ∧ f # g
20. fg ≅ b1b2
21. h : Point
22. f-g-h
23. gh ≅ c1c2
24. x' : Point
25. B(Xfx')
26. X # f ∧ f # x'
27. Xf ≅ fx'
28. f-x'-h
29. h' : Point
30. h-g-h'
31. gh ≅ gh'
32. X-h'-h
33. out(X h'x')
34. |Xh'| < |Xx'| ⇒ |Xh'| + |h'g| < |Xx'| + |h'g|
35. B(Xh'g)
36. |Xg| = |Xh'| + |h'g| ∈ Length
37. |Xg| = |Xf| + |fg| ∈ Length
38. |Xx'| = |Xf| + |fx'| ∈ Length
⊢ |a1a2| + |b1b2| < |a1a2| + |a1a2| + |c1c2|

---

Latex:

---

Latex:
.....antecedent..... 
1.  e  :  EuclideanPlane
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  |a1a2|  <  |b1b2|  +  |c1c2|
9.  |b1b2|  <  |a1a2|  +  |c1c2|
10.  |c1c2|  <  |a1a2|  +  |b1b2|
11.  a1  \#  a2
12.  b1  \#  b2
13.  c1  \#  c2
14.  f  :  Point
15.  O-X-f
16.  Xf  \mcong{}  a1a2
17.  g  :  Point
18.  X-f-g
19.  fg  \mcong{}  b1b2
20.  h  :  Point
21.  f-g-h
22.  gh  \mcong{}  c1c2
23.  x'  :  Point
24.  X-f-x'
25.  Xf  \mcong{}  fx'
26.  f-x'-h
27.  h'  :  Point
28.  h-g-h'
29.  gh  \mcong{}  gh'
30.  X-h'-h
31.  out(X  h'x')
32.  |Xh'|  <  |Xx'|  {}\mRightarrow{}  |Xh'|  +  |h'g|  <  |Xx'|  +  |h'g|
\mvdash{}  |Xh'|  +  |h'g|  <  |Xx'|  +  |h'g|


By

---

Latex:
(((Assert  B(Xh'g)  BY
                  Auto)
    THEN  (FLemma  `geo-add-length-between`  [-1]  THENA  Auto)
    THEN  D  18
    THEN  (FLemma  `geo-add-length-between`  [18]  THENA  Auto))
  THEN  (Subst'  |Xh'|  +  |h'g|  =  |Xg|  0  THENA  Auto)
  THEN  (Subst'  |Xg|  =  |Xf|  +  |fg|  0  THENA  Auto)
  THEN  (Subst'  |Xf|  +  |fg|  =  |a1a2|  +  |b1b2|  0  THENA  Auto)
  THEN  (D  25  THEN  (FLemma  `geo-add-length-between`  [25]  THENA  Auto))
  THEN  (Subst'  |Xx'|  =  |Xf|  +  |fx'|  0  THENA  Auto)
  THEN  (Subst'  |Xf|  +  |fx'|  =  |a1a2|  +  |a1a2|  0  THENA  Auto)
  THEN  (Subst'  |h'g|  =  |c1c2|  0  THENA  Auto))

---

Home Index