Proof of Theorem prmlem0
Step | Hyp | Ref
| Expression |
1 | | eldifi 4066 |
. . . . 5
⊢ (𝑥 ∈ (ℙ ∖ {2})
→ 𝑥 ∈
ℙ) |
2 | | prmlem0.2 |
. . . . . 6
⊢ (𝐾 ∈ ℙ → ¬
𝐾 ∥ 𝑁) |
3 | | eleq1 2828 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (𝑥 ∈ ℙ ↔ 𝐾 ∈ ℙ)) |
4 | | breq1 5082 |
. . . . . . . 8
⊢ (𝑥 = 𝐾 → (𝑥 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁)) |
5 | 4 | notbid 318 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (¬ 𝑥 ∥ 𝑁 ↔ ¬ 𝐾 ∥ 𝑁)) |
6 | 3, 5 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝐾 → ((𝑥 ∈ ℙ → ¬ 𝑥 ∥ 𝑁) ↔ (𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁))) |
7 | 2, 6 | mpbiri 257 |
. . . . 5
⊢ (𝑥 = 𝐾 → (𝑥 ∈ ℙ → ¬ 𝑥 ∥ 𝑁)) |
8 | 1, 7 | syl5 34 |
. . . 4
⊢ (𝑥 = 𝐾 → (𝑥 ∈ (ℙ ∖ {2}) → ¬
𝑥 ∥ 𝑁)) |
9 | 8 | adantrd 492 |
. . 3
⊢ (𝑥 = 𝐾 → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
10 | 9 | a1i 11 |
. 2
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 = 𝐾 → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
11 | | uzp1 12630 |
. . 3
⊢ (𝑥 ∈
(ℤ≥‘(𝐾 + 1)) → (𝑥 = (𝐾 + 1) ∨ 𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1)))) |
12 | | eleq1 2828 |
. . . . . . . 8
⊢ (𝑥 = (𝐾 + 1) → (𝑥 ∈ (ℙ ∖ {2}) ↔ (𝐾 + 1) ∈ (ℙ ∖
{2}))) |
13 | 12 | adantl 482 |
. . . . . . 7
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 ∈ (ℙ ∖ {2}) ↔ (𝐾 + 1) ∈ (ℙ ∖
{2}))) |
14 | | eldifsn 4726 |
. . . . . . . . 9
⊢ ((𝐾 + 1) ∈ (ℙ ∖
{2}) ↔ ((𝐾 + 1) ∈
ℙ ∧ (𝐾 + 1) ≠
2)) |
15 | | eluzel2 12598 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
(ℤ≥‘𝐾) → 𝐾 ∈ ℤ) |
16 | 15 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 𝐾 ∈ ℤ) |
17 | | simpl 483 |
. . . . . . . . . . . . . . . 16
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ¬ 2 ∥ 𝐾) |
18 | | 1z 12361 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
19 | | n2dvds1 16088 |
. . . . . . . . . . . . . . . . 17
⊢ ¬ 2
∥ 1 |
20 | | opoe 16083 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐾 + 1)) |
21 | 18, 19, 20 | mpanr12 702 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) → 2 ∥
(𝐾 + 1)) |
22 | 16, 17, 21 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 2 ∥ (𝐾 + 1)) |
23 | 22 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → 2 ∥
(𝐾 + 1)) |
24 | | 2z 12363 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
25 | | uzid 12608 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
26 | 24, 25 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 2 ∈
(ℤ≥‘2)) |
27 | | dvdsprm 16419 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ (ℤ≥‘2) ∧ (𝐾 + 1) ∈ ℙ) → (2 ∥
(𝐾 + 1) ↔ 2 = (𝐾 + 1))) |
28 | 26, 27 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → (2 ∥
(𝐾 + 1) ↔ 2 = (𝐾 + 1))) |
29 | 23, 28 | mpbid 231 |
. . . . . . . . . . . . 13
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → 2 = (𝐾 + 1)) |
30 | 29 | eqcomd 2746 |
. . . . . . . . . . . 12
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → (𝐾 + 1) = 2) |
31 | 30 | a1d 25 |
. . . . . . . . . . 11
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → (𝑥 ∥ 𝑁 → (𝐾 + 1) = 2)) |
32 | 31 | necon3ad 2958 |
. . . . . . . . . 10
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → ((𝐾 + 1) ≠ 2 → ¬ 𝑥 ∥ 𝑁)) |
33 | 32 | expimpd 454 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (((𝐾 + 1) ∈ ℙ ∧ (𝐾 + 1) ≠ 2) → ¬ 𝑥 ∥ 𝑁)) |
34 | 14, 33 | syl5bi 241 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝐾 + 1) ∈ (ℙ ∖ {2}) →
¬ 𝑥 ∥ 𝑁)) |
35 | 34 | adantr 481 |
. . . . . . 7
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → ((𝐾 + 1) ∈ (ℙ ∖ {2}) →
¬ 𝑥 ∥ 𝑁)) |
36 | 13, 35 | sylbid 239 |
. . . . . 6
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 ∈ (ℙ ∖ {2}) → ¬
𝑥 ∥ 𝑁)) |
37 | 36 | adantrd 492 |
. . . . 5
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
38 | 37 | ex 413 |
. . . 4
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 = (𝐾 + 1) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
39 | 16 | zcnd 12438 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 𝐾 ∈ ℂ) |
40 | | ax-1cn 10940 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
41 | | addass 10969 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) + 1) = (𝐾 + (1 + 1))) |
42 | 40, 40, 41 | mp3an23 1452 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℂ → ((𝐾 + 1) + 1) = (𝐾 + (1 + 1))) |
43 | 39, 42 | syl 17 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝐾 + 1) + 1) = (𝐾 + (1 + 1))) |
44 | | 1p1e2 12109 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
45 | 44 | oveq2i 7283 |
. . . . . . . . 9
⊢ (𝐾 + (1 + 1)) = (𝐾 + 2) |
46 | | prmlem0.3 |
. . . . . . . . 9
⊢ (𝐾 + 2) = 𝑀 |
47 | 45, 46 | eqtri 2768 |
. . . . . . . 8
⊢ (𝐾 + (1 + 1)) = 𝑀 |
48 | 43, 47 | eqtrdi 2796 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝐾 + 1) + 1) = 𝑀) |
49 | 48 | fveq2d 6775 |
. . . . . 6
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) →
(ℤ≥‘((𝐾 + 1) + 1)) =
(ℤ≥‘𝑀)) |
50 | 49 | eleq2d 2826 |
. . . . 5
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1)) ↔ 𝑥 ∈
(ℤ≥‘𝑀))) |
51 | | dvdsaddr 16023 |
. . . . . . . . 9
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 ∥ 𝐾 ↔ 2 ∥ (𝐾 + 2))) |
52 | 24, 16, 51 | sylancr 587 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (2 ∥ 𝐾 ↔ 2 ∥ (𝐾 + 2))) |
53 | 46 | breq2i 5087 |
. . . . . . . 8
⊢ (2
∥ (𝐾 + 2) ↔ 2
∥ 𝑀) |
54 | 52, 53 | bitrdi 287 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (2 ∥ 𝐾 ↔ 2 ∥ 𝑀)) |
55 | 17, 54 | mtbid 324 |
. . . . . 6
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ¬ 2 ∥ 𝑀) |
56 | | prmlem0.1 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
57 | 56 | ex 413 |
. . . . . 6
⊢ (¬ 2
∥ 𝑀 → (𝑥 ∈
(ℤ≥‘𝑀) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
58 | 55, 57 | syl 17 |
. . . . 5
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘𝑀) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
59 | 50, 58 | sylbid 239 |
. . . 4
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1)) → ((𝑥 ∈ (ℙ ∖ {2})
∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
60 | 38, 59 | jaod 856 |
. . 3
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝑥 = (𝐾 + 1) ∨ 𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1))) → ((𝑥 ∈ (ℙ ∖ {2})
∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
61 | 11, 60 | syl5 34 |
. 2
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘(𝐾 + 1)) → ((𝑥 ∈ (ℙ ∖ {2})
∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
62 | | uzp1 12630 |
. . 3
⊢ (𝑥 ∈
(ℤ≥‘𝐾) → (𝑥 = 𝐾 ∨ 𝑥 ∈ (ℤ≥‘(𝐾 + 1)))) |
63 | 62 | adantl 482 |
. 2
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 = 𝐾 ∨ 𝑥 ∈ (ℤ≥‘(𝐾 + 1)))) |
64 | 10, 61, 63 | mpjaod 857 |
1
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |