Nuprl Lemma : rng_sum_unroll_unit

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


Proof




Definitions occuring in Statement :  rng_sum: rng_sum rng: Rng rng_car: |r| int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] add: 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) uimplies: supposing a rng: Rng
Lemmas referenced :  mon_itop_unroll_unit 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 equal_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 intEquality addEquality natural_numberEquality equalityTransitivity equalitySymmetry

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



Date html generated: 2016_05_15-PM-00_28_06
Last ObjectModification: 2015_12_26-PM-11_58_36

Theory : rings_1


Home Index