Step
*
1
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,p',d',f':Point. (((abc ≅a ijp ∧ kjp ≅a xyz) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')
12. i # jk
⊢ ∃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 (Assert ∃D',F:Point
(((out(j iD') ∧ out(j kF)) ∧ D'jF ≅a f'jd') ∧ D'F ≅ d'f' ∧ D' ≠ F ∧ jD' ≅ jf' ∧ jF ≅ jd') BY
(((((gProperProlong ⌜d'⌝⌜j⌝`j1'⌜O⌝⌜X⌝⋅ THENA Auto) THEN (gProperProlong ⌜f'⌝⌜j⌝`j2'⌜O⌝⌜X⌝⋅ THENA Auto))
THEN ExRepD
)
THEN (gProperProlong ⌜j1⌝⌜j⌝`D\''⌜j⌝⌜f'⌝⋅ THENA Auto)
THEN (gProperProlong ⌜j2⌝⌜j⌝`F'⌜j⌝⌜d'⌝⋅ THENA Auto)
THEN ExRepD)
THEN InstConcl [⌜D'⌝;⌜F⌝]⋅
THEN Auto))
) }
1
.....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. 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. j1 : Point
23. d'-j-j1
24. jj1 ≅ OX
25. j2 : Point
26. f'-j-j2
27. jj2 ≅ OX
28. D' : Point
29. j1-j-D'
30. jD' ≅ jf'
31. F : Point
32. j2-j-F
33. jF ≅ jd'
⊢ out(j iD')
2
.....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. 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. j1 : Point
23. d'-j-j1
24. jj1 ≅ OX
25. j2 : Point
26. f'-j-j2
27. jj2 ≅ OX
28. D' : Point
29. j1-j-D'
30. jD' ≅ jf'
31. F : Point
32. j2-j-F
33. jF ≅ jd'
34. out(j iD')
⊢ out(j kF)
3
.....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. 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. j1 : Point
23. d'-j-j1
24. jj1 ≅ OX
25. j2 : Point
26. f'-j-j2
27. jj2 ≅ OX
28. D' : Point
29. j1-j-D'
30. jD' ≅ jf'
31. F : Point
32. j2-j-F
33. jF ≅ jd'
34. out(j iD')
35. out(j kF)
⊢ D'jF ≅a f'jd'
4
.....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. 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. j1 : Point
23. d'-j-j1
24. jj1 ≅ OX
25. j2 : Point
26. f'-j-j2
27. jj2 ≅ OX
28. D' : Point
29. j1-j-D'
30. jD' ≅ jf'
31. F : Point
32. j2-j-F
33. jF ≅ jd'
34. out(j iD')
35. out(j kF)
36. D'jF ≅a f'jd'
⊢ D'F ≅ d'f'
5
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',F:Point. (((out(j iD') ∧ out(j kF)) ∧ D'jF ≅a f'jd') ∧ D'F ≅ d'f' ∧ D' ≠ F ∧ jD' ≅ jf' ∧ jF ≅ jd')
⊢ ∃p,p',d',f':Point. (((xyz ≅a ijp ∧ kjp ≅a abc) ∧ j_p'_p) ∧ (out(j id') ∧ 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. \mexists{}p,p',d',f':Point. (((abc \mcong{}\msuba{} ijp \mwedge{} kjp \mcong{}\msuba{} xyz) \mwedge{} j\_p'\_p) \mwedge{} (out(j id') \mwedge{} out(j kf')) \mwedge{} d'-p'-f')
12. i \# jk
\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 (Assert \mexists{}D',F:Point
(((out(j iD') \mwedge{} out(j kF)) \mwedge{} D'jF \mcong{}\msuba{} f'jd')
\mwedge{} D'F \mcong{} d'f'
\mwedge{} D' \mneq{} F
\mwedge{} jD' \mcong{} jf'
\mwedge{} jF \mcong{} jd') BY
(((((gProperProlong \mkleeneopen{}d'\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`j1'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{} THENA Auto)
THEN (gProperProlong \mkleeneopen{}f'\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`j2'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{} THENA Auto)
)
THEN ExRepD
)
THEN (gProperProlong \mkleeneopen{}j1\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`D\mbackslash{}''\mkleeneopen{}j\mkleeneclose{}\mkleeneopen{}f'\mkleeneclose{}\mcdot{} THENA Auto)
THEN (gProperProlong \mkleeneopen{}j2\mkleeneclose{}\mkleeneopen{}j\mkleeneclose{}`F'\mkleeneopen{}j\mkleeneclose{}\mkleeneopen{}d'\mkleeneclose{}\mcdot{} THENA Auto)
THEN ExRepD)
THEN InstConcl [\mkleeneopen{}D'\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}
THEN Auto))
)
Home
Index