---

Step * of Lemma ip-circle-circle-lemma2

∀rv:InnerProductSpace. ∀r1,r2:{r:ℝ| r0 ≤ r} . ∀b:Point.
  ((r0 < ||b||)
  ⇒ ((r1^2 - r2^2) + ||b||^2^2 ≤ (r(4) * ||b||^2 * r1^2))
  ⇒ (∃u,v:Point
       (((||u|| = r1) ∧ (||u - b|| = r2))
       ∧ ((||v|| = r1) ∧ (||v - b|| = r2))
       ∧ (((r1^2 - r2^2) + ||b||^2^2 < (r(4) * ||b||^2 * r1^2)) ⇒ u # v))))
BY
{ (InstLemma `ip-circle-circle-lemma1` []
   THEN (RepeatFor 5 ((ParallelLast' THENA Auto)) THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (InstLemma `rv-perp-same-norm` [⌜rv⌝;⌜b⌝]⋅ THENA EAuto 1)
   THEN D -1
   THEN RenameVar `b\'' (-2)
   THEN (InstHyp [⌜b'⌝] 6⋅ THENA Auto)
   THEN Thin 6) }

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||) ∧ (b ⋅ b' = r0)
9. let c = ((r1^2 - r2^2) + ||b||^2/r(2)) in
    let d = (||b||^2 * r1^2) - c^2 in
    ∀x:Point
      ((x ≡ (r1/||b||^2)*c*b + rsqrt(d)*b' ∨ x ≡ (r1/||b||^2)*c*b - rsqrt(d)*b') ⇒ ((||x|| = r1) ∧ (||x - b|| = r2)))
⊢ ∃u,v:Point
   (((||u|| = r1) ∧ (||u - b|| = r2))
   ∧ ((||v|| = r1) ∧ (||v - b|| = r2))
   ∧ (((r1^2 - r2^2) + ||b||^2^2 < (r(4) * ||b||^2 * r1^2)) ⇒ u # v))

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}r1,r2:\{r:\mBbbR{}|  r0  \mleq{}  r\}  .  \mforall{}b:Point.
    ((r0  <  ||b||)
    {}\mRightarrow{}  ((r1\^{}2  -  r2\^{}2)  +  ||b||\^{}2\^{}2  \mleq{}  (r(4)  *  ||b||\^{}2  *  r1\^{}2))
    {}\mRightarrow{}  (\mexists{}u,v:Point
              (((||u||  =  r1)  \mwedge{}  (||u  -  b||  =  r2))
              \mwedge{}  ((||v||  =  r1)  \mwedge{}  (||v  -  b||  =  r2))
              \mwedge{}  (((r1\^{}2  -  r2\^{}2)  +  ||b||\^{}2\^{}2  <  (r(4)  *  ||b||\^{}2  *  r1\^{}2))  {}\mRightarrow{}  u  \#  v))))


By

---

Latex:
(InstLemma  `ip-circle-circle-lemma1`  []
  THEN  (RepeatFor  5  ((ParallelLast'  THENA  Auto))  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (InstLemma  `rv-perp-same-norm`  [\mkleeneopen{}rv\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  D  -1
  THEN  RenameVar  `b\mbackslash{}''  (-2)
  THEN  (InstHyp  [\mkleeneopen{}b'\mkleeneclose{}]  6\mcdot{}  THENA  Auto)
  THEN  Thin  6)

---

Home Index