---

Step * 1 of Lemma fund-theorem-arithmetic


1. a1 : ℕ+
2. a2 : ℕ+
3. factors(a1) = factors(a2) ∈ bag(Prime)
⊢ a1 = a2 ∈ ℕ+
BY
{ xxx((ApFunToHypEquands `Z' ⌜Π(Z)⌝ ⌜ℤ⌝ (-1)⋅ THENA Auto) THEN RWO "product-factors" (-1) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  a1  :  \mBbbN{}\msupplus{}
2.  a2  :  \mBbbN{}\msupplus{}
3.  factors(a1)  =  factors(a2)
\mvdash{}  a1  =  a2


By

---

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

---

Home Index