---

Step * of Lemma ip-circle-circle-lemma1

No Annotations
∀rv:InnerProductSpace. ∀r1,r2:{r:ℝ| r0 ≤ r} . ∀b:Point(rv).
  ((r0 < ||b||)
  ⇒ (∀b':Point(rv)
        ((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:Point(rv)
              ((x ≡ (r1/||b||^2)*c*b + rsqrt(d)*b' ∨ 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. rv : InnerProductSpace
2. r1 : {r:ℝ| r0 ≤ r} 
3. r2 : {r:ℝ| r0 ≤ r} 
4. b : Point(rv)
5. r0 < ||b||
6. b' : Point(rv)
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. rv : InnerProductSpace
2. r1 : {r:ℝ| r0 ≤ r} 
3. r2 : {r:ℝ| r0 ≤ r} 
4. b : Point(rv)
5. r0 < ||b||
6. b' : Point(rv)
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:Point(rv)
    ((x ≡ (r1/||b||^2)*(cc/r(2))*b + rsqrt((||b||^2 * r1^2) - (cc/r(2))^2)*b'
    ∨ 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:
No  Annotations
\mforall{}rv:InnerProductSpace.  \mforall{}r1,r2:\{r:\mBbbR{}|  r0  \mleq{}  r\}  .  \mforall{}b:Point(rv).
    ((r0  <  ||b||)
    {}\mRightarrow{}  (\mforall{}b':Point(rv)
                ((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:Point(rv)
                            ((x  \mequiv{}  (r1/||b||\^{}2)*c*b  +  rsqrt(d)*b'  \mvee{}  x  \mequiv{}  (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