Nuprl Lemma : add-rpolynomials

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


Proof




Definitions occuring in Statement :  rpolynomial: i≤n. a_i x^i) req: y radd: b real: int_seg: {i..j-} nat: le_int: i ≤j ifthenelse: if then else fi  uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B 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 uimplies: supposing a rpolynomial: i≤n. a_i x^i) int_seg: {i..j-} nat: all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) and: P ∧ Q lelt: i ≤ j < k ge: i ≥  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 so_lambda: λ2x.t[x] subtype_rel: A ⊆B le: A ≤ B less_than': less_than'(a;b) so_apply: x[s] guard: {T} sq_type: SQType(T) bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q rev_uimplies: rev_uimplies(P;Q) subtract: m true: True pointwise-req: x[k] y[k] for k ∈ [n,m] req_int_terms: t1 ≡ t2
Lemmas referenced :  req_witness radd_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 rsum-split-shift rmul_wf rnexp_wf int_seg_subtype_nat istype-false decidable__le rsum_wf subtract_wf int_seg_properties itermSubtract_wf int_term_value_subtract_lemma 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 radd_functionality req_weakening ifthenelse_wf btrue_wf int_seg_subtype not-le-2 condition-implies-le add-associates minus-add minus-one-mul add-swap minus-one-mul-top add-commutes add_functionality_wrt_le le-add-cancel2 bfalse_wf rsum_functionality rmul-distrib2 req_inversion rsum_linearity1 req-iff-rsub-is-0 real_polynomial_null int-to-real_wf real_term_value_sub_lemma real_term_value_add_lemma real_term_value_var_lemma real_term_value_const_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality_alt setElimination rename because_Cache inhabitedIsType lambdaFormation_alt unionElimination equalityElimination 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 closedConclusion promote_hyp instantiate cumulativity minusEquality

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_02
Last ObjectModification: 2019_01_06-PM-05_13_03

Theory : reals


Home Index