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 ⊢ 𝑁 ∈ ℕ
prmlem1.gt ⊢ 1 < 𝑁
prmlem1.2 ⊢ ¬ 2 ∥ 𝑁
prmlem1.3 ⊢ ¬ 3 ∥ 𝑁
prmlem1.lt ⊢ 𝑁 < 2 5
Assertion prmlem1 𝑁 ∈ ℙ

Proof

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