---

Step * of 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))))))])))
BY
{ Extract of Obid: rv-line-circle-3
  not unfolding  rvlinecircle0
  finishing with (Auto THEN Computation)
  normalizes to:
  
  λn,c,b,d,q,%,%1. rvlinecircle0(n;c;d;b;q) }

---

Latex:

---

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


By

---

Latex:
Extract  of  Obid:  rv-line-circle-3
not  unfolding    rvlinecircle0
finishing  with  (Auto  THEN  Computation)
normalizes  to:

\mlambda{}n,c,b,d,q,\%,\%1.  rvlinecircle0(n;c;d;b;q)

---

Home Index