---

Step * of Lemma mprime_imp_matomic

∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a:|g|. (IsPrime(a) ⇒ Atomic(a))))
BY
{ UnivCD THENA Auto }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. IsPrime(a)
⊢ Atomic(a)

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  (Cancel(|g|;|g|;*)  {}\mRightarrow{}  (\mforall{}a:|g|.  (IsPrime(a)  {}\mRightarrow{}  Atomic(a))))


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index