---

Step * 1 1 2 1 1 2 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')
⊢ False
BY
{ ((Assert EC ≅ EC' BY
          (Using [`C', ⌜D⌝ ; `A', ⌜D'⌝ ; `c', ⌜D⌝; `a', ⌜D'⌝ ] (BLemma `geo-inner-five-segment`) ⋅ THEN Auto))
   THEN (Assert ED ≅ ED' BY
               (Using [`C', ⌜C⌝ ; `A', ⌜C'⌝ ; `c', ⌜C⌝; `a', ⌜C'⌝ ] (BLemma `geo-inner-five-segment`) ⋅ THEN 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'
⊢ 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')
\mvdash{}  False


By

---

Latex:
((Assert  EC  \mcong{}  EC'  BY
                (Using  [`C',  \mkleeneopen{}D\mkleeneclose{}  ;  `A',  \mkleeneopen{}D'\mkleeneclose{}  ;  `c',  \mkleeneopen{}D\mkleeneclose{};  `a',  \mkleeneopen{}D'\mkleeneclose{}  ]  (BLemma  `geo-inner-five-segment`)  \mcdot{}
                  THEN  Auto
                  ))
  THEN  (Assert  ED  \mcong{}  ED'  BY
                          (Using  [`C',  \mkleeneopen{}C\mkleeneclose{}  ;  `A',  \mkleeneopen{}C'\mkleeneclose{}  ;  `c',  \mkleeneopen{}C\mkleeneclose{};  `a',  \mkleeneopen{}C'\mkleeneclose{}  ]  (BLemma  `geo-inner-five-segment`) 
                            \mcdot{}
                            THEN  Auto
                            ))
  )

---

Home Index