---

Step * 1 of Lemma geo-between-same-side


1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. B(ABD)
7. B(ABC)
8. A # B
9. ¬B(ACD)
10. ¬B(ADC)
11. A # D
12. A # C
13. D # C
14. C' : Point
15. B(ADC')
16. DC' ≅ CD
17. D' : Point
18. B(ACD')
19. CD' ≅ CD
20. A # C'
21. A # D'
22. C' # C
23. D' # D
24. B' : Point
25. B(AC'B') ∧ C'B' ≅ CB
26. B'' : Point
27. B(AD'B'') ∧ D'B'' ≅ DB
⊢ False
BY
{ (ExRepD
   THEN (gProveSeparatedWhenStable ⌜B⌝ ⌜C⌝⋅ THENA Auto)
   THEN (gProveSeparatedWhenStable ⌜B⌝ ⌜D⌝⋅ THENA Auto)
   THEN (gProveSeparatedWhenStable ⌜B''⌝ ⌜D'⌝⋅ THENA Auto)
   THEN (Assert BC' ≅ B''C BY
               ((Assert B(BDC') BY
                       Auto)
                THEN (Assert B(B''D'C) BY
                            Auto)
                THEN FLemma `geo-three-segment` [-1;-2]
                THEN Auto))) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. B(ABD)
7. B(ABC)
8. A # B
9. ¬B(ACD)
10. ¬B(ADC)
11. A # D
12. A # C
13. D # C
14. C' : Point
15. B(ADC')
16. DC' ≅ CD
17. D' : Point
18. B(ACD')
19. CD' ≅ CD
20. A # C'
21. A # D'
22. C' # C
23. D' # D
24. B' : Point
25. B(AC'B')
26. C'B' ≅ CB
27. B'' : Point
28. B(AD'B'')
29. D'B'' ≅ DB
30. B # C
31. B # D
32. B'' # D'
33. BC' ≅ B''C
⊢ False

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  D  :  Point
6.  B(ABD)
7.  B(ABC)
8.  A  \#  B
9.  \mneg{}B(ACD)
10.  \mneg{}B(ADC)
11.  A  \#  D
12.  A  \#  C
13.  D  \#  C
14.  C'  :  Point
15.  B(ADC')
16.  DC'  \mcong{}  CD
17.  D'  :  Point
18.  B(ACD')
19.  CD'  \mcong{}  CD
20.  A  \#  C'
21.  A  \#  D'
22.  C'  \#  C
23.  D'  \#  D
24.  B'  :  Point
25.  B(AC'B')  \mwedge{}  C'B'  \mcong{}  CB
26.  B''  :  Point
27.  B(AD'B'')  \mwedge{}  D'B''  \mcong{}  DB
\mvdash{}  False


By

---

Latex:
(ExRepD
  THEN  (gProveSeparatedWhenStable  \mkleeneopen{}B\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProveSeparatedWhenStable  \mkleeneopen{}B\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProveSeparatedWhenStable  \mkleeneopen{}B''\mkleeneclose{}  \mkleeneopen{}D'\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  BC'  \mcong{}  B''C  BY
                          ((Assert  B(BDC')  BY
                                          Auto)
                            THEN  (Assert  B(B''D'C)  BY
                                                    Auto)
                            THEN  FLemma  `geo-three-segment`  [-1;-2]
                            THEN  Auto)))

---

Home Index