---

Step * 1 1 2 1 1 2 1 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'
39. C' # C
40. D' # C
⊢ False
BY
{ ((gProlong ⌜C'⌝ ⌜C⌝ `P' ⌜C⌝ ⌜D'⌝⋅ THENA Auto) THEN (gProlong ⌜D'⌝ ⌜C⌝ `R' ⌜C⌝ ⌜E⌝⋅ 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
41. P : Point
42. B(C'CP) ∧ CP ≅ CD'
43. R : Point
44. B(D'CR) ∧ CR ≅ CE
⊢ 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'
39.  C'  \#  C
40.  D'  \#  C
\mvdash{}  False


By

---

Latex:
((gProlong  \mkleeneopen{}C'\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}  `P'  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}D'\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (gProlong  \mkleeneopen{}D'\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}  `R'  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}E\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index