Step
*
1
1
1
1
4
2
1
1
1
of Lemma
geo-lt-angle-trans
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. p1 : Point
12. p2 : Point
13. x1 : Point
14. z1 : Point
15. abc ≅a dep1
16. B(ep2p1)
17. out(e dx1)
18. out(e fz1)
19. ¬B(dep1)
20. B(x1p2z1)
21. p2 # z1
22. p : Point
23. p' : Point
24. x' : Point
25. z' : Point
26. def ≅a xyp
27. B(yp'p)
28. out(y xx')
29. out(y zz')
30. ¬B(xyp)
31. B(x'p'z')
32. p' # z'
33. a # bc
34. d # ef
35. x # yz
36. x' # yz'
37. out(y pp')
38. x' # p'
39. p' # yx'
40. x2 : Point
41. z2 : Point
42. out(y x2x')
43. out(y z2p')
44. Cong3(x2yz2,x1ez1)
45. x2 # yz2
46. z1 # x1e
47. e # p2
48. p'' : Point
49. Cong3(x2p''z2,x1p2z1)
50. yp'' ≅ ep2
51. y # p''
52. x2-p''-z2
53. P : Point
54. x'-P-p'
55. out(y p''P)
56. x2yp'' ≅a x'yP
57. z2yp'' ≅a p'yP
⊢ abc ≅a xyP
BY
{ ((Assert xyP ≅a x2yp'' BY
((InstLemma `out-cong-angle` [⌜g⌝;⌜x⌝;⌜y⌝;⌜P⌝;⌜x'⌝;⌜P⌝]⋅ THENA EAuto 1)
THEN (InstLemma `out-cong-angle` [⌜g⌝;⌜x'⌝;⌜y⌝;⌜P⌝;⌜x'⌝;⌜p''⌝]⋅ THENA EAuto 1)
THEN (InstLemma `out-cong-angle` [⌜g⌝;⌜x'⌝;⌜y⌝;⌜p''⌝;⌜x2⌝;⌜p''⌝]⋅ THENA EAuto 1)
THEN (FLemma `geo-cong-angle-transitivity` [-3;-2] THENA Auto)
THEN FLemma `geo-cong-angle-transitivity` [-1;-2]
THEN Auto))
THEN (Enough to prove abc ≅a x2yp''
Because (Lemmaize [-2;-1] THEN Auto THEN EasyGeometry))
) }
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. p1 : Point
12. p2 : Point
13. x1 : Point
14. z1 : Point
15. abc ≅a dep1
16. B(ep2p1)
17. out(e dx1)
18. out(e fz1)
19. ¬B(dep1)
20. B(x1p2z1)
21. p2 # z1
22. p : Point
23. p' : Point
24. x' : Point
25. z' : Point
26. def ≅a xyp
27. B(yp'p)
28. out(y xx')
29. out(y zz')
30. ¬B(xyp)
31. B(x'p'z')
32. p' # z'
33. a # bc
34. d # ef
35. x # yz
36. x' # yz'
37. out(y pp')
38. x' # p'
39. p' # yx'
40. x2 : Point
41. z2 : Point
42. out(y x2x')
43. out(y z2p')
44. Cong3(x2yz2,x1ez1)
45. x2 # yz2
46. z1 # x1e
47. e # p2
48. p'' : Point
49. Cong3(x2p''z2,x1p2z1)
50. yp'' ≅ ep2
51. y # p''
52. x2-p''-z2
53. P : Point
54. x'-P-p'
55. out(y p''P)
56. x2yp'' ≅a x'yP
57. z2yp'' ≅a p'yP
58. xyP ≅a x2yp''
⊢ abc ≅a x2yp''
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. p1 : Point
12. p2 : Point
13. x1 : Point
14. z1 : Point
15. abc \mcong{}\msuba{} dep1
16. B(ep2p1)
17. out(e dx1)
18. out(e fz1)
19. \mneg{}B(dep1)
20. B(x1p2z1)
21. p2 \# z1
22. p : Point
23. p' : Point
24. x' : Point
25. z' : Point
26. def \mcong{}\msuba{} xyp
27. B(yp'p)
28. out(y xx')
29. out(y zz')
30. \mneg{}B(xyp)
31. B(x'p'z')
32. p' \# z'
33. a \# bc
34. d \# ef
35. x \# yz
36. x' \# yz'
37. out(y pp')
38. x' \# p'
39. p' \# yx'
40. x2 : Point
41. z2 : Point
42. out(y x2x')
43. out(y z2p')
44. Cong3(x2yz2,x1ez1)
45. x2 \# yz2
46. z1 \# x1e
47. e \# p2
48. p'' : Point
49. Cong3(x2p''z2,x1p2z1)
50. yp'' \mcong{} ep2
51. y \# p''
52. x2-p''-z2
53. P : Point
54. x'-P-p'
55. out(y p''P)
56. x2yp'' \mcong{}\msuba{} x'yP
57. z2yp'' \mcong{}\msuba{} p'yP
\mvdash{} abc \mcong{}\msuba{} xyP
By
Latex:
((Assert xyP \mcong{}\msuba{} x2yp'' BY
((InstLemma `out-cong-angle` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{} THENA EAuto 1)
THEN (InstLemma `out-cong-angle` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}p''\mkleeneclose{}]\mcdot{} THENA EAuto 1)
THEN (InstLemma `out-cong-angle` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p''\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}p''\mkleeneclose{}]\mcdot{} THENA EAuto 1)
THEN (FLemma `geo-cong-angle-transitivity` [-3;-2] THENA Auto)
THEN FLemma `geo-cong-angle-transitivity` [-1;-2]
THEN Auto))
THEN (Enough to prove abc \mcong{}\msuba{} x2yp''
Because (Lemmaize [-2;-1] THEN Auto THEN EasyGeometry))
)
Home
Index