### Nuprl Lemma : sum-reindex2

`∀[n:ℕ]. ∀[a:ℕn ⟶ ℤ]. ∀[m:ℕ]. ∀[b:ℕm ⟶ ℤ]. ∀[f:{i:ℕn| ¬(a[i] = 0 ∈ ℤ)}  ⟶ {j:ℕm| ¬(b[j] = 0 ∈ ℤ)} ].`
`  (Σ(a[i] | i < n) = Σ(b[j] | j < m) ∈ ℤ) supposing `
`     ((∀i:{i:ℕn| ¬(a[i] = 0 ∈ ℤ)} . (a[i] = b[f i] ∈ ℤ)) and `
`     Bij({i:ℕn| ¬(a[i] = 0 ∈ ℤ)} ;{j:ℕm| ¬(b[j] = 0 ∈ ℤ)} ;f))`

Proof

Definitions occuring in Statement :  sum: `Σ(f[x] | x < k)` biject: `Bij(A;B;f)` int_seg: `{i..j-}` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` nat: `ℕ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` exists: `∃x:A. B[x]` and: `P ∧ Q`
Lemmas referenced :  sum-reindex nat_wf biject_wf equal_wf equal-wf-T-base not_wf int_seg_wf all_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin setEquality natural_numberEquality setElimination rename hypothesisEquality intEquality applyEquality baseClosed sqequalRule lambdaEquality lambdaFormation dependent_set_memberEquality because_Cache isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry functionEquality independent_isectElimination dependent_pairFormation independent_pairFormation productEquality

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[m:\mBbbN{}].  \mforall{}[b:\mBbbN{}m  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[f:\{i:\mBbbN{}n|  \mneg{}(a[i]  =  0)\}    {}\mrightarrow{}  \{j:\mBbbN{}m|  \mneg{}(b[j]  =  0)\}  ].
(\mSigma{}(a[i]  |  i  <  n)  =  \mSigma{}(b[j]  |  j  <  m))  supposing
((\mforall{}i:\{i:\mBbbN{}n|  \mneg{}(a[i]  =  0)\}  .  (a[i]  =  b[f  i]))  and
Bij(\{i:\mBbbN{}n|  \mneg{}(a[i]  =  0)\}  ;\{j:\mBbbN{}m|  \mneg{}(b[j]  =  0)\}  ;f))

Date html generated: 2016_05_15-PM-07_23_37
Last ObjectModification: 2016_01_16-AM-09_41_45

Theory : general

Home Index