This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prmlem1

Description: A quick proof skeleton to show that the numbers less than 25 are prime, by trial division. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Hypotheses prmlem1.n ⊢ N ∈ ℕ
prmlem1.gt ⊢ 1 < N
prmlem1.2 ⊢ ¬ 2 ∥ N
prmlem1.3 ⊢ ¬ 3 ∥ N
prmlem1.lt ⊢ N < 25
Assertion prmlem1 ⊢ N ∈ ℙ

Proof

Step Hyp Ref Expression
1 prmlem1.n ⊢ N ∈ ℕ
2 prmlem1.gt ⊢ 1 < N
3 prmlem1.2 ⊢ ¬ 2 ∥ N
4 prmlem1.3 ⊢ ¬ 3 ∥ N
5 prmlem1.lt ⊢ N < 25
6 eluzelre ⊢ x ∈ ℤ ≥ 5 → x ∈ ℝ
7 6 resqcld ⊢ x ∈ ℤ ≥ 5 → x 2 ∈ ℝ
8 eluzle ⊢ x ∈ ℤ ≥ 5 → 5 ≤ x
9 5re ⊢ 5 ∈ ℝ
10 5nn0 ⊢ 5 ∈ ℕ 0
11 10 nn0ge0i ⊢ 0 ≤ 5
12 le2sq2 ⊢ 5 ∈ ℝ ∧ 0 ≤ 5 ∧ x ∈ ℝ ∧ 5 ≤ x → 5 2 ≤ x 2
13 9 11 12 mpanl12 ⊢ x ∈ ℝ ∧ 5 ≤ x → 5 2 ≤ x 2
14 6 8 13 syl2anc ⊢ x ∈ ℤ ≥ 5 → 5 2 ≤ x 2
15 1 nnrei ⊢ N ∈ ℝ
16 9 resqcli ⊢ 5 2 ∈ ℝ
17 5cn ⊢ 5 ∈ ℂ
18 17 sqvali ⊢ 5 2 = 5 ⋅ 5
19 5t5e25 ⊢ 5 ⋅ 5 = 25
20 18 19 eqtri ⊢ 5 2 = 25
21 5 20 breqtrri ⊢ N < 5 2
22 ltletr ⊢ N ∈ ℝ ∧ 5 2 ∈ ℝ ∧ x 2 ∈ ℝ → N < 5 2 ∧ 5 2 ≤ x 2 → N < x 2
23 21 22 mpani ⊢ N ∈ ℝ ∧ 5 2 ∈ ℝ ∧ x 2 ∈ ℝ → 5 2 ≤ x 2 → N < x 2
24 15 16 23 mp3an12 ⊢ x 2 ∈ ℝ → 5 2 ≤ x 2 → N < x 2
25 7 14 24 sylc ⊢ x ∈ ℤ ≥ 5 → N < x 2
26 ltnle ⊢ N ∈ ℝ ∧ x 2 ∈ ℝ → N < x 2 ↔ ¬ x 2 ≤ N
27 15 7 26 sylancr ⊢ x ∈ ℤ ≥ 5 → N < x 2 ↔ ¬ x 2 ≤ N
28 25 27 mpbid ⊢ x ∈ ℤ ≥ 5 → ¬ x 2 ≤ N
29 28 pm2.21d ⊢ x ∈ ℤ ≥ 5 → x 2 ≤ N → ¬ x ∥ N
30 29 adantld ⊢ x ∈ ℤ ≥ 5 → x ∈ ℙ ∖ 2 ∧ x 2 ≤ N → ¬ x ∥ N
31 30 adantl ⊢ ¬ 2 ∥ 5 ∧ x ∈ ℤ ≥ 5 → x ∈ ℙ ∖ 2 ∧ x 2 ≤ N → ¬ x ∥ N
32 1 2 3 4 31 prmlem1a ⊢ N ∈ ℙ