`∀[I:Interval]. ∀[f1,f2,g1,g2:I ⟶ℝ].`
`  (d(f1[x])/dx = λx.g1[x] on I `` d(f2[x])/dx = λx.g2[x] on I `` d(f1[x] + f2[x])/dx = λx.g1[x] + g2[x] on I)`

Proof

Definitions occuring in Statement :  derivative: `d(f[x])/dx = λz.g[z] on I` rfun: `I ⟶ℝ` interval: `Interval` radd: `a + b` uall: `∀[x:A]. B[x]` so_apply: `x[s]` implies: `P `` Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` derivative: `d(f[x])/dx = λz.g[z] on I` all: `∀x:A. B[x]` member: `t ∈ T` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` and: `P ∧ Q` prop: `ℙ` sq_exists: `∃x:{A| B[x]}` cand: `A c∧ B` iff: `P `⇐⇒` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` label: `...\$L... t` rfun: `I ⟶ℝ` uimplies: `b supposing a` rneq: `x ≠ y` guard: `{T}` or: `P ∨ Q` rev_implies: `P `` Q` rless: `x < y` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` rsub: `x - y` uiff: `uiff(P;Q)` subtype_rel: `A ⊆r B` real: `ℝ` sq_stable: `SqStable(P)`
Lemmas referenced :  mul_nat_plus less_than_wf rmin_wf rmin_strict_ub i-member-approx rleq_wf rabs_wf rsub_wf i-member_wf i-approx_wf real_wf set_wf nat_plus_wf icompact_wf iproper_wf derivative_wf rfun_wf interval_wf rless_wf int-to-real_wf all_wf radd_wf rmul_wf rdiv_wf rless-int nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf rmin-rleq rleq_functionality_wrt_implies rleq_weakening_equal equal_wf req_wf rminus_wf req_weakening uiff_transitivity req_functionality radd_functionality rminus_functionality req_transitivity rmul-distrib rmul_over_rminus rminus-radd req_inversion radd-assoc radd-ac radd_comm rmul_functionality rminus-as-rmul rminus-rminus rleq_functionality rabs_functionality itermMultiply_wf int_term_value_mul_lemma rleq_transitivity r-triangle-inequality radd_functionality_wrt_rleq rmul-distrib2 radd-rdiv rdiv_functionality radd-int rleq-int-fractions sq_stable__less_than sq_stable__and sq_stable__icompact sq_stable__iproper decidable__le intformle_wf int_formula_prop_le_lemma rleq-int-fractions2 zero-rleq-rabs rmul_functionality_wrt_rleq2
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation sqequalHypSubstitution cut hypothesis dependent_functionElimination thin introduction extract_by_obid isectElimination dependent_set_memberEquality natural_numberEquality sqequalRule independent_pairFormation imageMemberEquality hypothesisEquality baseClosed setElimination rename dependent_set_memberFormation productElimination because_Cache independent_functionElimination lambdaEquality productEquality applyEquality setEquality functionEquality independent_isectElimination inrFormation unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll equalityTransitivity equalitySymmetry minusEquality multiplyEquality addEquality imageElimination inlFormation

Latex:
\mforall{}[I:Interval].  \mforall{}[f1,f2,g1,g2:I  {}\mrightarrow{}\mBbbR{}].
(d(f1[x])/dx  =  \mlambda{}x.g1[x]  on  I
{}\mRightarrow{}  d(f2[x])/dx  =  \mlambda{}x.g2[x]  on  I
{}\mRightarrow{}  d(f1[x]  +  f2[x])/dx  =  \mlambda{}x.g1[x]  +  g2[x]  on  I)

Date html generated: 2017_10_03-PM-00_08_44
Last ObjectModification: 2017_07_28-AM-08_34_15

Theory : reals

Home Index