---

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


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|
BY
{ ((((gProperProlong ⌜X⌝⌜f⌝`y'⌜c1⌝⌜c2⌝⋅ THENA Auto) THEN ExRepD)
    THEN D -2
    THEN (FLemma `geo-add-length-between` [-3] THENA Auto))
   THEN ((Subst' |Xf| + |fy| = |a1a2| + |c1c2| ∈ Length -1 THENA Auto)
         THEN (Assert |b1b2| < |Xy| BY
                     (Subst' |a1a2| + |c1c2| = |Xy| ∈ Length 0 THEN Auto))
         )
   THEN (InstLemma `geo-lt-add1-iff2` [⌜e⌝;⌜b1⌝;⌜b2⌝;⌜X⌝;⌜y⌝;⌜a1⌝;⌜a2⌝]⋅ THEN Auto)
   THEN (Subst' |Xy| = |a1a2| + |c1c2| ∈ Length 49 THEN Auto)
   THEN (Subst' |a1a2| + |c1c2| + |a1a2| = |a1a2| + |c1c2| + |a1a2| ∈ Length 49 THEN Auto)
   THEN (Subst' |a1a2| + |c1c2| + |a1a2| = |a1a2| + |a1a2| + |c1c2| ∈ Length 49 THEN Auto)
   THEN Subst' |b1b2| + |a1a2| = |a1a2| + |b1b2| ∈ Length 49
   THEN Auto) }

---

Latex:

---

Latex:

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.  B(Xfg)
19.  X  \#  f  \mwedge{}  f  \#  g
20.  fg  \mcong{}  b1b2
21.  h  :  Point
22.  f-g-h
23.  gh  \mcong{}  c1c2
24.  x'  :  Point
25.  B(Xfx')
26.  X  \#  f  \mwedge{}  f  \#  x'
27.  Xf  \mcong{}  fx'
28.  f-x'-h
29.  h'  :  Point
30.  h-g-h'
31.  gh  \mcong{}  gh'
32.  X-h'-h
33.  out(X  h'x')
34.  |Xh'|  <  |Xx'|  {}\mRightarrow{}  |Xh'|  +  |h'g|  <  |Xx'|  +  |h'g|
35.  B(Xh'g)
36.  |Xg|  =  |Xh'|  +  |h'g|
37.  |Xg|  =  |Xf|  +  |fg|
38.  |Xx'|  =  |Xf|  +  |fx'|
\mvdash{}  |a1a2|  +  |b1b2|  <  |a1a2|  +  |a1a2|  +  |c1c2|


By

---

Latex:
((((gProperProlong  \mkleeneopen{}X\mkleeneclose{}\mkleeneopen{}f\mkleeneclose{}`y'\mkleeneopen{}c1\mkleeneclose{}\mkleeneopen{}c2\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
    THEN  D  -2
    THEN  (FLemma  `geo-add-length-between`  [-3]  THENA  Auto))
  THEN  ((Subst'  |Xf|  +  |fy|  =  |a1a2|  +  |c1c2|  -1  THENA  Auto)
              THEN  (Assert  |b1b2|  <  |Xy|  BY
                                      (Subst'  |a1a2|  +  |c1c2|  =  |Xy|  0  THEN  Auto))
              )
  THEN  (InstLemma  `geo-lt-add1-iff2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{};\mkleeneopen{}a2\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (Subst'  |Xy|  =  |a1a2|  +  |c1c2|  49  THEN  Auto)
  THEN  (Subst'  |a1a2|  +  |c1c2|  +  |a1a2|  =  |a1a2|  +  |c1c2|  +  |a1a2|  49  THEN  Auto)
  THEN  (Subst'  |a1a2|  +  |c1c2|  +  |a1a2|  =  |a1a2|  +  |a1a2|  +  |c1c2|  49  THEN  Auto)
  THEN  Subst'  |b1b2|  +  |a1a2|  =  |a1a2|  +  |b1b2|  49
  THEN  Auto)

---

Home Index