---

Step * of Lemma mdivisor_of_atom_is_assoc2

∀g:IAbMonoid. ((∀a,b:|g|.  Stable{a | b}) ⇒ (∀a,b:|g|.  ((¬(g-unit(a))) ⇒ Atomic(b) ⇒ (a | b) ⇒ (a ~ b))))
BY
{ UnivCD THENA Auto }

1
1. g : IAbMonoid
2. ∀a,b:|g|.  Stable{a | b}
3. a : |g|
4. b : |g|
5. ¬(g-unit(a))
6. Atomic(b)
7. a | b
⊢ a ~ b

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid
    ((\mforall{}a,b:|g|.    Stable\{a  |  b\})  {}\mRightarrow{}  (\mforall{}a,b:|g|.    ((\mneg{}(g-unit(a)))  {}\mRightarrow{}  Atomic(b)  {}\mRightarrow{}  (a  |  b)  {}\mRightarrow{}  (a  \msim{}  b))))


By

---

Latex:
UnivCD  THENA  Auto

---

Home Index