---

Step * 1 2 1 of Lemma mprime_imp_matomic


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. IsPrime(a)
5. Reducible(a)
⊢ False
BY
{ OnHyps [4;5] UnfoldTopAb }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. a : |g|
4. (¬(g-unit(a))) ∧ (∀b,c:|g|.  ((a | (b * c)) ⇒ ((a | b) ∨ (a | c))))
5. ∃b,c:|g|. ((¬(g-unit(b))) ∧ (¬(g-unit(c))) ∧ (a = (b * c) ∈ |g|))
⊢ False

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  a  :  |g|
4.  IsPrime(a)
5.  Reducible(a)
\mvdash{}  False


By

---

Latex:
OnHyps  [4;5]  UnfoldTopAb

---

Home Index