Nuprl Lemma : rpolynomial-composition1

n:ℕ. ∀a:ℕ1 ⟶ ℝ. ∀b,c,d:ℝ.  ∃a':ℕ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: y req: y rmul: b radd: b real: int_seg: {i..j-} nat: all: x:A. B[x] exists: x:A. B[x] function: x:A ⟶ B[x] add: 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:  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: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False prop: so_apply: x[s] ge: i ≥  less_than': less_than'(a;b) rev_implies:  Q iff: ⇐⇒ Q uiff: uiff(P;Q) req_int_terms: t1 ≡ t2 subtype_rel: A ⊆B cand: c∧ B subtract: 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 ∈  assert: b bnot: ¬bb sq_type: SQType(T) bfalse: ff ifthenelse: if then else 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