Nuprl Lemma : derivative-const

[I:Interval]. ∀[c:ℝ].  d(c)/dx = λx.r0 on I


Proof




Definitions occuring in Statement :  derivative: d(f[x])/dx = λz.g[z] on I interval: Interval int-to-real: r(n) real: uall: [x:A]. B[x] natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] derivative: d(f[x])/dx = λz.g[z] on I all: x:A. B[x] sq_exists: x:{A| B[x]} member: t ∈ T and: P ∧ Q cand: c∧ B iff: ⇐⇒ Q rev_implies:  Q implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) true: True prop: nat_plus: + so_lambda: λ2x.t[x] uimplies: supposing a rneq: x ≠ y guard: {T} or: 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 so_apply: x[s] subtype_rel: A ⊆B nat: uiff: uiff(P;Q) absval: |i| itermConstant: "const" req_int_terms: t1 ≡ t2 rev_uimplies: rev_uimplies(P;Q) real: sq_stable: SqStable(P)
Lemmas referenced :  int-to-real_wf rless-int rleq_wf rabs_wf rsub_wf i-member_wf i-approx_wf less_than_wf rless_wf all_wf real_wf rmul_wf rdiv_wf 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 set_wf nat_plus_wf icompact_wf iproper_wf interval_wf req_wf absval_wf nat_wf req-int decidable__equal_int intformeq_wf int_formula_prop_eq_lemma uiff_transitivity2 req_functionality rabs_functionality real_term_polynomial itermSubtract_wf itermMultiply_wf real_term_value_const_lemma real_term_value_sub_lemma real_term_value_var_lemma real_term_value_mul_lemma req-iff-rsub-is-0 req_weakening squash_wf true_wf rabs-int rmul-nonneg-case1 rleq-int-fractions2 sq_stable__less_than sq_stable__and sq_stable__icompact sq_stable__iproper decidable__le intformle_wf int_formula_prop_le_lemma int_term_value_mul_lemma zero-rleq-rabs rleq_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation dependent_set_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality hypothesis dependent_functionElimination productElimination independent_functionElimination sqequalRule independent_pairFormation imageMemberEquality hypothesisEquality baseClosed dependent_set_memberEquality setElimination rename because_Cache productEquality lambdaEquality functionEquality independent_isectElimination inrFormation unionElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality computeAll applyEquality minusEquality imageElimination equalityTransitivity equalitySymmetry addEquality multiplyEquality

Latex:
\mforall{}[I:Interval].  \mforall{}[c:\mBbbR{}].    d(c)/dx  =  \mlambda{}x.r0  on  I



Date html generated: 2017_10_03-PM-00_11_15
Last ObjectModification: 2017_07_28-AM-08_35_27

Theory : reals


Home Index