Nuprl Lemma : rpoly-nth-deriv_functionality

[d,n:ℕ]. ∀[a,b:ℕ1 ⟶ ℝ]. ∀[x1,x2:ℝ].
  (rpoly-nth-deriv(n;d;a;x1) rpoly-nth-deriv(n;d;b;x2)) supposing ((x1 x2) and (∀i:ℕ1. ((a i) (b i))))


Definitions occuring in Statement :  rpoly-nth-deriv: rpoly-nth-deriv(n;d;a;x) req: y real: int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] apply: a function: x:A ⟶ B[x] add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a rpoly-nth-deriv: rpoly-nth-deriv(n;d;a;x) nat: all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A rpolynomial: i≤n. a_i x^i) ge: i ≥  decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top subtract: m so_lambda: λ2x.t[x] subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) so_apply: x[s] pointwise-req: x[k] y[k] for k ∈ [n,m] int_seg: {i..j-} lelt: i ≤ j < k nat_plus: + int_nzero: -o nequal: a ≠ b ∈  rev_uimplies: rev_uimplies(P;Q) rneq: x ≠ y iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int req_weakening int-to-real_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot less_than_wf poly-nth-deriv_wf subtract_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermAdd_wf itermSubtract_wf itermVar_wf intformless_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf int_subtype_base add-commutes add-associates minus-one-mul add-swap add-mul-special zero-mul add-zero rsum_functionality rmul_wf rnexp_wf int_seg_subtype_nat false_wf int_seg_wf rmul_functionality decidable__lt lelt_wf req_witness rpoly-nth-deriv_wf req_wf all_wf real_wf nat_wf poly-nth-deriv-req int-rdiv_wf fact_wf subtype_rel_sets nequal_wf nat_plus_properties intformeq_wf int_formula_prop_eq_lemma equal-wf-base nat_plus_wf req_functionality rdiv_wf rless-int rless_wf int-rdiv-req rdiv_functionality rnexp_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename because_Cache hypothesis hypothesisEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule natural_numberEquality dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination dependent_set_memberEquality addEquality lambdaEquality int_eqEquality intEquality isect_memberEquality voidEquality independent_pairFormation computeAll multiplyEquality applyEquality functionExtensionality functionEquality setEquality applyLambdaEquality baseClosed inrFormation

\mforall{}[d,n:\mBbbN{}].  \mforall{}[a,b:\mBbbN{}d  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x1,x2:\mBbbR{}].
    (rpoly-nth-deriv(n;d;a;x1)  =  rpoly-nth-deriv(n;d;b;x2))  supposing 
          ((x1  =  x2)  and 
          (\mforall{}i:\mBbbN{}d  +  1.  ((a  i)  =  (b  i))))

Date html generated: 2017_10_03-PM-00_15_38
Last ObjectModification: 2017_07_28-AM-08_37_59

Theory : reals

Home Index