Step
*
1
1
1
1
1
1
of Lemma
ip-circle-circle-lemma2
1. rv : InnerProductSpace
2. r1 : {r:ℝ| r0 ≤ r}
3. r2 : {r:ℝ| r0 ≤ r}
4. b : Point
5. r0 < ||b||
6. (r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2)
7. b' : Point
8. ||b'|| = ||b||
9. b ⋅ b' = r0
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:Point
((x ≡ (r1/||b||^2)*(cc/r(2))*b + v*b' ∨ 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. M*(cc/r(2))*b + v*b' - M*(cc/r(2))*b - v*b' ≡ (r(2) * M) * v*b'
⊢ M*(cc/r(2))*b + v*b' # M*(cc/r(2))*b - v*b'
BY
{ (MoveToConcl (-1)
THEN (GenConcl ⌜M*(cc/r(2))*b + v*b' = x ∈ Point⌝⋅ THENA Auto)
THEN GenConcl ⌜M*(cc/r(2))*b - v*b' = y ∈ Point⌝⋅
THEN Auto
THEN (BLemma `rv-sep-iff-norm` THENA Auto)
THEN (RWO "-1" 0 THENA Auto)) }
1
1. rv : InnerProductSpace
2. r1 : {r:ℝ| r0 ≤ r}
3. r2 : {r:ℝ| r0 ≤ r}
4. b : Point
5. r0 < ||b||
6. (r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2)
7. b' : Point
8. ||b'|| = ||b||
9. b ⋅ b' = r0
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:Point
((x ≡ (r1/||b||^2)*(cc/r(2))*b + v*b' ∨ 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. x : Point
30. M*(cc/r(2))*b + v*b' = x ∈ Point
31. y : Point
32. M*(cc/r(2))*b - v*b' = y ∈ Point
33. x - y ≡ (r(2) * M) * v*b'
⊢ r0 < ||(r(2) * M) * v*b'||
Latex:
Latex:
1. rv : InnerProductSpace
2. r1 : \{r:\mBbbR{}| r0 \mleq{} r\}
3. r2 : \{r:\mBbbR{}| r0 \mleq{} r\}
4. b : Point
5. r0 < ||b||
6. (r1\^{}2 - r2\^{}2) + ||b||\^{}2\^{}2 \mleq{} (r(4) * ||b||\^{}2 * r1\^{}2)
7. b' : Point
8. ||b'|| = ||b||
9. b \mcdot{} b' = r0
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:Point
((x \mequiv{} (r1/||b||\^{}2)*(cc/r(2))*b + v*b' \mvee{} x \mequiv{} (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. M*(cc/r(2))*b + v*b' - M*(cc/r(2))*b - v*b' \mequiv{} (r(2) * M) * v*b'
\mvdash{} M*(cc/r(2))*b + v*b' \# M*(cc/r(2))*b - v*b'
By
Latex:
(MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}M*(cc/r(2))*b + v*b' = x\mkleeneclose{}\mcdot{} THENA Auto)
THEN GenConcl \mkleeneopen{}M*(cc/r(2))*b - v*b' = y\mkleeneclose{}\mcdot{}
THEN Auto
THEN (BLemma `rv-sep-iff-norm` THENA Auto)
THEN (RWO "-1" 0 THENA Auto))
Home
Index