### Nuprl Lemma : gen-divisors-sum-int-ring

[n:ℕ+]. ∀[f:ℕ+1 ⟶ ℤ].  (Σ i|n. f[i] = Σ i|n. f[i]  ∈ ℤ)

Proof

Definitions occuring in Statement :  gen-divisors-sum: Σ i|n. f[i] divisors-sum: Σ i|n. f[i]  int_seg: {i..j-} nat_plus: + uall: [x:A]. B[x] so_apply: x[s] function: x:A ⟶ B[x] add: m natural_number: \$n int: equal: t ∈ T int_ring: -rng
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T divisors-sum: Σ i|n. f[i]  gen-divisors-sum: Σ i|n. f[i] int_ring: -rng rng_zero: 0 pi2: snd(t) pi1: fst(t) rng_plus: +r nat_plus: + subtype_rel: A ⊆B and: P ∧ Q prop: uimplies: supposing a int_seg: {i..j-} lelt: i ≤ j < k squash: T so_lambda: λ2x.t[x] nequal: a ≠ b ∈  guard: {T} not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False all: x:A. B[x] top: Top bool: 𝔹 unit: Unit it: btrue: tt ifthenelse: if then else fi  uiff: uiff(P;Q) so_apply: x[s] bfalse: ff or: P ∨ Q sq_type: SQType(T) bnot: ¬bb assert: b decidable: Dec(P) subtract: m true: True iff: ⇐⇒ Q rev_implies:  Q nat:
Lemmas referenced :  from-upto_wf list-subtype-bag le_wf less_than_wf int_seg_wf nat_plus_wf equal_wf squash_wf true_wf bag-summation-from-upto eq_int_wf int_seg_properties nat_plus_properties satisfiable-full-omega-tt intformand_wf intformeq_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf equal-wf-base int_subtype_base bool_wf eqtt_to_assert assert_of_eq_int eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot neg_assert_of_eq_int sum_wf nat_plus_subtype_nat itermAdd_wf int_term_value_add_lemma add-member-int_seg2 decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma add-subtract-cancel decidable__lt intformless_wf int_formula_prop_less_lemma lelt_wf iff_weakening_equal nat_wf decidable__equal_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin natural_numberEquality addEquality setElimination rename because_Cache hypothesis applyEquality setEquality intEquality productEquality hypothesisEquality independent_isectElimination lambdaEquality functionEquality isect_memberEquality axiomEquality imageElimination equalityTransitivity equalitySymmetry universeEquality remainderEquality productElimination lambdaFormation dependent_pairFormation int_eqEquality dependent_functionElimination voidElimination voidEquality independent_pairFormation computeAll baseClosed unionElimination equalityElimination functionExtensionality promote_hyp instantiate cumulativity independent_functionElimination baseApply closedConclusion dependent_set_memberEquality imageMemberEquality

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[f:\mBbbN{}\msupplus{}n  +  1  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}  i|n.  f[i]  =  \mSigma{}  i|n.  f[i]  )

Date html generated: 2018_05_21-PM-07_31_40
Last ObjectModification: 2017_07_26-PM-05_06_52

Theory : general

Home Index