Step
*
1
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. ¬out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc ≅a dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. ¬B(dep1)
21. B(x1p2z1)
22. p2 # z1
23. ¬out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def ≅a xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. ¬B(xyp)
33. B(x'p'z')
34. p' # z'
35. a # bc
36. d # ef
37. x # yz
38. x' # yz'
39. out(y pp')
40. x' # p'
41. p' # yx'
42. ∃x2,z2:Point. (((out(y x2x') ∧ out(y z2p')) ∧ Cong3(x2yz2,x1ez1)) ∧ x2 # yz2)
43. z1 # x1e
44. e # p2
⊢ (¬out(y xz))
∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ B(yp'p) ∧ (out(y xx') ∧ out(y zz')) ∧ (¬B(xyp)) ∧ B(x'p'z') ∧ p' # z'))
BY
{ (ExRepD
THEN (Assert ∃p'':Point. ((Cong3(x2p''z2,x1p2z1) ∧ yp'' ≅ ep2 ∧ y # p'') ∧ x2-p''-z2) BY
(((D -4 THEN InstLemma `geo-congruent-between-exists` [⌜g⌝;⌜z1⌝;⌜p2⌝;⌜x1⌝;⌜z2⌝;⌜x2⌝]⋅ THEN Auto)
THEN ExRepD
)
THEN D 0 With ⌜b'⌝
THEN Auto))
) }
1
.....aux.....
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. ¬out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc ≅a dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. ¬B(dep1)
21. B(x1p2z1)
22. p2 # z1
23. ¬out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def ≅a xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. ¬B(xyp)
33. B(x'p'z')
34. p' # z'
35. a # bc
36. d # ef
37. x # yz
38. x' # yz'
39. out(y pp')
40. x' # p'
41. p' # yx'
42. x2 : Point
43. z2 : Point
44. out(y x2x')
45. out(y z2p')
46. x2y ≅ x1e
47. yz2 ≅ ez1
48. z2x2 ≅ z1x1
49. x2 # yz2
50. z1 # x1e
51. e # p2
52. b' : Point
53. B(z2b'x2)
54. z1p2 ≅ z2b'
55. p2x1 ≅ b'x2
⊢ Cong3(x2b'z2,x1p2z1)
2
.....aux.....
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. ¬out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc ≅a dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. ¬B(dep1)
21. B(x1p2z1)
22. p2 # z1
23. ¬out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def ≅a xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. ¬B(xyp)
33. B(x'p'z')
34. p' # z'
35. a # bc
36. d # ef
37. x # yz
38. x' # yz'
39. out(y pp')
40. x' # p'
41. p' # yx'
42. x2 : Point
43. z2 : Point
44. out(y x2x')
45. out(y z2p')
46. x2y ≅ x1e
47. yz2 ≅ ez1
48. z2x2 ≅ z1x1
49. x2 # yz2
50. z1 # x1e
51. e # p2
52. b' : Point
53. B(z2b'x2)
54. z1p2 ≅ z2b'
55. p2x1 ≅ b'x2
56. Cong3(x2b'z2,x1p2z1)
⊢ yb' ≅ ep2
3
.....aux.....
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. ¬out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc ≅a dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. ¬B(dep1)
21. B(x1p2z1)
22. p2 # z1
23. ¬out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def ≅a xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. ¬B(xyp)
33. B(x'p'z')
34. p' # z'
35. a # bc
36. d # ef
37. x # yz
38. x' # yz'
39. out(y pp')
40. x' # p'
41. p' # yx'
42. x2 : Point
43. z2 : Point
44. out(y x2x')
45. out(y z2p')
46. x2y ≅ x1e
47. yz2 ≅ ez1
48. z2x2 ≅ z1x1
49. x2 # yz2
50. z1 # x1e
51. e # p2
52. b' : Point
53. B(z2b'x2)
54. z1p2 ≅ z2b'
55. p2x1 ≅ b'x2
56. Cong3(x2b'z2,x1p2z1)
57. yb' ≅ ep2
58. y # b'
⊢ x2-b'-z2
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. ¬out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc ≅a dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. ¬B(dep1)
21. B(x1p2z1)
22. p2 # z1
23. ¬out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def ≅a xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. ¬B(xyp)
33. B(x'p'z')
34. p' # z'
35. a # bc
36. d # ef
37. x # yz
38. x' # yz'
39. out(y pp')
40. x' # p'
41. p' # yx'
42. x2 : Point
43. z2 : Point
44. out(y x2x')
45. out(y z2p')
46. Cong3(x2yz2,x1ez1)
47. x2 # yz2
48. z1 # x1e
49. e # p2
50. ∃p'':Point. ((Cong3(x2p''z2,x1p2z1) ∧ yp'' ≅ ep2 ∧ y # p'') ∧ x2-p''-z2)
⊢ (¬out(y xz))
∧ (∃p,p',x',z':Point. (abc ≅a xyp ∧ B(yp'p) ∧ (out(y xx') ∧ out(y zz')) ∧ (¬B(xyp)) ∧ B(x'p'z') ∧ p' # z'))
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. \mneg{}out(e df)
12. p1 : Point
13. p2 : Point
14. x1 : Point
15. z1 : Point
16. abc \mcong{}\msuba{} dep1
17. B(ep2p1)
18. out(e dx1)
19. out(e fz1)
20. \mneg{}B(dep1)
21. B(x1p2z1)
22. p2 \# z1
23. \mneg{}out(y xz)
24. p : Point
25. p' : Point
26. x' : Point
27. z' : Point
28. def \mcong{}\msuba{} xyp
29. B(yp'p)
30. out(y xx')
31. out(y zz')
32. \mneg{}B(xyp)
33. B(x'p'z')
34. p' \# z'
35. a \# bc
36. d \# ef
37. x \# yz
38. x' \# yz'
39. out(y pp')
40. x' \# p'
41. p' \# yx'
42. \mexists{}x2,z2:Point. (((out(y x2x') \mwedge{} out(y z2p')) \mwedge{} Cong3(x2yz2,x1ez1)) \mwedge{} x2 \# yz2)
43. z1 \# x1e
44. e \# p2
\mvdash{} (\mneg{}out(y xz))
\mwedge{} (\mexists{}p,p',x',z':Point
(abc \mcong{}\msuba{} xyp \mwedge{} B(yp'p) \mwedge{} (out(y xx') \mwedge{} out(y zz')) \mwedge{} (\mneg{}B(xyp)) \mwedge{} B(x'p'z') \mwedge{} p' \# z'))
By
Latex:
(ExRepD
THEN (Assert \mexists{}p'':Point. ((Cong3(x2p''z2,x1p2z1) \mwedge{} yp'' \mcong{} ep2 \mwedge{} y \# p'') \mwedge{} x2-p''-z2) BY
(((D -4
THEN InstLemma `geo-congruent-between-exists` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}z1\mkleeneclose{};\mkleeneopen{}p2\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}z2\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{}]\mcdot{}
THEN Auto)
THEN ExRepD
)
THEN D 0 With \mkleeneopen{}b'\mkleeneclose{}
THEN Auto))
)
Home
Index