Nuprl Lemma : subtract-rpolynomials

∀[n,m:ℕ]. ∀[a:ℕn + 1 ⟶ ℝ]. ∀[b:ℕm + 1 ⟶ ℝ]. ∀[x:ℝ].
  ((Σi≤n. a_i * x^i) - (Σi≤m. b_i * x^i)) = (Σi≤n. λi.if i ≤z m then (a i) - b i else a i fi _i * x^i) supposing m ≤ n


Proof



Definitions occuring in Statement :  rpolynomial: (Σi≤n. a_i * x^i),  rsub: x - y,  req: x = y,  real: ℝ,  int_seg: {i..j-},  nat: ℕ,  le_int: i ≤z j,  ifthenelse: if b then t else f fi ,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  le: A ≤ B,  apply: f a,  lambda: λx.A[x],  function: x:A ⟶ B[x],  add: n + m,  natural_number: $n
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  int_seg: {i..j-},  nat: ℕ,  all: ∀x:A. B[x],  implies: P ⇒ Q,  bool: 𝔹,  unit: Unit,  it: ⋅,  btrue: tt,  ifthenelse: if b then t else f fi ,  uiff: uiff(P;Q),  and: P ∧ Q,  lelt: i ≤ j < k,  ge: i ≥ j ,  decidable: Dec(P),  or: P ∨ Q,  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  false: False,  top: Top,  prop: ℙ,  bfalse: ff,  rsub: x - y,  rev_uimplies: rev_uimplies(P;Q),  pointwise-req: x[k] = y[k] for k ∈ [n,m],  so_apply: x[s],  sq_type: SQType(T),  guard: {T},  bnot: ¬bb,  assert: ↑b,  rev_implies: P ⇐ Q,  iff: P ⇐⇒ Q,  req_int_terms: t1 ≡ t2
Lemmas referenced :  req_witness,  rsub_wf,  rpolynomial_wf,  le_int_wf,  eqtt_to_assert,  assert_of_le_int,  nat_properties,  decidable__lt,  full-omega-unsat,  intformand_wf,  intformnot_wf,  intformless_wf,  itermVar_wf,  itermAdd_wf,  itermConstant_wf,  intformle_wf,  istype-int,  int_formula_prop_and_lemma,  istype-void,  int_formula_prop_not_lemma,  int_formula_prop_less_lemma,  int_term_value_var_lemma,  int_term_value_add_lemma,  int_term_value_constant_lemma,  int_formula_prop_le_lemma,  int_formula_prop_wf,  istype-le,  istype-less_than,  int_seg_wf,  real_wf,  istype-nat,  radd_wf,  rminus_wf,  rmul_wf,  int-to-real_wf,  req_functionality,  radd_functionality,  rminus-as-rmul,  req_weakening,  req_wf,  uiff_transitivity,  rmul-rpolynomial,  add-rpolynomials,  rpolynomial_functionality,  eqff_to_assert,  bool_cases_sqequal,  subtype_base_sq,  bool_wf,  bool_subtype_base,  assert-bnot,  iff_weakening_uiff,  assert_wf,  le_wf,  decidable__le,  itermSubtract_wf,  itermMultiply_wf,  itermMinus_wf,  req-iff-rsub-is-0,  real_polynomial_null,  real_term_value_sub_lemma,  real_term_value_add_lemma,  real_term_value_var_lemma,  real_term_value_mul_lemma,  real_term_value_const_lemma,  real_term_value_minus_lemma
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  introduction,  cut,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  hypothesisEquality,  hypothesis,  lambdaEquality_alt,  setElimination,  rename,  because_Cache,  inhabitedIsType,  lambdaFormation_alt,  unionElimination,  equalityElimination,  sqequalRule,  productElimination,  independent_isectElimination,  applyEquality,  dependent_set_memberEquality_alt,  independent_pairFormation,  dependent_functionElimination,  addEquality,  natural_numberEquality,  approximateComputation,  independent_functionElimination,  dependent_pairFormation_alt,  int_eqEquality,  isect_memberEquality_alt,  voidElimination,  universeIsType,  productIsType,  equalityIstype,  equalityTransitivity,  equalitySymmetry,  isectIsTypeImplies,  functionIsType,  minusEquality,  closedConclusion,  promote_hyp,  instantiate,  cumulativity
Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[b:\mBbbN{}m  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].
    ((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  -  (\mSigma{}i\mleq{}m.  b\_i  *  x\^{}i))
    =  (\mSigma{}i\mleq{}n.  \mlambda{}i.if  i  \mleq{}z  m  then  (a  i)  -  b  i  else  a  i  fi  \_i  *  x\^{}i) 
    supposing  m  \mleq{}  n


Date html generated: 2019_10_29-AM-10_14_17
Last ObjectModification: 2019_01_06-PM-05_23_52

Theory : reals


Home Index