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