Nuprl Lemma : derivative-const-mul2

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


Proof




Definitions occuring in Statement :  derivative: λz.g[z] d(f[x])/dx on I rfun: I ⟶ℝ interval: Interval rmul: b real: so_apply: x[s] all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T implies:  Q prop: uall: [x:A]. B[x] so_lambda: λ2x.t[x] label: ...$L... t rfun: I ⟶ℝ so_apply: x[s] rfun-eq: rfun-eq(I;f;g) r-ap: f(x)
Lemmas referenced :  derivative-const-mul derivative_wf real_wf i-member_wf rfun_wf interval_wf rmul_wf rmul_comm set_wf derivative_functionality
Rules used in proof :  cut lemma_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality independent_functionElimination isectElimination sqequalRule lambdaEquality applyEquality setEquality because_Cache

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



Date html generated: 2016_05_18-AM-10_06_54
Last ObjectModification: 2015_12_27-PM-11_03_30

Theory : reals


Home Index