Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾)) |
2 | 1 | iuneq1d 4545 |
. . . . . 6
⊢ (𝑥 = 𝐾 → ∪
𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) |
3 | 2 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 = 𝐾 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘))) |
4 | 1 | sumeq1d 14431 |
. . . . . 6
⊢ (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
5 | 4 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
6 | 3, 5 | breq12d 4666 |
. . . 4
⊢ (𝑥 = 𝐾 → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
7 | 6 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝐾 → ((𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) |
8 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗)) |
9 | 8 | iuneq1d 4545 |
. . . . . 6
⊢ (𝑥 = 𝑗 → ∪
𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) |
10 | 9 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 = 𝑗 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘))) |
11 | 8 | sumeq1d 14431 |
. . . . . 6
⊢ (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
12 | 11 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
13 | 10, 12 | breq12d 4666 |
. . . 4
⊢ (𝑥 = 𝑗 → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
14 | 13 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑗 → ((𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) |
15 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1))) |
16 | 15 | iuneq1d 4545 |
. . . . . 6
⊢ (𝑥 = (𝑗 + 1) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) |
17 | 16 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘))) |
18 | 15 | sumeq1d 14431 |
. . . . . 6
⊢ (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
19 | 18 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
20 | 17, 19 | breq12d 4666 |
. . . 4
⊢ (𝑥 = (𝑗 + 1) → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
21 | 20 | imbi2d 330 |
. . 3
⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) |
22 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁)) |
23 | 22 | iuneq1d 4545 |
. . . . . 6
⊢ (𝑥 = 𝑁 → ∪
𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
24 | 23 | fveq2d 6195 |
. . . . 5
⊢ (𝑥 = 𝑁 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
25 | 22 | sumeq1d 14431 |
. . . . . 6
⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
26 | 25 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
27 | 24, 26 | breq12d 4666 |
. . . 4
⊢ (𝑥 = 𝑁 → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
28 | 27 | imbi2d 330 |
. . 3
⊢ (𝑥 = 𝑁 → ((𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) |
29 | | 0le0 11110 |
. . . . . 6
⊢ 0 ≤
0 |
30 | | prmrec.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑁 ∈ ℕ) |
31 | 30 | nncnd 11036 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℂ) |
32 | 31 | mul01d 10235 |
. . . . . 6
⊢ (𝜑 → (𝑁 · 0) = 0) |
33 | 29, 32 | syl5breqr 4691 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝑁 · 0)) |
34 | | prmrec.2 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℕ) |
35 | 34 | nnred 11035 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℝ) |
36 | 35 | ltp1d 10954 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 < (𝐾 + 1)) |
37 | 34 | nnzd 11481 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℤ) |
38 | 37 | peano2zd 11485 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) |
39 | | fzn 12357 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅)) |
40 | 38, 37, 39 | syl2anc 693 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅)) |
41 | 36, 40 | mpbid 222 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐾 + 1)...𝐾) = ∅) |
42 | 41 | iuneq1d 4545 |
. . . . . . . 8
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘)) |
43 | | 0iun 4577 |
. . . . . . . 8
⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅ |
44 | 42, 43 | syl6eq 2672 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∅) |
45 | 44 | fveq2d 6195 |
. . . . . 6
⊢ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = (#‘∅)) |
46 | | hash0 13158 |
. . . . . 6
⊢
(#‘∅) = 0 |
47 | 45, 46 | syl6eq 2672 |
. . . . 5
⊢ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = 0) |
48 | 41 | sumeq1d 14431 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
49 | | sum0 14452 |
. . . . . . 7
⊢
Σ𝑘 ∈
∅ if(𝑘 ∈
ℙ, (1 / 𝑘), 0) =
0 |
50 | 48, 49 | syl6eq 2672 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0) |
51 | 50 | oveq2d 6666 |
. . . . 5
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0)) |
52 | 33, 47, 51 | 3brtr4d 4685 |
. . . 4
⊢ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
53 | 52 | a1i 11 |
. . 3
⊢ (𝐾 ∈ ℤ → (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
54 | | fzfi 12771 |
. . . . . . . . . . 11
⊢
(1...𝑁) ∈
Fin |
55 | | elfzuz 12338 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
56 | 34 | peano2nnd 11037 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐾 + 1) ∈ ℕ) |
57 | | eluznn 11758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ) |
58 | 56, 57 | sylan 488 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈
ℕ) |
59 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
60 | | breq1 4656 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) |
61 | 59, 60 | anbi12d 747 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛))) |
62 | 61 | rabbidv 3189 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
63 | | prmrec.7 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)}) |
64 | | ovex 6678 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(1...𝑁) ∈
V |
65 | 64 | rabex 4813 |
. . . . . . . . . . . . . . . . . . 19
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V |
66 | 62, 63, 65 | fvmpt 6282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
67 | 66 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
68 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁) |
69 | 67, 68 | syl6eqss 3655 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
70 | 58, 69 | syldan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
71 | 55, 70 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
72 | 71 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) |
73 | 72 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) |
74 | | iunss 4561 |
. . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) |
75 | 73, 74 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) |
76 | | ssfi 8180 |
. . . . . . . . . . 11
⊢
(((1...𝑁) ∈ Fin
∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin) |
77 | 54, 75, 76 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin) |
78 | | hashcl 13147 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈
ℕ0) |
79 | 77, 78 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈
ℕ0) |
80 | 79 | nn0red 11352 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℝ) |
81 | 30 | nnred 11035 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℝ) |
82 | 81 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈ ℝ) |
83 | | fzfid 12772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin) |
84 | 56 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈ ℕ) |
85 | 84, 55, 57 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ) |
86 | | nnrecre 11057 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
87 | | 0re 10040 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
88 | | ifcl 4130 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑘) ∈ ℝ ∧ 0
∈ ℝ) → if(𝑘
∈ ℙ, (1 / 𝑘), 0)
∈ ℝ) |
89 | 86, 87, 88 | sylancl 694 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
90 | 85, 89 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
91 | 83, 90 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
92 | 82, 91 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) |
93 | | prmnn 15388 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℙ →
(𝑗 + 1) ∈
ℕ) |
94 | | nnrecre 11057 |
. . . . . . . . . . . 12
⊢ ((𝑗 + 1) ∈ ℕ → (1 /
(𝑗 + 1)) ∈
ℝ) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑗 + 1) ∈ ℙ → (1 /
(𝑗 + 1)) ∈
ℝ) |
96 | 95 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈
ℝ) |
97 | | 0red 10041 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0
∈ ℝ) |
98 | 96, 97 | ifclda 4120 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈
ℝ) |
99 | 82, 98 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈
ℝ) |
100 | 80, 92, 99 | leadd1d 10621 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))) |
101 | | eluzp1p1 11713 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → (𝑗 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
102 | 101 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ∈
(ℤ≥‘(𝐾 + 1))) |
103 | | simpl 473 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝜑) |
104 | | elfzuz 12338 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
105 | 89 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ) |
106 | 58, 105 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ) |
107 | 103, 104,
106 | syl2an 494 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ) |
108 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ)) |
109 | | oveq2 6658 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1))) |
110 | 108, 109 | ifbieq1d 4109 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) |
111 | 102, 107,
110 | fsumm1 14480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) |
112 | | eluzelz 11697 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → 𝑗 ∈ ℤ) |
113 | 112 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ ℤ) |
114 | 113 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ ℂ) |
115 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
116 | | pncan 10287 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) |
117 | 114, 115,
116 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝑗 + 1) − 1) = 𝑗) |
118 | 117 | oveq2d 6666 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗)) |
119 | 118 | sumeq1d 14431 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
120 | 119 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) |
121 | 111, 120 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) |
122 | 121 | oveq2d 6666 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) |
123 | 31 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈ ℂ) |
124 | 91 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ) |
125 | 98 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈
ℂ) |
126 | 123, 124,
125 | adddid 10064 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) |
127 | 122, 126 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) |
128 | 127 | breq2d 4665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))) |
129 | 100, 128 | bitr4d 271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
130 | 104, 70 | sylan2 491 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
131 | 130 | ralrimiva 2966 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) |
132 | 131 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) |
133 | | iunss 4561 |
. . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) |
134 | 132, 133 | sylibr 224 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) |
135 | | ssfi 8180 |
. . . . . . . . . . 11
⊢
(((1...𝑁) ∈ Fin
∧ ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin) |
136 | 54, 134, 135 | sylancr 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin) |
137 | | hashcl 13147 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈
ℕ0) |
138 | 136, 137 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈
ℕ0) |
139 | 138 | nn0red 11352 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ) |
140 | | eluznn 11758 |
. . . . . . . . . . . . . . 15
⊢ ((𝐾 ∈ ℕ ∧ 𝑗 ∈
(ℤ≥‘𝐾)) → 𝑗 ∈ ℕ) |
141 | 34, 140 | sylan 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ ℕ) |
142 | 141 | peano2nnd 11037 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ∈ ℕ) |
143 | 69 | ralrimiva 2966 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁)) |
144 | 143 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁)) |
145 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑗 + 1) → (𝑊‘𝑘) = (𝑊‘(𝑗 + 1))) |
146 | 145 | sseq1d 3632 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑗 + 1) → ((𝑊‘𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))) |
147 | 146 | rspcv 3305 |
. . . . . . . . . . . . 13
⊢ ((𝑗 + 1) ∈ ℕ →
(∀𝑘 ∈ ℕ
(𝑊‘𝑘) ⊆ (1...𝑁) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))) |
148 | 142, 144,
147 | sylc 65 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) |
149 | | ssfi 8180 |
. . . . . . . . . . . 12
⊢
(((1...𝑁) ∈ Fin
∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin) |
150 | 54, 148, 149 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin) |
151 | | hashcl 13147 |
. . . . . . . . . . 11
⊢ ((𝑊‘(𝑗 + 1)) ∈ Fin → (#‘(𝑊‘(𝑗 + 1))) ∈
ℕ0) |
152 | 150, 151 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘(𝑊‘(𝑗 + 1))) ∈
ℕ0) |
153 | 152 | nn0red 11352 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘(𝑊‘(𝑗 + 1))) ∈ ℝ) |
154 | 80, 153 | readdcld 10069 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (#‘(𝑊‘(𝑗 + 1)))) ∈ ℝ) |
155 | 80, 99 | readdcld 10069 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈
ℝ) |
156 | 38 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝐾 + 1) ∈ ℤ) |
157 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ (ℤ≥‘𝐾)) |
158 | 34 | nncnd 11036 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ ℂ) |
159 | 158 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐾 ∈ ℂ) |
160 | | pncan 10287 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 + 1)
− 1) = 𝐾) |
161 | 159, 115,
160 | sylancl 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1) − 1) = 𝐾) |
162 | 161 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
(ℤ≥‘((𝐾 + 1) − 1)) =
(ℤ≥‘𝐾)) |
163 | 157, 162 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑗 ∈ (ℤ≥‘((𝐾 + 1) −
1))) |
164 | | fzsuc2 12398 |
. . . . . . . . . . . . 13
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈
(ℤ≥‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})) |
165 | 156, 163,
164 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})) |
166 | 165 | iuneq1d 4545 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘)) |
167 | | iunxun 4605 |
. . . . . . . . . . . 12
⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪
𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) |
168 | | ovex 6678 |
. . . . . . . . . . . . . 14
⊢ (𝑗 + 1) ∈ V |
169 | 168, 145 | iunxsn 4603 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘) = (𝑊‘(𝑗 + 1)) |
170 | 169 | uneq2i 3764 |
. . . . . . . . . . . 12
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪
𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))) |
171 | 167, 170 | eqtri 2644 |
. . . . . . . . . . 11
⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))) |
172 | 166, 171 | syl6eq 2672 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = (∪
𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) |
173 | 172 | fveq2d 6195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) = (#‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))))) |
174 | | hashun2 13172 |
. . . . . . . . . 10
⊢
((∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) → (#‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (#‘(𝑊‘(𝑗 + 1))))) |
175 | 77, 150, 174 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (#‘(𝑊‘(𝑗 + 1))))) |
176 | 173, 175 | eqbrtrd 4675 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (#‘(𝑊‘(𝑗 + 1))))) |
177 | 82, 142 | nndivred 11069 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ) |
178 | | flle 12600 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 / (𝑗 + 1)) ∈ ℝ →
(⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1))) |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1))) |
180 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ) |
181 | 180 | nncnd 11036 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ) |
182 | 181 | subid1d 10381 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛) |
183 | 182 | breq2d 4665 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛)) |
184 | 183 | rabbiia 3185 |
. . . . . . . . . . . . . . 15
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} |
185 | 184 | fveq2i 6194 |
. . . . . . . . . . . . . 14
⊢
(#‘{𝑛 ∈
(1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (#‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) |
186 | | 1zzd 11408 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 1 ∈
ℤ) |
187 | 30 | nnnn0d 11351 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
188 | | nn0uz 11722 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
189 | | 1m1e0 11089 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (1
− 1) = 0 |
190 | 189 | fveq2i 6194 |
. . . . . . . . . . . . . . . . . . 19
⊢
(ℤ≥‘(1 − 1)) =
(ℤ≥‘0) |
191 | 188, 190 | eqtr4i 2647 |
. . . . . . . . . . . . . . . . . 18
⊢
ℕ0 = (ℤ≥‘(1 −
1)) |
192 | 187, 191 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘(1
− 1))) |
193 | 192 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝑁 ∈ (ℤ≥‘(1
− 1))) |
194 | | 0zd 11389 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 0 ∈
ℤ) |
195 | 142, 186,
193, 194 | hashdvds 15480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) −
(⌊‘(((1 − 1) − 0) / (𝑗 + 1))))) |
196 | 123 | subid1d 10381 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 − 0) = 𝑁) |
197 | 196 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝑁 − 0) / (𝑗 + 1)) = (𝑁 / (𝑗 + 1))) |
198 | 197 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1)))) |
199 | 189 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((1
− 1) − 0) = (0 − 0) |
200 | | 0m0e0 11130 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (0
− 0) = 0 |
201 | 199, 200 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
− 1) − 0) = 0 |
202 | 201 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((1
− 1) − 0) / (𝑗
+ 1)) = (0 / (𝑗 +
1)) |
203 | 142 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ∈ ℂ) |
204 | 142 | nnne0d 11065 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑗 + 1) ≠ 0) |
205 | 203, 204 | div0d 10800 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (0 / (𝑗 + 1)) = 0) |
206 | 202, 205 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (((1 − 1)
− 0) / (𝑗 + 1)) =
0) |
207 | 206 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(((1
− 1) − 0) / (𝑗
+ 1))) = (⌊‘0)) |
208 | | 0z 11388 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℤ |
209 | | flid 12609 |
. . . . . . . . . . . . . . . . . 18
⊢ (0 ∈
ℤ → (⌊‘0) = 0) |
210 | 208, 209 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢
(⌊‘0) = 0 |
211 | 207, 210 | syl6eq 2672 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(((1
− 1) − 0) / (𝑗
+ 1))) = 0) |
212 | 198, 211 | oveq12d 6668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) →
((⌊‘((𝑁 −
0) / (𝑗 + 1))) −
(⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0)) |
213 | 177 | flcld 12599 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ) |
214 | 213 | zcnd 11483 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ) |
215 | 214 | subid1d 10381 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1)))) |
216 | 195, 212,
215 | 3eqtrd 2660 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1)))) |
217 | 185, 216 | syl5eqr 2670 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1)))) |
218 | 123, 203,
204 | divrecd 10804 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1)))) |
219 | 218 | eqcomd 2628 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1))) |
220 | 179, 217,
219 | 3brtr4d 4685 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1)))) |
221 | 220 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (#‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1)))) |
222 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ)) |
223 | | breq1 4656 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∥ 𝑛 ↔ (𝑗 + 1) ∥ 𝑛)) |
224 | 222, 223 | anbi12d 747 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = (𝑗 + 1) → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))) |
225 | 224 | rabbidv 3189 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = (𝑗 + 1) → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) |
226 | 64 | rabex 4813 |
. . . . . . . . . . . . . . . 16
⊢ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V |
227 | 225, 63, 226 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
⊢ ((𝑗 + 1) ∈ ℕ →
(𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) |
228 | 142, 227 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) |
229 | 228 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) |
230 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑗 + 1) ∈
ℙ) |
231 | 230 | biantrurd 529 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → ((𝑗 + 1) ∥ 𝑛 ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))) |
232 | 231 | rabbidv 3189 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)}) |
233 | 229, 232 | eqtr4d 2659 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) |
234 | 233 | fveq2d 6195 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (#‘(𝑊‘(𝑗 + 1))) = (#‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})) |
235 | | iftrue 4092 |
. . . . . . . . . . . . 13
⊢ ((𝑗 + 1) ∈ ℙ →
if((𝑗 + 1) ∈ ℙ,
(1 / (𝑗 + 1)), 0) = (1 /
(𝑗 + 1))) |
236 | 235 | adantl 482 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → if((𝑗 + 1) ∈ ℙ, (1 /
(𝑗 + 1)), 0) = (1 / (𝑗 + 1))) |
237 | 236 | oveq2d 6666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1)))) |
238 | 221, 234,
237 | 3brtr4d 4685 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (#‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) |
239 | 29 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0
≤ 0) |
240 | | simpl 473 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑗 + 1) ∈ ℙ ∧
(𝑗 + 1) ∥ 𝑛) → (𝑗 + 1) ∈ ℙ) |
241 | 240 | con3i 150 |
. . . . . . . . . . . . . . . 16
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ ¬ ((𝑗 + 1)
∈ ℙ ∧ (𝑗 +
1) ∥ 𝑛)) |
242 | 241 | ralrimivw 2967 |
. . . . . . . . . . . . . . 15
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ ∀𝑛 ∈
(1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧
(𝑗 + 1) ∥ 𝑛)) |
243 | | rabeq0 3957 |
. . . . . . . . . . . . . . 15
⊢ ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)) |
244 | 242, 243 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅) |
245 | 228, 244 | sylan9eq 2676 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(𝑊‘(𝑗 + 1)) =
∅) |
246 | 245 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(#‘(𝑊‘(𝑗 + 1))) =
(#‘∅)) |
247 | 246, 46 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(#‘(𝑊‘(𝑗 + 1))) = 0) |
248 | | iffalse 4095 |
. . . . . . . . . . . . 13
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ if((𝑗 + 1) ∈
ℙ, (1 / (𝑗 + 1)), 0)
= 0) |
249 | 248 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (¬
(𝑗 + 1) ∈ ℙ
→ (𝑁 ·
if((𝑗 + 1) ∈ ℙ,
(1 / (𝑗 + 1)), 0)) = (𝑁 · 0)) |
250 | 32 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · 0) = 0) |
251 | 249, 250 | sylan9eqr 2678 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(𝑁 · if((𝑗 + 1) ∈ ℙ, (1 /
(𝑗 + 1)), 0)) =
0) |
252 | 239, 247,
251 | 3brtr4d 4685 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) →
(#‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) |
253 | 238, 252 | pm2.61dan 832 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) |
254 | 153, 99, 80, 253 | leadd2dd 10642 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (#‘(𝑊‘(𝑗 + 1)))) ≤ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) |
255 | 139, 154,
155, 176, 254 | letrd 10194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))) |
256 | | fzfid 12772 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) ∈ Fin) |
257 | 58, 89 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
258 | 103, 104,
257 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
259 | 256, 258 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
260 | 82, 259 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) |
261 | | letr 10131 |
. . . . . . . 8
⊢
(((#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ ∧ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ
∧ (𝑁 ·
Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) →
(((#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∧
((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
262 | 139, 155,
260, 261 | syl3anc 1326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (((#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∧
((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
263 | 255, 262 | mpand 711 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → (((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
264 | 129, 263 | sylbid 230 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
265 | 264 | expcom 451 |
. . . 4
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → (𝜑 → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) |
266 | 265 | a2d 29 |
. . 3
⊢ (𝑗 ∈
(ℤ≥‘𝐾) → ((𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))) |
267 | 7, 14, 21, 28, 53, 266 | uzind4 11746 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
268 | 267 | com12 32 |
1
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |