---

Step * 1 1 of Lemma primality-test


1. b : ℕ
2. ∀b:ℕb. (prime(b)) supposing ((∀p:ℕ. (prime(p) ⇒ ((p * p) ≤ b) ⇒ (¬(p | b)))) and (2 ≤ b))
3. 2 ≤ b
4. ∀p:ℕ. (prime(p) ⇒ ((p * p) ≤ b) ⇒ (¬(p | b)))
⊢ ¬(b ~ 1)
BY
{ (RWO "assoced_nelim" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}
2.  \mforall{}b:\mBbbN{}b.  (prime(b))  supposing  ((\mforall{}p:\mBbbN{}.  (prime(p)  {}\mRightarrow{}  ((p  *  p)  \mleq{}  b)  {}\mRightarrow{}  (\mneg{}(p  |  b))))  and  (2  \mleq{}  b))
3.  2  \mleq{}  b
4.  \mforall{}p:\mBbbN{}.  (prime(p)  {}\mRightarrow{}  ((p  *  p)  \mleq{}  b)  {}\mRightarrow{}  (\mneg{}(p  |  b)))
\mvdash{}  \mneg{}(b  \msim{}  1)


By

---

Latex:
(RWO  "assoced\_nelim"  0  THEN  Auto)

---

Home Index