Step
*
1
of Lemma
zero-angles-congruent2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. out(b ac)
9. out(y xz)
10. A : Point
11. b-a-A
12. aA ≅ yx
13. b ≠ c
14. y ≠ z
15. C : Point
16. b-c-C
17. cC ≅ yz
18. X : Point
19. y-x-X
20. xX ≅ ab
21. Z : Point
22. y-z-Z
23. zZ ≅ bc
24. b_a_A
25. b_c_C
26. y_x_X
27. y_z_Z
28. bA ≅ yX
29. bC ≅ yZ
⊢ AC ≅ XZ
BY
{ (Assert out(b AC) BY
(((InstLemma `geo-between-out` [⌜g⌝;⌜b⌝;⌜c⌝;⌜C⌝]⋅ THENA Auto)
THEN (InstLemma`geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜C⌝]⋅ THENA Auto)
THEN (InstLemma `geo-between-out` [⌜g⌝;⌜b⌝;⌜a⌝;⌜A⌝]⋅ THENA Auto)
THEN (InstLemma`geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜A⌝]⋅ THENA EAuto 1))
THEN InstLemma`geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜C⌝;⌜c⌝;⌜A⌝]⋅
THEN EAuto 1)) }
1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. out(b ac)
9. out(y xz)
10. A : Point
11. b-a-A
12. aA ≅ yx
13. b ≠ c
14. y ≠ z
15. C : Point
16. b-c-C
17. cC ≅ yz
18. X : Point
19. y-x-X
20. xX ≅ ab
21. Z : Point
22. y-z-Z
23. zZ ≅ bc
24. b_a_A
25. b_c_C
26. y_x_X
27. y_z_Z
28. bA ≅ yX
29. bC ≅ yZ
30. out(b AC)
⊢ AC ≅ XZ
Latex:
Latex:
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. out(b ac)
9. out(y xz)
10. A : Point
11. b-a-A
12. aA \mcong{} yx
13. b \mneq{} c
14. y \mneq{} z
15. C : Point
16. b-c-C
17. cC \mcong{} yz
18. X : Point
19. y-x-X
20. xX \mcong{} ab
21. Z : Point
22. y-z-Z
23. zZ \mcong{} bc
24. b\_a\_A
25. b\_c\_C
26. y\_x\_X
27. y\_z\_Z
28. bA \mcong{} yX
29. bC \mcong{} yZ
\mvdash{} AC \mcong{} XZ
By
Latex:
(Assert out(b AC) BY
(((InstLemma `geo-between-out` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma`geo-out\_transitivity` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma `geo-between-out` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{} THENA Auto)
THEN (InstLemma`geo-out\_transitivity` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{} THENA EAuto 1))
THEN InstLemma`geo-out\_transitivity` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{}]\mcdot{}
THEN EAuto 1))
Home
Index