Nuprl Lemma : subtract-rpolynomials-same-degree

[n:ℕ]. ∀[a,b:ℕ1 ⟶ ℝ]. ∀[x:ℝ].  (((Σi≤n. a_i x^i) i≤n. b_i x^i)) i≤n. λi.((a i) i)_i x^i))


Proof




Definitions occuring in Statement :  rpolynomial: i≤n. a_i x^i) rsub: y req: y real: int_seg: {i..j-} nat: uall: [x:A]. B[x] apply: a lambda: λx.A[x] function: x:A ⟶ B[x] add: m natural_number: $n
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q int_seg: {i..j-} ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top prop: pointwise-req: x[k] y[k] for k ∈ [n,m] so_apply: x[s] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  lelt: i ≤ j < k bfalse: ff sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  req_witness rsub_wf rpolynomial_wf int_seg_wf real_wf istype-nat ifthenelse_wf le_int_wf nat_properties decidable__le full-omega-unsat intformnot_wf intformle_wf itermVar_wf istype-int int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_var_lemma int_formula_prop_wf eqtt_to_assert assert_of_le_int req_weakening intformand_wf itermConstant_wf int_formula_prop_and_lemma int_term_value_constant_lemma decidable__lt intformless_wf itermAdd_wf int_formula_prop_less_lemma int_term_value_add_lemma istype-le istype-less_than eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base assert-bnot iff_weakening_uiff assert_wf le_wf req_functionality subtract-rpolynomials rpolynomial_functionality
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality_alt applyEquality universeIsType natural_numberEquality addEquality setElimination rename independent_functionElimination sqequalRule isect_memberEquality_alt because_Cache isectIsTypeImplies inhabitedIsType functionIsType dependent_functionElimination unionElimination independent_isectElimination approximateComputation dependent_pairFormation_alt int_eqEquality voidElimination lambdaFormation_alt equalityElimination productElimination dependent_set_memberEquality_alt independent_pairFormation productIsType equalityTransitivity equalitySymmetry equalityIstype promote_hyp instantiate cumulativity

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbR{}].  \mforall{}[x:\mBbbR{}].
    (((\mSigma{}i\mleq{}n.  a\_i  *  x\^{}i)  -  (\mSigma{}i\mleq{}n.  b\_i  *  x\^{}i))  =  (\mSigma{}i\mleq{}n.  \mlambda{}i.((a  i)  -  b  i)\_i  *  x\^{}i))



Date html generated: 2019_10_29-AM-10_14_44
Last ObjectModification: 2019_01_06-PM-05_25_06

Theory : reals


Home Index