### Nuprl Lemma : rng_sum_swap

`∀[r:Rng]. ∀[k,m:ℕ]. ∀[F:ℕm ⟶ ℕk ⟶ |r|].`
`  ((Σ(r) 0 ≤ i < m. Σ(r) 0 ≤ j < k. F[i;j]) = (Σ(r) 0 ≤ j < k. Σ(r) 0 ≤ i < m. F[i;j]) ∈ |r|)`

Proof

Definitions occuring in Statement :  rng_sum: rng_sum rng: `Rng` rng_car: `|r|` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` function: `x:A ⟶ B[x]` natural_number: `\$n` equal: `s = t ∈ T`
Definitions unfolded in proof :  or: `P ∨ Q` decidable: `Dec(P)` rng: `Rng` prop: `ℙ` and: `P ∧ Q` top: `Top` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` ge: `i ≥ j ` false: `False` implies: `P `` Q` nat: `ℕ` member: `t ∈ T` uall: `∀[x:A]. B[x]` true: `True` so_apply: `x[s]` so_apply: `x[s1;s2]` so_lambda: `λ2x.t[x]` squash: `↓T` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` infix_ap: `x f y` lelt: `i ≤ j < k` int_seg: `{i..j-}` so_lambda: `λ2x y.t[x; y]`
Lemmas referenced :  rng_wf nat_wf int_term_value_subtract_lemma int_formula_prop_not_lemma itermSubtract_wf intformnot_wf subtract_wf decidable__le rng_car_wf int_seg_wf less_than_wf ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_and_lemma intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat nat_properties rng_zero_wf rng_sum_wf equal_wf squash_wf true_wf rng_sum_unroll_base iff_weakening_equal rng_sum_unroll_hi rng_plus_zero rng_plus_wf lelt_wf decidable__lt int_seg_properties infix_ap_wf rng_sum_plus
Rules used in proof :  unionElimination because_Cache functionEquality axiomEquality independent_pairFormation sqequalRule voidEquality voidElimination isect_memberEquality dependent_functionElimination intEquality int_eqEquality lambdaEquality dependent_pairFormation independent_functionElimination approximateComputation independent_isectElimination natural_numberEquality lambdaFormation intWeakElimination rename setElimination hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution functionExtensionality applyEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed productElimination dependent_set_memberEquality

Latex:
\mforall{}[r:Rng].  \mforall{}[k,m:\mBbbN{}].  \mforall{}[F:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  |r|].
((\mSigma{}(r)  0  \mleq{}  i  <  m.  \mSigma{}(r)  0  \mleq{}  j  <  k.  F[i;j])  =  (\mSigma{}(r)  0  \mleq{}  j  <  k.  \mSigma{}(r)  0  \mleq{}  i  <  m.  F[i;j]))

Date html generated: 2018_05_21-PM-03_15_09
Last ObjectModification: 2017_12_11-PM-05_05_44

Theory : rings_1

Home Index