### Nuprl Lemma : bag-summation-partitions-primes

`∀[h:ℕ+ ⟶ ℕ+ ⟶ ℤ]. ∀[b:bag(Prime)].`
`  (Σ(p∈bag-partitions(IntDeq;b)). h[Π(fst(p));Π(snd(p))] = Σ i|Π(b). h[i;Π(b) ÷ i]  ∈ ℤ)`

Proof

Definitions occuring in Statement :  bag-partitions: `bag-partitions(eq;bs)` divisors-sum: `Σ i|n. f[i] ` Prime: `Prime` int-bag-product: `Π(b)` bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` int-deq: `IntDeq` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` so_apply: `x[s1;s2]` pi1: `fst(t)` pi2: `snd(t)` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` divide: `n ÷ m` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` subtype_rel: `A ⊆r B` integ_dom: `IntegDom{i}` int_ring: `ℤ-rng` rng_car: `|r|` pi1: `fst(t)` rng_zero: `0` pi2: `snd(t)` rng_plus: `+r` uimplies: `b supposing a` sq_type: `SQType(T)` all: `∀x:A. B[x]` implies: `P `` Q` guard: `{T}` let: let squash: `↓T` prop: `ℙ` nat_plus: `ℕ+` Prime: `Prime` int_upper: `{i...}` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2]` int_seg: `{i..j-}` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` rev_implies: `P `` Q` false: `False` uiff: `uiff(P;Q)` lelt: `i ≤ j < k` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` nequal: `a ≠ b ∈ T ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` subtract: `n - m` so_apply: `x[s]`
Lemmas referenced :  bag-summation-partitions-primes-general int_ring_wf integ_dom_wf nat_plus_wf subtype_base_sq int_subtype_base equal_wf squash_wf true_wf gen-divisors-sum-int-ring int-bag-product_wf subtype_rel_bag Prime_wf bag-product-primes less_than_wf decidable__lt false_wf not-lt-2 add_functionality_wrt_le add-zero le-add-cancel int_seg_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 div-positive-1 less-iff-le condition-implies-le add-associates minus-add minus-one-mul add-swap minus-one-mul-top add-commutes zero-add le-add-cancel2 int_seg_wf divisors-sum_wf iff_weakening_equal bag_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis applyEquality lambdaEquality setElimination rename hypothesisEquality sqequalRule functionExtensionality functionEquality intEquality instantiate cumulativity independent_isectElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination imageElimination universeEquality dependent_set_memberEquality because_Cache natural_numberEquality unionElimination independent_pairFormation lambdaFormation voidElimination productElimination divideEquality addEquality dependent_pairFormation int_eqEquality isect_memberEquality voidEquality computeAll baseClosed minusEquality imageMemberEquality axiomEquality

Latex:
\mforall{}[h:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[b:bag(Prime)].
(\mSigma{}(p\mmember{}bag-partitions(IntDeq;b)).  h[\mPi{}(fst(p));\mPi{}(snd(p))]  =  \mSigma{}  i|\mPi{}(b).  h[i;\mPi{}(b)  \mdiv{}  i]  )

Date html generated: 2018_05_21-PM-09_50_28
Last ObjectModification: 2017_07_26-PM-06_31_21

Theory : bags_2

Home Index