---

Step * 1 1 2 of Lemma unique_mfact


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. ∀a,b:|g|.  Dec(a | b)
4. u : Prime(g)
5. v : Prime(g) List
6. g-unit(u * (Π v))
⊢ [] ≡ [u / v] upto ~
BY
{ TACTIC:Assert False THENM Trivial 
THEN D 4 THEN D 5 
 ⋅ }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. ∀a,b:|g|.  Dec(a | b)
4. u : |g|
5. ¬(g-unit(u))
6. ∀b,c:|g|.  ((u | (b * c)) ⇒ ((u | b) ∨ (u | c)))
7. v : Prime(g) List
8. g-unit(u * (Π v))
⊢ False

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  \mforall{}a,b:|g|.    Dec(a  |  b)
4.  u  :  Prime(g)
5.  v  :  Prime(g)  List
6.  g-unit(u  *  (\mPi{}  v))
\mvdash{}  []  \mequiv{}  [u  /  v]  upto  \msim{}


By

---

Latex:
TACTIC:Assert  False  THENM  Trivial 
THEN  D  4  THEN  D  5 
  \mcdot{}

---

Home Index