Nuprl Lemma : imonomial-req-lemma

∀f:ℤ ⟶ ℝ. ∀ws:ℤ List. ∀t:int_term().
  (real_term_value(f;accumulate (with value t and list item v):
                      t (*) vv
                     over list:
                       ws
                     with starting value:
                      t))
  = (real_term_value(f;t)
    * real_term_value(f;accumulate (with value t and list item v):
                         t (*) vv
                        over list:
                          ws
                        with starting value:
                         "1"))))


Proof



Definitions occuring in Statement :  real_term_value: real_term_value(f;t),  req: x = y,  rmul: a * b,  real: ℝ,  itermMultiply: left (*) right,  itermVar: vvar,  itermConstant: "const",  int_term: int_term(),  list_accum: list_accum,  list: T List,  all: ∀x:A. B[x],  function: x:A ⟶ B[x],  natural_number: $n,  int: ℤ
Definitions unfolded in proof :  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  member: t ∈ T,  so_lambda: λ2x.t[x],  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  so_apply: x[s],  implies: P ⇒ Q,  top: Top,  prop: ℙ,  uimplies: b supposing a,  real_term_value: real_term_value(f;t),  itermMultiply: left (*) right,  int_term_ind: int_term_ind,  itermVar: vvar,  itermConstant: "const",  uiff: uiff(P;Q),  and: P ∧ Q,  rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :  list_induction,  all_wf,  int_term_wf,  req_wf,  real_term_value_wf,  list_accum_wf,  itermMultiply_wf,  itermVar_wf,  rmul_wf,  itermConstant_wf,  list_wf,  list_accum_nil_lemma,  real_term_value_const_lemma,  list_accum_cons_lemma,  real_wf,  int-to-real_wf,  req_weakening,  equal_wf,  req_functionality,  rmul-one,  rmul_functionality,  uiff_transitivity,  req_inversion,  rmul-assoc,  rmul-one-both,  rmul-ac
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation,  cut,  thin,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  intEquality,  sqequalRule,  lambdaEquality,  hypothesis,  functionExtensionality,  applyEquality,  hypothesisEquality,  natural_numberEquality,  independent_functionElimination,  dependent_functionElimination,  isect_memberEquality,  voidElimination,  voidEquality,  rename,  because_Cache,  functionEquality,  independent_isectElimination,  equalityTransitivity,  equalitySymmetry,  productElimination
Latex:
\mforall{}f:\mBbbZ{}  {}\mrightarrow{}  \mBbbR{}.  \mforall{}ws:\mBbbZ{}  List.  \mforall{}t:int\_term().
    (real\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                            t  (*)  vv
                                          over  list:
                                              ws
                                          with  starting  value:
                                            t))
    =  (real\_term\_value(f;t)
        *  real\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                                  t  (*)  vv
                                                over  list:
                                                    ws
                                                with  starting  value:
                                                  "1"))))


Date html generated: 2017_10_02-PM-07_18_59
Last ObjectModification: 2017_07_28-AM-07_21_17

Theory : reals


Home Index