---

Step * of Lemma rv-circle-circle-lemma

∀n:ℕ. ∀r1,r2:{r:ℝ| r0 ≤ r} . ∀b:ℝ^n.
  ((r0 < ||b||)
  ⇒ (∀b':ℝ^n
        ((b⋅b' = r0)
        ⇒ (||b'|| = ||b||)
        ⇒ ((r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2))
        ⇒ let c = ((r1^2 - r2^2) + ||b||^2/r(2)) in
            let d = (||b||^2 * r1^2) - c^2 in
            ∀x:ℝ^n
              ((req-vec(n;x;(r1/||b||^2)*c*b + rsqrt(d)*b') ∨ req-vec(n;x;(r1/||b||^2)*c*b - rsqrt(d)*b'))
              ⇒ ((||x|| = r1) ∧ (||x - b|| = r2))))))
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜((r1^2 - r2^2) + ||b||^2) = cc ∈ ℝ⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepUR ``let`` 0
   THEN Assert ⌜r0 ≤ ((||b||^2 * r1^2) - (cc/r(2))^2)⌝⋅) }

1
.....assertion..... 
1. n : ℕ
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. cc : ℝ
10. ((r1^2 - r2^2) + ||b||^2) = cc ∈ ℝ
11. cc^2 ≤ (r(4) * ||b||^2 * r1^2)
⊢ r0 ≤ ((||b||^2 * r1^2) - (cc/r(2))^2)

2
1. n : ℕ
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. cc : ℝ
10. ((r1^2 - r2^2) + ||b||^2) = cc ∈ ℝ
11. cc^2 ≤ (r(4) * ||b||^2 * r1^2)
12. r0 ≤ ((||b||^2 * r1^2) - (cc/r(2))^2)
⊢ ∀x:ℝ^n
    ((req-vec(n;x;(r1/||b||^2)*(cc/r(2))*b + rsqrt((||b||^2 * r1^2) - (cc/r(2))^2)*b')
    ∨ req-vec(n;x;(r1/||b||^2)*(cc/r(2))*b - rsqrt((||b||^2 * r1^2) - (cc/r(2))^2)*b'))
    ⇒ ((||x|| = r1) ∧ (||x - b|| = r2)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}r1,r2:\{r:\mBbbR{}|  r0  \mleq{}  r\}  .  \mforall{}b:\mBbbR{}\^{}n.
    ((r0  <  ||b||)
    {}\mRightarrow{}  (\mforall{}b':\mBbbR{}\^{}n
                ((b\mcdot{}b'  =  r0)
                {}\mRightarrow{}  (||b'||  =  ||b||)
                {}\mRightarrow{}  ((r1\^{}2  -  r2\^{}2)  +  ||b||\^{}2\^{}2  \mleq{}  (r(4)  *  ||b||\^{}2  *  r1\^{}2))
                {}\mRightarrow{}  let  c  =  ((r1\^{}2  -  r2\^{}2)  +  ||b||\^{}2/r(2))  in
                        let  d  =  (||b||\^{}2  *  r1\^{}2)  -  c\^{}2  in
                        \mforall{}x:\mBbbR{}\^{}n
                            ((req-vec(n;x;(r1/||b||\^{}2)*c*b  +  rsqrt(d)*b')
                            \mvee{}  req-vec(n;x;(r1/||b||\^{}2)*c*b  -  rsqrt(d)*b'))
                            {}\mRightarrow{}  ((||x||  =  r1)  \mwedge{}  (||x  -  b||  =  r2))))))


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}((r1\^{}2  -  r2\^{}2)  +  ||b||\^{}2)  =  cc\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``let``  0
  THEN  Assert  \mkleeneopen{}r0  \mleq{}  ((||b||\^{}2  *  r1\^{}2)  -  (cc/r(2))\^{}2)\mkleeneclose{}\mcdot{})

---

Home Index