---

Step * of 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)
BY
{ ((Intros THEN Unhide)
   THEN RenameVar `x' (-3)
   THEN RenameVar `y' (-2)
   THEN RenameVar `z' (-1)
   THEN (Subst' rvlinecircle0(n;a;b;p;q) ~ TERMOF{rv-line-circle-0:o, \\v:l} n a b p q x y z 0 THENA Computation)
   THEN (Fold `sq_exists` 0 THEN Fold `exists` 0)
   THEN Auto) }

---

Latex:

---

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)


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  RenameVar  `x'  (-3)
  THEN  RenameVar  `y'  (-2)
  THEN  RenameVar  `z'  (-1)
  THEN  (Subst'  rvlinecircle0(n;a;b;p;q)  \msim{}  TERMOF\{rv-line-circle-0:o,  \mbackslash{}\mbackslash{}v:l\}  n  a  b  p  q  x  y  z  0
              THENA  Computation
              )
  THEN  (Fold  `sq\_exists`  0  THEN  Fold  `exists`  0)
  THEN  Auto)

---

Home Index