### Nuprl Lemma : append-factors

`∀n,m:ℕ+.  (factors(n * m) = (factors(n) + factors(m)) ∈ bag(Prime))`

Proof

Definitions occuring in Statement :  factors: `factors(n)` Prime: `Prime` bag-append: `as + bs` bag: `bag(T)` nat_plus: `ℕ+` all: `∀x:A. B[x]` multiply: `n * m` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` inject: `Inj(A;B;f)` member: `t ∈ T` uall: `∀[x:A]. B[x]` implies: `P `` Q` nat_plus: `ℕ+` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` uimplies: `b supposing a` Prime: `Prime` int_upper: `{i...}` true: `True` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  prime-product-injection factors_wf mul_nat_plus bag-append_wf Prime_wf bag-product-primes equal_wf squash_wf true_wf product-factors int-bag-product_wf subtype_rel_bag iff_weakening_equal int-bag-product-append less_than_wf nat_plus_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution sqequalRule hypothesis dependent_functionElimination thin isectElimination hypothesisEquality independent_functionElimination dependent_set_memberEquality applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality intEquality because_Cache independent_isectElimination setElimination rename natural_numberEquality imageMemberEquality baseClosed productElimination multiplyEquality

Latex:
\mforall{}n,m:\mBbbN{}\msupplus{}.    (factors(n  *  m)  =  (factors(n)  +  factors(m)))

Date html generated: 2018_05_21-PM-07_23_28
Last ObjectModification: 2017_07_26-PM-05_06_22

Theory : general

Home Index