Nuprl Lemma : derivative-rsum

`∀[I:Interval]`
`  ∀n:ℕ. ∀m:{n...}.`
`    ∀[f,f':{n..m + 1-} ⟶ I ⟶ℝ].`
`      ((∀k:{n..m + 1-}. d(f[k;x])/dx = λx.f'[k;x] on I) `` d(Σ{f[k;x] | n≤k≤m})/dx = λx.Σ{f'[k;x] | n≤k≤m} on I)`

Proof

Definitions occuring in Statement :  derivative: `d(f[x])/dx = λz.g[z] on I` rfun: `I ⟶ℝ` interval: `Interval` rsum: `Σ{x[k] | n≤k≤m}` int_upper: `{i...}` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` add: `n + m` natural_number: `\$n`
Definitions unfolded in proof :  rev_uimplies: `rev_uimplies(P;Q)` r-ap: `f(x)` rfun-eq: `rfun-eq(I;f;g)` nequal: `a ≠ b ∈ T ` assert: `↑b` bnot: `¬bb` sq_type: `SQType(T)` bfalse: `ff` uiff: `uiff(P;Q)` ifthenelse: `if b then t else f fi ` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` top: `Top` false: `False` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` ge: `i ≥ j ` guard: `{T}` and: `P ∧ Q` lelt: `i ≤ j < k` int_seg: `{i..j-}` so_apply: `x[s]` subtype_rel: `A ⊆r B` so_apply: `x[s1;s2]` rfun: `I ⟶ℝ` label: `...\$L... t` so_lambda: `λ2x.t[x]` int_upper: `{i...}` nat: `ℕ` prop: `ℙ` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]`
Lemmas referenced :  trivial-int-eq1 decidable__equal_int int_subtype_base derivative-add rsum_unroll req_functionality derivative_functionality req_weakening int_formula_prop_eq_lemma intformeq_wf int_seg_properties radd_wf neg_assert_of_eq_int assert_of_eq_int eq_int_wf assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal equal_wf eqff_to_assert int-to-real_wf assert_of_lt_int eqtt_to_assert bool_wf lt_int_wf decidable__le primrec-wf2 less_than_wf set_wf lelt_wf int_formula_prop_wf int_formula_prop_le_lemma int_term_value_subtract_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf itermSubtract_wf itermConstant_wf itermAdd_wf itermVar_wf intformless_wf intformnot_wf intformand_wf full-omega-unsat decidable__lt nat_properties int_upper_properties rsum_wf subtract_wf le_wf interval_wf nat_wf int_upper_wf rfun_wf i-member_wf real_wf subtype_rel_self derivative_wf int_seg_wf all_wf
Rules used in proof :  cumulativity promote_hyp equalitySymmetry equalityTransitivity equalityElimination instantiate voidEquality voidElimination isect_memberEquality intEquality int_eqEquality dependent_pairFormation independent_functionElimination approximateComputation independent_isectElimination unionElimination dependent_functionElimination independent_pairFormation productElimination dependent_set_memberEquality functionExtensionality setEquality functionEquality applyEquality hypothesisEquality lambdaEquality sqequalRule natural_numberEquality addEquality hypothesis because_Cache rename setElimination thin isectElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[I:Interval]
\mforall{}n:\mBbbN{}.  \mforall{}m:\{n...\}.
\mforall{}[f,f':\{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  I  {}\mrightarrow{}\mBbbR{}].
((\mforall{}k:\{n..m  +  1\msupminus{}\}.  d(f[k;x])/dx  =  \mlambda{}x.f'[k;x]  on  I)
{}\mRightarrow{}  d(\mSigma{}\{f[k;x]  |  n\mleq{}k\mleq{}m\})/dx  =  \mlambda{}x.\mSigma{}\{f'[k;x]  |  n\mleq{}k\mleq{}m\}  on  I)

Date html generated: 2018_05_22-PM-02_45_43
Last ObjectModification: 2018_05_21-AM-00_54_12

Theory : reals

Home Index