Step
*
1
1
2
1
1
2
1
of Lemma
geo-between-same-side
1. e : BasicGeometry
2. B' : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. B(ABD)
8. B(ABC)
9. A # B
10. ¬B(ACD)
11. ¬B(ADC)
12. A # D
13. A # C
14. D # C
15. C' : Point
16. B(ADC')
17. DC' ≅ CD
18. D' : Point
19. B(ACD')
20. CD' ≅ CD
21. A # C'
22. A # D'
23. C' # C
24. D' # D
25. B(AC'B')
26. C'B' ≅ CB
27. B(AD'B')
28. D'B' ≅ DB
29. B # C
30. B # D
31. B' # D'
32. BC' ≅ B'C
33. D'C' ≅ DC
34. E : Point
35. B(CEC')
36. B(DED')
37. EC ≅ EC'
38. ED ≅ ED'
⊢ False
BY
{ ((gProveSeparatedWhenStable ⌜C'⌝ ⌜C⌝⋅ THENA Auto) THEN (gProveSeparatedWhenStable ⌜D'⌝ ⌜C⌝⋅ THENA Auto)) }
1
1. e : BasicGeometry
2. B' : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. B(ABD)
8. B(ABC)
9. A # B
10. ¬B(ACD)
11. ¬B(ADC)
12. A # D
13. A # C
14. D # C
15. C' : Point
16. B(ADC')
17. DC' ≅ CD
18. D' : Point
19. B(ACD')
20. CD' ≅ CD
21. A # C'
22. A # D'
23. C' # C
24. D' # D
25. B(AC'B')
26. C'B' ≅ CB
27. B(AD'B')
28. D'B' ≅ DB
29. B # C
30. B # D
31. B' # D'
32. BC' ≅ B'C
33. D'C' ≅ DC
34. E : Point
35. B(CEC')
36. B(DED')
37. EC ≅ EC'
38. ED ≅ ED'
39. C' # C
40. D' # C
⊢ False
Latex:
Latex:
1. e : BasicGeometry
2. B' : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. B(ABD)
8. B(ABC)
9. A \# B
10. \mneg{}B(ACD)
11. \mneg{}B(ADC)
12. A \# D
13. A \# C
14. D \# C
15. C' : Point
16. B(ADC')
17. DC' \mcong{} CD
18. D' : Point
19. B(ACD')
20. CD' \mcong{} CD
21. A \# C'
22. A \# D'
23. C' \# C
24. D' \# D
25. B(AC'B')
26. C'B' \mcong{} CB
27. B(AD'B')
28. D'B' \mcong{} DB
29. B \# C
30. B \# D
31. B' \# D'
32. BC' \mcong{} B'C
33. D'C' \mcong{} DC
34. E : Point
35. B(CEC')
36. B(DED')
37. EC \mcong{} EC'
38. ED \mcong{} ED'
\mvdash{} False
By
Latex:
((gProveSeparatedWhenStable \mkleeneopen{}C'\mkleeneclose{} \mkleeneopen{}C\mkleeneclose{}\mcdot{} THENA Auto)
THEN (gProveSeparatedWhenStable \mkleeneopen{}D'\mkleeneclose{} \mkleeneopen{}C\mkleeneclose{}\mcdot{} THENA Auto)
)
Home
Index