Nuprl Lemma : rpolynomial-complete-roots-unique
∀[n:ℕ+]. ∀[a:ℕn + 1 ⟶ ℝ].
∀[z,y:ℕn ⟶ ℝ].
(∀[j:ℕn]. ((z j) = (y j))) supposing
((∀j:ℕn. ((Σi≤n. a_i * z j^i) = r0)) and
(∀j:ℕn. ((Σi≤n. a_i * y j^i) = r0)) and
(∀j:ℕn - 1. ((y j) < (y (j + 1)))) and
(∀j:ℕn - 1. ((z j) < (z (j + 1)))))
supposing a n ≠ r0
Proof
Definitions occuring in Statement :
rpolynomial: (Σi≤n. a_i * x^i),
rneq: x ≠ y,
rless: x < y,
req: x = y,
int-to-real: r(n),
real: ℝ,
int_seg: {i..j-},
nat_plus: ℕ+,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
apply: f a,
function: x:A ⟶ B[x],
subtract: n - m,
add: n + m,
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
all: ∀x:A. B[x],
implies: P ⇒ Q,
int_seg: {i..j-},
lelt: i ≤ j < k,
and: P ∧ Q,
le: A ≤ B,
less_than: a < b,
squash: ↓T,
so_lambda: λ2x.t[x],
nat_plus: ℕ+,
decidable: Dec(P),
or: P ∨ Q,
not: ¬A,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
prop: ℙ,
so_apply: x[s],
uiff: uiff(P;Q),
rev_uimplies: rev_uimplies(P;Q),
nat: ℕ,
req_int_terms: t1 ≡ t2,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
sequence: sequence(T),
trans: Trans(T;x,y.E[x; y]),
rev_implies: P ⇐ Q,
rge: x ≥ y,
guard: {T},
iff: P ⇐⇒ Q,
seq-item: s[i],
seq-len: ||s||,
pi1: fst(t),
pi2: snd(t),
sorted-seq: sorted-seq(x,y.R[x; y];s),
cand: A c∧ B,
top: Top,
true: True,
less_than': less_than'(a;b),
sq_type: SQType(T),
sq_exists: ∃x:A [B[x]],
rless: x < y,
sq_stable: SqStable(P),
real: ℝ,
subtype_rel: A ⊆r B,
subtract: n - m,
ge: i ≥ j ,
rneq: x ≠ y,
stable: Stable{P}
Latex:
\mforall{}[n:\mBbbN{}\msupplus{}]. \mforall{}[a:\mBbbN{}n + 1 {}\mrightarrow{} \mBbbR{}].
\mforall{}[z,y:\mBbbN{}n {}\mrightarrow{} \mBbbR{}].
(\mforall{}[j:\mBbbN{}n]. ((z j) = (y j))) supposing
((\mforall{}j:\mBbbN{}n. ((\mSigma{}i\mleq{}n. a\_i * z j\^{}i) = r0)) and
(\mforall{}j:\mBbbN{}n. ((\mSigma{}i\mleq{}n. a\_i * y j\^{}i) = r0)) and
(\mforall{}j:\mBbbN{}n - 1. ((y j) < (y (j + 1)))) and
(\mforall{}j:\mBbbN{}n - 1. ((z j) < (z (j + 1)))))
supposing a n \mneq{} r0
Date html generated:
2020_05_20-AM-11_12_59
Last ObjectModification:
2020_01_06-PM-00_44_42
Theory : reals
Home
Index