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))


Definitions occuring in Statement :  sum: Σ(f[x] x < k) biject: Bij(A;B;f) int_seg: {i..j-} nat: uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] all: x:A. B[x] not: ¬A set: {x:A| B[x]}  apply: a function: x:A ⟶ B[x] natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: nat: so_apply: x[s] so_lambda: λ2x.t[x] all: x:A. B[x] subtype_rel: A ⊆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

\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