Nuprl 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))))))


Proof



Definitions occuring in Statement :  real-vec-norm: ||x||,  dot-product: x⋅y,  real-vec-mul: a*X,  real-vec-sub: X - Y,  real-vec-add: X + Y,  req-vec: req-vec(n;x;y),  real-vec: ℝ^n,  rsqrt: rsqrt(x),  rdiv: (x/y),  rleq: x ≤ y,  rless: x < y,  rnexp: x^k1,  rsub: x - y,  req: x = y,  rmul: a * b,  radd: a + b,  int-to-real: r(n),  real: ℝ,  nat: ℕ,  let: let,  all: ∀x:A. B[x],  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  set: {x:A| B[x]} ,  natural_number: $n
Definitions unfolded in proof :  all: ∀x:A. B[x],  implies: P ⇒ Q,  member: t ∈ T,  uall: ∀[x:A]. B[x],  let: let,  prop: ℙ,  nat: ℕ,  le: A ≤ B,  and: P ∧ Q,  less_than': less_than'(a;b),  false: False,  not: ¬A,  so_lambda: λ2x.t[x],  so_apply: x[s],  uimplies: b supposing a,  rneq: x ≠ y,  guard: {T},  or: P ∨ Q,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  less_than: a < b,  squash: ↓T,  true: True,  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q),  exp: i^n,  primrec: primrec(n;b;c),  subtract: n - m,  itermConstant: "const",  req_int_terms: t1 ≡ t2,  top: Top,  rdiv: (x/y),  sq_stable: SqStable(P),  cand: A c∧ B,  subtype_rel: A ⊆r B,  rsub: x - y
Lemmas referenced :  radd_wf,  rsub_wf,  rnexp_wf,  real_wf,  rleq_wf,  rmul_wf,  equal_wf,  false_wf,  le_wf,  real-vec-norm_wf,  int-to-real_wf,  req_wf,  dot-product_wf,  real-vec_wf,  rless_wf,  set_wf,  nat_wf,  radd-preserves-rleq,  rdiv_wf,  rless-int,  rinv_wf2,  exp_wf2,  req-int,  rless_transitivity1,  rleq_weakening,  rmul_preserves_rleq,  rleq-implies-rleq,  real_term_polynomial,  itermSubtract_wf,  itermMultiply_wf,  itermConstant_wf,  itermVar_wf,  itermAdd_wf,  real_term_value_const_lemma,  real_term_value_sub_lemma,  real_term_value_mul_lemma,  real_term_value_var_lemma,  real_term_value_add_lemma,  req-iff-rsub-is-0,  rleq_functionality,  req_transitivity,  rmul_functionality,  req_weakening,  rnexp_functionality,  rinv-mul-as-rdiv,  radd_functionality,  req_functionality,  rnexp-int,  rless_functionality,  req_inversion,  rnexp-rdiv,  rdiv_functionality,  rmul-rinv3,  real-vec-norm-squared,  real-vec-add_wf,  real-vec-mul_wf,  req-vec_wf,  or_wf,  real-vec-sub_wf,  sq_stable__rleq,  real-vec-norm-nonneg,  square-req-iff,  rsqrt_wf,  rnexp-positive,  dot-product_functionality,  dot-product-comm,  dot-product-linearity2,  rmul-one-both,  rmul-int-rdiv,  rmul-rdiv-cancel,  rmul-ac,  rmul_comm,  rmul-assoc,  uiff_transitivity,  rmul_preserves_req,  iff_weakening_equal,  true_wf,  squash_wf,  dot-product-linearity1,  radd-zero-both,  radd-ac,  radd-assoc,  rmul-zero-both,  sq_stable__req,  radd-rminus-assoc,  radd_comm,  rnexp2,  rminus_wf,  rmul-distrib,  rsub_functionality,  dot-product-linearity1-sub,  rminus-rminus,  rminus-as-rmul,  rmul-int,  rminus-zero,  rminus-radd,  rminus_functionality,  radd-int,  rmul-distrib2,  radd-rminus-both,  radd-preserves-req,  req-vec_weakening,  rmul_over_rminus,  rmul-rdiv-cancel2
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation,  cut,  thin,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  because_Cache,  hypothesis,  sqequalRule,  hypothesisEquality,  equalityTransitivity,  equalitySymmetry,  dependent_functionElimination,  independent_functionElimination,  dependent_set_memberEquality,  natural_numberEquality,  independent_pairFormation,  setElimination,  rename,  lambdaEquality,  independent_isectElimination,  inrFormation,  productElimination,  imageMemberEquality,  baseClosed,  computeAll,  int_eqEquality,  intEquality,  isect_memberEquality,  voidElimination,  voidEquality,  imageElimination,  addLevel,  productEquality,  unionElimination,  multiplyEquality,  universeEquality,  applyEquality,  comment,  minusEquality,  addEquality
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))))))


Date html generated: 2017_10_03-AM-11_36_35
Last ObjectModification: 2017_07_28-AM-08_28_13

Theory : reals


Home Index