Step
*
1
2
of Lemma
hp-angle-sum-subst4
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. a # bc
27. d # ef
28. ∃x',b':Point. (out(j ib') ∧ x' # jb' ∧ x'jb' ≅a abc)
⊢ ∃p,p',d',f':Point. (((abc ≅a ijp ∧ kjp ≅a def) ∧ j_p'_p) ∧ (out(j id') ∧ out(j kf')) ∧ d'-p'-f')
BY
{ (ExRepD THEN InstConcl [⌜x'⌝;⌜j⌝;⌜b'⌝;⌜k⌝]⋅ THEN Auto) }
1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. a # bc
27. d # ef
28. x' : Point
29. b' : Point
30. out(j ib')
31. x' # jb'
32. x'jb' ≅a abc
⊢ abc ≅a ijx'
2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. a # bc
27. d # ef
28. x' : Point
29. b' : Point
30. out(j ib')
31. x' # jb'
32. x'jb' ≅a abc
33. abc ≅a ijx'
⊢ kjx' ≅a def
3
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. a # bc
27. d # ef
28. x' : Point
29. b' : Point
30. out(j ib')
31. x' # jb'
32. x'jb' ≅a abc
33. abc ≅a ijx'
34. kjx' ≅a def
35. j_j_x'
36. out(j ib')
⊢ out(j kk)
4
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc ≅a xyp
19. zyp ≅a def
20. y_p'_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz ≅a ijk
25. x-y-z
26. a # bc
27. d # ef
28. x' : Point
29. b' : Point
30. out(j ib')
31. x' # jb'
32. x'jb' ≅a abc
33. abc ≅a ijx'
34. kjx' ≅a def
35. j_j_x'
36. out(j ib')
37. out(j kk)
⊢ b'-j-k
Latex:
Latex:
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. z : Point
11. i : Point
12. j : Point
13. k : Point
14. p : Point
15. p' : Point
16. d' : Point
17. f' : Point
18. abc \mcong{}\msuba{} xyp
19. zyp \mcong{}\msuba{} def
20. y\_p'\_p
21. out(y xd')
22. out(y zf')
23. d'-p'-f'
24. xyz \mcong{}\msuba{} ijk
25. x-y-z
26. a \# bc
27. d \# ef
28. \mexists{}x',b':Point. (out(j ib') \mwedge{} x' \# jb' \mwedge{} x'jb' \mcong{}\msuba{} abc)
\mvdash{} \mexists{}p,p',d',f':Point. (((abc \mcong{}\msuba{} ijp \mwedge{} kjp \mcong{}\msuba{} def) \mwedge{} j\_p'\_p) \mwedge{} (out(j id') \mwedge{} out(j kf')) \mwedge{} d'-p'-f')
By
Latex:
(ExRepD THEN InstConcl [\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{} THEN Auto)
Home
Index