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

Metamath Proof Explorer

Theorem prmlem1a

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 ∥ 𝑁
prmlem1a.x ⊢ ( ( ¬ 2 ∥ 5 ∧ 𝑥 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
Assertion prmlem1a 𝑁 ∈ ℙ

Proof

Step Hyp Ref Expression
1 prmlem1.n ⊢ 𝑁 ∈ ℕ
2 prmlem1.gt ⊢ 1 < 𝑁
3 prmlem1.2 ⊢ ¬ 2 ∥ 𝑁
4 prmlem1.3 ⊢ ¬ 3 ∥ 𝑁
5 prmlem1a.x ⊢ ( ( ¬ 2 ∥ 5 ∧ 𝑥 ∈ ( ℤ≥ ‘ 5 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
6 eluz2b2 ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ↔ ( 𝑁 ∈ ℕ ∧ 1 < 𝑁 ) )
7 1 2 6 mpbir2an ⊢ 𝑁 ∈ ( ℤ≥ ‘ 2 )
8 breq1 ⊢ ( 𝑥 = 2 → ( 𝑥 ∥ 𝑁 ↔ 2 ∥ 𝑁 ) )
9 8 notbid ⊢ ( 𝑥 = 2 → ( ¬ 𝑥 ∥ 𝑁 ↔ ¬ 2 ∥ 𝑁 ) )
10 9 imbi2d ⊢ ( 𝑥 = 2 → ( ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ↔ ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 2 ∥ 𝑁 ) ) )
11 prmnn ⊢ ( 𝑥 ∈ ℙ → 𝑥 ∈ ℕ )
12 11 adantr ⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) → 𝑥 ∈ ℕ )
13 eldifsn ⊢ ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ↔ ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) )
14 n2dvds1 ⊢ ¬ 2 ∥ 1
15 4 a1i ⊢ ( 3 ∈ ℙ → ¬ 3 ∥ 𝑁 )
16 3p2e5 ⊢ ( 3 + 2 ) = 5
17 5 15 16 prmlem0 ⊢ ( ( ¬ 2 ∥ 3 ∧ 𝑥 ∈ ( ℤ≥ ‘ 3 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
18 1nprm ⊢ ¬ 1 ∈ ℙ
19 18 pm2.21i ⊢ ( 1 ∈ ℙ → ¬ 1 ∥ 𝑁 )
20 1p2e3 ⊢ ( 1 + 2 ) = 3
21 17 19 20 prmlem0 ⊢ ( ( ¬ 2 ∥ 1 ∧ 𝑥 ∈ ( ℤ≥ ‘ 1 ) ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
22 14 21 mpan ⊢ ( 𝑥 ∈ ( ℤ≥ ‘ 1 ) → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
23 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
24 22 23 eleq2s ⊢ ( 𝑥 ∈ ℕ → ( ( 𝑥 ∈ ( ℙ ∖ { 2 } ) ∧ ( 𝑥 ↑ 2 ) ≤ 𝑁 ) → ¬ 𝑥 ∥ 𝑁 ) )
25 24 expd ⊢ ( 𝑥 ∈ ℕ → ( 𝑥 ∈ ( ℙ ∖ { 2 } ) → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ) )
26 13 25 biimtrrid ⊢ ( 𝑥 ∈ ℕ → ( ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ) )
27 12 26 mpcom ⊢ ( ( 𝑥 ∈ ℙ ∧ 𝑥 ≠ 2 ) → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) )
28 3 2a1i ⊢ ( 𝑥 ∈ ℙ → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 2 ∥ 𝑁 ) )
29 10 27 28 pm2.61ne ⊢ ( 𝑥 ∈ ℙ → ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) )
30 29 rgen ⊢ ∀ 𝑥 ∈ ℙ ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 )
31 isprm5 ⊢ ( 𝑁 ∈ ℙ ↔ ( 𝑁 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑥 ∈ ℙ ( ( 𝑥 ↑ 2 ) ≤ 𝑁 → ¬ 𝑥 ∥ 𝑁 ) ) )
32 7 30 31 mpbir2an ⊢ 𝑁 ∈ ℙ