---

Step * of Lemma prime_elim

∀p:ℤ. (prime(p) ⇒ ((¬(p = 0 ∈ ℤ)) ∧ (¬(p ~ 1)) ∧ (∀a:ℤ. ((a | p) ⇒ ((a ~ 1) ∨ (a ~ p))))))
BY
{ (((((RepD THENM FLemma `prime_imp_atomic` [-1]) THENM (Unfold `atomic` (-1))) THENM GenRepD) THENM Try (Auto))
   THENA Auto
   ) }

1
1. p : ℤ
2. prime(p)
3. ¬(p = 0 ∈ ℤ)
4. ¬(p ~ 1)
5. ¬reducible(p)
6. a : ℤ
7. a | p
⊢ (a ~ 1) ∨ (a ~ p)

---

Latex:

---

Latex:
\mforall{}p:\mBbbZ{}.  (prime(p)  {}\mRightarrow{}  ((\mneg{}(p  =  0))  \mwedge{}  (\mneg{}(p  \msim{}  1))  \mwedge{}  (\mforall{}a:\mBbbZ{}.  ((a  |  p)  {}\mRightarrow{}  ((a  \msim{}  1)  \mvee{}  (a  \msim{}  p))))))


By

---

Latex:
(((((RepD  THENM  FLemma  `prime\_imp\_atomic`  [-1])  THENM  (Unfold  `atomic`  (-1)))  THENM  GenRepD)
  THENM  Try  (Auto)
  )
  THENA  Auto
  )

---

Home Index