Step
*
1
2
1
1
1
1
1
1
1
of Lemma
rv-circle-circle-lemma2
1. n : {2...}
2. r1 : {r:ℝ| r0 ≤ r}
3. r2 : {r:ℝ| r0 ≤ r}
4. b : ℝ^n
5. r0 < ||b||
6. b' : ℝ^n
7. b⋅b' = r0
8. ||b'|| = ||b||
9. (r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2)
10. cc : ℝ
11. ((r1^2 - r2^2) + ||b||^2) = cc ∈ ℝ
12. r0 ≤ ((||b||^2 * r1^2) - (cc/r(2))^2)
13. r0 < ||b||^2
14. v : {r:ℝ| (r0 ≤ r) ∧ ((r * r) = ((||b||^2 * r1^2) - (cc/r(2))^2))}
15. rsqrt((||b||^2 * r1^2) - (cc/r(2))^2) = v ∈ {r:ℝ| (r0 ≤ r) ∧ ((r * r) = ((||b||^2 * r1^2) - (cc/r(2))^2))}
16. ∀x:ℝ^n
((req-vec(n;x;(r1/||b||^2)*(cc/r(2))*b + v*b') ∨ req-vec(n;x;(r1/||b||^2)*(cc/r(2))*b - v*b'))
⇒ ((||x|| = r1) ∧ (||x - b|| = r2)))
17. ||(r1/||b||^2)*(cc/r(2))*b + v*b'|| = r1
18. ||(r1/||b||^2)*(cc/r(2))*b + v*b' - b|| = r2
19. ||(r1/||b||^2)*(cc/r(2))*b - v*b'|| = r1
20. ||(r1/||b||^2)*(cc/r(2))*b - v*b' - b|| = r2
21. ||(r1/||b||^2)*(cc/r(2))*b + v*b'|| = r1
22. ||(r1/||b||^2)*(cc/r(2))*b + v*b' - b|| = r2
23. ||(r1/||b||^2)*(cc/r(2))*b - v*b'|| = r1
24. ||(r1/||b||^2)*(cc/r(2))*b - v*b' - b|| = r2
25. cc^2 < (r(4) * ||b||^2 * r1^2)
26. M : ℝ
27. (r1/||b||^2) = M ∈ ℝ
28. r0 < M
29. req-vec(n;M*(cc/r(2))*b + v*b' - M*(cc/r(2))*b - v*b';(r(2) * M) * v*b')
⊢ r0 < ||(r(2) * M) * v*b'||
BY
{ ((RWO "real-vec-norm-mul" 0 THENA Auto) THEN (BLemma `rmul-is-positive` THENM OrLeft) THEN Auto) }
1
1. n : {2...}
2. r1 : {r:ℝ| r0 ≤ r}
3. r2 : {r:ℝ| r0 ≤ r}
4. b : ℝ^n
5. r0 < ||b||
6. b' : ℝ^n
7. b⋅b' = r0
8. ||b'|| = ||b||
9. (r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2)
10. cc : ℝ
11. ((r1^2 - r2^2) + ||b||^2) = cc ∈ ℝ
12. r0 ≤ ((||b||^2 * r1^2) - (cc/r(2))^2)
13. r0 < ||b||^2
14. v : {r:ℝ| (r0 ≤ r) ∧ ((r * r) = ((||b||^2 * r1^2) - (cc/r(2))^2))}
15. rsqrt((||b||^2 * r1^2) - (cc/r(2))^2) = v ∈ {r:ℝ| (r0 ≤ r) ∧ ((r * r) = ((||b||^2 * r1^2) - (cc/r(2))^2))}
16. ∀x:ℝ^n
((req-vec(n;x;(r1/||b||^2)*(cc/r(2))*b + v*b') ∨ req-vec(n;x;(r1/||b||^2)*(cc/r(2))*b - v*b'))
⇒ ((||x|| = r1) ∧ (||x - b|| = r2)))
17. ||(r1/||b||^2)*(cc/r(2))*b + v*b'|| = r1
18. ||(r1/||b||^2)*(cc/r(2))*b + v*b' - b|| = r2
19. ||(r1/||b||^2)*(cc/r(2))*b - v*b'|| = r1
20. ||(r1/||b||^2)*(cc/r(2))*b - v*b' - b|| = r2
21. ||(r1/||b||^2)*(cc/r(2))*b + v*b'|| = r1
22. ||(r1/||b||^2)*(cc/r(2))*b + v*b' - b|| = r2
23. ||(r1/||b||^2)*(cc/r(2))*b - v*b'|| = r1
24. ||(r1/||b||^2)*(cc/r(2))*b - v*b' - b|| = r2
25. cc^2 < (r(4) * ||b||^2 * r1^2)
26. M : ℝ
27. (r1/||b||^2) = M ∈ ℝ
28. r0 < M
29. req-vec(n;M*(cc/r(2))*b + v*b' - M*(cc/r(2))*b - v*b';(r(2) * M) * v*b')
⊢ r0 < |(r(2) * M) * v|
Latex:
Latex:
1. n : \{2...\}
2. r1 : \{r:\mBbbR{}| r0 \mleq{} r\}
3. r2 : \{r:\mBbbR{}| r0 \mleq{} r\}
4. b : \mBbbR{}\^{}n
5. r0 < ||b||
6. b' : \mBbbR{}\^{}n
7. b\mcdot{}b' = r0
8. ||b'|| = ||b||
9. (r1\^{}2 - r2\^{}2) + ||b||\^{}2\^{}2 \mleq{} (r(4) * ||b||\^{}2 * r1\^{}2)
10. cc : \mBbbR{}
11. ((r1\^{}2 - r2\^{}2) + ||b||\^{}2) = cc
12. r0 \mleq{} ((||b||\^{}2 * r1\^{}2) - (cc/r(2))\^{}2)
13. r0 < ||b||\^{}2
14. v : \{r:\mBbbR{}| (r0 \mleq{} r) \mwedge{} ((r * r) = ((||b||\^{}2 * r1\^{}2) - (cc/r(2))\^{}2))\}
15. rsqrt((||b||\^{}2 * r1\^{}2) - (cc/r(2))\^{}2) = v
16. \mforall{}x:\mBbbR{}\^{}n
((req-vec(n;x;(r1/||b||\^{}2)*(cc/r(2))*b + v*b') \mvee{} req-vec(n;x;(r1/||b||\^{}2)*(cc/r(2))*b - v*b'))
{}\mRightarrow{} ((||x|| = r1) \mwedge{} (||x - b|| = r2)))
17. ||(r1/||b||\^{}2)*(cc/r(2))*b + v*b'|| = r1
18. ||(r1/||b||\^{}2)*(cc/r(2))*b + v*b' - b|| = r2
19. ||(r1/||b||\^{}2)*(cc/r(2))*b - v*b'|| = r1
20. ||(r1/||b||\^{}2)*(cc/r(2))*b - v*b' - b|| = r2
21. ||(r1/||b||\^{}2)*(cc/r(2))*b + v*b'|| = r1
22. ||(r1/||b||\^{}2)*(cc/r(2))*b + v*b' - b|| = r2
23. ||(r1/||b||\^{}2)*(cc/r(2))*b - v*b'|| = r1
24. ||(r1/||b||\^{}2)*(cc/r(2))*b - v*b' - b|| = r2
25. cc\^{}2 < (r(4) * ||b||\^{}2 * r1\^{}2)
26. M : \mBbbR{}
27. (r1/||b||\^{}2) = M
28. r0 < M
29. req-vec(n;M*(cc/r(2))*b + v*b' - M*(cc/r(2))*b - v*b';(r(2) * M) * v*b')
\mvdash{} r0 < ||(r(2) * M) * v*b'||
By
Latex:
((RWO "real-vec-norm-mul" 0 THENA Auto) THEN (BLemma `rmul-is-positive` THENM OrLeft) THEN Auto)
Home
Index