Step
*
of Lemma
rv-line-circle-0-ext
∀n:ℕ. ∀a,b,p,q:ℝ^n.
(p ≠ q
⇒ (d(a;p) ≤ d(a;b))
⇒ (d(a;b) ≤ d(a;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))))))])))
BY
{ (Intros THEN UseWitness ⌜rvlinecircle0(n;a;b;p;q)⌝⋅ THEN Unfolds ``sq_exists exists`` 0 THEN MemCD THEN Auto) }
Latex:
Latex:
\mforall{}n:\mBbbN{}. \mforall{}a,b,p,q:\mBbbR{}\^{}n.
(p \mneq{} q
{}\mRightarrow{} (d(a;p) \mleq{} d(a;b))
{}\mRightarrow{} (d(a;b) \mleq{} d(a;q))
{}\mRightarrow{} (\mexists{}u:\mexists{}u:\mBbbR{}\^{}n [(ab=au \mwedge{} (\mneg{}(q \mneq{} u \mwedge{} u \mneq{} p \mwedge{} (\mneg{}q-u-p))))]
(\mexists{}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))))))])))
By
Latex:
(Intros
THEN UseWitness \mkleeneopen{}rvlinecircle0(n;a;b;p;q)\mkleeneclose{}\mcdot{}
THEN Unfolds ``sq\_exists exists`` 0
THEN MemCD
THEN Auto)
Home
Index