---

Step * 1 1 13 1 1 2 of Lemma Prop22-symmetric-point-construction-lemma


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  a-c1-c2'  BY
              (((Assert  |ac|  =  |ac1|  BY
                                Auto)
                  THEN  (Assert  |ab|  +  |bc|  =  |ac2'|  BY
                                          ((Assert  a\_b\_c2'  BY  Auto)  THEN  FLemma  `geo-add-length-between`  [-1]  THEN  Auto))
                  )
                THEN  (((Assert  |ab|  +  |bc|  =  |ba|  +  |bc|  BY
                                            Auto)
                              THEN  (RWO  "-1"  41  THENA  Auto)
                              THEN  (RWO  "-2"  7  THENA  Auto))
                            THEN  (RWO  "-4"  42  THENA  Auto)
                            )
                THEN  (InstLemma  `geo-lt-out-to-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  (InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c2'\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  (InstLemma  `extended-out-preserves-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}c1'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  (InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  D  -2
                THEN  Auto))

---

Home Index