---

Step * of Lemma factors-prime-product

∀[b:bag(Prime)]. (factors(Π(b)) = b ∈ bag(Prime))
BY
{ (Auto THEN Assert ⌜0 < Π(b)⌝⋅) }

1
.....assertion..... 
1. b : bag(Prime)
⊢ 0 < Π(b)

2
1. b : bag(Prime)
2. 0 < Π(b)
⊢ factors(Π(b)) = b ∈ bag(Prime)

---

Latex:

---

Latex:
\mforall{}[b:bag(Prime)].  (factors(\mPi{}(b))  =  b)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}0  <  \mPi{}(b)\mkleeneclose{}\mcdot{})

---

Home Index