Step
*
1
1
1
1
1
of Lemma
ip-five-segment-lemma
1. rv : InnerProductSpace
2. A : Point(rv)
3. B : Point(rv)
4. C : Point(rv)
5. D : Point(rv)
6. t : ℝ
7. r0 < t
8. t < r1
9. B ≡ t*A + r1 - t*C
10. (t - r1) < r0
11. D - C ≡ D - B + B - C
12. A - D ≡ A - B - D - B
13. BD : Point(rv)
14. D - B = BD ∈ Point(rv)
15. CB : Point(rv)
16. B - C = CB ∈ Point(rv)
17. (((A - B^2 - r(2) * A - B ⋅ BD) + BD^2) - ((A^2 - r(2) * A ⋅ B) + B^2) + BD^2) = -(r(2) * A - B ⋅ BD)
⊢ ((BD^2 + (r(2) * BD ⋅ CB)) + CB^2)
= (CB^2 + BD^2 + ((t/t - r1) * (((A - B^2 - r(2) * A - B ⋅ BD) + BD^2) - ((A^2 - r(2) * A ⋅ B) + B^2) + BD^2)))
BY
{ (RWO "-1" 0 THENA Auto) }
1
1. rv : InnerProductSpace
2. A : Point(rv)
3. B : Point(rv)
4. C : Point(rv)
5. D : Point(rv)
6. t : ℝ
7. r0 < t
8. t < r1
9. B ≡ t*A + r1 - t*C
10. (t - r1) < r0
11. D - C ≡ D - B + B - C
12. A - D ≡ A - B - D - B
13. BD : Point(rv)
14. D - B = BD ∈ Point(rv)
15. CB : Point(rv)
16. B - C = CB ∈ Point(rv)
17. (((A - B^2 - r(2) * A - B ⋅ BD) + BD^2) - ((A^2 - r(2) * A ⋅ B) + B^2) + BD^2) = -(r(2) * A - B ⋅ BD)
⊢ ((BD^2 + (r(2) * BD ⋅ CB)) + CB^2) = (CB^2 + BD^2 + ((t/t - r1) * -(r(2) * A - B ⋅ BD)))
Latex:
Latex:
1. rv : InnerProductSpace
2. A : Point(rv)
3. B : Point(rv)
4. C : Point(rv)
5. D : Point(rv)
6. t : \mBbbR{}
7. r0 < t
8. t < r1
9. B \mequiv{} t*A + r1 - t*C
10. (t - r1) < r0
11. D - C \mequiv{} D - B + B - C
12. A - D \mequiv{} A - B - D - B
13. BD : Point(rv)
14. D - B = BD
15. CB : Point(rv)
16. B - C = CB
17. (((A - B\^{}2 - r(2) * A - B \mcdot{} BD) + BD\^{}2) - ((A\^{}2 - r(2) * A \mcdot{} B) + B\^{}2) + BD\^{}2)
= -(r(2) * A - B \mcdot{} BD)
\mvdash{} ((BD\^{}2 + (r(2) * BD \mcdot{} CB)) + CB\^{}2)
= (CB\^{}2
+ BD\^{}2
+ ((t/t - r1) * (((A - B\^{}2 - r(2) * A - B \mcdot{} BD) + BD\^{}2) - ((A\^{}2 - r(2) * A \mcdot{} B) + B\^{}2) + BD\^{}2)))
By
Latex:
(RWO "-1" 0 THENA Auto)
Home
Index