### Nuprl Lemma : derivative-minus

`∀I:Interval. ∀f,g:I ⟶ℝ.  (λx.g[x] = d(f[x])/dx on I `` λx.-(g[x]) = d(-(f[x]))/dx on I)`

Proof

Definitions occuring in Statement :  derivative: `λz.g[z] = d(f[x])/dx on I` rfun: `I ⟶ℝ` interval: `Interval` rminus: `-(x)` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` prop: `ℙ` so_lambda: `λ2x.t[x]` label: `...\$L... t` rfun: `I ⟶ℝ` so_apply: `x[s]` uimplies: `b supposing a` rfun-eq: `rfun-eq(I;f;g)` r-ap: `f(x)` uiff: `uiff(P;Q)` and: `P ∧ Q` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  derivative-const-mul int-to-real_wf derivative_wf real_wf i-member_wf rfun_wf interval_wf rmul_wf rminus_wf req_wf req_weakening set_wf derivative_functionality uiff_transitivity req_functionality rminus-as-rmul req_inversion
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity dependent_functionElimination thin isectElimination minusEquality natural_numberEquality hypothesis lambdaFormation hypothesisEquality independent_functionElimination sqequalRule lambdaEquality applyEquality setEquality because_Cache independent_isectElimination productElimination

Latex:
\mforall{}I:Interval.  \mforall{}f,g:I  {}\mrightarrow{}\mBbbR{}.    (\mlambda{}x.g[x]  =  d(f[x])/dx  on  I  {}\mRightarrow{}  \mlambda{}x.-(g[x])  =  d(-(f[x]))/dx  on  I)

Date html generated: 2016_05_18-AM-10_07_08
Last ObjectModification: 2015_12_27-PM-11_03_44

Theory : reals

Home Index