Nuprl Lemma : rvlinecircle0_wf

∀[n:ℕ]. ∀[a,b,p,q:ℝ^n].
  (rvlinecircle0(n;a;b;p;q) ∈ u:{u:ℝ^n| ab=au ∧ (¬(q ≠ u ∧ u ≠ p ∧ (¬q-u-p)))}  × {v:ℝ^n| 
                                                     ab=av
                                                     ∧ (¬(q ≠ p ∧ p ≠ v ∧ (¬q-p-v)))
                                                     ∧ ((d(a;p) < d(a;b)) ⇒ (q-p-v ∧ ((d(a;b) < d(a;q)) ⇒ q-u-p)))
                                                     ∧ ((d(a;p) = d(a;b))
                                                       ⇒ ((u ≠ v
                                                          ⇒ ((req-vec(n;u;p) ∧ (r0 < p - a⋅q - p))
                                                             ∨ (req-vec(n;v;p) ∧ (p - a⋅q - p < r0))))
                                                          ∧ (req-vec(n;u;v)
                                                            ⇒ ((p - a⋅q - p = r0) ∧ req-vec(n;u;p)))))} ) supposing 
     ((d(a;b) ≤ d(a;q)) and 
     (d(a;p) ≤ d(a;b)) and 
     p ≠ q)


Proof



Definitions occuring in Statement :  rvlinecircle0: rvlinecircle0(n;a;b;p;q),  rv-between: a-b-c,  real-vec-sep: a ≠ b,  rv-congruent: ab=cd,  real-vec-dist: d(x;y),  dot-product: x⋅y,  real-vec-sub: X - Y,  req-vec: req-vec(n;x;y),  real-vec: ℝ^n,  rleq: x ≤ y,  rless: x < y,  req: x = y,  int-to-real: r(n),  nat: ℕ,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  not: ¬A,  implies: P ⇒ Q,  or: P ∨ Q,  and: P ∧ Q,  member: t ∈ T,  set: {x:A| B[x]} ,  product: x:A × B[x],  natural_number: $n
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  uimplies: b supposing a,  member: t ∈ T,  rvlinecircle0: rvlinecircle0(n;a;b;p;q),  rv-line-circle-0,  rv-line-circle-lemma,  real-vec-add: X + Y,  sq_exists: ∃x:A [B[x]],  exists: ∃x:A. B[x],  subtype_rel: A ⊆r B,  all: ∀x:A. B[x],  so_lambda: λ2x.t[x],  implies: P ⇒ Q,  prop: ℙ,  and: P ∧ Q,  or: P ∨ Q,  so_apply: x[s]
Lemmas referenced :  rv-line-circle-0,  subtype_rel_self,  nat_wf,  all_wf,  real-vec_wf,  real-vec-sep_wf,  rleq_wf,  real-vec-dist_wf,  exists_wf,  rv-congruent_wf,  not_wf,  rv-between_wf,  sq_exists_wf,  rless_wf,  req_wf,  or_wf,  req-vec_wf,  int-to-real_wf,  dot-product_wf,  real-vec-sub_wf,  subtype_rel_function,  real_wf,  rv-line-circle-lemma
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  cut,  rename,  sqequalRule,  applyEquality,  thin,  instantiate,  extract_by_obid,  hypothesis,  introduction,  sqequalHypSubstitution,  isectElimination,  functionEquality,  hypothesisEquality,  lambdaEquality,  because_Cache,  setEquality,  productEquality,  setElimination,  natural_numberEquality,  independent_isectElimination
Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b,p,q:\mBbbR{}\^{}n].
    (rvlinecircle0(n;a;b;p;q)  \mmember{}  u:\{u:\mBbbR{}\^{}n|  ab=au  \mwedge{}  (\mneg{}(q  \mneq{}  u  \mwedge{}  u  \mneq{}  p  \mwedge{}  (\mneg{}q-u-p)))\}    \mtimes{}  \{v:\mBbbR{}\^{}n| 
                                                                                                          ab=av
                                                                                                          \mwedge{}  (\mneg{}(q  \mneq{}  p  \mwedge{}  p  \mneq{}  v  \mwedge{}  (\mneg{}q-p-v)))
                                                                                                          \mwedge{}  ((d(a;p)  <  d(a;b))
                                                                                                              {}\mRightarrow{}  (q-p-v  \mwedge{}  ((d(a;b)  <  d(a;q))  {}\mRightarrow{}  q-u-p)))
                                                                                                          \mwedge{}  ((d(a;p)  =  d(a;b))
                                                                                                              {}\mRightarrow{}  ((u  \mneq{}  v
                                                                                                                    {}\mRightarrow{}  ((req-vec(n;u;p)  \mwedge{}  (r0  <  p  -  a\mcdot{}q  -  p))
                                                                                                                          \mvee{}  (req-vec(n;v;p)
                                                                                                                              \mwedge{}  (p  -  a\mcdot{}q  -  p  <  r0))))
                                                                                                                    \mwedge{}  (req-vec(n;u;v)
                                                                                                                        {}\mRightarrow{}  ((p  -  a\mcdot{}q  -  p  =  r0)
                                                                                                                              \mwedge{}  req-vec(n;u;p)))))\}  )  supposing 
          ((d(a;b)  \mleq{}  d(a;q))  and 
          (d(a;p)  \mleq{}  d(a;b))  and 
          p  \mneq{}  q)


Date html generated: 2018_05_22-PM-02_34_07
Last ObjectModification: 2018_03_27-PM-05_13_16

Theory : reals


Home Index