Nuprl Lemma : rng_sum_unroll_hi

[r:Rng]. ∀[i,j:ℤ].
  ∀[E:{i..j-} ⟶ |r|]. ((Σ(r) i ≤ k < j. E[k]) ((Σ(r) i ≤ k < 1. E[k]) +r E[j 1]) ∈ |r|) supposing i < j


Proof




Definitions occuring in Statement :  rng_sum: rng_sum rng: Rng rng_plus: +r rng_car: |r| int_seg: {i..j-} less_than: a < b uimplies: supposing a uall: [x:A]. B[x] infix_ap: y so_apply: x[s] function: x:A ⟶ B[x] subtract: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B grp: Group{i} mon: Mon imon: IMonoid prop: rng_sum: rng_sum add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) uimplies: supposing a rng: Rng
Lemmas referenced :  mon_itop_unroll_hi add_grp_of_rng_wf_a grp_sig_wf monoid_p_wf grp_car_wf grp_op_wf grp_id_wf inverse_wf grp_inv_wf int_seg_wf rng_car_wf less_than_wf rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality sqequalRule lambdaEquality setElimination rename setEquality cumulativity isect_memberEquality axiomEquality functionEquality equalityTransitivity equalitySymmetry intEquality

Latex:
\mforall{}[r:Rng].  \mforall{}[i,j:\mBbbZ{}].
    \mforall{}[E:\{i..j\msupminus{}\}  {}\mrightarrow{}  |r|].  ((\mSigma{}(r)  i  \mleq{}  k  <  j.  E[k])  =  ((\mSigma{}(r)  i  \mleq{}  k  <  j  -  1.  E[k])  +r  E[j  -  1])) 
    supposing  i  <  j



Date html generated: 2016_05_15-PM-00_28_03
Last ObjectModification: 2015_12_26-PM-11_58_38

Theory : rings_1


Home Index