Nuprl Lemma : intermediate-value-theorem-rpolynomial
∀n:ℕ. ∀a:ℕn + 1 ⟶ ℝ. ∀b,c,d:ℝ.
(∃x:{x:ℝ| x ∈ [b, c]} . ((Σi≤n. a_i * x^i) = d)) supposing
((d < (Σi≤n. a_i * c^i)) and
((Σi≤n. a_i * b^i) < d) and
(b ≤ c))
Proof
Definitions occuring in Statement :
rccint: [l, u],
i-member: r ∈ I,
rpolynomial: (Σi≤n. a_i * x^i),
rleq: x ≤ y,
rless: x < y,
req: x = y,
real: ℝ,
int_seg: {i..j-},
nat: ℕ,
uimplies: b supposing a,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
set: {x:A| B[x]} ,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions unfolded in proof :
nat: ℕ,
squash: ↓T,
sq_stable: SqStable(P),
prop: ℙ,
real: ℝ,
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
false: False,
implies: P ⇒ Q,
not: ¬A,
and: P ∧ Q,
le: A ≤ B,
rnonneg: rnonneg(x),
rleq: x ≤ y,
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x]
Lemmas referenced :
less_than'_wf,
rsub_wf,
real_wf,
nat_plus_wf,
IVT-rpolynomial2,
sq_stable__rless,
rpolynomial_wf,
rless_wf,
rleq_wf,
int_seg_wf,
nat_wf
Rules used in proof :
addEquality,
functionEquality,
imageElimination,
baseClosed,
imageMemberEquality,
because_Cache,
independent_functionElimination,
equalitySymmetry,
equalityTransitivity,
axiomEquality,
natural_numberEquality,
minusEquality,
rename,
setElimination,
hypothesis,
applyEquality,
isectElimination,
lemma_by_obid,
voidElimination,
independent_pairEquality,
productElimination,
hypothesisEquality,
thin,
dependent_functionElimination,
lambdaEquality,
sqequalHypSubstitution,
sqequalRule,
introduction,
cut,
isect_memberFormation,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution
Latex:
\mforall{}n:\mBbbN{}. \mforall{}a:\mBbbN{}n + 1 {}\mrightarrow{} \mBbbR{}. \mforall{}b,c,d:\mBbbR{}.
(\mexists{}x:\{x:\mBbbR{}| x \mmember{} [b, c]\} . ((\mSigma{}i\mleq{}n. a\_i * x\^{}i) = d)) supposing
((d < (\mSigma{}i\mleq{}n. a\_i * c\^{}i)) and
((\mSigma{}i\mleq{}n. a\_i * b\^{}i) < d) and
(b \mleq{} c))
Date html generated:
2016_05_18-AM-10_27_15
Last ObjectModification:
2016_01_17-AM-00_26_24
Theory : reals
Home
Index