Proof of Nuprl Lemma : hp-angle-sum-lt

Step * 4 1 1 of Lemma hp-angle-sum-lt

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')
BY
{ ((Assert p'@0 ≠ j' BY
          ((InstLemma `colinear-lsep` [⌜e⌝;⌜x1⌝;⌜z1⌝;⌜j'⌝;⌜p'@0⌝]⋅ THEN Auto)
           THEN InstLemma `out-preserves-lsep` [⌜e⌝;⌜j'⌝;⌜p'⌝;⌜k'⌝;⌜x1⌝;⌜z1⌝]⋅
           THEN Auto))
   THEN (Assert p' # j'p3 BY

               (InstLemma  `cong-angle-preserves-lsep_strong` [⌜e⌝;⌜p'⌝;⌜j'⌝;⌜p3⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THEN EAuto 1))

THEN InstLemma `out-preserves-lsep` [⌜e⌝;⌜j'⌝;⌜p'⌝;⌜p3⌝;⌜x1⌝;⌜p'@0⌝]⋅
THEN Auto) }

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. 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
58. p'@0 ≠ j'
59. p' # j'p3
⊢ out(j' p3p'@0)

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. 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
58. p'@0 ≠ j'
59. p' # j'p3
60. j' # x1p'@0
⊢ ∃q:Point. (p'-q-f' ∧ xyz ≅_a qj'p')

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. 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') 47. p3 : Point 48. p'@0 : Point 49. x1 : Point 50. z1 : Point 51. xyz \mcong{}\msuba{} p'j'p3 52. j'\_p'@0\_p3 53. out(j' p'x1) 54. out(j' k'z1) 55. \mneg{}p'\_j'\_p3 56. x1\_p'@0\_z1 57. p'@0 \mneq{} z1 \mvdash{} \mexists{}q:Point. (p'-q-f' \mwedge{} xyz \mcong{}\msuba{} qj'p') By Latex: ((Assert p'@0 \mneq{} j' BY ((InstLemma `colinear-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p'@0\mkleeneclose{}]\mcdot{} THEN Auto) THEN InstLemma `out-preserves-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}k'\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{}]\mcdot{} THEN Auto)) THEN (Assert p' \# j'p3 BY (InstLemma `cong-angle-preserves-lsep\_strong` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p3\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{} THEN EAuto 1 )) THEN InstLemma `out-preserves-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{};\mkleeneopen{}p3\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}p'@0\mkleeneclose{}]\mcdot{} THEN Auto) Home Index