Nuprl Lemma : rv-line-circle-0
∀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))))))])))
Proof
Definitions occuring in Statement :
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: ℕ,
all: ∀x:A. B[x],
sq_exists: ∃x:A [B[x]],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
natural_number: $n
Definitions unfolded in proof :
all: ∀x:A. B[x],
implies: P ⇒ Q,
member: t ∈ T,
uall: ∀[x:A]. B[x],
subtype_rel: A ⊆r B,
prop: ℙ,
real-vec-dist: d(x;y),
and: P ∧ Q,
cand: A c∧ B,
uimplies: b supposing a,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
real-vec-sep: a ≠ b,
let: let,
nat: ℕ,
le: A ≤ B,
less_than': less_than'(a;b),
not: ¬A,
false: False,
rneq: x ≠ y,
or: P ∨ Q,
rless: x < y,
sq_exists: ∃x:A [B[x]],
sq_stable: SqStable(P),
guard: {T},
so_apply: x[s],
so_lambda: λ2x.t[x],
top: Top,
quadratic1: quadratic1(a;b;c),
true: True,
squash: ↓T,
less_than: a < b,
req_int_terms: t1 ≡ t2,
rdiv: (x/y),
nat_plus: ℕ+,
exists: ∃x:A. B[x],
satisfiable_int_formula: satisfiable_int_formula(fmla),
decidable: Dec(P),
ge: i ≥ j ,
rge: x ≥ y,
real-vec-add: X + Y,
real-vec-sub: X - Y,
req-vec: req-vec(n;x;y),
real-vec: ℝ^n,
int_seg: {i..j-},
lelt: i ≤ j < k,
rv-congruent: ab=cd,
real-vec-be: real-vec-be(n;a;b;c),
real-vec-mul: a*X,
quadratic2: quadratic2(a;b;c),
rat_term_to_real: rat_term_to_real(f;t),
rtermAdd: left "+" right,
rat_term_ind: rat_term_ind,
rtermMultiply: left "*" right,
rtermDivide: num "/" denom,
rtermMinus: rtermMinus(num),
rtermVar: rtermVar(var),
rtermSubtract: left "-" right,
rtermConstant: "const",
pi1: fst(t),
pi2: snd(t),
real-vec-between: a-b-c,
rv-between: a-b-c,
hd: hd(l),
eq_int: (i =z j),
tl: tl(l),
null: null(as),
bor: p ∨bq,
even-int-list: even-int-list(L),
btrue: tt,
bfalse: ff,
lt_int: i <z j,
bnot: ¬bb,
le_int: i ≤z j,
nonneg-monomial: nonneg-monomial(m),
band: p ∧b q,
list_accum: list_accum,
rev-append: rev(as) + bs,
itermConstant: "const",
map: map(f;as),
minus-poly: minus-poly(p),
insert-int: insert-int(x;l),
evalall: evalall(t),
callbyvalueall: callbyvalueall,
eager-accum: eager-accum(x,a.f[x; a];y;l),
merge-int-accum: merge-int-accum(as;bs),
mul-monomials: mul-monomials(m1;m2),
mul-mono-poly: mul-mono-poly(m;p),
it: ⋅,
nil: [],
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
cons: [a / b],
itermVar: vvar,
mul_ipoly: mul_ipoly(p;q),
itermMultiply: left (*) right,
add-ipoly-prepend: add-ipoly-prepend(p;q;l),
add_ipoly: add_ipoly(p;q),
itermSubtract: left (-) right,
int_term_ind: int_term_ind,
int_term_to_ipoly: int_term_to_ipoly(t),
list_ind: list_ind,
reduce: reduce(f;k;as),
bl-all: (∀x∈L.P[x])_b,
nonneg-poly: nonneg-poly(p),
ifthenelse: if b then t else f fi ,
assert: ↑b
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:\{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))))))])))
Date html generated:
2020_05_20-PM-00_54_46
Last ObjectModification:
2020_01_06-AM-11_19_05
Theory : reals
Home
Index