Proof of Theorem isprm3
Step | Hyp | Ref
| Expression |
1 | | isprm2 16387 |
. 2
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
2 | | iman 402 |
. . . . . . 7
⊢ ((𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ¬ (𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
3 | | eluz2nn 12624 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℕ) |
4 | | nnz 12342 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
5 | | dvdsle 16019 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃)) |
6 | 4, 5 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃)) |
7 | | nnge1 12001 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ → 1 ≤
𝑧) |
8 | 7 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ) → 1 ≤
𝑧) |
9 | 6, 8 | jctild 526 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → (1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃))) |
10 | 3, 9 | sylan2 593 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → (𝑧 ∥ 𝑃 → (1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃))) |
11 | | zre 12323 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
12 | | nnre 11980 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
13 | | 1re 10975 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℝ |
14 | | leltne 11064 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ 𝑧
∈ ℝ ∧ 1 ≤ 𝑧) → (1 < 𝑧 ↔ 𝑧 ≠ 1)) |
15 | 13, 14 | mp3an1 1447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℝ ∧ 1 ≤
𝑧) → (1 < 𝑧 ↔ 𝑧 ≠ 1)) |
16 | 15 | 3adant2 1130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 1 ≤
𝑧) → (1 < 𝑧 ↔ 𝑧 ≠ 1)) |
17 | 16 | 3expia 1120 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 ≤
𝑧 → (1 < 𝑧 ↔ 𝑧 ≠ 1))) |
18 | | leltne 11064 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑧 ≤ 𝑃) → (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)) |
19 | 18 | 3expia 1120 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑧 ≤ 𝑃 → (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧))) |
20 | 17, 19 | anim12d 609 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((1 ≤
𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)))) |
21 | 11, 12, 20 | syl2an 596 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((1 ≤
𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)))) |
22 | | pm4.38 635 |
. . . . . . . . . . . . . . . . . 18
⊢ (((1 <
𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ (𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧))) |
23 | | df-ne 2944 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ≠ 1 ↔ ¬ 𝑧 = 1) |
24 | | nesym 3000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ≠ 𝑧 ↔ ¬ 𝑧 = 𝑃) |
25 | 23, 24 | anbi12i 627 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧) ↔ (¬ 𝑧 = 1 ∧ ¬ 𝑧 = 𝑃)) |
26 | | ioran 981 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ (¬ 𝑧 = 1 ∧ ¬ 𝑧 = 𝑃)) |
27 | 25, 26 | bitr4i 277 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) |
28 | 22, 27 | bitrdi 287 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 <
𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
29 | 21, 28 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((1 ≤
𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
30 | 4, 3, 29 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → ((1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
31 | 10, 30 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → (𝑧 ∥ 𝑃 → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
32 | 31 | imp 407 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) ∧ 𝑧 ∥ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
33 | | eluzelz 12592 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℤ) |
34 | | 1z 12350 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℤ |
35 | | zltp1le 12370 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℤ ∧ 𝑧
∈ ℤ) → (1 < 𝑧 ↔ (1 + 1) ≤ 𝑧)) |
36 | 34, 35 | mpan 687 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℤ → (1 <
𝑧 ↔ (1 + 1) ≤ 𝑧)) |
37 | | df-2 12036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 = (1 +
1) |
38 | 37 | breq1i 5081 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ≤
𝑧 ↔ (1 + 1) ≤ 𝑧) |
39 | 36, 38 | bitr4di 289 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℤ → (1 <
𝑧 ↔ 2 ≤ 𝑧)) |
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (1 <
𝑧 ↔ 2 ≤ 𝑧)) |
41 | | zltlem1 12373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑧 < 𝑃 ↔ 𝑧 ≤ (𝑃 − 1))) |
42 | 40, 41 | anbi12d 631 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((1 <
𝑧 ∧ 𝑧 < 𝑃) ↔ (2 ≤ 𝑧 ∧ 𝑧 ≤ (𝑃 − 1)))) |
43 | | peano2zm 12363 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
44 | | 2z 12352 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℤ |
45 | | elfz 13245 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 2 ∈
ℤ ∧ (𝑃 − 1)
∈ ℤ) → (𝑧
∈ (2...(𝑃 − 1))
↔ (2 ≤ 𝑧 ∧
𝑧 ≤ (𝑃 − 1)))) |
46 | 44, 45 | mp3an2 1448 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ (𝑃 − 1) ∈ ℤ)
→ (𝑧 ∈
(2...(𝑃 − 1)) ↔
(2 ≤ 𝑧 ∧ 𝑧 ≤ (𝑃 − 1)))) |
47 | 43, 46 | sylan2 593 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑧 ∈ (2...(𝑃 − 1)) ↔ (2 ≤ 𝑧 ∧ 𝑧 ≤ (𝑃 − 1)))) |
48 | 42, 47 | bitr4d 281 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((1 <
𝑧 ∧ 𝑧 < 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
49 | 4, 33, 48 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
50 | 49 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) ∧ 𝑧 ∥ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
51 | 32, 50 | bitr3d 280 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) ∧ 𝑧 ∥ 𝑃) → (¬ (𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
52 | 51 | anasss 467 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℕ ∧ (𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃)) → (¬ (𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
53 | 52 | expcom 414 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → (𝑧 ∈ ℕ → (¬ (𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1))))) |
54 | 53 | pm5.32d 577 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ (𝑧 ∈ ℕ ∧ 𝑧 ∈ (2...(𝑃 − 1))))) |
55 | | fzssuz 13297 |
. . . . . . . . . . . . 13
⊢
(2...(𝑃 − 1))
⊆ (ℤ≥‘2) |
56 | | 2eluzge1 12634 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(ℤ≥‘1) |
57 | | uzss 12605 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
(ℤ≥‘1) → (ℤ≥‘2)
⊆ (ℤ≥‘1)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘2) ⊆
(ℤ≥‘1) |
59 | 55, 58 | sstri 3930 |
. . . . . . . . . . . 12
⊢
(2...(𝑃 − 1))
⊆ (ℤ≥‘1) |
60 | | nnuz 12621 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
61 | 59, 60 | sseqtrri 3958 |
. . . . . . . . . . 11
⊢
(2...(𝑃 − 1))
⊆ ℕ |
62 | 61 | sseli 3917 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (2...(𝑃 − 1)) → 𝑧 ∈ ℕ) |
63 | 62 | pm4.71ri 561 |
. . . . . . . . 9
⊢ (𝑧 ∈ (2...(𝑃 − 1)) ↔ (𝑧 ∈ ℕ ∧ 𝑧 ∈ (2...(𝑃 − 1)))) |
64 | 54, 63 | bitr4di 289 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
65 | 64 | notbid 318 |
. . . . . . 7
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → (¬ (𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ¬ 𝑧 ∈ (2...(𝑃 − 1)))) |
66 | 2, 65 | bitrid 282 |
. . . . . 6
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ¬ 𝑧 ∈ (2...(𝑃 − 1)))) |
67 | 66 | pm5.74da 801 |
. . . . 5
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∥ 𝑃 → (𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑧 ∥ 𝑃 → ¬ 𝑧 ∈ (2...(𝑃 − 1))))) |
68 | | bi2.04 389 |
. . . . 5
⊢ ((𝑧 ∥ 𝑃 → (𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
69 | | con2b 360 |
. . . . 5
⊢ ((𝑧 ∥ 𝑃 → ¬ 𝑧 ∈ (2...(𝑃 − 1))) ↔ (𝑧 ∈ (2...(𝑃 − 1)) → ¬ 𝑧 ∥ 𝑃)) |
70 | 67, 68, 69 | 3bitr3g 313 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑧 ∈ (2...(𝑃 − 1)) → ¬ 𝑧 ∥ 𝑃))) |
71 | 70 | ralbidv2 3110 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ∀𝑧 ∈ (2...(𝑃 − 1)) ¬ 𝑧 ∥ 𝑃)) |
72 | 71 | pm5.32i 575 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑃 ∈ (ℤ≥‘2)
∧ ∀𝑧 ∈
(2...(𝑃 − 1)) ¬
𝑧 ∥ 𝑃)) |
73 | 1, 72 | bitri 274 |
1
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ (2...(𝑃 − 1)) ¬ 𝑧 ∥ 𝑃)) |