Step
*
1
5
4
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. ((D'_P'_F ∧ Cong3(D'P'F,f'p'd')) ∧ jp' ≅ jP' ∧ P' ≠ j)
⊢ ∃p,p',d',f':Point. (((xyz ≅a ijp ∧ kjp ≅a abc) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')
BY
{ (ExRepD THEN InstConcl [⌜P'⌝;⌜P'⌝;⌜D'⌝;⌜F⌝]⋅ THEN Auto) }
1
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
⊢ xyz ≅a ijP'
2
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
3
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. kjP' ≅a abc
38. j_P'_P'
39. out(j iD')
40. out(j kF)
⊢ D'-P'-F
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. \mexists{}P':Point. ((D'\_P'\_F \mwedge{} Cong3(D'P'F,f'p'd')) \mwedge{} jp' \mcong{} jP' \mwedge{} P' \mneq{} j)
\mvdash{} \mexists{}p,p',d',f':Point. (((xyz \mcong{}\msuba{} ijp \mwedge{} kjp \mcong{}\msuba{} abc) \mwedge{} j\_p'\_p) \mwedge{} (out(j id') \mwedge{} out(j kf')) \mwedge{} d'-p'-f')
By
Latex:
(ExRepD THEN InstConcl [\mkleeneopen{}P'\mkleeneclose{};\mkleeneopen{}P'\mkleeneclose{};\mkleeneopen{}D'\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index