### Nuprl Lemma : rpolynomial-composition1

`∀n:ℕ. ∀a:ℕn + 1 ⟶ ℝ. ∀b,c,d:ℝ.  ∃a':ℕn + 1 ⟶ ℝ. ∀x:ℝ. ((Σi≤n. a'_i * x^i) = ((Σi≤n. a_i * ((c - b) * x) + b^i) - d))`

Proof

Definitions occuring in Statement :  rpolynomial: `(Σi≤n. a_i * x^i)` rsub: `x - y` req: `x = y` rmul: `a * b` radd: `a + b` real: `ℝ` int_seg: `{i..j-}` nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  rpolynomial: `(Σi≤n. a_i * x^i)` all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` exists: `∃x:A. B[x]` so_lambda: `λ2x.t[x]` nat: `ℕ` int_seg: `{i..j-}` lelt: `i ≤ j < k` and: `P ∧ Q` le: `A ≤ B` less_than: `a < b` squash: `↓T` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` prop: `ℙ` so_apply: `x[s]` ge: `i ≥ j ` less_than': `less_than'(a;b)` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` uiff: `uiff(P;Q)` req_int_terms: `t1 ≡ t2` subtype_rel: `A ⊆r B` cand: `A c∧ B` subtract: `n - m` true: `True` nat_plus: `ℕ+` guard: `{T}` int_iseg: `{i...j}` pointwise-req: `x[k] = y[k] for k ∈ [n,m]` rev_uimplies: `rev_uimplies(P;Q)` nequal: `a ≠ b ∈ T ` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` bfalse: `ff` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹`

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}b,c,d:\mBbbR{}.
\mexists{}a':\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}.  \mforall{}x:\mBbbR{}.  ((\mSigma{}i\mleq{}n.  a'\_i  *  x\^{}i)  =  ((\mSigma{}i\mleq{}n.  a\_i  *  ((c  -  b)  *  x)  +  b\^{}i)  -  d))

Date html generated: 2020_05_20-AM-11_13_55
Last ObjectModification: 2020_01_02-PM-02_01_05

Theory : reals

Home Index