---

Step * of Lemma non_munit_diff_imp_mpdivides

∀g:IAbMonoid. (Cancel(|g|;|g|;*) ⇒ (∀a,b,c:|g|.  ((¬(g-unit(b))) ⇒ ((a * b) = c ∈ |g|) ⇒ (a p| c))))
BY
{ ((UnivCD) THENA Auto) }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. b : |g|
5. c : |g|
6. ¬(g-unit(b))
7. (a * b) = c ∈ |g|
⊢ a p| c

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  (Cancel(|g|;|g|;*)  {}\mRightarrow{}  (\mforall{}a,b,c:|g|.    ((\mneg{}(g-unit(b)))  {}\mRightarrow{}  ((a  *  b)  =  c)  {}\mRightarrow{}  (a  p|  c))))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index