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