Step
*
4
1
of Lemma
hp-angle-sum-lt
.....aux.....
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. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. (¬out(j' p'k'))
∧ (∃p,p'@0,x',z':Point
(xyz ≅a p'j'p ∧ j'_p'@0_p ∧ (out(j' p'x') ∧ out(j' k'z')) ∧ (¬p'_j'_p) ∧ x'_p'@0_z' ∧ p'@0 ≠ z'))
⊢ ∃q:Point. (p'-q-f' ∧ xyz ≅a qj'p')
BY
{ ExRepD }
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. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc ≅a a'b'c'
21. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc ≅a ijp1
26. kjp1 ≅a xyz
27. j_p2_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' ≅a i'j'p
36. k'j'p ≅a x'y'z'
37. j'_p'_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. i # jk
42. i' # j'k'
43. x # yz
44. xyz < x'y'z'
45. p' # j'k'
46. ¬out(j' p'k')
47. p3 : Point
48. p'@0 : Point
49. x1 : Point
50. z1 : Point
51. xyz ≅a p'j'p3
52. j'_p'@0_p3
53. out(j' p'x1)
54. out(j' k'z1)
55. ¬p'_j'_p3
56. x1_p'@0_z1
57. p'@0 ≠ z1
⊢ ∃q:Point. (p'-q-f' ∧ xyz ≅a qj'p')
Latex:
Latex:
.....aux.....
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. a' : Point
12. b' : Point
13. c' : Point
14. x' : Point
15. y' : Point
16. z' : Point
17. i' : Point
18. j' : Point
19. k' : Point
20. abc \mcong{}\msuba{} a'b'c'
21. p1 : Point
22. p2 : Point
23. d1 : Point
24. f1 : Point
25. abc \mcong{}\msuba{} ijp1
26. kjp1 \mcong{}\msuba{} xyz
27. j\_p2\_p1
28. out(j id1)
29. out(j kf1)
30. d1-p2-f1
31. p : Point
32. p' : Point
33. d' : Point
34. f' : Point
35. a'b'c' \mcong{}\msuba{} i'j'p
36. k'j'p \mcong{}\msuba{} x'y'z'
37. j'\_p'\_p
38. out(j' i'd')
39. out(j' k'f')
40. d'-p'-f'
41. i \# jk
42. i' \# j'k'
43. x \# yz
44. xyz < x'y'z'
45. p' \# j'k'
46. (\mneg{}out(j' p'k'))
\mwedge{} (\mexists{}p,p'@0,x',z':Point
(xyz \mcong{}\msuba{} p'j'p
\mwedge{} j'\_p'@0\_p
\mwedge{} (out(j' p'x') \mwedge{} out(j' k'z'))
\mwedge{} (\mneg{}p'\_j'\_p)
\mwedge{} x'\_p'@0\_z'
\mwedge{} p'@0 \mneq{} z'))
\mvdash{} \mexists{}q:Point. (p'-q-f' \mwedge{} xyz \mcong{}\msuba{} qj'p')
By
Latex:
ExRepD
Home
Index