---

Step * 2 1 1 of Lemma divides-iff-factors


1. n : ℕ+
2. m : ℕ+
3. cs : bag(Prime)
4. factors(m) = (factors(n) + cs) ∈ bag(Prime)
5. m = (n * Π(cs)) ∈ ℤ
⊢ n | m
BY
{ xxx(With ⌜Π(cs)⌝ (D 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(With  \mkleeneopen{}\mPi{}(cs)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index