---

Step * of Lemma mprime_divs_list_el

∀g:IAbMonoid. ∀p:|g|.  (IsPrime(p) ⇒ (∀as:|g| List. ((p | (Π as)) ⇒ (∃i:ℕ||as||. (p | as[i])))))
BY
{ (((UnivCD) THENA Auto) THEN ListInd 4 THEN Auto THEN Reduce -1 THEN D 3 THEN Try ((Fold `munit` (-1) THEN Trivial))) }

1
1. g : IAbMonoid
2. p : |g|
3. ¬(g-unit(p))
4. ∀b,c:|g|.  ((p | (b * c)) ⇒ ((p | b) ∨ (p | c)))
5. u : |g|
6. v : |g| List
7. (p | (Π v)) ⇒ (∃i:ℕ||v||. (p | v[i]))
8. p | (u * (Π v))
⊢ ∃i:ℕ||[u / v]||. (p | [u / v][i])

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}p:|g|.    (IsPrime(p)  {}\mRightarrow{}  (\mforall{}as:|g|  List.  ((p  |  (\mPi{}  as))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||as||.  (p  |  as[i])))))


By

---

Latex:
(((UnivCD)  THENA  Auto)
  THEN  ListInd  4
  THEN  Auto
  THEN  Reduce  -1
  THEN  D  3
  THEN  Try  ((Fold  `munit`  (-1)  THEN  Trivial)))

---

Home Index