Step
*
1
5
4
2
of Lemma
hp-angle-sum-symm
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. p : Point
12. p' : Point
13. d' : Point
14. f' : Point
15. abc ≅a ijp
16. kjp ≅a xyz
17. j_p'_p
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. i # jk
22. D' : Point
23. F : Point
24. out(j iD')
25. out(j kF)
26. D'jF ≅a f'jd'
27. D'F ≅ d'f'
28. D' ≠ F
29. jD' ≅ jf'
30. jF ≅ jd'
31. P' : Point
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
⊢ kjP' ≅a abc
BY
{ (((InstLemma `out-cong-angle` [⌜e⌝;⌜i⌝;⌜j⌝;⌜p⌝;⌜d'⌝;⌜p'⌝]⋅ THEN Auto)
THENA (InstLemma `geo-between-out` [⌜e⌝;⌜j⌝;⌜p'⌝;⌜p⌝]⋅ THEN EAuto 1)
)
THEN (InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜d'⌝;⌜j⌝;⌜p'⌝;⌜i⌝;⌜j⌝;⌜p⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA EAuto 1)
THEN (InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d'⌝;⌜j⌝;⌜p'⌝;⌜k⌝;⌜j⌝;⌜P'⌝]⋅ THEN EAuto 1)
THEN InstLemma `geo-cong-angle-transitivity` [⌜e⌝;⌜d'⌝;⌜j⌝;⌜p'⌝;⌜F⌝;⌜j⌝;⌜P'⌝;⌜k⌝;⌜j⌝;⌜P'⌝]⋅
THEN EAuto 1) }
1
.....antecedent.....
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. p : Point
12. p' : Point
13. d' : Point
14. f' : Point
15. abc ≅a ijp
16. kjp ≅a xyz
17. j_p'_p
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. i # jk
22. D' : Point
23. F : Point
24. out(j iD')
25. out(j kF)
26. D'jF ≅a f'jd'
27. D'F ≅ d'f'
28. D' ≠ F
29. jD' ≅ jf'
30. jF ≅ jd'
31. P' : Point
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ d'jp' ≅a FjP'
2
.....antecedent.....
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. p : Point
12. p' : Point
13. d' : Point
14. f' : Point
15. abc ≅a ijp
16. kjp ≅a xyz
17. j_p'_p
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. i # jk
22. D' : Point
23. F : Point
24. out(j iD')
25. out(j kF)
26. D'jF ≅a f'jd'
27. D'F ≅ d'f'
28. D' ≠ F
29. jD' ≅ jf'
30. jF ≅ jd'
31. P' : Point
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ FjP' ≅a kjP'
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. i : Point
9. j : Point
10. k : Point
11. p : Point
12. p' : Point
13. d' : Point
14. f' : Point
15. abc \mcong{}\msuba{} ijp
16. kjp \mcong{}\msuba{} xyz
17. j\_p'\_p
18. out(j id')
19. out(j kf')
20. d'-p'-f'
21. i \# jk
22. D' : Point
23. F : Point
24. out(j iD')
25. out(j kF)
26. D'jF \mcong{}\msuba{} f'jd'
27. D'F \mcong{} d'f'
28. D' \mneq{} F
29. jD' \mcong{} jf'
30. jF \mcong{} jd'
31. P' : Point
32. D'\_P'\_F
33. Cong3(D'P'F,f'p'd')
34. jp' \mcong{} jP'
35. P' \mneq{} j
36. xyz \mcong{}\msuba{} ijP'
\mvdash{} kjP' \mcong{}\msuba{} abc
By
Latex:
(((InstLemma `out-cong-angle` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{} THEN Auto)
THENA (InstLemma `geo-between-out` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{} THEN EAuto 1)
)
THEN (InstLemma `geo-cong-angle-transitivity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
THENA EAuto 1
)
THEN (InstLemma `geo-cong-angle-transitivity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}P'\mkleeneclose{}]\mcdot{}
THEN EAuto 1
)
THEN InstLemma `geo-cong-angle-transitivity` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}P'\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}P'\mkleeneclose{}]\mcdot{}
THEN EAuto 1)
Home
Index