Metamath Proof Explorer

Theorem isprm3

Description: The predicate "is a prime number". A prime number is an integer greater than or equal to 2 with no divisors strictly between 1 and itself. (Contributed by Paul Chapman, 26-Oct-2012)

Ref Expression
Assertion isprm3 ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ¬ 𝑧 ∥ 𝑃 ) )

Proof

Step Hyp Ref Expression
1 isprm2 ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
2 iman ⊢ ( ( 𝑧 ∈ ℕ → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ¬ ( 𝑧 ∈ ℕ ∧ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
3 eluz2nn ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℕ )
4 nnz ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℤ )
5 dvdsle ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( 𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃 ) )
6 4 5 sylan ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃 ) )
7 nnge1 ⊢ ( 𝑧 ∈ ℕ → 1 ≤ 𝑧 )
8 7 adantr ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → 1 ≤ 𝑧 )
9 6 8 jctild ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ ) → ( 𝑧 ∥ 𝑃 → ( 1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃 ) ) )
10 3 9 sylan2 ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑧 ∥ 𝑃 → ( 1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃 ) ) )
11 zre ⊢ ( 𝑧 ∈ ℤ → 𝑧 ∈ ℝ )
12 nnre ⊢ ( 𝑃 ∈ ℕ → 𝑃 ∈ ℝ )
13 1re ⊢ 1 ∈ ℝ
14 leltne ⊢ ( ( 1 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 1 ≤ 𝑧 ) → ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) )
15 13 14 mp3an1 ⊢ ( ( 𝑧 ∈ ℝ ∧ 1 ≤ 𝑧 ) → ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) )
16 15 3adant2 ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 1 ≤ 𝑧 ) → ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) )
17 16 3expia ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 1 ≤ 𝑧 → ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) ) )
18 leltne ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑧 ≤ 𝑃 ) → ( 𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧 ) )
19 18 3expia ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( 𝑧 ≤ 𝑃 → ( 𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧 ) ) )
20 17 19 anim12d ⊢ ( ( 𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ) → ( ( 1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃 ) → ( ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) ∧ ( 𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧 ) ) ) )
21 11 12 20 syl2an ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( 1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃 ) → ( ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) ∧ ( 𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧 ) ) ) )
22 pm4.38 ⊢ ( ( ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) ∧ ( 𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧 ) ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ ( 𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧 ) ) )
23 df-ne ⊢ ( 𝑧 ≠ 1 ↔ ¬ 𝑧 = 1 )
24 nesym ⊢ ( 𝑃 ≠ 𝑧 ↔ ¬ 𝑧 = 𝑃 )
25 23 24 anbi12i ⊢ ( ( 𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧 ) ↔ ( ¬ 𝑧 = 1 ∧ ¬ 𝑧 = 𝑃 ) )
26 ioran ⊢ ( ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ↔ ( ¬ 𝑧 = 1 ∧ ¬ 𝑧 = 𝑃 ) )
27 25 26 bitr4i ⊢ ( ( 𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧 ) ↔ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) )
28 22 27 syl6bb ⊢ ( ( ( 1 < 𝑧 ↔ 𝑧 ≠ 1 ) ∧ ( 𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧 ) ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
29 21 28 syl6 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ ) → ( ( 1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃 ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
30 4 3 29 syl2an ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃 ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
31 10 30 syld ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) → ( 𝑧 ∥ 𝑃 → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
32 31 imp ⊢ ( ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑧 ∥ 𝑃 ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) )
33 eluzelz ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → 𝑃 ∈ ℤ )
34 1z ⊢ 1 ∈ ℤ
35 zltp1le ⊢ ( ( 1 ∈ ℤ ∧ 𝑧 ∈ ℤ ) → ( 1 < 𝑧 ↔ ( 1 + 1 ) ≤ 𝑧 ) )
36 34 35 mpan ⊢ ( 𝑧 ∈ ℤ → ( 1 < 𝑧 ↔ ( 1 + 1 ) ≤ 𝑧 ) )
37 df-2 ⊢ 2 = ( 1 + 1 )
38 37 breq1i ⊢ ( 2 ≤ 𝑧 ↔ ( 1 + 1 ) ≤ 𝑧 )
39 36 38 syl6bbr ⊢ ( 𝑧 ∈ ℤ → ( 1 < 𝑧 ↔ 2 ≤ 𝑧 ) )
40 39 adantr ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 1 < 𝑧 ↔ 2 ≤ 𝑧 ) )
41 zltlem1 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑧 < 𝑃 ↔ 𝑧 ≤ ( 𝑃 − 1 ) ) )
42 40 41 anbi12d ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ ( 2 ≤ 𝑧 ∧ 𝑧 ≤ ( 𝑃 − 1 ) ) ) )
43 peano2zm ⊢ ( 𝑃 ∈ ℤ → ( 𝑃 − 1 ) ∈ ℤ )
44 2z ⊢ 2 ∈ ℤ
45 elfz ⊢ ( ( 𝑧 ∈ ℤ ∧ 2 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ) → ( 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ↔ ( 2 ≤ 𝑧 ∧ 𝑧 ≤ ( 𝑃 − 1 ) ) ) )
46 44 45 mp3an2 ⊢ ( ( 𝑧 ∈ ℤ ∧ ( 𝑃 − 1 ) ∈ ℤ ) → ( 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ↔ ( 2 ≤ 𝑧 ∧ 𝑧 ≤ ( 𝑃 − 1 ) ) ) )
47 43 46 sylan2 ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ↔ ( 2 ≤ 𝑧 ∧ 𝑧 ≤ ( 𝑃 − 1 ) ) ) )
48 42 47 bitr4d ⊢ ( ( 𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
49 4 33 48 syl2an ⊢ ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
50 49 adantr ⊢ ( ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑧 ∥ 𝑃 ) → ( ( 1 < 𝑧 ∧ 𝑧 < 𝑃 ) ↔ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
51 32 50 bitr3d ⊢ ( ( ( 𝑧 ∈ ℕ ∧ 𝑃 ∈ ( ℤ≥ ‘ 2 ) ) ∧ 𝑧 ∥ 𝑃 ) → ( ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ↔ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
52 51 anasss ⊢ ( ( 𝑧 ∈ ℕ ∧ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ 𝑃 ) ) → ( ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ↔ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
53 52 expcom ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ 𝑃 ) → ( 𝑧 ∈ ℕ → ( ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ↔ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ) )
54 53 pm5.32d ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ 𝑃 ) → ( ( 𝑧 ∈ ℕ ∧ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ( 𝑧 ∈ ℕ ∧ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ) )
55 fzssuz ⊢ ( 2 ... ( 𝑃 − 1 ) ) ⊆ ( ℤ≥ ‘ 2 )
56 2eluzge1 ⊢ 2 ∈ ( ℤ≥ ‘ 1 )
57 uzss ⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( ℤ≥ ‘ 2 ) ⊆ ( ℤ≥ ‘ 1 ) )
58 56 57 ax-mp ⊢ ( ℤ≥ ‘ 2 ) ⊆ ( ℤ≥ ‘ 1 )
59 55 58 sstri ⊢ ( 2 ... ( 𝑃 − 1 ) ) ⊆ ( ℤ≥ ‘ 1 )
60 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
61 59 60 sseqtrri ⊢ ( 2 ... ( 𝑃 − 1 ) ) ⊆ ℕ
62 61 sseli ⊢ ( 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) → 𝑧 ∈ ℕ )
63 62 pm4.71ri ⊢ ( 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ↔ ( 𝑧 ∈ ℕ ∧ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
64 54 63 syl6bbr ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ 𝑃 ) → ( ( 𝑧 ∈ ℕ ∧ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
65 64 notbid ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ 𝑃 ) → ( ¬ ( 𝑧 ∈ ℕ ∧ ¬ ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ¬ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
66 2 65 syl5bb ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ 𝑧 ∥ 𝑃 ) → ( ( 𝑧 ∈ ℕ → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ¬ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) )
67 66 pm5.74da ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∥ 𝑃 → ( 𝑧 ∈ ℕ → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) ↔ ( 𝑧 ∥ 𝑃 → ¬ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ) )
68 bi2.04 ⊢ ( ( 𝑧 ∥ 𝑃 → ( 𝑧 ∈ ℕ → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) ↔ ( 𝑧 ∈ ℕ → ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) )
69 con2b ⊢ ( ( 𝑧 ∥ 𝑃 → ¬ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ) ↔ ( 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) → ¬ 𝑧 ∥ 𝑃 ) )
70 67 68 69 3bitr3g ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ( 𝑧 ∈ ℕ → ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) ↔ ( 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) → ¬ 𝑧 ∥ 𝑃 ) ) )
71 70 ralbidv2 ⊢ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) → ( ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ↔ ∀ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ¬ 𝑧 ∥ 𝑃 ) )
72 71 pm5.32i ⊢ ( ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ℕ ( 𝑧 ∥ 𝑃 → ( 𝑧 = 1 ∨ 𝑧 = 𝑃 ) ) ) ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ¬ 𝑧 ∥ 𝑃 ) )
73 1 72 bitri ⊢ ( 𝑃 ∈ ℙ ↔ ( 𝑃 ∈ ( ℤ≥ ‘ 2 ) ∧ ∀ 𝑧 ∈ ( 2 ... ( 𝑃 − 1 ) ) ¬ 𝑧 ∥ 𝑃 ) )