### Nuprl Lemma : derivative-rdiv-const

`∀a:ℝ. (a ≠ r0 `` (∀I:Interval. ∀f,f':I ⟶ℝ.  (λx.f'[x] = d(f[x])/dx on I `` λx.(f'[x]/a) = 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` rdiv: `(x/y)` rneq: `x ≠ y` int-to-real: `r(n)` real: `ℝ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` natural_number: `\$n`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` rdiv: `(x/y)` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` rfun: `I ⟶ℝ` so_apply: `x[s]` prop: `ℙ` label: `...\$L... t`
Lemmas referenced :  derivative-const-mul2 rinv_wf2 real_wf i-member_wf derivative_wf rfun_wf interval_wf rneq_wf int-to-real_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalRule cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isectElimination hypothesisEquality independent_functionElimination hypothesis lambdaEquality applyEquality setEquality because_Cache natural_numberEquality

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

Date html generated: 2016_05_18-AM-10_13_18
Last ObjectModification: 2015_12_27-PM-10_58_35

Theory : reals

Home Index