---

Step * 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))
⊢ ∃i:ℕ||[u / v]||. (p | [u / v][i])
BY
{ TACTIC:((FHyp 4 [-1]) THENA Auto) 
THEN D (-1) }

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
⊢ ∃i:ℕ||[u / v]||. (p | [u / v][i])

2
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 | (Π
         v)
⊢ ∃i:ℕ||[u / v]||. (p | [u / v][i])

---

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))
\mvdash{}  \mexists{}i:\mBbbN{}||[u  /  v]||.  (p  |  [u  /  v][i])


By

---

Latex:
TACTIC:((FHyp  4  [-1])  THENA  Auto) 
THEN  D  (-1)

---

Home Index