Step
*
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)
⊢ (r1/||b||^2)*(cc/r(2))*b + v*b' # (r1/||b||^2)*(cc/r(2))*b - v*b'
BY
{ ((Assert r0 < (r1/||b||^2) BY
(nRMul ⌜||b||^2⌝ 0⋅ THEN Auto))
THEN MoveToConcl (-1)
THEN GenConclTerm ⌜(r1/||b||^2)⌝⋅
THEN Auto
THEN RenameVar `M' (-3)) }
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
⊢ M*(cc/r(2))*b + v*b' # M*(cc/r(2))*b - 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)
\mvdash{} (r1/||b||\^{}2)*(cc/r(2))*b + v*b' \# (r1/||b||\^{}2)*(cc/r(2))*b - v*b'
By
Latex:
((Assert r0 < (r1/||b||\^{}2) BY
(nRMul \mkleeneopen{}||b||\^{}2\mkleeneclose{} 0\mcdot{} THEN Auto))
THEN MoveToConcl (-1)
THEN GenConclTerm \mkleeneopen{}(r1/||b||\^{}2)\mkleeneclose{}\mcdot{}
THEN Auto
THEN RenameVar `M' (-3))
Home
Index