Step
*
1
5
4
2
1
of Lemma
hp-angle-sum-symm
.....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. 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
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ d'jp' ≅a FjP'
BY
{ (Unfold `geo-cong-angle` 0 THEN GenRepD) }
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. 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
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ d' ≠ j
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. 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
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ j ≠ p'
3
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
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ F ≠ 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
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ j ≠ P'
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' : 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
32. D'_P'_F
33. Cong3(D'P'F,f'p'd')
34. jp' ≅ jP'
35. P' ≠ j
36. xyz ≅a ijP'
37. ijp ≅a d'jp'
38. d'jp' ≅a abc
⊢ ∃a',c',x',z':Point. (j_d'_a' ∧ j_p'_c' ∧ j_F_x' ∧ j_P'_z' ∧ ja' ≅ jx' ∧ jc' ≅ jz' ∧ a'c' ≅ x'z')
Latex:
Latex:
.....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. 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. D' : Point
23. F : Point
24. out(j iD')
25. out(j kF)
26. D'jF \mcong{}\msuba{} f'jd'
27. D'F \mcong{} d'f'
28. D' \mneq{} F
29. jD' \mcong{} jf'
30. jF \mcong{} jd'
31. P' : Point
32. D'\_P'\_F
33. Cong3(D'P'F,f'p'd')
34. jp' \mcong{} jP'
35. P' \mneq{} j
36. xyz \mcong{}\msuba{} ijP'
37. ijp \mcong{}\msuba{} d'jp'
38. d'jp' \mcong{}\msuba{} abc
\mvdash{} d'jp' \mcong{}\msuba{} FjP'
By
Latex:
(Unfold `geo-cong-angle` 0 THEN GenRepD)
Home
Index