Proof of Theorem isprm3
Step | Hyp | Ref
| Expression |
1 | | isprm2 16136 |
. 2
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
2 | | iman 405 |
. . . . . . 7
⊢ ((𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ¬ (𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
3 | | eluz2nn 12379 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℕ) |
4 | | nnz 12098 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ → 𝑧 ∈
ℤ) |
5 | | dvdsle 15768 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃)) |
6 | 4, 5 | sylan 583 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → 𝑧 ≤ 𝑃)) |
7 | | nnge1 11757 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℕ → 1 ≤
𝑧) |
8 | 7 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ) → 1 ≤
𝑧) |
9 | 6, 8 | jctild 529 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈ ℕ) → (𝑧 ∥ 𝑃 → (1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃))) |
10 | 3, 9 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → (𝑧 ∥ 𝑃 → (1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃))) |
11 | | zre 12079 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
12 | | nnre 11736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑃 ∈ ℕ → 𝑃 ∈
ℝ) |
13 | | 1re 10732 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℝ |
14 | | leltne 10821 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((1
∈ ℝ ∧ 𝑧
∈ ℝ ∧ 1 ≤ 𝑧) → (1 < 𝑧 ↔ 𝑧 ≠ 1)) |
15 | 13, 14 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧 ∈ ℝ ∧ 1 ≤
𝑧) → (1 < 𝑧 ↔ 𝑧 ≠ 1)) |
16 | 15 | 3adant2 1132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 1 ≤
𝑧) → (1 < 𝑧 ↔ 𝑧 ≠ 1)) |
17 | 16 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (1 ≤
𝑧 → (1 < 𝑧 ↔ 𝑧 ≠ 1))) |
18 | | leltne 10821 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ ∧ 𝑧 ≤ 𝑃) → (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)) |
19 | 18 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ) → (𝑧 ≤ 𝑃 → (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧))) |
20 | 17, 19 | anim12d 612 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℝ ∧ 𝑃 ∈ ℝ) → ((1 ≤
𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)))) |
21 | 11, 12, 20 | syl2an 599 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((1 ≤
𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)))) |
22 | | pm4.38 638 |
. . . . . . . . . . . . . . . . . 18
⊢ (((1 <
𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ (𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧))) |
23 | | df-ne 2936 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ≠ 1 ↔ ¬ 𝑧 = 1) |
24 | | nesym 2991 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑃 ≠ 𝑧 ↔ ¬ 𝑧 = 𝑃) |
25 | 23, 24 | anbi12i 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧) ↔ (¬ 𝑧 = 1 ∧ ¬ 𝑧 = 𝑃)) |
26 | | ioran 983 |
. . . . . . . . . . . . . . . . . . 19
⊢ (¬
(𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ (¬ 𝑧 = 1 ∧ ¬ 𝑧 = 𝑃)) |
27 | 25, 26 | bitr4i 281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ≠ 1 ∧ 𝑃 ≠ 𝑧) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) |
28 | 22, 27 | bitrdi 290 |
. . . . . . . . . . . . . . . . 17
⊢ (((1 <
𝑧 ↔ 𝑧 ≠ 1) ∧ (𝑧 < 𝑃 ↔ 𝑃 ≠ 𝑧)) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
29 | 21, 28 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℕ) → ((1 ≤
𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
30 | 4, 3, 29 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → ((1 ≤ 𝑧 ∧ 𝑧 ≤ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
31 | 10, 30 | syld 47 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → (𝑧 ∥ 𝑃 → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
32 | 31 | imp 410 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) ∧ 𝑧 ∥ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃))) |
33 | | eluzelz 12347 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈
(ℤ≥‘2) → 𝑃 ∈ ℤ) |
34 | | 1z 12106 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℤ |
35 | | zltp1le 12126 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℤ ∧ 𝑧
∈ ℤ) → (1 < 𝑧 ↔ (1 + 1) ≤ 𝑧)) |
36 | 34, 35 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 ∈ ℤ → (1 <
𝑧 ↔ (1 + 1) ≤ 𝑧)) |
37 | | df-2 11792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 = (1 +
1) |
38 | 37 | breq1i 5047 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ≤
𝑧 ↔ (1 + 1) ≤ 𝑧) |
39 | 36, 38 | bitr4di 292 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℤ → (1 <
𝑧 ↔ 2 ≤ 𝑧)) |
40 | 39 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (1 <
𝑧 ↔ 2 ≤ 𝑧)) |
41 | | zltlem1 12129 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑧 < 𝑃 ↔ 𝑧 ≤ (𝑃 − 1))) |
42 | 40, 41 | anbi12d 634 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((1 <
𝑧 ∧ 𝑧 < 𝑃) ↔ (2 ≤ 𝑧 ∧ 𝑧 ≤ (𝑃 − 1)))) |
43 | | peano2zm 12119 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑃 ∈ ℤ → (𝑃 − 1) ∈
ℤ) |
44 | | 2z 12108 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℤ |
45 | | elfz 13000 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∈ ℤ ∧ 2 ∈
ℤ ∧ (𝑃 − 1)
∈ ℤ) → (𝑧
∈ (2...(𝑃 − 1))
↔ (2 ≤ 𝑧 ∧
𝑧 ≤ (𝑃 − 1)))) |
46 | 44, 45 | mp3an2 1450 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑧 ∈ ℤ ∧ (𝑃 − 1) ∈ ℤ)
→ (𝑧 ∈
(2...(𝑃 − 1)) ↔
(2 ≤ 𝑧 ∧ 𝑧 ≤ (𝑃 − 1)))) |
47 | 43, 46 | sylan2 596 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → (𝑧 ∈ (2...(𝑃 − 1)) ↔ (2 ≤ 𝑧 ∧ 𝑧 ≤ (𝑃 − 1)))) |
48 | 42, 47 | bitr4d 285 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∈ ℤ ∧ 𝑃 ∈ ℤ) → ((1 <
𝑧 ∧ 𝑧 < 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
49 | 4, 33, 48 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
50 | 49 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) ∧ 𝑧 ∥ 𝑃) → ((1 < 𝑧 ∧ 𝑧 < 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
51 | 32, 50 | bitr3d 284 |
. . . . . . . . . . . 12
⊢ (((𝑧 ∈ ℕ ∧ 𝑃 ∈
(ℤ≥‘2)) ∧ 𝑧 ∥ 𝑃) → (¬ (𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
52 | 51 | anasss 470 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℕ ∧ (𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃)) → (¬ (𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
53 | 52 | expcom 417 |
. . . . . . . . . 10
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → (𝑧 ∈ ℕ → (¬ (𝑧 = 1 ∨ 𝑧 = 𝑃) ↔ 𝑧 ∈ (2...(𝑃 − 1))))) |
54 | 53 | pm5.32d 580 |
. . . . . . . . 9
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ (𝑧 ∈ ℕ ∧ 𝑧 ∈ (2...(𝑃 − 1))))) |
55 | | fzssuz 13052 |
. . . . . . . . . . . . 13
⊢
(2...(𝑃 − 1))
⊆ (ℤ≥‘2) |
56 | | 2eluzge1 12389 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
(ℤ≥‘1) |
57 | | uzss 12360 |
. . . . . . . . . . . . . 14
⊢ (2 ∈
(ℤ≥‘1) → (ℤ≥‘2)
⊆ (ℤ≥‘1)) |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘2) ⊆
(ℤ≥‘1) |
59 | 55, 58 | sstri 3896 |
. . . . . . . . . . . 12
⊢
(2...(𝑃 − 1))
⊆ (ℤ≥‘1) |
60 | | nnuz 12376 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
61 | 59, 60 | sseqtrri 3924 |
. . . . . . . . . . 11
⊢
(2...(𝑃 − 1))
⊆ ℕ |
62 | 61 | sseli 3883 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (2...(𝑃 − 1)) → 𝑧 ∈ ℕ) |
63 | 62 | pm4.71ri 564 |
. . . . . . . . 9
⊢ (𝑧 ∈ (2...(𝑃 − 1)) ↔ (𝑧 ∈ ℕ ∧ 𝑧 ∈ (2...(𝑃 − 1)))) |
64 | 54, 63 | bitr4di 292 |
. . . . . . . 8
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ 𝑧 ∈ (2...(𝑃 − 1)))) |
65 | 64 | notbid 321 |
. . . . . . 7
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → (¬ (𝑧 ∈ ℕ ∧ ¬ (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ¬ 𝑧 ∈ (2...(𝑃 − 1)))) |
66 | 2, 65 | syl5bb 286 |
. . . . . 6
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ 𝑧 ∥ 𝑃) → ((𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ¬ 𝑧 ∈ (2...(𝑃 − 1)))) |
67 | 66 | pm5.74da 804 |
. . . . 5
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∥ 𝑃 → (𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑧 ∥ 𝑃 → ¬ 𝑧 ∈ (2...(𝑃 − 1))))) |
68 | | bi2.04 392 |
. . . . 5
⊢ ((𝑧 ∥ 𝑃 → (𝑧 ∈ ℕ → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)))) |
69 | | con2b 363 |
. . . . 5
⊢ ((𝑧 ∥ 𝑃 → ¬ 𝑧 ∈ (2...(𝑃 − 1))) ↔ (𝑧 ∈ (2...(𝑃 − 1)) → ¬ 𝑧 ∥ 𝑃)) |
70 | 67, 68, 69 | 3bitr3g 316 |
. . . 4
⊢ (𝑃 ∈
(ℤ≥‘2) → ((𝑧 ∈ ℕ → (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑧 ∈ (2...(𝑃 − 1)) → ¬ 𝑧 ∥ 𝑃))) |
71 | 70 | ralbidv2 3108 |
. . 3
⊢ (𝑃 ∈
(ℤ≥‘2) → (∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃)) ↔ ∀𝑧 ∈ (2...(𝑃 − 1)) ¬ 𝑧 ∥ 𝑃)) |
72 | 71 | pm5.32i 578 |
. 2
⊢ ((𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ ℕ (𝑧 ∥ 𝑃 → (𝑧 = 1 ∨ 𝑧 = 𝑃))) ↔ (𝑃 ∈ (ℤ≥‘2)
∧ ∀𝑧 ∈
(2...(𝑃 − 1)) ¬
𝑧 ∥ 𝑃)) |
73 | 1, 72 | bitri 278 |
1
⊢ (𝑃 ∈ ℙ ↔ (𝑃 ∈
(ℤ≥‘2) ∧ ∀𝑧 ∈ (2...(𝑃 − 1)) ¬ 𝑧 ∥ 𝑃)) |