Proof of Theorem prmlem0
Step | Hyp | Ref
| Expression |
1 | | eldifi 3694 |
. . . . 5
⊢ (𝑥 ∈ (ℙ ∖ {2})
→ 𝑥 ∈
ℙ) |
2 | | prmlem0.2 |
. . . . . 6
⊢ (𝐾 ∈ ℙ → ¬
𝐾 ∥ 𝑁) |
3 | | eleq1 2676 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (𝑥 ∈ ℙ ↔ 𝐾 ∈ ℙ)) |
4 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑥 = 𝐾 → (𝑥 ∥ 𝑁 ↔ 𝐾 ∥ 𝑁)) |
5 | 4 | notbid 307 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → (¬ 𝑥 ∥ 𝑁 ↔ ¬ 𝐾 ∥ 𝑁)) |
6 | 3, 5 | imbi12d 333 |
. . . . . 6
⊢ (𝑥 = 𝐾 → ((𝑥 ∈ ℙ → ¬ 𝑥 ∥ 𝑁) ↔ (𝐾 ∈ ℙ → ¬ 𝐾 ∥ 𝑁))) |
7 | 2, 6 | mpbiri 247 |
. . . . 5
⊢ (𝑥 = 𝐾 → (𝑥 ∈ ℙ → ¬ 𝑥 ∥ 𝑁)) |
8 | 1, 7 | syl5 33 |
. . . 4
⊢ (𝑥 = 𝐾 → (𝑥 ∈ (ℙ ∖ {2}) → ¬
𝑥 ∥ 𝑁)) |
9 | 8 | adantrd 483 |
. . 3
⊢ (𝑥 = 𝐾 → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
10 | 9 | a1i 11 |
. 2
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 = 𝐾 → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
11 | | uzp1 11597 |
. . 3
⊢ (𝑥 ∈
(ℤ≥‘(𝐾 + 1)) → (𝑥 = (𝐾 + 1) ∨ 𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1)))) |
12 | | eleq1 2676 |
. . . . . . . 8
⊢ (𝑥 = (𝐾 + 1) → (𝑥 ∈ (ℙ ∖ {2}) ↔ (𝐾 + 1) ∈ (ℙ ∖
{2}))) |
13 | 12 | adantl 481 |
. . . . . . 7
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 ∈ (ℙ ∖ {2}) ↔ (𝐾 + 1) ∈ (ℙ ∖
{2}))) |
14 | | eldifsn 4260 |
. . . . . . . . 9
⊢ ((𝐾 + 1) ∈ (ℙ ∖
{2}) ↔ ((𝐾 + 1) ∈
ℙ ∧ (𝐾 + 1) ≠
2)) |
15 | | eluzel2 11568 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈
(ℤ≥‘𝐾) → 𝐾 ∈ ℤ) |
16 | 15 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 𝐾 ∈ ℤ) |
17 | | simpl 472 |
. . . . . . . . . . . . . . . 16
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ¬ 2 ∥ 𝐾) |
18 | | 1z 11284 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℤ |
19 | | n2dvds1 14942 |
. . . . . . . . . . . . . . . . 17
⊢ ¬ 2
∥ 1 |
20 | | opoe 14925 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) ∧ (1 ∈
ℤ ∧ ¬ 2 ∥ 1)) → 2 ∥ (𝐾 + 1)) |
21 | 18, 19, 20 | mpanr12 717 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ ¬ 2
∥ 𝐾) → 2 ∥
(𝐾 + 1)) |
22 | 16, 17, 21 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 2 ∥ (𝐾 + 1)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → 2 ∥
(𝐾 + 1)) |
24 | | 2z 11286 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
25 | | uzid 11578 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℤ → 2 ∈ (ℤ≥‘2)) |
26 | 24, 25 | mp1i 13 |
. . . . . . . . . . . . . . 15
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 2 ∈
(ℤ≥‘2)) |
27 | | dvdsprm 15253 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ (ℤ≥‘2) ∧ (𝐾 + 1) ∈ ℙ) → (2 ∥
(𝐾 + 1) ↔ 2 = (𝐾 + 1))) |
28 | 26, 27 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → (2 ∥
(𝐾 + 1) ↔ 2 = (𝐾 + 1))) |
29 | 23, 28 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → 2 = (𝐾 + 1)) |
30 | 29 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → (𝐾 + 1) = 2) |
31 | 30 | a1d 25 |
. . . . . . . . . . 11
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → (𝑥 ∥ 𝑁 → (𝐾 + 1) = 2)) |
32 | 31 | necon3ad 2795 |
. . . . . . . . . 10
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ (𝐾 + 1) ∈ ℙ) → ((𝐾 + 1) ≠ 2 → ¬ 𝑥 ∥ 𝑁)) |
33 | 32 | expimpd 627 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (((𝐾 + 1) ∈ ℙ ∧ (𝐾 + 1) ≠ 2) → ¬ 𝑥 ∥ 𝑁)) |
34 | 14, 33 | syl5bi 231 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝐾 + 1) ∈ (ℙ ∖ {2}) →
¬ 𝑥 ∥ 𝑁)) |
35 | 34 | adantr 480 |
. . . . . . 7
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → ((𝐾 + 1) ∈ (ℙ ∖ {2}) →
¬ 𝑥 ∥ 𝑁)) |
36 | 13, 35 | sylbid 229 |
. . . . . 6
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → (𝑥 ∈ (ℙ ∖ {2}) → ¬
𝑥 ∥ 𝑁)) |
37 | 36 | adantrd 483 |
. . . . 5
⊢ (((¬
2 ∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) ∧ 𝑥 = (𝐾 + 1)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
38 | 37 | ex 449 |
. . . 4
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 = (𝐾 + 1) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
39 | 16 | zcnd 11359 |
. . . . . . . . 9
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → 𝐾 ∈ ℂ) |
40 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
41 | | addass 9902 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) + 1) = (𝐾 + (1 + 1))) |
42 | 40, 40, 41 | mp3an23 1408 |
. . . . . . . . 9
⊢ (𝐾 ∈ ℂ → ((𝐾 + 1) + 1) = (𝐾 + (1 + 1))) |
43 | 39, 42 | syl 17 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝐾 + 1) + 1) = (𝐾 + (1 + 1))) |
44 | | 1p1e2 11011 |
. . . . . . . . . 10
⊢ (1 + 1) =
2 |
45 | 44 | oveq2i 6560 |
. . . . . . . . 9
⊢ (𝐾 + (1 + 1)) = (𝐾 + 2) |
46 | | prmlem0.3 |
. . . . . . . . 9
⊢ (𝐾 + 2) = 𝑀 |
47 | 45, 46 | eqtri 2632 |
. . . . . . . 8
⊢ (𝐾 + (1 + 1)) = 𝑀 |
48 | 43, 47 | syl6eq 2660 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝐾 + 1) + 1) = 𝑀) |
49 | 48 | fveq2d 6107 |
. . . . . 6
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) →
(ℤ≥‘((𝐾 + 1) + 1)) =
(ℤ≥‘𝑀)) |
50 | 49 | eleq2d 2673 |
. . . . 5
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1)) ↔ 𝑥 ∈
(ℤ≥‘𝑀))) |
51 | | dvdsaddr 14863 |
. . . . . . . . 9
⊢ ((2
∈ ℤ ∧ 𝐾
∈ ℤ) → (2 ∥ 𝐾 ↔ 2 ∥ (𝐾 + 2))) |
52 | 24, 16, 51 | sylancr 694 |
. . . . . . . 8
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (2 ∥ 𝐾 ↔ 2 ∥ (𝐾 + 2))) |
53 | 46 | breq2i 4591 |
. . . . . . . 8
⊢ (2
∥ (𝐾 + 2) ↔ 2
∥ 𝑀) |
54 | 52, 53 | syl6bb 275 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (2 ∥ 𝐾 ↔ 2 ∥ 𝑀)) |
55 | 17, 54 | mtbid 313 |
. . . . . 6
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ¬ 2 ∥ 𝑀) |
56 | | prmlem0.1 |
. . . . . . 7
⊢ ((¬ 2
∥ 𝑀 ∧ 𝑥 ∈
(ℤ≥‘𝑀)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |
57 | 56 | ex 449 |
. . . . . 6
⊢ (¬ 2
∥ 𝑀 → (𝑥 ∈
(ℤ≥‘𝑀) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
58 | 55, 57 | syl 17 |
. . . . 5
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘𝑀) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
59 | 50, 58 | sylbid 229 |
. . . 4
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1)) → ((𝑥 ∈ (ℙ ∖ {2})
∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
60 | 38, 59 | jaod 394 |
. . 3
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝑥 = (𝐾 + 1) ∨ 𝑥 ∈ (ℤ≥‘((𝐾 + 1) + 1))) → ((𝑥 ∈ (ℙ ∖ {2})
∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
61 | 11, 60 | syl5 33 |
. 2
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 ∈ (ℤ≥‘(𝐾 + 1)) → ((𝑥 ∈ (ℙ ∖ {2})
∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁))) |
62 | | uzp1 11597 |
. . 3
⊢ (𝑥 ∈
(ℤ≥‘𝐾) → (𝑥 = 𝐾 ∨ 𝑥 ∈ (ℤ≥‘(𝐾 + 1)))) |
63 | 62 | adantl 481 |
. 2
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → (𝑥 = 𝐾 ∨ 𝑥 ∈ (ℤ≥‘(𝐾 + 1)))) |
64 | 10, 61, 63 | mpjaod 395 |
1
⊢ ((¬ 2
∥ 𝐾 ∧ 𝑥 ∈
(ℤ≥‘𝐾)) → ((𝑥 ∈ (ℙ ∖ {2}) ∧ (𝑥↑2) ≤ 𝑁) → ¬ 𝑥 ∥ 𝑁)) |