Step
*
1
1
2
1
2
1
of Lemma
real-vec-between-inner-trans
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : ℝ^n
6. s : ℝ
7. s ∈ (r0, r1)
8. req-vec(n;b;s*a + r1 - s*d)
9. t : ℝ
10. t ∈ (r0, r1)
11. r0 < (t * s)
12. (t * s) < r1
13. (s - t * s/r1 - t * s) ∈ (r0, r1)
14. i : ℕn
15. v : ℝ
16. (r1 - t * s) = v ∈ ℝ
17. r0 < v
18. (c i) = ((t * ((s * (a i)) + ((r1 - s) * (d i)))) + ((r1 - t) * (d i)))
19. v1 : ℝ
20. (a i) = v1 ∈ ℝ
21. v2 : ℝ
22. (d i) = v2 ∈ ℝ
⊢ ((s * v1) + ((r1 - s) * v2))
= (((s - t * s/v) * v1) + ((r1 - (s - t * s/v)) * ((t * ((s * v1) + ((r1 - s) * v2))) + ((r1 - t) * v2))))
BY
{ (GenConclTerm ⌜(s - t * s/v)⌝⋅ THENA Auto) }
1
1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. d : ℝ^n
6. s : ℝ
7. s ∈ (r0, r1)
8. req-vec(n;b;s*a + r1 - s*d)
9. t : ℝ
10. t ∈ (r0, r1)
11. r0 < (t * s)
12. (t * s) < r1
13. (s - t * s/r1 - t * s) ∈ (r0, r1)
14. i : ℕn
15. v : ℝ
16. (r1 - t * s) = v ∈ ℝ
17. r0 < v
18. (c i) = ((t * ((s * (a i)) + ((r1 - s) * (d i)))) + ((r1 - t) * (d i)))
19. v1 : ℝ
20. (a i) = v1 ∈ ℝ
21. v2 : ℝ
22. (d i) = v2 ∈ ℝ
23. v3 : ℝ
24. (s - t * s/v) = v3 ∈ ℝ
⊢ ((s * v1) + ((r1 - s) * v2)) = ((v3 * v1) + ((r1 - v3) * ((t * ((s * v1) + ((r1 - s) * v2))) + ((r1 - t) * v2))))
Latex:
Latex:
1. n : \mBbbN{}
2. a : \mBbbR{}\^{}n
3. b : \mBbbR{}\^{}n
4. c : \mBbbR{}\^{}n
5. d : \mBbbR{}\^{}n
6. s : \mBbbR{}
7. s \mmember{} (r0, r1)
8. req-vec(n;b;s*a + r1 - s*d)
9. t : \mBbbR{}
10. t \mmember{} (r0, r1)
11. r0 < (t * s)
12. (t * s) < r1
13. (s - t * s/r1 - t * s) \mmember{} (r0, r1)
14. i : \mBbbN{}n
15. v : \mBbbR{}
16. (r1 - t * s) = v
17. r0 < v
18. (c i) = ((t * ((s * (a i)) + ((r1 - s) * (d i)))) + ((r1 - t) * (d i)))
19. v1 : \mBbbR{}
20. (a i) = v1
21. v2 : \mBbbR{}
22. (d i) = v2
\mvdash{} ((s * v1) + ((r1 - s) * v2))
= (((s - t * s/v) * v1)
+ ((r1 - (s - t * s/v)) * ((t * ((s * v1) + ((r1 - s) * v2))) + ((r1 - t) * v2))))
By
Latex:
(GenConclTerm \mkleeneopen{}(s - t * s/v)\mkleeneclose{}\mcdot{} THENA Auto)
Home
Index