---

Step * 1 1 2 1 1 2 1 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
41. P : Point
42. B(C'CP) ∧ CP ≅ CD'
43. R : Point
44. B(D'CR) ∧ CR ≅ CE
⊢ False
BY
{ ((Assert D'R ≅ PE BY
          (Using [`B',⌜C⌝; `b', ⌜C⌝] (BLemma `geo-three-segment`)⋅ THEN Auto))
   THEN (InstLemma `geo-colinear-five-segment` [⌜e⌝; ⌜D'⌝; ⌜C⌝; ⌜R⌝; ⌜P⌝; ⌜P⌝;⌜C⌝; ⌜E⌝; ⌜D'⌝]⋅ THENA EAuto 1)
   ) }

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
45. D'R ≅ PE
46. RP ≅ ED'
⊢ 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
41.  P  :  Point
42.  B(C'CP)  \mwedge{}  CP  \mcong{}  CD'
43.  R  :  Point
44.  B(D'CR)  \mwedge{}  CR  \mcong{}  CE
\mvdash{}  False


By

---

Latex:
((Assert  D'R  \mcong{}  PE  BY
                (Using  [`B',\mkleeneopen{}C\mkleeneclose{};  `b',  \mkleeneopen{}C\mkleeneclose{}]  (BLemma  `geo-three-segment`)\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `geo-colinear-five-segment`  [\mkleeneopen{}e\mkleeneclose{};  \mkleeneopen{}D'\mkleeneclose{};  \mkleeneopen{}C\mkleeneclose{};  \mkleeneopen{}R\mkleeneclose{};  \mkleeneopen{}P\mkleeneclose{};  \mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};  \mkleeneopen{}E\mkleeneclose{};  \mkleeneopen{}D'\mkleeneclose{}]\mcdot{}
              THENA  EAuto  1
              )
  )

---

Home Index