---

Step * 1 of Lemma prime-product-injection


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

1
1. a1 : bag(Prime)
2. a2 : bag(Prime)
3. Π(a1) = Π(a2) ∈ ℕ+
4. factors(Π(a1)) = factors(Π(a2)) ∈ bag(Prime)
⊢ a1 = a2 ∈ bag(Prime)

---

Latex:

---

Latex:

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


By

---

Latex:
xxx(ApFunToHypEquands  `Z'  \mkleeneopen{}factors(Z)\mkleeneclose{}  \mkleeneopen{}bag(Prime)\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)xxx

---

Home Index