Step
*
1
5
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',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')
BY
{ (ExRepD
THEN (Assert ∃P':Point. ((D'_P'_F ∧ Cong3(D'P'F,f'p'd')) ∧ jp' ≅ jP' ∧ P' ≠ j) BY
(Assert j ≠ p' BY
((InstLemma `out-preserves-lsep` [⌜e⌝;⌜j⌝;⌜i⌝;⌜k⌝;⌜d'⌝;⌜f'⌝]⋅ THENA EAuto 1)
THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜d'⌝;⌜f'⌝;⌜p'⌝]⋅ THENA Auto)
THEN D -1)))
) }
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. 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. j # d'f'
32. d' ≠ p'
⊢ j ≠ p'
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. 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. j # d'f'
32. f' ≠ p'
⊢ j ≠ p'
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. 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. j ≠ p'
⊢ ∃P':Point. ((D'_P'_F ∧ Cong3(D'P'F,f'p'd')) ∧ jp' ≅ jP' ∧ P' ≠ j)
4
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')
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. \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')
\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{}P':Point. ((D'\_P'\_F \mwedge{} Cong3(D'P'F,f'p'd')) \mwedge{} jp' \mcong{} jP' \mwedge{} P' \mneq{} j) BY
(Assert j \mneq{} p' BY
((InstLemma `out-preserves-lsep` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}j\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{}]\mcdot{} THENA EAuto 1)
THEN (InstLemma `geo-sep-or` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}f'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{} THENA Auto)
THEN D -1)))
)
Home
Index