---

Step * of Lemma product-factors

∀[n:ℕ+]. (Π(factors(n)) = n ∈ ℤ)
BY
{ xxx(Auto THEN RepUR ``factors empty-bag`` 0 THEN (RWO "mul-list-bag-product<" 0 THENA Auto) THEN AutoSplit)xxx }

1
1. n : ℕ+
2. n ≠ 1
⊢ Π(factorization(n))  = n ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  (\mPi{}(factors(n))  =  n)


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``factors  empty-bag``  0
        THEN  (RWO  "mul-list-bag-product<"  0  THENA  Auto)
        THEN  AutoSplit)xxx

---

Home Index