Step | Hyp | Ref
| Expression |
1 | | mertenslemub.elt |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑇) |
2 | | eqeq1 2177 |
. . . . . . 7
⊢ (𝑧 = 𝑋 → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
3 | 2 | rexbidv 2471 |
. . . . . 6
⊢ (𝑧 = 𝑋 → (∃𝑛 ∈ (0...(𝑆 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑆 − 1))𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
4 | | mertenslemub.t |
. . . . . 6
⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑆 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} |
5 | 3, 4 | elab2g 2877 |
. . . . 5
⊢ (𝑋 ∈ 𝑇 → (𝑋 ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑆 − 1))𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
6 | 1, 5 | syl 14 |
. . . 4
⊢ (𝜑 → (𝑋 ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑆 − 1))𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
7 | 1, 6 | mpbid 146 |
. . 3
⊢ (𝜑 → ∃𝑛 ∈ (0...(𝑆 − 1))𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
8 | | fvoveq1 5876 |
. . . . . . 7
⊢ (𝑛 = 𝑎 → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘(𝑎 + 1))) |
9 | 8 | sumeq1d 11329 |
. . . . . 6
⊢ (𝑛 = 𝑎 → Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)) |
10 | 9 | fveq2d 5500 |
. . . . 5
⊢ (𝑛 = 𝑎 → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘))) |
11 | 10 | eqeq2d 2182 |
. . . 4
⊢ (𝑛 = 𝑎 → (𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) |
12 | 11 | cbvrexv 2697 |
. . 3
⊢
(∃𝑛 ∈
(0...(𝑆 − 1))𝑋 = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑎 ∈ (0...(𝑆 − 1))𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘))) |
13 | 7, 12 | sylib 121 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ (0...(𝑆 − 1))𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘))) |
14 | | simprr 527 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘))) |
15 | | 0zd 9224 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → 0 ∈
ℤ) |
16 | | mertenslemub.s |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ ℕ) |
17 | 16 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → 𝑆 ∈ ℕ) |
18 | 17 | nnzd 9333 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → 𝑆 ∈ ℤ) |
19 | | 1zzd 9239 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → 1 ∈
ℤ) |
20 | 18, 19 | zsubcld 9339 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → (𝑆 − 1) ∈ ℤ) |
21 | 15, 20 | fzfigd 10387 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → (0...(𝑆 − 1)) ∈ Fin) |
22 | | eqid 2170 |
. . . . . . 7
⊢
(ℤ≥‘(𝑛 + 1)) = (ℤ≥‘(𝑛 + 1)) |
23 | | elfzelz 9981 |
. . . . . . . . 9
⊢ (𝑛 ∈ (0...(𝑆 − 1)) → 𝑛 ∈ ℤ) |
24 | 23 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → 𝑛 ∈ ℤ) |
25 | 24 | peano2zd 9337 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → (𝑛 + 1) ∈ ℤ) |
26 | | eqidd 2171 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
27 | | simpll 524 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝜑) |
28 | | elfznn0 10070 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (0...(𝑆 − 1)) → 𝑛 ∈ ℕ0) |
29 | 28 | ad2antlr 486 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑛 ∈
ℕ0) |
30 | | peano2nn0 9175 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ0) |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝑛 + 1) ∈
ℕ0) |
32 | | eluznn0 9558 |
. . . . . . . . 9
⊢ (((𝑛 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑘 ∈ ℕ0) |
33 | 31, 32 | sylancom 418 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑘 ∈
ℕ0) |
34 | | mertenslemub.gb |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) |
35 | | mertenslemub.b |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) |
36 | 34, 35 | eqeltrd 2247 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
37 | 27, 33, 36 | syl2anc 409 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) ∈ ℂ) |
38 | | mertenslemub.cvg |
. . . . . . . . 9
⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝
) |
39 | 38 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → seq0( + , 𝐺) ∈ dom ⇝
) |
40 | | nn0uz 9521 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
41 | 28 | adantl 275 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → 𝑛 ∈ ℕ0) |
42 | 41, 30 | syl 14 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → (𝑛 + 1) ∈
ℕ0) |
43 | 36 | adantlr 474 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
44 | 40, 42, 43 | iserex 11302 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝
)) |
45 | 39, 44 | mpbid 146 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ ) |
46 | 22, 25, 26, 37, 45 | isumcl 11388 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (0...(𝑆 − 1))) → Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) ∈ ℂ) |
47 | 46 | adantlr 474 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) ∧ 𝑛 ∈ (0...(𝑆 − 1))) → Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) ∈ ℂ) |
48 | 47 | abscld 11145 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) ∧ 𝑛 ∈ (0...(𝑆 − 1))) → (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ∈ ℝ) |
49 | 47 | absge0d 11148 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) ∧ 𝑛 ∈ (0...(𝑆 − 1))) → 0 ≤
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
50 | | simprl 526 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → 𝑎 ∈ (0...(𝑆 − 1))) |
51 | 21, 48, 49, 10, 50 | fsumge1 11424 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)) ≤ Σ𝑛 ∈ (0...(𝑆 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
52 | 14, 51 | eqbrtrd 4011 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ (0...(𝑆 − 1)) ∧ 𝑋 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑎 + 1))(𝐺‘𝑘)))) → 𝑋 ≤ Σ𝑛 ∈ (0...(𝑆 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
53 | 13, 52 | rexlimddv 2592 |
1
⊢ (𝜑 → 𝑋 ≤ Σ𝑛 ∈ (0...(𝑆 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |