---

Step * 1 1 of Lemma mprime_divs_list_el


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))
9. p | u
⊢ ∃i:ℕ||[u / v]||. (p | [u / v][i])
BY
{ TACTIC:With 0 (D 0) THENA Auto' THEN AbReduce 0 
 }

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))
9. p | u
⊢ p | u

---

Latex:

---

Latex:

1.  g  :  IAbMonoid
2.  p  :  |g|
3.  \mneg{}(g-unit(p))
4.  \mforall{}b,c:|g|.    ((p  |  (b  *  c))  {}\mRightarrow{}  ((p  |  b)  \mvee{}  (p  |  c)))
5.  u  :  |g|
6.  v  :  |g|  List
7.  (p  |  (\mPi{}  v))  {}\mRightarrow{}  (\mexists{}i:\mBbbN{}||v||.  (p  |  v[i]))
8.  p  |  (u  *  (\mPi{}  v))
9.  p  |  u
\mvdash{}  \mexists{}i:\mBbbN{}||[u  /  v]||.  (p  |  [u  /  v][i])


By

---

Latex:
TACTIC:With  0  (D  0)  THENA  Auto'  THEN  AbReduce  0 

---

Home Index