---

Step * 1 1 1 2 of Lemma Prop22-inequality-to-triangle-construction


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. |ac| < |ab| + |bc|
6. |ab| < |ac| + |bc|
7. |bc| < |ac| + |ab|
8. a ≠ b
9. b ≠ c
10. c ≠ a
11. x : Point
12. b-a-x
13. ax ≅ OX
14. y : Point
15. a-b-y
16. by ≅ OX
17. c1 : Point
18. x-a-c1
19. ac1 ≅ ac
20. c2 : Point
21. y-b-c2
22. bc2 ≅ bc
23. c1' : Point
24. b-a-c1'
25. ac1' ≅ ac1
26. c2' : Point
27. a-b-c2'
28. bc2' ≅ bc2
29. c1'' : Point
30. a_b_c1''
31. bc1'' ≅ bc1
32. c2'' : Point
33. b_a_c2''
34. ac2'' ≅ ac2
35. a-c1-c2'
36. c2'_b_c2
37. c1'-c2-c2'
⊢ ∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)
BY
{ ((Assert c1'-a-c1 BY
          ((InstLemma `extended-out-preserves-between` [⌜e⌝;⌜a⌝;⌜x⌝;⌜c1'⌝;⌜c1⌝]⋅ THEN Auto)
           THEN (InstLemma `geo-out-iff-between1` [⌜e⌝;⌜a⌝;⌜c1'⌝;⌜x⌝;⌜b⌝]⋅ THEN Auto)
           THEN D -2
           THEN EAuto 1))
   THEN (Assert c1'-c2-c1 BY
               ((Assert out(c1' c2c1) BY
                       ((Assert out(c1' c2c2') BY
                               (InstLemma `geo-between-out` [⌜e⌝;⌜c1'⌝;⌜c2⌝;⌜c2'⌝]⋅ THEN Auto))
                        THEN (Assert out(c1' c2'c1) BY
                                    (InstLemma `geo-between-out` [⌜e⌝;⌜c1'⌝;⌜c1⌝;⌜c2'⌝]⋅ THEN EAuto 1))
                        THEN InstLemma `geo-out_transitivity` [⌜e⌝;⌜c1'⌝;⌜c2⌝;⌜c2'⌝;⌜c1⌝]⋅
                        THEN Auto))
                THEN InstLemma `geo-lt-out-to-between` [⌜e⌝;⌜c1'⌝;⌜c2⌝;⌜c1⌝]⋅
                THEN Auto))
   ) }

1
.....aux..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. |ac| < |ab| + |bc|
6. |ab| < |ac| + |bc|
7. |bc| < |ac| + |ab|
8. a ≠ b
9. b ≠ c
10. c ≠ a
11. x : Point
12. b-a-x
13. ax ≅ OX
14. y : Point
15. a-b-y
16. by ≅ OX
17. c1 : Point
18. x-a-c1
19. ac1 ≅ ac
20. c2 : Point
21. y-b-c2
22. bc2 ≅ bc
23. c1' : Point
24. b-a-c1'
25. ac1' ≅ ac1
26. c2' : Point
27. a-b-c2'
28. bc2' ≅ bc2
29. c1'' : Point
30. a_b_c1''
31. bc1'' ≅ bc1
32. c2'' : Point
33. b_a_c2''
34. ac2'' ≅ ac2
35. a-c1-c2'
36. c2'_b_c2
37. c1'-c2-c2'
38. c1'-a-c1
39. out(c1' c2c1)
⊢ |c1'c2| < |c1'c1|

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. |ac| < |ab| + |bc|
6. |ab| < |ac| + |bc|
7. |bc| < |ac| + |ab|
8. a ≠ b
9. b ≠ c
10. c ≠ a
11. x : Point
12. b-a-x
13. ax ≅ OX
14. y : Point
15. a-b-y
16. by ≅ OX
17. c1 : Point
18. x-a-c1
19. ac1 ≅ ac
20. c2 : Point
21. y-b-c2
22. bc2 ≅ bc
23. c1' : Point
24. b-a-c1'
25. ac1' ≅ ac1
26. c2' : Point
27. a-b-c2'
28. bc2' ≅ bc2
29. c1'' : Point
30. a_b_c1''
31. bc1'' ≅ bc1
32. c2'' : Point
33. b_a_c2''
34. ac2'' ≅ ac2
35. a-c1-c2'
36. c2'_b_c2
37. c1'-c2-c2'
38. c1'-a-c1
39. c1'-c2-c1
⊢ ∃c1,c2:Point. ((ac ≅ ac1 ∧ bc2 > bc1) ∧ bc ≅ bc2 ∧ ac1 > ac2)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  |ac|  <  |ab|  +  |bc|
6.  |ab|  <  |ac|  +  |bc|
7.  |bc|  <  |ac|  +  |ab|
8.  a  \mneq{}  b
9.  b  \mneq{}  c
10.  c  \mneq{}  a
11.  x  :  Point
12.  b-a-x
13.  ax  \mcong{}  OX
14.  y  :  Point
15.  a-b-y
16.  by  \mcong{}  OX
17.  c1  :  Point
18.  x-a-c1
19.  ac1  \mcong{}  ac
20.  c2  :  Point
21.  y-b-c2
22.  bc2  \mcong{}  bc
23.  c1'  :  Point
24.  b-a-c1'
25.  ac1'  \mcong{}  ac1
26.  c2'  :  Point
27.  a-b-c2'
28.  bc2'  \mcong{}  bc2
29.  c1''  :  Point
30.  a\_b\_c1''
31.  bc1''  \mcong{}  bc1
32.  c2''  :  Point
33.  b\_a\_c2''
34.  ac2''  \mcong{}  ac2
35.  a-c1-c2'
36.  c2'\_b\_c2
37.  c1'-c2-c2'
\mvdash{}  \mexists{}c1,c2:Point.  ((ac  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  bc  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)


By

---

Latex:
((Assert  c1'-a-c1  BY
                ((InstLemma  `extended-out-preserves-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  (InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  D  -2
                  THEN  EAuto  1))
  THEN  (Assert  c1'-c2-c1  BY
                          ((Assert  out(c1'  c2c1)  BY
                                          ((Assert  out(c1'  c2c2')  BY
                                                          (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}c2'\mkleeneclose{}]\mcdot{}  THEN  Auto))
                                            THEN  (Assert  out(c1'  c2'c1)  BY
                                                                    (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2'\mkleeneclose{}]\mcdot{}
                                                                      THEN  EAuto  1
                                                                      ))
                                            THEN  InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}c2'\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}
                                            THEN  Auto))
                            THEN  InstLemma  `geo-lt-out-to-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index