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 bitrdi ( ( ( 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 bitr4di ( 𝑧 ∈ ℤ → ( 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 bitr4di ( ( 𝑃 ∈ ( ℤ ‘ 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 ) ) ¬ 𝑧𝑃 ) )