Step | Hyp | Ref
| Expression |
1 | | elrabi 3328 |
. . . 4
⊢ (𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑟 ∈ ℙ) |
2 | 1 | ad2antlr 759 |
. . 3
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ ∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟) → 𝑟 ∈ ℙ) |
3 | | breq1 4586 |
. . . . 5
⊢ (𝑝 = 𝑟 → (𝑝 < 𝑁 ↔ 𝑟 < 𝑁)) |
4 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑝 = 𝑟 → (𝑝 + 1) = (𝑟 + 1)) |
5 | 4 | oveq1d 6564 |
. . . . . 6
⊢ (𝑝 = 𝑟 → ((𝑝 + 1)..^𝑁) = ((𝑟 + 1)..^𝑁)) |
6 | 5 | raleqdv 3121 |
. . . . 5
⊢ (𝑝 = 𝑟 → (∀𝑧 ∈ ((𝑝 + 1)..^𝑁)𝑧 ∉ ℙ ↔ ∀𝑧 ∈ ((𝑟 + 1)..^𝑁)𝑧 ∉ ℙ)) |
7 | 3, 6 | anbi12d 743 |
. . . 4
⊢ (𝑝 = 𝑟 → ((𝑝 < 𝑁 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑁)𝑧 ∉ ℙ) ↔ (𝑟 < 𝑁 ∧ ∀𝑧 ∈ ((𝑟 + 1)..^𝑁)𝑧 ∉ ℙ))) |
8 | 7 | adantl 481 |
. . 3
⊢ ((((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ ∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟) ∧ 𝑝 = 𝑟) → ((𝑝 < 𝑁 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑁)𝑧 ∉ ℙ) ↔ (𝑟 < 𝑁 ∧ ∀𝑧 ∈ ((𝑟 + 1)..^𝑁)𝑧 ∉ ℙ))) |
9 | | breq1 4586 |
. . . . . . 7
⊢ (𝑞 = 𝑟 → (𝑞 < 𝑁 ↔ 𝑟 < 𝑁)) |
10 | 9 | elrab 3331 |
. . . . . 6
⊢ (𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} ↔ (𝑟 ∈ ℙ ∧ 𝑟 < 𝑁)) |
11 | 10 | simprbi 479 |
. . . . 5
⊢ (𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑟 < 𝑁) |
12 | 11 | ad2antlr 759 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ ∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟) → 𝑟 < 𝑁) |
13 | | elfzo2 12342 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝑟 + 1)..^𝑁) ↔ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) |
14 | | simpl 472 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℙ ∧ (𝑧 ∈
(ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → 𝑧 ∈ ℙ) |
15 | | simpr3 1062 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ ℙ ∧ (𝑧 ∈
(ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → 𝑧 < 𝑁) |
16 | | breq1 4586 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 = 𝑧 → (𝑞 < 𝑁 ↔ 𝑧 < 𝑁)) |
17 | 16 | elrab 3331 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} ↔ (𝑧 ∈ ℙ ∧ 𝑧 < 𝑁)) |
18 | 14, 15, 17 | sylanbrc 695 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∈ ℙ ∧ (𝑧 ∈
(ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → 𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) |
19 | 18 | adantrl 748 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℙ ∧ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁))) → 𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) |
20 | | eluz2 11569 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈
(ℤ≥‘(𝑟 + 1)) ↔ ((𝑟 + 1) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ (𝑟 + 1) ≤ 𝑧)) |
21 | | prmz 15227 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑟 ∈ ℙ → 𝑟 ∈
ℤ) |
22 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑟 ∈ ℤ ∧ 𝑧 ∈ ℤ) → (𝑟 < 𝑧 ↔ (𝑟 + 1) ≤ 𝑧)) |
23 | 21, 22 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ) → (𝑟 < 𝑧 ↔ (𝑟 + 1) ≤ 𝑧)) |
24 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑟 ∈ ℙ → 𝑟 ∈
ℕ) |
25 | 24 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑟 ∈ ℙ → 𝑟 ∈
ℝ) |
26 | | zre 11258 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑧 ∈ ℤ → 𝑧 ∈
ℝ) |
27 | | ltnle 9996 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑟 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑟 < 𝑧 ↔ ¬ 𝑧 ≤ 𝑟)) |
28 | 27 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑟 ∈ ℝ ∧ 𝑧 ∈ ℝ) → (𝑟 < 𝑧 → ¬ 𝑧 ≤ 𝑟)) |
29 | 25, 26, 28 | syl2an 493 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ) → (𝑟 < 𝑧 → ¬ 𝑧 ≤ 𝑟)) |
30 | | pm2.21 119 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (¬
𝑧 ≤ 𝑟 → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ)) |
31 | 29, 30 | syl6 34 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ) → (𝑟 < 𝑧 → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))) |
32 | 23, 31 | sylbird 249 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ ℙ ∧ 𝑧 ∈ ℤ) → ((𝑟 + 1) ≤ 𝑧 → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))) |
33 | 32 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ ℤ → (𝑟 ∈ ℙ → ((𝑟 + 1) ≤ 𝑧 → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ)))) |
34 | 33 | com23 84 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ ℤ → ((𝑟 + 1) ≤ 𝑧 → (𝑟 ∈ ℙ → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ)))) |
35 | 34 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑟 + 1) ∈ ℤ →
(𝑧 ∈ ℤ →
((𝑟 + 1) ≤ 𝑧 → (𝑟 ∈ ℙ → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))))) |
36 | 35 | 3imp 1249 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑟 + 1) ∈ ℤ ∧ 𝑧 ∈ ℤ ∧ (𝑟 + 1) ≤ 𝑧) → (𝑟 ∈ ℙ → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))) |
37 | 20, 36 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 ∈
(ℤ≥‘(𝑟 + 1)) → (𝑟 ∈ ℙ → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))) |
38 | 37 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∈
(ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁) → (𝑟 ∈ ℙ → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))) |
39 | 1, 38 | syl5com 31 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → ((𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁) → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) → ((𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁) → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ))) |
41 | 40 | imp 444 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ)) |
42 | 41 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈ ℙ ∧ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁))) → (𝑧 ≤ 𝑟 → 𝑧 ∉ ℙ)) |
43 | 19, 42 | embantd 57 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ ℙ ∧ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁))) → ((𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟) → 𝑧 ∉ ℙ)) |
44 | 43 | ex 449 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ℙ → (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → ((𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟) → 𝑧 ∉ ℙ))) |
45 | | df-nel 2783 |
. . . . . . . . . . 11
⊢ (𝑧 ∉ ℙ ↔ ¬
𝑧 ∈
ℙ) |
46 | | ax-1 6 |
. . . . . . . . . . . 12
⊢ (𝑧 ∉ ℙ → ((𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟) → 𝑧 ∉ ℙ)) |
47 | 46 | a1d 25 |
. . . . . . . . . . 11
⊢ (𝑧 ∉ ℙ → (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → ((𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟) → 𝑧 ∉ ℙ))) |
48 | 45, 47 | sylbir 224 |
. . . . . . . . . 10
⊢ (¬
𝑧 ∈ ℙ →
(((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → ((𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟) → 𝑧 ∉ ℙ))) |
49 | 44, 48 | pm2.61i 175 |
. . . . . . . . 9
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁)) → ((𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟) → 𝑧 ∉ ℙ)) |
50 | 49 | impancom 455 |
. . . . . . . 8
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟)) → ((𝑧 ∈ (ℤ≥‘(𝑟 + 1)) ∧ 𝑁 ∈ ℤ ∧ 𝑧 < 𝑁) → 𝑧 ∉ ℙ)) |
51 | 13, 50 | syl5bi 231 |
. . . . . . 7
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ (𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟)) → (𝑧 ∈ ((𝑟 + 1)..^𝑁) → 𝑧 ∉ ℙ)) |
52 | 51 | ex 449 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) → ((𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} → 𝑧 ≤ 𝑟) → (𝑧 ∈ ((𝑟 + 1)..^𝑁) → 𝑧 ∉ ℙ))) |
53 | 52 | ralimdv2 2944 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) → (∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟 → ∀𝑧 ∈ ((𝑟 + 1)..^𝑁)𝑧 ∉ ℙ)) |
54 | 53 | imp 444 |
. . . 4
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ ∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟) → ∀𝑧 ∈ ((𝑟 + 1)..^𝑁)𝑧 ∉ ℙ) |
55 | 12, 54 | jca 553 |
. . 3
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ ∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟) → (𝑟 < 𝑁 ∧ ∀𝑧 ∈ ((𝑟 + 1)..^𝑁)𝑧 ∉ ℙ)) |
56 | 2, 8, 55 | rspcedvd 3289 |
. 2
⊢ (((𝑁 ∈
(ℤ≥‘3) ∧ 𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}) ∧ ∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟) → ∃𝑝 ∈ ℙ (𝑝 < 𝑁 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑁)𝑧 ∉ ℙ)) |
57 | | eqid 2610 |
. . 3
⊢ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} = {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁} |
58 | 57 | prmgaplem3 15595 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘3) → ∃𝑟 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}∀𝑧 ∈ {𝑞 ∈ ℙ ∣ 𝑞 < 𝑁}𝑧 ≤ 𝑟) |
59 | 56, 58 | r19.29a 3060 |
1
⊢ (𝑁 ∈
(ℤ≥‘3) → ∃𝑝 ∈ ℙ (𝑝 < 𝑁 ∧ ∀𝑧 ∈ ((𝑝 + 1)..^𝑁)𝑧 ∉ ℙ)) |