Step
*
1
1
1
1
5
1
1
1
of Lemma
interior-angles-unique
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. a # bc
10. out(b dc)
11. out(a bb')
12. out(a cc')
13. B(b'pc')
14. p # c'
15. bad < bac
16. b # a
17. a # p
18. b # a
19. a # d
20. a' : Point
21. c1 : Point
22. x' : Point
23. z' : Point
24. B(aba')
25. B(apc1)
26. B(abx')
27. B(adz')
28. aa' ≅ ax'
29. ac1 ≅ az'
30. a'c1 ≅ x'z'
31. a # p
32. b # p
33. b' # p
34. b # ap
35. a' ≡ x'
36. p leftof ab
37. d leftof ab
⊢ ¬((¬B(adp)) ∧ (¬B(apd)))
BY
{ ((EliminatePoint (-3) THEN Auto) THEN (InstLemma `Euclid-Prop7` [⌜e⌝;⌜a⌝;⌜x'⌝;⌜c1⌝;⌜z'⌝]⋅ THENA Auto)) }
1
.....wf.....
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. a # bc
10. out(b dc)
11. out(a bb')
12. out(a cc')
13. B(b'pc')
14. p # c'
15. bad < bac
16. b # a
17. a # p
18. b # a
19. a # d
20. a' : Point
21. c1 : Point
22. x' : Point
23. z' : Point
24. B(abx')
25. B(apc1)
26. B(abx')
27. B(adz')
28. ax' ≅ ax'
29. ac1 ≅ az'
30. x'c1 ≅ x'z'
31. a # p
32. b # p
33. b' # p
34. b # ap
35. a' ≡ x'
36. p leftof ab
37. d leftof ab
⊢ c1 ∈ {c:Point| c leftof ax'}
2
.....wf.....
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. a # bc
10. out(b dc)
11. out(a bb')
12. out(a cc')
13. B(b'pc')
14. p # c'
15. bad < bac
16. b # a
17. a # p
18. b # a
19. a # d
20. a' : Point
21. c1 : Point
22. x' : Point
23. z' : Point
24. B(abx')
25. B(apc1)
26. B(abx')
27. B(adz')
28. ax' ≅ ax'
29. ac1 ≅ az'
30. x'c1 ≅ x'z'
31. a # p
32. b # p
33. b' # p
34. b # ap
35. a' ≡ x'
36. p leftof ab
37. d leftof ab
⊢ z' ∈ {p:Point| p leftof ax'}
3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. a # bc
10. out(b dc)
11. out(a bb')
12. out(a cc')
13. B(b'pc')
14. p # c'
15. bad < bac
16. b # a
17. a # p
18. b # a
19. a # d
20. a' : Point
21. c1 : Point
22. x' : Point
23. z' : Point
24. B(abx')
25. B(apc1)
26. B(abx')
27. B(adz')
28. ax' ≅ ax'
29. ac1 ≅ az'
30. x'c1 ≅ x'z'
31. a # p
32. b # p
33. b' # p
34. b # ap
35. a' ≡ x'
36. p leftof ab
37. d leftof ab
38. c1 ≡ z'
⊢ ¬((¬B(adp)) ∧ (¬B(apd)))
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. a \# bc
10. out(b dc)
11. out(a bb')
12. out(a cc')
13. B(b'pc')
14. p \# c'
15. bad < bac
16. b \# a
17. a \# p
18. b \# a
19. a \# d
20. a' : Point
21. c1 : Point
22. x' : Point
23. z' : Point
24. B(aba')
25. B(apc1)
26. B(abx')
27. B(adz')
28. aa' \mcong{} ax'
29. ac1 \mcong{} az'
30. a'c1 \mcong{} x'z'
31. a \# p
32. b \# p
33. b' \# p
34. b \# ap
35. a' \mequiv{} x'
36. p leftof ab
37. d leftof ab
\mvdash{} \mneg{}((\mneg{}B(adp)) \mwedge{} (\mneg{}B(apd)))
By
Latex:
((EliminatePoint (-3) THEN Auto)
THEN (InstLemma `Euclid-Prop7` [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{} THENA Auto)
)
Home
Index