Nuprl Lemma : ip-circle-circle-lemma1

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


Proof



Definitions occuring in Statement :  rv-norm: ||x||,  rv-sub: x - y,  rv-ip: x ⋅ y,  inner-product-space: InnerProductSpace,  rv-mul: a*x,  rv-add: x + y,  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: ℝ,  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],  nat: ℕ,  le: A ≤ B,  and: P ∧ Q,  less_than': less_than'(a;b),  not: ¬A,  false: False,  subtype_rel: A ⊆r B,  let: let,  prop: ℙ,  guard: {T},  uimplies: b supposing a,  rneq: x ≠ y,  or: P ∨ Q,  iff: P ⇐⇒ Q,  rev_implies: P ⇐ Q,  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q),  less_than: a < b,  squash: ↓T,  true: True,  rdiv: (x/y),  exp: i^n,  primrec: primrec(n;b;c),  primtailrec: primtailrec(n;i;b;f),  subtract: n - m,  req_int_terms: t1 ≡ t2,  sq_stable: SqStable(P),  rless: x < y,  sq_exists: ∃x:A [B[x]],  nat_plus: ℕ+,  decidable: Dec(P),  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  rv-sub: x - y,  rv-minus: -x,  int_nzero: ℤ-o,  nequal: a ≠ b ∈ T ,  sq_type: SQType(T)
Lemmas referenced :  radd_wf,  rsub_wf,  rnexp_wf,  istype-void,  istype-le,  rv-norm_wf,  rleq_wf,  rmul_wf,  int-to-real_wf,  req_wf,  rv-ip_wf,  rless_wf,  Error :ss-point_wf,  real-vector-space_subtype1,  inner-product-space_subtype,  subtype_rel_transitivity,  inner-product-space_wf,  real-vector-space_wf,  Error :separation-space_wf,  real_wf,  radd-preserves-rleq,  rdiv_wf,  rless-int,  rleq_functionality,  rinv_wf2,  itermSubtract_wf,  itermAdd_wf,  itermVar_wf,  itermConstant_wf,  req-iff-rsub-is-0,  itermMultiply_wf,  exp_wf2,  req-int,  rless_transitivity1,  rleq_weakening,  rmul_preserves_rleq,  real_polynomial_null,  istype-int,  real_term_value_sub_lemma,  real_term_value_add_lemma,  real_term_value_var_lemma,  real_term_value_const_lemma,  real_term_value_mul_lemma,  req_functionality,  rnexp-int,  req_weakening,  rless_functionality,  req_transitivity,  req_inversion,  rnexp-rdiv,  rdiv_functionality,  rmul-rinv3,  rnexp-positive,  rsqrt_wf,  square-req-iff,  rv-norm-nonneg,  sq_stable__rleq,  rv-sub_wf,  Error :ss-eq_wf,  rv-mul_wf,  rv-add_wf,  iff_weakening_uiff,  rv-norm-squared,  rmul_preserves_req,  rv-ip-mul,  rv-ip-mul2,  req-same,  rv-ip_functionality,  rv-mul_functionality,  rv-mul-mul,  rmul-rinv,  Error :ss-eq_weakening,  rv-mul1,  rv-ip-add-squared,  radd_functionality,  rmul_functionality,  rv-ip-sub-squared,  rsub_functionality,  sq_stable__req,  rnexp_functionality,  rmul_assoc,  rnexp2,  rmul-assoc,  nat_plus_properties,  decidable__le,  full-omega-unsat,  intformnot_wf,  intformle_wf,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_constant_lemma,  int_term_value_add_lemma,  int_formula_prop_wf,  rnexp-add,  int_term_value_mul_lemma,  rnexp-mul,  rv-mul-rv-sub,  Error :ss-eq_functionality,  rminus_wf,  itermMinus_wf,  rv-minus_wf,  rv-sub_functionality,  uiff_transitivity,  rv-add_functionality,  rv-add-swap,  rv-mul-add,  real_term_value_minus_lemma,  squash_wf,  true_wf,  istype-nat,  rneq_wf,  subtype_rel_self,  iff_weakening_equal,  minus-one-mul-top,  subtype_base_sq,  int_subtype_base,  nequal_wf,  int-rinv-cancel,  square-nonzero,  rneq_functionality,  rmul-int,  rmul-rdiv,  radd-preserves-req,  rminus_functionality,  req-implies-req
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  cut,  thin,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  dependent_set_memberEquality_alt,  natural_numberEquality,  independent_pairFormation,  sqequalRule,  voidElimination,  hypothesis,  hypothesisEquality,  setElimination,  rename,  because_Cache,  applyEquality,  inhabitedIsType,  universeIsType,  lambdaEquality_alt,  equalityTransitivity,  equalitySymmetry,  equalityIstype,  dependent_functionElimination,  independent_functionElimination,  instantiate,  independent_isectElimination,  setIsType,  inrFormation_alt,  productElimination,  closedConclusion,  imageMemberEquality,  baseClosed,  approximateComputation,  int_eqEquality,  Error :memTop,  imageElimination,  promote_hyp,  unionIsType,  unionElimination,  addEquality,  dependent_pairFormation_alt,  multiplyEquality,  inlFormation_alt,  minusEquality,  universeEquality,  cumulativity,  intEquality,  sqequalBase
Latex:
\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))))))


Date html generated: 2020_05_20-PM-01_14_57
Last ObjectModification: 2020_01_03-PM-07_33_56

Theory : inner!product!spaces


Home Index