Nuprl Lemma : rv-line-circle-3-ext

∀n:ℕ. ∀c,b,d,q:ℝ^n.
  (c_b_d
  ⇒ (d(c;d) < d(c;q))
  ⇒ (∃u:{u:ℝ^n| cd=cu ∧ q_u_b} 
       (∃v:ℝ^n [(cd=cv
               ∧ q_b_v
               ∧ (b ≠ d ⇒ (u ≠ v ∧ u ≠ b ∧ v ≠ b))
               ∧ (req-vec(n;b;d)
                 ⇒ ((u ≠ v ⇒ ((req-vec(n;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(n;v;b) ∧ (b - c⋅q - b < r0))))
                    ∧ (req-vec(n;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(n;u;b))))))])))


Proof



Definitions occuring in Statement :  rv-be: 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,  rless: x < y,  req: x = y,  int-to-real: r(n),  nat: ℕ,  all: ∀x:A. B[x],  sq_exists: ∃x:A [B[x]],  exists: ∃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 :  member: t ∈ T,  rvlinecircle0: rvlinecircle0(n;a;b;p;q),  rv-line-circle-3,  rv-line-circle-0-ext,  rless_transitivity2,  rless_functionality,  radd-preserves-rless,  rless_transitivity1,  rleq_functionality,  rleq_weakening_rless
Lemmas referenced :  rv-line-circle-3,  rv-line-circle-0-ext,  rless_transitivity2,  rless_functionality,  radd-preserves-rless,  rless_transitivity1,  rleq_functionality,  rleq_weakening_rless
Rules used in proof :  introduction,  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  cut,  instantiate,  extract_by_obid,  hypothesis,  sqequalRule,  thin,  sqequalHypSubstitution,  equalityTransitivity,  equalitySymmetry
Latex:
\mforall{}n:\mBbbN{}.  \mforall{}c,b,d,q:\mBbbR{}\^{}n.
    (c\_b\_d
    {}\mRightarrow{}  (d(c;d)  <  d(c;q))
    {}\mRightarrow{}  (\mexists{}u:\{u:\mBbbR{}\^{}n|  cd=cu  \mwedge{}  q\_u\_b\} 
              (\mexists{}v:\mBbbR{}\^{}n  [(cd=cv
                              \mwedge{}  q\_b\_v
                              \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  (u  \mneq{}  v  \mwedge{}  u  \mneq{}  b  \mwedge{}  v  \mneq{}  b))
                              \mwedge{}  (req-vec(n;b;d)
                                  {}\mRightarrow{}  ((u  \mneq{}  v
                                        {}\mRightarrow{}  ((req-vec(n;u;b)  \mwedge{}  (r0  <  b  -  c\mcdot{}q  -  b))
                                              \mvee{}  (req-vec(n;v;b)  \mwedge{}  (b  -  c\mcdot{}q  -  b  <  r0))))
                                        \mwedge{}  (req-vec(n;u;v)  {}\mRightarrow{}  ((b  -  c\mcdot{}q  -  b  =  r0)  \mwedge{}  req-vec(n;u;b))))))])))


Date html generated: 2018_05_22-PM-02_35_44
Last ObjectModification: 2018_05_18-AM-09_40_48

Theory : reals


Home Index