---

Step * 1 1 1 1 of Lemma mfact_exists


1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. WellFnd{i}(|g|;x,y.x p| y)
4. ∀c:|g|. Dec(Reducible(c))
5. j : |g|
6. ∀k:|g|. ((k p| j) ⇒ (¬(g-unit(k))) ⇒ (∃as:Atom{g} List. (k = (Π as) ∈ |g|)))
7. ¬(g-unit(j))
8. b : |g|
9. c : |g|
10. ¬(g-unit(b))
11. ¬(g-unit(c))
12. j = (b * c) ∈ |g|
⊢ ∃as:Atom{g} List. (j = (Π as) ∈ |g|)
BY
{ ((SwapEquands 12 
THEN FLemma `non_munit_diff_imp_mpdivides` [12]) THENA Auto) }

1
1. g : IAbMonoid
2. Cancel(|g|;|g|;*)
3. WellFnd{i}(|g|;x,y.x p| y)
4. ∀c:|g|. Dec(Reducible(c))
5. j : |g|
6. ∀k:|g|. ((k p| j) ⇒ (¬(g-unit(k))) ⇒ (∃as:Atom{g} List. (k = (Π as) ∈ |g|)))
7. ¬(g-unit(j))
8. b : |g|
9. c : |g|
10. ¬(g-unit(b))
11. ¬(g-unit(c))
12. (b * c) = j ∈ |g|
13. b p| j
⊢ ∃as:Atom{g} List. (j = (Π as) ∈ |g|)

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  Cancel(|g|;|g|;*)
3.  WellFnd\{i\}(|g|;x,y.x  p|  y)
4.  \mforall{}c:|g|.  Dec(Reducible(c))
5.  j  :  |g|
6.  \mforall{}k:|g|.  ((k  p|  j)  {}\mRightarrow{}  (\mneg{}(g-unit(k)))  {}\mRightarrow{}  (\mexists{}as:Atom\{g\}  List.  (k  =  (\mPi{}  as))))
7.  \mneg{}(g-unit(j))
8.  b  :  |g|
9.  c  :  |g|
10.  \mneg{}(g-unit(b))
11.  \mneg{}(g-unit(c))
12.  j  =  (b  *  c)
\mvdash{}  \mexists{}as:Atom\{g\}  List.  (j  =  (\mPi{}  as))


By

---

Latex:
((SwapEquands  12 
THEN  FLemma  `non\_munit\_diff\_imp\_mpdivides`  [12])  THENA  Auto)

---

Home Index