### Nuprl Lemma : rpoly-nth-deriv-linear

[d,n:ℕ]. ∀[a,b:ℕ1 ⟶ ℝ]. ∀[x:ℝ].
(rpoly-nth-deriv(n;d;λi.((a i) (b i));x) (rpoly-nth-deriv(n;d;a;x) rpoly-nth-deriv(n;d;b;x)))

Proof

Definitions occuring in Statement :  rpoly-nth-deriv: rpoly-nth-deriv(n;d;a;x) req: y radd: b real: int_seg: {i..j-} nat: uall: [x:A]. B[x] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] add: m natural_number: \$n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T rpoly-nth-deriv: rpoly-nth-deriv(n;d;a;x) nat: all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  itermConstant: "const" req_int_terms: t1 ≡ t2 real_term_value: real_term_value(f;t) int_term_ind: int_term_ind itermSubtract: left (-) right itermAdd: left (+) right bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A rpolynomial: i≤n. a_i x^i) rev_uimplies: rev_uimplies(P;Q) pointwise-req: x[k] y[k] for k ∈ [n,m] so_apply: x[s] less_than': less_than'(a;b) le: A ≤ B subtype_rel: A ⊆B so_lambda: λ2x.t[x] lelt: i ≤ j < k int_seg: {i..j-} subtract: m top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) decidable: Dec(P) ge: i ≥  nequal: a ≠ b ∈  int_nzero: -o nat_plus: + rev_implies:  Q iff: ⇐⇒ Q rneq: x ≠ y
Lemmas referenced :  lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int real_term_polynomial itermSubtract_wf itermConstant_wf itermAdd_wf int-to-real_wf req-iff-rsub-is-0 radd_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot less_than_wf req_witness rpoly-nth-deriv_wf int_seg_wf real_wf nat_wf rsum_linearity1 req_inversion req_weakening req_functionality rsum_functionality false_wf int_seg_subtype_nat rnexp_wf rmul_wf rsum_wf lelt_wf decidable__lt add-zero zero-mul add-mul-special add-swap minus-one-mul add-associates add-commutes int_subtype_base le_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties subtract_wf poly-nth-deriv_wf radd_functionality rmul_functionality nat_plus_wf equal-wf-base int_formula_prop_eq_lemma intformeq_wf nat_plus_properties nequal_wf subtype_rel_sets fact_wf int-rdiv_wf poly-nth-deriv-req int-rdiv-req rless_wf rless-int rdiv_wf rmul-rdiv-cancel rmul-ac rmul_comm rmul-assoc rmul-distrib rdiv_functionality uiff_transitivity req_wf rmul_preserves_req
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis hypothesisEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule dependent_functionElimination natural_numberEquality computeAll lambdaEquality intEquality dependent_pairFormation promote_hyp instantiate cumulativity independent_functionElimination voidElimination applyEquality functionExtensionality addEquality isect_memberEquality functionEquality multiplyEquality independent_pairFormation voidEquality int_eqEquality dependent_set_memberEquality baseClosed applyLambdaEquality setEquality inrFormation

Latex:
\mforall{}[d,n:\mBbbN{}].  \mforall{}[a,b:\mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].
(rpoly-nth-deriv(n;d;\mlambda{}i.((a  i)  +  (b  i));x)
=  (rpoly-nth-deriv(n;d;a;x)  +  rpoly-nth-deriv(n;d;b;x)))

Date html generated: 2017_10_03-PM-00_16_02
Last ObjectModification: 2017_07_28-AM-08_38_16

Theory : reals

Home Index