---

Step * 1 2 2 1 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)))
5. ¬(b ~ 1)
6. reducible(b)
7. a : {2..b-}
8. c : {2..b-}
9. b = (a * c) ∈ ℤ
10. a | b
11. prime(a)
12. c | b
13. prime(c)
⊢ False
BY
{ (Decide ⌜(a * a) ≤ b⌝⋅ THENA Auto) }

1
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)))
5. ¬(b ~ 1)
6. reducible(b)
7. a : {2..b-}
8. c : {2..b-}
9. b = (a * c) ∈ ℤ
10. a | b
11. prime(a)
12. c | b
13. prime(c)
14. (a * a) ≤ b
⊢ False

2
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)))
5. ¬(b ~ 1)
6. reducible(b)
7. a : {2..b-}
8. c : {2..b-}
9. b = (a * c) ∈ ℤ
10. a | b
11. prime(a)
12. c | b
13. prime(c)
14. ¬((a * a) ≤ b)
⊢ False

---

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)))
5.  \mneg{}(b  \msim{}  1)
6.  reducible(b)
7.  a  :  \{2..b\msupminus{}\}
8.  c  :  \{2..b\msupminus{}\}
9.  b  =  (a  *  c)
10.  a  |  b
11.  prime(a)
12.  c  |  b
13.  prime(c)
\mvdash{}  False


By

---

Latex:
(Decide  \mkleeneopen{}(a  *  a)  \mleq{}  b\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index