### Nuprl Lemma : sum-reindex

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

Proof

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] exists: x:A. B[x] not: ¬A and: P ∧ Q 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 so_lambda: λ2x.t[x] so_apply: x[s] nat: all: x:A. B[x] implies:  Q prop: so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] subtype_rel: A ⊆B ge: i ≥  exists: x:A. B[x] and: P ∧ Q decidable: Dec(P) or: P ∨ Q not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False top: Top bag-no-repeats: bag-no-repeats(T;bs) cand: c∧ B squash: T int_seg: {i..j-} istype: istype(T) lelt: i ≤ j < k le: A ≤ B iff: ⇐⇒ Q rev_implies:  Q uiff: uiff(P;Q) bag-member: x ↓∈ bs less_than: a < b biject: Bij(A;B;f) inject: Inj(A;B;f) bnot: ¬bb ifthenelse: if then else fi  btrue: tt true: True guard: {T} sq_type: SQType(T) rev_uimplies: rev_uimplies(P;Q) surject: Surj(A;B;f) less_than': less_than'(a;b) compose: g
Lemmas referenced :  sum-as-bag-accum int_seg_wf bag-accum_wf assert_wf bnot_wf eq_int_wf istype-assert istype-int bag-filter_wf bag-map_wf list-subtype-bag nat_properties decidable__equal_int full-omega-unsat intformnot_wf intformeq_wf itermAdd_wf itermVar_wf int_formula_prop_not_lemma istype-void int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf equal-wf-base int_subtype_base biject_wf not_wf bag-filter-map upto_wf subtype_rel_self no_repeats_upto equal_wf bag_wf no_repeats_wf bag-no-repeats_wf le_wf lelt_wf set_subtype_base list_subtype_base bag-extensionality-no-repeats decidable__equal_int_seg subtype_rel_bag subtype_rel_dep_function subtype_rel_sets_simple iff_transitivity iff_weakening_uiff assert_of_bnot assert_of_eq_int bag-member_wf bag-filter-no-repeats bag-map-no-repeats assert_elim bfalse_wf squash_wf true_wf istype-universe bool_wf eq_int_eq_true iff_weakening_equal btrue_neq_bfalse subtype_base_sq bag-filter-no-repeats2 subtype_rel_sets bag-member-map bag-member-filter bag-member-filter-set istype-less_than istype-le l_member_wf int_formula_prop_less_lemma int_formula_prop_and_lemma intformless_wf intformand_wf decidable__lt int_seg_properties istype-false int_seg_subtype_nat nat_wf subtype_rel_set member_upto2 int_term_value_constant_lemma itermConstant_wf list_wf bag-map-map set_wf equal-wf-T-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality_alt applyEquality universeIsType natural_numberEquality setElimination rename hypothesis because_Cache inhabitedIsType lambdaFormation_alt closedConclusion setEquality intEquality addEquality setIsType independent_isectElimination productElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination equalityIstype equalityTransitivity equalitySymmetry hyp_replacement applyLambdaEquality productIsType functionIsType baseClosed sqequalBase axiomEquality isectIsTypeImplies dependent_set_memberEquality dependent_pairFormation independent_pairFormation productEquality imageMemberEquality baseApply equalityIsType4 dependent_set_memberEquality_alt imageElimination instantiate universeEquality cumulativity equalityIsType1 lambdaFormation isect_memberEquality voidEquality lambdaEquality functionExtensionality functionEquality impliesFunctionality

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

Date html generated: 2019_10_15-AM-11_33_28
Last ObjectModification: 2019_06_26-PM-04_41_32

Theory : general

Home Index