| Step | Hyp | Ref
| Expression |
| 1 | | prmrec.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | 1 | nnred 12281 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℝ) |
| 3 | 2 | rehalfcld 12513 |
. 2
⊢ (𝜑 → (𝑁 / 2) ∈ ℝ) |
| 4 | | fzfi 14013 |
. . . . . 6
⊢
(1...𝑁) ∈
Fin |
| 5 | | prmrec.4 |
. . . . . . 7
⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} |
| 6 | 5 | ssrab3 4082 |
. . . . . 6
⊢ 𝑀 ⊆ (1...𝑁) |
| 7 | | ssfi 9213 |
. . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin) |
| 8 | 4, 6, 7 | mp2an 692 |
. . . . 5
⊢ 𝑀 ∈ Fin |
| 9 | | hashcl 14395 |
. . . . 5
⊢ (𝑀 ∈ Fin →
(♯‘𝑀) ∈
ℕ0) |
| 10 | 8, 9 | ax-mp 5 |
. . . 4
⊢
(♯‘𝑀)
∈ ℕ0 |
| 11 | 10 | nn0rei 12537 |
. . 3
⊢
(♯‘𝑀)
∈ ℝ |
| 12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → (♯‘𝑀) ∈
ℝ) |
| 13 | | 2nn 12339 |
. . . . 5
⊢ 2 ∈
ℕ |
| 14 | | prmrec.2 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
| 15 | 14 | nnnn0d 12587 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
| 16 | | nnexpcl 14115 |
. . . . 5
⊢ ((2
∈ ℕ ∧ 𝐾
∈ ℕ0) → (2↑𝐾) ∈ ℕ) |
| 17 | 13, 15, 16 | sylancr 587 |
. . . 4
⊢ (𝜑 → (2↑𝐾) ∈ ℕ) |
| 18 | 17 | nnred 12281 |
. . 3
⊢ (𝜑 → (2↑𝐾) ∈ ℝ) |
| 19 | 1 | nnrpd 13075 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
| 20 | 19 | rpsqrtcld 15450 |
. . . 4
⊢ (𝜑 → (√‘𝑁) ∈
ℝ+) |
| 21 | 20 | rpred 13077 |
. . 3
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) |
| 22 | 18, 21 | remulcld 11291 |
. 2
⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ) |
| 23 | 2 | recnd 11289 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) |
| 24 | 23 | 2halvesd 12512 |
. . . . 5
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁) |
| 25 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ⊆ (1...𝑁)) |
| 26 | 14 | peano2nnd 12283 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 1) ∈ ℕ) |
| 27 | | elfzuz 13560 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
| 28 | | eluznn 12960 |
. . . . . . . . . . . . 13
⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ) |
| 29 | 26, 27, 28 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ) |
| 30 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
| 31 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) |
| 32 | 30, 31 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛))) |
| 33 | 32 | rabbidv 3444 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
| 34 | | prmrec.7 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)}) |
| 35 | | ovex 7464 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑁) ∈
V |
| 36 | 35 | rabex 5339 |
. . . . . . . . . . . . . . 15
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V |
| 37 | 33, 34, 36 | fvmpt 7016 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
| 38 | 37 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
| 39 | | ssrab2 4080 |
. . . . . . . . . . . . 13
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁) |
| 40 | 38, 39 | eqsstrdi 4028 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
| 41 | 29, 40 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
| 42 | 41 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
| 43 | | iunss 5045 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
| 44 | 42, 43 | sylibr 234 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
| 45 | 25, 44 | unssd 4192 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ⊆ (1...𝑁)) |
| 46 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑛 ↔ 𝑞 ∥ 𝑛)) |
| 47 | 46 | notbid 318 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑞 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑛)) |
| 48 | 47 | cbvralvw 3237 |
. . . . . . . . . . . . . 14
⊢
(∀𝑝 ∈
(ℙ ∖ (1...𝐾))
¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖
(1...𝐾)) ¬ 𝑞 ∥ 𝑛) |
| 49 | | breq2 5147 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → (𝑞 ∥ 𝑛 ↔ 𝑞 ∥ 𝑥)) |
| 50 | 49 | notbid 318 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → (¬ 𝑞 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑥)) |
| 51 | 50 | ralbidv 3178 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
| 52 | 48, 51 | bitrid 283 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
| 53 | 52, 5 | elrab2 3695 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
| 54 | | elun1 4182 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑀 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 55 | 53, 54 | sylbir 235 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 56 | 55 | ex 412 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 57 | 56 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 58 | | dfrex2 3073 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈
(ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) |
| 59 | 14 | nnzd 12640 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 60 | 59 | peano2zd 12725 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) |
| 61 | 60 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ∈ ℤ) |
| 62 | 1 | nnzd 12640 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) |
| 63 | 62 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℤ) |
| 64 | | eldifi 4131 |
. . . . . . . . . . . . . . . 16
⊢ (𝑞 ∈ (ℙ ∖
(1...𝐾)) → 𝑞 ∈
ℙ) |
| 65 | 64 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℙ) |
| 66 | | prmz 16712 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
| 67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℤ) |
| 68 | | eldifn 4132 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 ∈ (ℙ ∖
(1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾)) |
| 69 | 68 | ad2antrl 728 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ∈ (1...𝐾)) |
| 70 | | prmnn 16711 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
| 71 | 65, 70 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℕ) |
| 72 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) |
| 73 | 71, 72 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈
(ℤ≥‘1)) |
| 74 | 59 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℤ) |
| 75 | | elfz5 13556 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈
(ℤ≥‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾)) |
| 76 | 73, 74, 75 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾)) |
| 77 | 69, 76 | mtbid 324 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ≤ 𝐾) |
| 78 | 14 | nnred 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 79 | 78 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℝ) |
| 80 | 71 | nnred 12281 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℝ) |
| 81 | 79, 80 | ltnled 11408 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞 ≤ 𝐾)) |
| 82 | 77, 81 | mpbird 257 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 < 𝑞) |
| 83 | | zltp1le 12667 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞)) |
| 84 | 74, 67, 83 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞)) |
| 85 | 82, 84 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ≤ 𝑞) |
| 86 | | elfznn 13593 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
| 87 | 86 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℕ) |
| 88 | 87 | nnred 12281 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℝ) |
| 89 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℝ) |
| 90 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∥ 𝑥) |
| 91 | | dvdsle 16347 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
| 92 | 67, 87, 91 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
| 93 | 90, 92 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑥) |
| 94 | | elfzle2 13568 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁) |
| 95 | 94 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ≤ 𝑁) |
| 96 | 80, 88, 89, 93, 95 | letrd 11418 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑁) |
| 97 | 61, 63, 67, 85, 96 | elfzd 13555 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁)) |
| 98 | 49 | anbi2d 630 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥))) |
| 99 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (1...𝑁)) |
| 100 | 65, 90 | jca 511 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥)) |
| 101 | 98, 99, 100 | elrabd 3694 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
| 102 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ)) |
| 103 | 102, 46 | anbi12d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛))) |
| 104 | 103 | rabbidv 3444 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
| 105 | 35 | rabex 5339 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)} ∈ V |
| 106 | 104, 34, 105 | fvmpt 7016 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ ℕ → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
| 107 | 71, 106 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
| 108 | 101, 107 | eleqtrrd 2844 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑊‘𝑞)) |
| 109 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑞 → (𝑊‘𝑘) = (𝑊‘𝑞)) |
| 110 | 109 | eliuni 4997 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊‘𝑞)) → 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
| 111 | 97, 108, 110 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
| 112 | | elun2 4183 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 113 | 111, 112 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 114 | 113 | rexlimdvaa 3156 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 115 | 58, 114 | biimtrrid 243 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 116 | 57, 115 | pm2.61d 179 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 117 | 45, 116 | eqelssd 4005 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (1...𝑁)) |
| 118 | 117 | fveq2d 6910 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = (♯‘(1...𝑁))) |
| 119 | 1 | nnnn0d 12587 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 120 | | hashfz1 14385 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
| 121 | 119, 120 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) |
| 122 | 118, 121 | eqtr2d 2778 |
. . . . 5
⊢ (𝜑 → 𝑁 = (♯‘(𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 123 | 8 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ Fin) |
| 124 | | ssfi 9213 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin) |
| 125 | 4, 44, 124 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin) |
| 126 | | breq1 5146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑥 ↔ 𝑘 ∥ 𝑥)) |
| 127 | 126 | notbid 318 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑘 → (¬ 𝑝 ∥ 𝑥 ↔ ¬ 𝑘 ∥ 𝑥)) |
| 128 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑥 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑥)) |
| 129 | 128 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑥 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑥)) |
| 130 | 129 | ralbidv 3178 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)) |
| 131 | 130, 5 | elrab2 3695 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)) |
| 132 | 131 | simprbi 496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥) |
| 133 | 132 | ad2antlr 727 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖
(1...𝐾)) ¬ 𝑝 ∥ 𝑥) |
| 134 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ) |
| 135 | | noel 4338 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
𝑘 ∈
∅ |
| 136 | | simprl 771 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁)) |
| 137 | 136 | biantrud 531 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))) |
| 138 | | elin 3967 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))) |
| 139 | 137, 138 | bitr4di 289 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)))) |
| 140 | 78 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐾 < (𝐾 + 1)) |
| 141 | | fzdisj 13591 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
| 142 | 140, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
| 143 | 142 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
| 144 | 143 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅)) |
| 145 | 139, 144 | bitrd 279 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅)) |
| 146 | 135, 145 | mtbiri 327 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾)) |
| 147 | 134, 146 | eldifd 3962 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾))) |
| 148 | 127, 133,
147 | rspcdva 3623 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∥ 𝑥) |
| 149 | 148 | expr 456 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥)) |
| 150 | | imnan 399 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℙ → ¬
𝑘 ∥ 𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
| 151 | 149, 150 | sylib 218 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
| 152 | 29 | adantlr 715 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ) |
| 153 | 152, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
| 154 | 153 | eleq2d 2827 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})) |
| 155 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑥 → (𝑘 ∥ 𝑛 ↔ 𝑘 ∥ 𝑥)) |
| 156 | 155 | anbi2d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
| 157 | 156 | elrab 3692 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
| 158 | 157 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
| 159 | 154, 158 | biimtrdi 253 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
| 160 | 151, 159 | mtod 198 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊‘𝑘)) |
| 161 | 160 | nrexdv 3149 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘)) |
| 162 | | eliun 4995 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘)) |
| 163 | 161, 162 | sylnibr 329 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
| 164 | 163 | ex 412 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 165 | | imnan 399 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 166 | 164, 165 | sylib 218 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 167 | | elin 3967 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 168 | 166, 167 | sylnibr 329 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑥 ∈ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
| 169 | 168 | eq0rdv 4407 |
. . . . . 6
⊢ (𝜑 → (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) |
| 170 | | hashun 14421 |
. . . . . 6
⊢ ((𝑀 ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin ∧ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 171 | 123, 125,
169, 170 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 172 | 24, 122, 171 | 3eqtrd 2781 |
. . . 4
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
| 173 | | hashcl 14395 |
. . . . . . 7
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈
ℕ0) |
| 174 | 125, 173 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈
ℕ0) |
| 175 | 174 | nn0red 12588 |
. . . . 5
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℝ) |
| 176 | | fzfid 14014 |
. . . . . . . 8
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin) |
| 177 | 26, 28 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈
ℕ) |
| 178 | | nnrecre 12308 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
| 179 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 180 | | ifcl 4571 |
. . . . . . . . . . 11
⊢ (((1 /
𝑘) ∈ ℝ ∧ 0
∈ ℝ) → if(𝑘
∈ ℙ, (1 / 𝑘), 0)
∈ ℝ) |
| 181 | 178, 179,
180 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
| 182 | 177, 181 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
| 183 | 27, 182 | sylan2 593 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
| 184 | 176, 183 | fsumrecl 15770 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
| 185 | 2, 184 | remulcld 11291 |
. . . . . 6
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) |
| 186 | | prmrec.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) |
| 187 | | prmrec.5 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝
) |
| 188 | | prmrec.6 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) |
| 189 | 186, 14, 1, 5, 187, 188, 34 | prmreclem4 16957 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
| 190 | | eluz 12892 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈
(ℤ≥‘𝑁) ↔ 𝑁 ≤ 𝐾)) |
| 191 | 62, 59, 190 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) ↔ 𝑁 ≤ 𝐾)) |
| 192 | | nnleltp1 12673 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1))) |
| 193 | 1, 14, 192 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1))) |
| 194 | | fzn 13580 |
. . . . . . . . . 10
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
| 195 | 60, 62, 194 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
| 196 | 191, 193,
195 | 3bitrd 305 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
| 197 | | 0le0 12367 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
| 198 | 23 | mul01d 11460 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · 0) = 0) |
| 199 | 197, 198 | breqtrrid 5181 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑁 · 0)) |
| 200 | | iuneq1 5008 |
. . . . . . . . . . . . 13
⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘)) |
| 201 | | 0iun 5063 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅ |
| 202 | 200, 201 | eqtrdi 2793 |
. . . . . . . . . . . 12
⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∅) |
| 203 | 202 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) =
(♯‘∅)) |
| 204 | | hash0 14406 |
. . . . . . . . . . 11
⊢
(♯‘∅) = 0 |
| 205 | 203, 204 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = 0) |
| 206 | | sumeq1 15725 |
. . . . . . . . . . . 12
⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
| 207 | | sum0 15757 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈
∅ if(𝑘 ∈
ℙ, (1 / 𝑘), 0) =
0 |
| 208 | 206, 207 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0) |
| 209 | 208 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0)) |
| 210 | 205, 209 | breq12d 5156 |
. . . . . . . . 9
⊢ (((𝐾 + 1)...𝑁) = ∅ → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0))) |
| 211 | 199, 210 | syl5ibrcom 247 |
. . . . . . . 8
⊢ (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
| 212 | 196, 211 | sylbid 240 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
| 213 | | uztric 12902 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
| 214 | 59, 62, 213 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
| 215 | 189, 212,
214 | mpjaod 861 |
. . . . . 6
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
| 216 | | eqid 2737 |
. . . . . . . . . 10
⊢
(ℤ≥‘(𝐾 + 1)) =
(ℤ≥‘(𝐾 + 1)) |
| 217 | | eleq1w 2824 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
| 218 | | oveq2 7439 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
| 219 | 217, 218 | ifbieq1d 4550 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
| 220 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (1 /
𝑘) ∈
V |
| 221 | | c0ex 11255 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
| 222 | 220, 221 | ifex 4576 |
. . . . . . . . . . . 12
⊢ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V |
| 223 | 219, 186,
222 | fvmpt 7016 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
| 224 | 177, 223 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
| 225 | 181 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ) |
| 226 | 223, 225 | eqeltrd 2841 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ) |
| 227 | 226 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
| 228 | 72, 26, 227 | iserex 15693 |
. . . . . . . . . . 11
⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔
seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝
)) |
| 229 | 187, 228 | mpbid 232 |
. . . . . . . . . 10
⊢ (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ) |
| 230 | 216, 60, 224, 182, 229 | isumrecl 15801 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
| 231 | | halfre 12480 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℝ |
| 232 | 231 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
| 233 | | fzssuz 13605 |
. . . . . . . . . . 11
⊢ ((𝐾 + 1)...𝑁) ⊆
(ℤ≥‘(𝐾 + 1)) |
| 234 | 233 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ⊆
(ℤ≥‘(𝐾 + 1))) |
| 235 | | nnrp 13046 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 236 | 235 | rpreccld 13087 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
| 237 | 236 | rpge0d 13081 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 ≤ (1
/ 𝑘)) |
| 238 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ ((1 /
𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
| 239 | | breq2 5147 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑘 ∈ ℙ, (1 /
𝑘), 0) → (0 ≤ 0
↔ 0 ≤ if(𝑘 ∈
ℙ, (1 / 𝑘),
0))) |
| 240 | 238, 239 | ifboth 4565 |
. . . . . . . . . . . 12
⊢ ((0 ≤
(1 / 𝑘) ∧ 0 ≤ 0)
→ 0 ≤ if(𝑘 ∈
ℙ, (1 / 𝑘),
0)) |
| 241 | 237, 197,
240 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 0 ≤
if(𝑘 ∈ ℙ, (1 /
𝑘), 0)) |
| 242 | 177, 241 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
| 243 | 216, 60, 176, 234, 224, 182, 242, 229 | isumless 15881 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
| 244 | 184, 230,
232, 243, 188 | lelttrd 11419 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) |
| 245 | 1 | nngt0d 12315 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑁) |
| 246 | | ltmul2 12118 |
. . . . . . . . 9
⊢
((Σ𝑘 ∈
((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ ∧ (1 / 2) ∈
ℝ ∧ (𝑁 ∈
ℝ ∧ 0 < 𝑁))
→ (Σ𝑘 ∈
((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))) |
| 247 | 184, 232,
2, 245, 246 | syl112anc 1376 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))) |
| 248 | 244, 247 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))) |
| 249 | | 2cn 12341 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
| 250 | | 2ne0 12370 |
. . . . . . . . 9
⊢ 2 ≠
0 |
| 251 | | divrec 11938 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2))) |
| 252 | 249, 250,
251 | mp3an23 1455 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2))) |
| 253 | 23, 252 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2))) |
| 254 | 248, 253 | breqtrrd 5171 |
. . . . . 6
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2)) |
| 255 | 175, 185,
3, 215, 254 | lelttrd 11419 |
. . . . 5
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) < (𝑁 / 2)) |
| 256 | 175, 3, 12, 255 | ltadd2dd 11420 |
. . . 4
⊢ (𝜑 → ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) < ((♯‘𝑀) + (𝑁 / 2))) |
| 257 | 172, 256 | eqbrtrd 5165 |
. . 3
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2))) |
| 258 | 3, 12, 3 | ltadd1d 11856 |
. . 3
⊢ (𝜑 → ((𝑁 / 2) < (♯‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2)))) |
| 259 | 257, 258 | mpbird 257 |
. 2
⊢ (𝜑 → (𝑁 / 2) < (♯‘𝑀)) |
| 260 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2)) |
| 261 | 260 | breq1d 5153 |
. . . . . . 7
⊢ (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥)) |
| 262 | 261 | cbvrabv 3447 |
. . . . . 6
⊢ {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} |
| 263 | | breq2 5147 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛)) |
| 264 | 263 | rabbidv 3444 |
. . . . . 6
⊢ (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}) |
| 265 | 262, 264 | eqtrid 2789 |
. . . . 5
⊢ (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}) |
| 266 | 265 | supeq1d 9486 |
. . . 4
⊢ (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < )) |
| 267 | 266 | cbvmptv 5255 |
. . 3
⊢ (𝑥 ∈ ℕ ↦
sup({𝑘 ∈ ℕ
∣ (𝑘↑2) ∥
𝑥}, ℝ, < )) =
(𝑛 ∈ ℕ ↦
sup({𝑟 ∈ ℕ
∣ (𝑟↑2) ∥
𝑛}, ℝ, <
)) |
| 268 | 186, 14, 1, 5, 267 | prmreclem3 16956 |
. 2
⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁))) |
| 269 | 3, 12, 22, 259, 268 | ltletrd 11421 |
1
⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁))) |