---

Step * 1 1 of Lemma prime-product-injection


1. a1 : bag(Prime)
2. a2 : bag(Prime)
3. Π(a1) = Π(a2) ∈ ℕ+
4. factors(Π(a1)) = factors(Π(a2)) ∈ bag(Prime)
⊢ a1 = a2 ∈ bag(Prime)
BY
{ xxx(RWO "factors-prime-product" (-1) THEN Auto)xxx }

---

Latex:

---

Latex:

1.  a1  :  bag(Prime)
2.  a2  :  bag(Prime)
3.  \mPi{}(a1)  =  \mPi{}(a2)
4.  factors(\mPi{}(a1))  =  factors(\mPi{}(a2))
\mvdash{}  a1  =  a2


By

---

Latex:
xxx(RWO  "factors-prime-product"  (-1)  THEN  Auto)xxx

---

Home Index