Step | Hyp | Ref
| Expression |
1 | | prmrec.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnred 11641 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℝ) |
3 | 2 | rehalfcld 11872 |
. 2
⊢ (𝜑 → (𝑁 / 2) ∈ ℝ) |
4 | | fzfi 13328 |
. . . . . 6
⊢
(1...𝑁) ∈
Fin |
5 | | prmrec.4 |
. . . . . . 7
⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} |
6 | 5 | ssrab3 4054 |
. . . . . 6
⊢ 𝑀 ⊆ (1...𝑁) |
7 | | ssfi 8726 |
. . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin) |
8 | 4, 6, 7 | mp2an 688 |
. . . . 5
⊢ 𝑀 ∈ Fin |
9 | | hashcl 13705 |
. . . . 5
⊢ (𝑀 ∈ Fin →
(♯‘𝑀) ∈
ℕ0) |
10 | 8, 9 | ax-mp 5 |
. . . 4
⊢
(♯‘𝑀)
∈ ℕ0 |
11 | 10 | nn0rei 11896 |
. . 3
⊢
(♯‘𝑀)
∈ ℝ |
12 | 11 | a1i 11 |
. 2
⊢ (𝜑 → (♯‘𝑀) ∈
ℝ) |
13 | | 2nn 11698 |
. . . . 5
⊢ 2 ∈
ℕ |
14 | | prmrec.2 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
15 | 14 | nnnn0d 11943 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
16 | | nnexpcl 13430 |
. . . . 5
⊢ ((2
∈ ℕ ∧ 𝐾
∈ ℕ0) → (2↑𝐾) ∈ ℕ) |
17 | 13, 15, 16 | sylancr 587 |
. . . 4
⊢ (𝜑 → (2↑𝐾) ∈ ℕ) |
18 | 17 | nnred 11641 |
. . 3
⊢ (𝜑 → (2↑𝐾) ∈ ℝ) |
19 | 1 | nnrpd 12417 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
20 | 19 | rpsqrtcld 14759 |
. . . 4
⊢ (𝜑 → (√‘𝑁) ∈
ℝ+) |
21 | 20 | rpred 12419 |
. . 3
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) |
22 | 18, 21 | remulcld 10659 |
. 2
⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ) |
23 | 2 | recnd 10657 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) |
24 | 23 | 2halvesd 11871 |
. . . . 5
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁) |
25 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ⊆ (1...𝑁)) |
26 | 14 | peano2nnd 11643 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 1) ∈ ℕ) |
27 | | elfzuz 12892 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
28 | | eluznn 12306 |
. . . . . . . . . . . . 13
⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ) |
29 | 26, 27, 28 | syl2an 595 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ) |
30 | | eleq1w 2892 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
31 | | breq1 5060 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) |
32 | 30, 31 | anbi12d 630 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛))) |
33 | 32 | rabbidv 3478 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
34 | | prmrec.7 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)}) |
35 | | ovex 7178 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑁) ∈
V |
36 | 35 | rabex 5226 |
. . . . . . . . . . . . . . 15
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V |
37 | 33, 34, 36 | fvmpt 6761 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
38 | 37 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
39 | | ssrab2 4053 |
. . . . . . . . . . . . 13
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁) |
40 | 38, 39 | eqsstrdi 4018 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
41 | 29, 40 | syldan 591 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
42 | 41 | ralrimiva 3179 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
43 | | iunss 4960 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
44 | 42, 43 | sylibr 235 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
45 | 25, 44 | unssd 4159 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ⊆ (1...𝑁)) |
46 | | breq1 5060 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑛 ↔ 𝑞 ∥ 𝑛)) |
47 | 46 | notbid 319 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑞 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑛)) |
48 | 47 | cbvralvw 3447 |
. . . . . . . . . . . . . 14
⊢
(∀𝑝 ∈
(ℙ ∖ (1...𝐾))
¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖
(1...𝐾)) ¬ 𝑞 ∥ 𝑛) |
49 | | breq2 5061 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → (𝑞 ∥ 𝑛 ↔ 𝑞 ∥ 𝑥)) |
50 | 49 | notbid 319 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → (¬ 𝑞 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑥)) |
51 | 50 | ralbidv 3194 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
52 | 48, 51 | syl5bb 284 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
53 | 52, 5 | elrab2 3680 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
54 | | elun1 4149 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝑀 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
55 | 53, 54 | sylbir 236 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
56 | 55 | ex 413 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
57 | 56 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
58 | | dfrex2 3236 |
. . . . . . . . . 10
⊢
(∃𝑞 ∈
(ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) |
59 | | eldifn 4101 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑞 ∈ (ℙ ∖
(1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾)) |
60 | 59 | ad2antrl 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ∈ (1...𝐾)) |
61 | | eldifi 4100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑞 ∈ (ℙ ∖
(1...𝐾)) → 𝑞 ∈
ℙ) |
62 | 61 | ad2antrl 724 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℙ) |
63 | | prmnn 16006 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℕ) |
65 | | nnuz 12269 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℕ =
(ℤ≥‘1) |
66 | 64, 65 | eleqtrdi 2920 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈
(ℤ≥‘1)) |
67 | 14 | nnzd 12074 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈ ℤ) |
68 | 67 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℤ) |
69 | | elfz5 12888 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈
(ℤ≥‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾)) |
70 | 66, 68, 69 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾)) |
71 | 60, 70 | mtbid 325 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ≤ 𝐾) |
72 | 14 | nnred 11641 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈ ℝ) |
73 | 72 | ad2antrr 722 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℝ) |
74 | 64 | nnred 11641 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℝ) |
75 | 73, 74 | ltnled 10775 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞 ≤ 𝐾)) |
76 | 71, 75 | mpbird 258 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 < 𝑞) |
77 | | prmz 16007 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
78 | 62, 77 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℤ) |
79 | | zltp1le 12020 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞)) |
80 | 68, 78, 79 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞)) |
81 | 76, 80 | mpbid 233 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ≤ 𝑞) |
82 | | elfznn 12924 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
83 | 82 | ad2antlr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℕ) |
84 | 83 | nnred 11641 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℝ) |
85 | 2 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℝ) |
86 | | simprr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∥ 𝑥) |
87 | | dvdsle 15648 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
88 | 78, 83, 87 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
89 | 86, 88 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑥) |
90 | | elfzle2 12899 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁) |
91 | 90 | ad2antlr 723 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ≤ 𝑁) |
92 | 74, 84, 85, 89, 91 | letrd 10785 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑁) |
93 | 67 | peano2zd 12078 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) |
94 | 93 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ∈ ℤ) |
95 | 1 | nnzd 12074 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈ ℤ) |
96 | 95 | ad2antrr 722 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℤ) |
97 | | elfz 12886 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞 ∧ 𝑞 ≤ 𝑁))) |
98 | 78, 94, 96, 97 | syl3anc 1363 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞 ∧ 𝑞 ≤ 𝑁))) |
99 | 81, 92, 98 | mpbir2and 709 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁)) |
100 | 49 | anbi2d 628 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥))) |
101 | | simplr 765 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (1...𝑁)) |
102 | 62, 86 | jca 512 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥)) |
103 | 100, 101,
102 | elrabd 3679 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
104 | | eleq1w 2892 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ)) |
105 | 104, 46 | anbi12d 630 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛))) |
106 | 105 | rabbidv 3478 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
107 | 35 | rabex 5226 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)} ∈ V |
108 | 106, 34, 107 | fvmpt 6761 |
. . . . . . . . . . . . . . 15
⊢ (𝑞 ∈ ℕ → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
109 | 64, 108 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
110 | 103, 109 | eleqtrrd 2913 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑊‘𝑞)) |
111 | | fveq2 6663 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝑞 → (𝑊‘𝑘) = (𝑊‘𝑞)) |
112 | 111 | eliuni 4916 |
. . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊‘𝑞)) → 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
113 | 99, 110, 112 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
114 | | elun2 4150 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
116 | 115 | rexlimdvaa 3282 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
117 | 58, 116 | syl5bir 244 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
118 | 57, 117 | pm2.61d 180 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
119 | 45, 118 | eqelssd 3985 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (1...𝑁)) |
120 | 119 | fveq2d 6667 |
. . . . . 6
⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = (♯‘(1...𝑁))) |
121 | 1 | nnnn0d 11943 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
122 | | hashfz1 13694 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (♯‘(1...𝑁)) = 𝑁) |
123 | 121, 122 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁) |
124 | 120, 123 | eqtr2d 2854 |
. . . . 5
⊢ (𝜑 → 𝑁 = (♯‘(𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
125 | 8 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ Fin) |
126 | | ssfi 8726 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin) |
127 | 4, 44, 126 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin) |
128 | | breq1 5060 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑥 ↔ 𝑘 ∥ 𝑥)) |
129 | 128 | notbid 319 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑘 → (¬ 𝑝 ∥ 𝑥 ↔ ¬ 𝑘 ∥ 𝑥)) |
130 | | breq2 5061 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑥 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑥)) |
131 | 130 | notbid 319 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑥 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑥)) |
132 | 131 | ralbidv 3194 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)) |
133 | 132, 5 | elrab2 3680 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)) |
134 | 133 | simprbi 497 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥) |
135 | 134 | ad2antlr 723 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖
(1...𝐾)) ¬ 𝑝 ∥ 𝑥) |
136 | | simprr 769 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ) |
137 | | noel 4293 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
𝑘 ∈
∅ |
138 | | simprl 767 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁)) |
139 | 138 | biantrud 532 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))) |
140 | | elin 4166 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))) |
141 | 139, 140 | syl6bbr 290 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)))) |
142 | 72 | ltp1d 11558 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐾 < (𝐾 + 1)) |
143 | | fzdisj 12922 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
144 | 142, 143 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
145 | 144 | ad2antrr 722 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
146 | 145 | eleq2d 2895 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅)) |
147 | 141, 146 | bitrd 280 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅)) |
148 | 137, 147 | mtbiri 328 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾)) |
149 | 136, 148 | eldifd 3944 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾))) |
150 | 129, 135,
149 | rspcdva 3622 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∥ 𝑥) |
151 | 150 | expr 457 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥)) |
152 | | imnan 400 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℙ → ¬
𝑘 ∥ 𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
153 | 151, 152 | sylib 219 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
154 | 29 | adantlr 711 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ) |
155 | 154, 37 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
156 | 155 | eleq2d 2895 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})) |
157 | | breq2 5061 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑥 → (𝑘 ∥ 𝑛 ↔ 𝑘 ∥ 𝑥)) |
158 | 157 | anbi2d 628 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
159 | 158 | elrab 3677 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
160 | 159 | simprbi 497 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
161 | 156, 160 | syl6bi 254 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
162 | 153, 161 | mtod 199 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊‘𝑘)) |
163 | 162 | nrexdv 3267 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘)) |
164 | | eliun 4914 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘)) |
165 | 163, 164 | sylnibr 330 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
166 | 165 | ex 413 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
167 | | imnan 400 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
168 | 166, 167 | sylib 219 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
169 | | elin 4166 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
170 | 168, 169 | sylnibr 330 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑥 ∈ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
171 | 170 | eq0rdv 4354 |
. . . . . 6
⊢ (𝜑 → (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) |
172 | | hashun 13731 |
. . . . . 6
⊢ ((𝑀 ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin ∧ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
173 | 125, 127,
171, 172 | syl3anc 1363 |
. . . . 5
⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
174 | 24, 124, 173 | 3eqtrd 2857 |
. . . 4
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
175 | | hashcl 13705 |
. . . . . . 7
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈
ℕ0) |
176 | 127, 175 | syl 17 |
. . . . . 6
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈
ℕ0) |
177 | 176 | nn0red 11944 |
. . . . 5
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℝ) |
178 | | fzfid 13329 |
. . . . . . . 8
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin) |
179 | 26, 28 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈
ℕ) |
180 | | nnrecre 11667 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
181 | | 0re 10631 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
182 | | ifcl 4507 |
. . . . . . . . . . 11
⊢ (((1 /
𝑘) ∈ ℝ ∧ 0
∈ ℝ) → if(𝑘
∈ ℙ, (1 / 𝑘), 0)
∈ ℝ) |
183 | 180, 181,
182 | sylancl 586 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
184 | 179, 183 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
185 | 27, 184 | sylan2 592 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
186 | 178, 185 | fsumrecl 15079 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
187 | 2, 186 | remulcld 10659 |
. . . . . 6
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) |
188 | | prmrec.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) |
189 | | prmrec.5 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝
) |
190 | | prmrec.6 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) |
191 | 188, 14, 1, 5, 189, 190, 34 | prmreclem4 16243 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
192 | | eluz 12245 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈
(ℤ≥‘𝑁) ↔ 𝑁 ≤ 𝐾)) |
193 | 95, 67, 192 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) ↔ 𝑁 ≤ 𝐾)) |
194 | | nnleltp1 12025 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1))) |
195 | 1, 14, 194 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1))) |
196 | | fzn 12911 |
. . . . . . . . . 10
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
197 | 93, 95, 196 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
198 | 193, 195,
197 | 3bitrd 306 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
199 | | 0le0 11726 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
200 | 23 | mul01d 10827 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · 0) = 0) |
201 | 199, 200 | breqtrrid 5095 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑁 · 0)) |
202 | | iuneq1 4926 |
. . . . . . . . . . . . 13
⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘)) |
203 | | 0iun 4977 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅ |
204 | 202, 203 | syl6eq 2869 |
. . . . . . . . . . . 12
⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∅) |
205 | 204 | fveq2d 6667 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) =
(♯‘∅)) |
206 | | hash0 13716 |
. . . . . . . . . . 11
⊢
(♯‘∅) = 0 |
207 | 205, 206 | syl6eq 2869 |
. . . . . . . . . 10
⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = 0) |
208 | | sumeq1 15033 |
. . . . . . . . . . . 12
⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
209 | | sum0 15066 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈
∅ if(𝑘 ∈
ℙ, (1 / 𝑘), 0) =
0 |
210 | 208, 209 | syl6eq 2869 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0) |
211 | 210 | oveq2d 7161 |
. . . . . . . . . 10
⊢ (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0)) |
212 | 207, 211 | breq12d 5070 |
. . . . . . . . 9
⊢ (((𝐾 + 1)...𝑁) = ∅ → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0))) |
213 | 201, 212 | syl5ibrcom 248 |
. . . . . . . 8
⊢ (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
214 | 198, 213 | sylbid 241 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
215 | | uztric 12254 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
216 | 67, 95, 215 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
217 | 191, 214,
216 | mpjaod 854 |
. . . . . 6
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
218 | | eqid 2818 |
. . . . . . . . . 10
⊢
(ℤ≥‘(𝐾 + 1)) =
(ℤ≥‘(𝐾 + 1)) |
219 | | eleq1w 2892 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
220 | | oveq2 7153 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
221 | 219, 220 | ifbieq1d 4486 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
222 | | ovex 7178 |
. . . . . . . . . . . . 13
⊢ (1 /
𝑘) ∈
V |
223 | | c0ex 10623 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
224 | 222, 223 | ifex 4511 |
. . . . . . . . . . . 12
⊢ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V |
225 | 221, 188,
224 | fvmpt 6761 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
226 | 179, 225 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
227 | 183 | recnd 10657 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ) |
228 | 225, 227 | eqeltrd 2910 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ) |
229 | 228 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
230 | 65, 26, 229 | iserex 15001 |
. . . . . . . . . . 11
⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔
seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝
)) |
231 | 189, 230 | mpbid 233 |
. . . . . . . . . 10
⊢ (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ) |
232 | 218, 93, 226, 184, 231 | isumrecl 15108 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
233 | | halfre 11839 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℝ |
234 | 233 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
235 | | fzssuz 12936 |
. . . . . . . . . . 11
⊢ ((𝐾 + 1)...𝑁) ⊆
(ℤ≥‘(𝐾 + 1)) |
236 | 235 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ⊆
(ℤ≥‘(𝐾 + 1))) |
237 | | nnrp 12388 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
238 | 237 | rpreccld 12429 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
239 | 238 | rpge0d 12423 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 ≤ (1
/ 𝑘)) |
240 | | breq2 5061 |
. . . . . . . . . . . . 13
⊢ ((1 /
𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
241 | | breq2 5061 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑘 ∈ ℙ, (1 /
𝑘), 0) → (0 ≤ 0
↔ 0 ≤ if(𝑘 ∈
ℙ, (1 / 𝑘),
0))) |
242 | 240, 241 | ifboth 4501 |
. . . . . . . . . . . 12
⊢ ((0 ≤
(1 / 𝑘) ∧ 0 ≤ 0)
→ 0 ≤ if(𝑘 ∈
ℙ, (1 / 𝑘),
0)) |
243 | 239, 199,
242 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 0 ≤
if(𝑘 ∈ ℙ, (1 /
𝑘), 0)) |
244 | 179, 243 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
245 | 218, 93, 178, 236, 226, 184, 244, 231 | isumless 15188 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
246 | 186, 232,
234, 245, 190 | lelttrd 10786 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) |
247 | 1 | nngt0d 11674 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑁) |
248 | | ltmul2 11479 |
. . . . . . . . 9
⊢
((Σ𝑘 ∈
((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ ∧ (1 / 2) ∈
ℝ ∧ (𝑁 ∈
ℝ ∧ 0 < 𝑁))
→ (Σ𝑘 ∈
((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))) |
249 | 186, 234,
2, 247, 248 | syl112anc 1366 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))) |
250 | 246, 249 | mpbid 233 |
. . . . . . 7
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))) |
251 | | 2cn 11700 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
252 | | 2ne0 11729 |
. . . . . . . . 9
⊢ 2 ≠
0 |
253 | | divrec 11302 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2))) |
254 | 251, 252,
253 | mp3an23 1444 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2))) |
255 | 23, 254 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2))) |
256 | 250, 255 | breqtrrd 5085 |
. . . . . 6
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2)) |
257 | 177, 187,
3, 217, 256 | lelttrd 10786 |
. . . . 5
⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) < (𝑁 / 2)) |
258 | 177, 3, 12, 257 | ltadd2dd 10787 |
. . . 4
⊢ (𝜑 → ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) < ((♯‘𝑀) + (𝑁 / 2))) |
259 | 174, 258 | eqbrtrd 5079 |
. . 3
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2))) |
260 | 3, 12, 3 | ltadd1d 11221 |
. . 3
⊢ (𝜑 → ((𝑁 / 2) < (♯‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2)))) |
261 | 259, 260 | mpbird 258 |
. 2
⊢ (𝜑 → (𝑁 / 2) < (♯‘𝑀)) |
262 | | oveq1 7152 |
. . . . . . . 8
⊢ (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2)) |
263 | 262 | breq1d 5067 |
. . . . . . 7
⊢ (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥)) |
264 | 263 | cbvrabv 3489 |
. . . . . 6
⊢ {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} |
265 | | breq2 5061 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛)) |
266 | 265 | rabbidv 3478 |
. . . . . 6
⊢ (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}) |
267 | 264, 266 | syl5eq 2865 |
. . . . 5
⊢ (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}) |
268 | 267 | supeq1d 8898 |
. . . 4
⊢ (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < )) |
269 | 268 | cbvmptv 5160 |
. . 3
⊢ (𝑥 ∈ ℕ ↦
sup({𝑘 ∈ ℕ
∣ (𝑘↑2) ∥
𝑥}, ℝ, < )) =
(𝑛 ∈ ℕ ↦
sup({𝑟 ∈ ℕ
∣ (𝑟↑2) ∥
𝑛}, ℝ, <
)) |
270 | 188, 14, 1, 5, 269 | prmreclem3 16242 |
. 2
⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁))) |
271 | 3, 12, 22, 261, 270 | ltletrd 10788 |
1
⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁))) |