---

Step * 2 1 of Lemma divides-iff-factors


1. n : ℕ+
2. m : ℕ+
3. cs : bag(Prime)
4. factors(m) = (factors(n) + cs) ∈ bag(Prime)
⊢ n | m
BY
{ xxx((ApFunToHypEquands `Z' ⌜Π(Z)⌝ ⌜ℤ⌝ (-1)⋅ THENA Auto)
      THEN RWW "product-factors int-bag-product-append" (-1)
      THEN Auto)xxx }

1
1. n : ℕ+
2. m : ℕ+
3. cs : bag(Prime)
4. factors(m) = (factors(n) + cs) ∈ bag(Prime)
5. m = (n * Π(cs)) ∈ ℤ
⊢ n | m

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  m  :  \mBbbN{}\msupplus{}
3.  cs  :  bag(Prime)
4.  factors(m)  =  (factors(n)  +  cs)
\mvdash{}  n  |  m


By

---

Latex:
xxx((ApFunToHypEquands  `Z'  \mkleeneopen{}\mPi{}(Z)\mkleeneclose{}  \mkleeneopen{}\mBbbZ{}\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
        THEN  RWW  "product-factors  int-bag-product-append"  (-1)
        THEN  Auto)xxx

---

Home Index