---

Step * of Lemma ufm_char

∀g:IAbMonoid
  (Cancel(|g|;|g|;*)
  ⇒ WellFnd{i}(|g|;x,y.x p| y)
  ⇒ (∀a:Atom{g}. IsPrime(a))
  ⇒ (∀a:|g|. Dec(Reducible(a)))
  ⇒ (∀a,b:|g|.  Dec(a | b))
  ⇒ IsUFM(g))
BY
{ ((RepD) THENA Auto) }

1
1. g : IAbMonoid@i'
2. Cancel(|g|;|g|;*)@i
3. WellFnd{i}(|g|;x,y.x p| y)@i'
4. ∀a:Atom{g}. IsPrime(a)@i
5. ∀a:|g|. Dec(Reducible(a))@i
6. ∀a,b:|g|.  Dec(a | b)@i
⊢ IsUFM(g)

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid
    (Cancel(|g|;|g|;*)
    {}\mRightarrow{}  WellFnd\{i\}(|g|;x,y.x  p|  y)
    {}\mRightarrow{}  (\mforall{}a:Atom\{g\}.  IsPrime(a))
    {}\mRightarrow{}  (\mforall{}a:|g|.  Dec(Reducible(a)))
    {}\mRightarrow{}  (\mforall{}a,b:|g|.    Dec(a  |  b))
    {}\mRightarrow{}  IsUFM(g))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index