---

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

.....aux..... 
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
⊢ BB'' ≅ BB'
BY
{ (((Assert B(BD'B'') BY Auto) THEN (Assert B(BC'B') BY Auto))
   THEN (InstLemma `geo-add-length-between` [⌜e⌝;⌜B⌝;⌜C⌝;⌜D'⌝]⋅ THENA Auto)
   THEN ((InstLemma `geo-add-length-between` [⌜e⌝;⌜B⌝;⌜D⌝;⌜C'⌝]⋅ THENA Auto)
         THEN (InstLemma `geo-add-length-between` [⌜e⌝;⌜B⌝;⌜D'⌝;⌜B''⌝]⋅ THENA Auto)
         THEN (InstLemma `geo-add-length-between` [⌜e⌝;⌜B⌝;⌜C'⌝;⌜B'⌝]⋅ THENA Auto))
   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
34. B(BD'B'')
35. B(BC'B')
36. |BD'| = |BC| + |CD'| ∈ Length
37. |BC'| = |BD| + |DC'| ∈ Length
38. |BB''| = |BD'| + |D'B''| ∈ Length
39. |BB'| = |BC'| + |C'B'| ∈ Length
⊢ BB'' ≅ BB'

---

Latex:

---

Latex:
.....aux..... 
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')
26.  C'B'  \mcong{}  CB
27.  B''  :  Point
28.  B(AD'B'')
29.  D'B''  \mcong{}  DB
30.  B  \#  C
31.  B  \#  D
32.  B''  \#  D'
33.  BC'  \mcong{}  B''C
\mvdash{}  BB''  \mcong{}  BB'


By

---

Latex:
(((Assert  B(BD'B'')  BY  Auto)  THEN  (Assert  B(BC'B')  BY  Auto))
  THEN  (InstLemma  `geo-add-length-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `geo-add-length-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}C'\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `geo-add-length-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}D'\mkleeneclose{};\mkleeneopen{}B''\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `geo-add-length-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}C'\mkleeneclose{};\mkleeneopen{}B'\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  Auto)

---

Home Index