---

Step * 1 1 1 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')
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'
BY
{ (BLemma `geo-congruent-iff-length` 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'| ∈ Length

---

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')
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
34.  B(BD'B'')
35.  B(BC'B')
36.  |BD'|  =  |BC|  +  |CD'|
37.  |BC'|  =  |BD|  +  |DC'|
38.  |BB''|  =  |BD'|  +  |D'B''|
39.  |BB'|  =  |BC'|  +  |C'B'|
\mvdash{}  BB''  \mcong{}  BB'


By

---

Latex:
(BLemma  `geo-congruent-iff-length`  THEN  Auto)

---

Home Index