Proof of Theorem mertenslem1
Step | Hyp | Ref
| Expression |
1 | | mertens.12 |
. . . . . . 7
⊢ (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) |
2 | 1 | simpld 474 |
. . . . . 6
⊢ (𝜑 → 𝜓) |
3 | | mertens.11 |
. . . . . 6
⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
4 | 2, 3 | sylib 207 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
5 | 4 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝑠 ∈ ℕ) |
6 | 5 | nnnn0d 11228 |
. . 3
⊢ (𝜑 → 𝑠 ∈ ℕ0) |
7 | 1 | simprd 478 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
8 | 7 | simpld 474 |
. . 3
⊢ (𝜑 → 𝑡 ∈ ℕ0) |
9 | 6, 8 | nn0addcld 11232 |
. 2
⊢ (𝜑 → (𝑠 + 𝑡) ∈
ℕ0) |
10 | | fzfid 12634 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin) |
11 | | simpl 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝜑) |
12 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0) |
13 | | mertens.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈
ℂ) |
14 | 11, 12, 13 | syl2an 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ) |
15 | | eqid 2610 |
. . . . . . . 8
⊢
(ℤ≥‘((𝑚 − 𝑗) + 1)) =
(ℤ≥‘((𝑚 − 𝑗) + 1)) |
16 | | fznn0sub 12244 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈
ℕ0) |
17 | 16 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈
ℕ0) |
18 | | peano2nn0 11210 |
. . . . . . . . . 10
⊢ ((𝑚 − 𝑗) ∈ ℕ0 → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
20 | 19 | nn0zd 11356 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ) |
21 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) |
22 | | eluznn0 11633 |
. . . . . . . . . 10
⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ0 ∧ 𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
23 | 19, 22 | sylan 487 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
24 | | mertens.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) |
25 | 21, 23, 24 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) |
26 | | mertens.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) |
27 | 21, 23, 26 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ) |
28 | | mertens.8 |
. . . . . . . . . 10
⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝
) |
29 | 28 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ ) |
30 | | nn0uz 11598 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
31 | | simpll 786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑) |
32 | 24, 26 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
33 | 31, 32 | sylan 487 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
34 | 30, 19, 33 | iserex 14235 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )) |
35 | 29, 34 | mpbid 221 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ) |
36 | 15, 20, 25, 27, 35 | isumcl 14334 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ) |
37 | 14, 36 | mulcld 9939 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ) |
38 | 10, 37 | fsumcl 14311 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ) |
39 | 38 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
40 | 37 | abscld 14023 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
41 | 10, 40 | fsumrecl 14312 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
42 | | mertens.9 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
43 | 42 | rpred 11748 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) |
44 | 43 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ) |
45 | 10, 37 | fsumabs 14374 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
46 | | fzfid 12634 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin) |
47 | 6 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ0) |
48 | 47 | nn0ge0d 11231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠) |
49 | | eluzelz 11573 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ) |
50 | 49 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ) |
51 | 50 | zred 11358 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ) |
52 | 47 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ) |
53 | 51, 52 | subge02d 10498 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚)) |
54 | 48, 53 | mpbid 221 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚) |
55 | 47, 30 | syl6eleq 2698 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈
(ℤ≥‘0)) |
56 | 5 | nnzd 11357 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑠 ∈ ℤ) |
57 | | uzid 11578 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℤ → 𝑠 ∈
(ℤ≥‘𝑠)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑠 ∈ (ℤ≥‘𝑠)) |
59 | | uzaddcl 11620 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈
(ℤ≥‘𝑠) ∧ 𝑡 ∈ ℕ0) → (𝑠 + 𝑡) ∈ (ℤ≥‘𝑠)) |
60 | 58, 8, 59 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ≥‘𝑠)) |
61 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑠) = (ℤ≥‘𝑠) |
62 | 61 | uztrn2 11581 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑠 + 𝑡) ∈ (ℤ≥‘𝑠) ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘𝑠)) |
63 | 60, 62 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘𝑠)) |
64 | | elfzuzb 12207 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ≥‘0)
∧ 𝑚 ∈
(ℤ≥‘𝑠))) |
65 | 55, 63, 64 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚)) |
66 | | fznn0sub2 12315 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚)) |
68 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ) |
70 | | eluz 11577 |
. . . . . . . . . . . 12
⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚)) |
71 | 69, 50, 70 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚)) |
72 | 54, 71 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠))) |
73 | | fzss2 12252 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚)) |
74 | 72, 73 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚)) |
75 | 74 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚)) |
76 | 13 | abscld 14023 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) |
77 | 11, 12, 76 | syl2an 493 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ) |
78 | 36 | abscld 14023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) |
79 | 77, 78 | remulcld 9949 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
80 | 75, 79 | syldan 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
81 | 46, 80 | fsumrecl 14312 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
82 | | fzfid 12634 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) |
83 | | elfznn0 12302 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈
ℕ0) |
84 | 67, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈
ℕ0) |
85 | | peano2nn0 11210 |
. . . . . . . . . . . 12
⊢ ((𝑚 − 𝑠) ∈ ℕ0 → ((𝑚 − 𝑠) + 1) ∈
ℕ0) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
ℕ0) |
87 | 86, 30 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘0)) |
88 | | fzss1 12251 |
. . . . . . . . . 10
⊢ (((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚)) |
89 | 87, 88 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚)) |
90 | 89 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚)) |
91 | 90, 79 | syldan 486 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
92 | 82, 91 | fsumrecl 14312 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
93 | 42 | rphalfcld 11760 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 / 2) ∈
ℝ+) |
94 | 93 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → (𝐸 / 2) ∈ ℝ) |
95 | 94 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ) |
96 | | elfznn0 12302 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ0) |
97 | 11, 96, 76 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ) |
98 | 46, 97 | fsumrecl 14312 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ) |
99 | 98, 95 | remulcld 9949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ) |
100 | | 0zd 11266 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) |
101 | | eqidd 2611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (𝐾‘𝑗)) |
102 | | mertens.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) |
103 | 102, 76 | eqeltrd 2688 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) ∈ ℝ) |
104 | | mertens.7 |
. . . . . . . . . . 11
⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
) |
105 | 30, 100, 101, 103, 104 | isumrecl 14338 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) |
106 | 13 | absge0d 14031 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) |
107 | 106, 102 | breqtrrd 4611 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(𝐾‘𝑗)) |
108 | 30, 100, 101, 103, 104, 107 | isumge0 14339 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0
(𝐾‘𝑗)) |
109 | 105, 108 | ge0p1rpd 11778 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) |
110 | 109 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) |
111 | 99, 110 | rerpdivcld 11779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) |
112 | 93, 109 | rpdivcld 11765 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈
ℝ+) |
113 | 112 | rpred 11748 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) |
114 | 113 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) |
115 | 97, 114 | remulcld 9949 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) ∈ ℝ) |
116 | 75, 20 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ) |
117 | | simplll 794 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) |
118 | 75, 19 | syldan 486 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
119 | 118, 22 | sylan 487 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
120 | 117, 119,
24 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) |
121 | 117, 119,
26 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ) |
122 | 75, 35 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ) |
123 | 15, 116, 120, 121, 122 | isumcl 14334 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ) |
124 | 123 | abscld 14023 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) |
125 | 76, 106 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) |
126 | 11, 96, 125 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) |
127 | 120 | sumeq2dv 14281 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) |
128 | 127 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) |
129 | | elfzelz 12213 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ) |
130 | 129 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ) |
131 | 130 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ) |
132 | 49 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ) |
133 | 132 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ) |
134 | 56 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ) |
135 | 134 | zred 11358 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ) |
136 | | elfzle2 12216 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠)) |
137 | 136 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠)) |
138 | 131, 133,
135, 137 | lesubd 10510 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗)) |
139 | 132, 130 | zsubcld 11363 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ) |
140 | | eluz 11577 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗))) |
141 | 134, 139,
140 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗))) |
142 | 138, 141 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ≥‘𝑠)) |
143 | 4 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
144 | 143 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
145 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑚 − 𝑗) → (𝑛 + 1) = ((𝑚 − 𝑗) + 1)) |
146 | 145 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘((𝑚 − 𝑗) + 1))) |
147 | 146 | sumeq1d 14279 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) |
148 | 147 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) |
149 | 148 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
150 | 149 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) → (∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
151 | 142, 144,
150 | sylc 63 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
152 | 128, 151 | eqbrtrrd 4607 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
153 | 124, 114,
152 | ltled 10064 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
154 | | lemul2a 10757 |
. . . . . . . . . 10
⊢
((((abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ ∧
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
155 | 124, 114,
126, 153, 154 | syl31anc 1321 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
156 | 46, 80, 115, 155 | fsumle 14372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
157 | 98 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ) |
158 | 93 | rpcnd 11750 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / 2) ∈ ℂ) |
159 | 158 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ) |
160 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ) |
161 | 105, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ) |
162 | 161 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℂ) |
163 | 162 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℂ) |
164 | 109 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ≠ 0) |
165 | 164 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ≠ 0) |
166 | 157, 159,
163, 165 | divassd 10715 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
167 | | fveq2 6103 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗)) |
168 | 167 | cbvsumv 14274 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) = Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) |
169 | 168 | oveq1i 6559 |
. . . . . . . . . . . . . . 15
⊢
(Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) |
170 | 169 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0
(𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
171 | 170, 112 | syl5eqel 2692 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈
ℝ+) |
172 | 171 | rpcnd 11750 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈ ℂ) |
173 | 172 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈ ℂ) |
174 | 76 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℂ) |
175 | 11, 96, 174 | syl2an 493 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ) |
176 | 46, 173, 175 | fsummulc1 14359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)))) |
177 | 170 | oveq2i 6560 |
. . . . . . . . . 10
⊢
(Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
178 | 170 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢
((abs‘𝐴)
· ((𝐸 / 2) /
(Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
179 | 178 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
180 | 179 | sumeq2i 14277 |
. . . . . . . . . 10
⊢
Σ𝑗 ∈
(0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
181 | 176, 177,
180 | 3eqtr3g 2667 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
182 | 166, 181 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
183 | 156, 182 | breqtrrd 4611 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
184 | 105 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) |
185 | 161 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ) |
186 | | 0zd 11266 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ) |
187 | | fz0ssnn0 12304 |
. . . . . . . . . . . . 13
⊢
(0...(𝑚 −
𝑠)) ⊆
ℕ0 |
188 | 187 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆
ℕ0) |
189 | 102 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) |
190 | 76 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) |
191 | 106 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) |
192 | 104 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ ) |
193 | 30, 186, 46, 188, 189, 190, 191, 192 | isumless 14416 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (abs‘𝐴)) |
194 | 102 | sumeq2dv 14281 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴)) |
195 | 194 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴)) |
196 | 193, 195 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (𝐾‘𝑗)) |
197 | 105 | ltp1d 10833 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
198 | 197 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
199 | 98, 184, 185, 196, 198 | lelttrd 10074 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
200 | 93 | rpregt0d 11754 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) |
201 | 200 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) |
202 | | ltmul1 10752 |
. . . . . . . . . 10
⊢
((Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0
< (𝐸 / 2))) →
(Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) |
203 | 98, 185, 201, 202 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) |
204 | 199, 203 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2))) |
205 | 109 | rpregt0d 11754 |
. . . . . . . . . 10
⊢ (𝜑 → ((Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) |
206 | 205 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) |
207 | | ltdivmul 10777 |
. . . . . . . . 9
⊢
(((Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧
((Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) |
208 | 99, 95, 206, 207 | syl3anc 1318 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) |
209 | 204, 208 | mpbird 246 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2)) |
210 | 81, 111, 95, 183, 209 | lelttrd 10074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2)) |
211 | | mertens.13 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) |
212 | 211 | simprd 478 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) |
213 | | suprcl 10862 |
. . . . . . . . . . 11
⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈
ℝ) |
214 | 212, 213 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈
ℝ) |
215 | 94, 214 | remulcld 9949 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈
ℝ) |
216 | 211 | simpld 474 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, <
)) |
217 | 214, 216 | ge0p1rpd 11778 |
. . . . . . . . 9
⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ+) |
218 | 215, 217 | rerpdivcld 11779 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
219 | 218 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
220 | 5 | nnrpd 11746 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑠 ∈ ℝ+) |
221 | 93, 220 | rpdivcld 11765 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈
ℝ+) |
222 | 221, 217 | rpdivcld 11765 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ+) |
223 | 222 | rpred 11748 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
224 | 223, 214 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℝ) |
225 | 224 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℝ) |
226 | | simpll 786 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑) |
227 | 90, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ0) |
228 | 226, 227,
76 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ) |
229 | 223 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
230 | 226, 227,
102 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴)) |
231 | | elfzuz 12209 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ≥‘((𝑚 − 𝑠) + 1))) |
232 | | eluzle 11576 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚) |
233 | 232 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚) |
234 | 8 | nn0zd 11356 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑡 ∈ ℤ) |
235 | 234 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ) |
236 | 235 | zred 11358 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ) |
237 | 52, 236, 51 | leaddsub2d 10508 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠))) |
238 | 233, 237 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠)) |
239 | | eluz 11577 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠))) |
240 | 235, 69, 239 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠))) |
241 | 238, 240 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ≥‘𝑡)) |
242 | | peano2uz 11617 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) |
243 | 241, 242 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) |
244 | | uztrn 11580 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈
(ℤ≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) → 𝑗 ∈ (ℤ≥‘𝑡)) |
245 | 231, 243,
244 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ≥‘𝑡)) |
246 | 7 | simprd 478 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
247 | 246 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
248 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗)) |
249 | 248 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
250 | 249 | rspcv 3278 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑡) → (∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
251 | 245, 247,
250 | sylc 63 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
252 | 230, 251 | eqbrtrrd 4607 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
253 | 228, 229,
252 | ltled 10064 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
254 | 212 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) |
255 | 51 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ) |
256 | | peano2zm 11297 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈
ℤ) |
257 | 56, 256 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑠 − 1) ∈ ℤ) |
258 | 257 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑠 − 1) ∈ ℝ) |
259 | 258 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ) |
260 | 227 | nn0red 11229 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ) |
261 | 50 | zcnd 11359 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ) |
262 | 52 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ) |
263 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ) |
264 | 261, 262,
263 | subsubd 10299 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1)) |
265 | 264 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1)) |
266 | | elfzle1 12215 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗) |
267 | 266 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗) |
268 | 265, 267 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗) |
269 | 255, 259,
260, 268 | subled 10509 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1)) |
270 | 90, 16 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈
ℕ0) |
271 | 270, 30 | syl6eleq 2698 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈
(ℤ≥‘0)) |
272 | 257 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ) |
273 | | elfz5 12205 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 − 𝑗) ∈ (ℤ≥‘0)
∧ (𝑠 − 1) ∈
ℤ) → ((𝑚 −
𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1))) |
274 | 271, 272,
273 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1))) |
275 | 269, 274 | mpbird 246 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1))) |
276 | | simplll 794 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) |
277 | 90, 19 | syldan 486 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
278 | 277, 22 | sylan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
279 | 276, 278,
24 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) |
280 | 279 | sumeq2dv 14281 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) |
281 | 280 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) |
282 | 281 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) |
283 | 148 | eqeq2d 2620 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))) |
284 | 283 | rspcev 3282 |
. . . . . . . . . . . . 13
⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
285 | 275, 282,
284 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
286 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(abs‘Σ𝑘
∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V |
287 | | eqeq1 2614 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
288 | 287 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
289 | | mertens.10 |
. . . . . . . . . . . . 13
⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} |
290 | 286, 288,
289 | elab2 3323 |
. . . . . . . . . . . 12
⊢
((abs‘Σ𝑘
∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
291 | 285, 290 | sylibr 223 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) |
292 | | suprub 10863 |
. . . . . . . . . . 11
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) |
293 | 254, 291,
292 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) |
294 | 226, 227,
125 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) |
295 | 90, 78 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) |
296 | 36 | absge0d 14031 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) |
297 | 90, 296 | syldan 486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) |
298 | 295, 297 | jca 553 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
299 | 214 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈
ℝ) |
300 | | lemul12a 10760 |
. . . . . . . . . . 11
⊢
(((((abs‘𝐴)
∈ ℝ ∧ 0 ≤ (abs‘𝐴)) ∧ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈ ℝ)
∧ (((abs‘Σ𝑘
∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∧ sup(𝑇, ℝ, < ) ∈ ℝ)) →
(((abs‘𝐴) ≤
(((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) ·
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
301 | 294, 229,
298, 299, 300 | syl22anc 1319 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) ·
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
302 | 253, 293,
301 | mp2and 711 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
303 | 82, 91, 225, 302 | fsumle 14372 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
304 | 224 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) |
305 | 304 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) |
306 | | fsumconst 14364 |
. . . . . . . . . 10
⊢
(((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) → Σ𝑗
∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) =
((#‘(((𝑚 −
𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
307 | 82, 305, 306 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) =
((#‘(((𝑚 −
𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
308 | | 1zzd 11285 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ) |
309 | 56 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ) |
310 | | fzen 12229 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ (𝑚
− 𝑠) ∈ ℤ)
→ (1...𝑠) ≈ ((1
+ (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠)))) |
311 | 308, 309,
69, 310 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠)))) |
312 | | ax-1cn 9873 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
313 | 69 | zcnd 11359 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ) |
314 | | addcom 10101 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ (𝑚
− 𝑠) ∈ ℂ)
→ (1 + (𝑚 −
𝑠)) = ((𝑚 − 𝑠) + 1)) |
315 | 312, 313,
314 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1)) |
316 | 262, 261 | pncan3d 10274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚) |
317 | 315, 316 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚)) |
318 | 311, 317 | breqtrd 4609 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)) |
319 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin) |
320 | | hashen 12997 |
. . . . . . . . . . . . 13
⊢
(((1...𝑠) ∈ Fin
∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) → ((#‘(1...𝑠)) = (#‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))) |
321 | 319, 82, 320 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((#‘(1...𝑠)) = (#‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))) |
322 | 318, 321 | mpbird 246 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (#‘(1...𝑠)) = (#‘(((𝑚 − 𝑠) + 1)...𝑚))) |
323 | | hashfz1 12996 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ0
→ (#‘(1...𝑠)) =
𝑠) |
324 | 47, 323 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (#‘(1...𝑠)) = 𝑠) |
325 | 322, 324 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (#‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠) |
326 | 325 | oveq1d 6564 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((#‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
327 | 214 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈
ℂ) |
328 | 217 | rpcnne0d 11757 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧
(sup(𝑇, ℝ, < ) +
1) ≠ 0)) |
329 | | div23 10583 |
. . . . . . . . . . . 12
⊢ (((𝐸 / 2) ∈ ℂ ∧
sup(𝑇, ℝ, < )
∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧
(sup(𝑇, ℝ, < ) +
1) ≠ 0)) → (((𝐸 /
2) · sup(𝑇, ℝ,
< )) / (sup(𝑇, ℝ,
< ) + 1)) = (((𝐸 / 2) /
(sup(𝑇, ℝ, < ) +
1)) · sup(𝑇,
ℝ, < ))) |
330 | 158, 327,
328, 329 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
331 | 56 | zcnd 11359 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑠 ∈ ℂ) |
332 | 221 | rpcnd 11750 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ) |
333 | | divass 10582 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈
ℂ ∧ (sup(𝑇,
ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
334 | 331, 332,
328, 333 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
335 | 5 | nnne0d 10942 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑠 ≠ 0) |
336 | 158, 331,
335 | divcan2d 10682 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2)) |
337 | 336 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1))) |
338 | 334, 337 | eqtr3d 2646 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1))) |
339 | 338 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
340 | 222 | rpcnd 11750 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℂ) |
341 | 331, 340,
327 | mulassd 9942 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
342 | 330, 339,
341 | 3eqtr2rd 2651 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) |
343 | 342 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) |
344 | 307, 326,
343 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) |
345 | 303, 344 | breqtrd 4609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1))) |
346 | | peano2re 10088 |
. . . . . . . . . . 11
⊢
(sup(𝑇, ℝ,
< ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ) |
347 | 214, 346 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ) |
348 | 214 | ltp1d 10833 |
. . . . . . . . . 10
⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1)) |
349 | 214, 347,
93, 348 | ltmul2dd 11804 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))) |
350 | 215, 94, 217 | ltdivmul2d 11800 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))) |
351 | 349, 350 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2)) |
352 | 351 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2)) |
353 | 92, 219, 95, 345, 352 | lelttrd 10074 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2)) |
354 | 81, 92, 95, 95, 210, 353 | lt2addd 10529 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2))) |
355 | 14, 36 | absmuld 14041 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
356 | 355 | sumeq2dv 14281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
357 | 69 | zred 11358 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ) |
358 | 357 | ltp1d 10833 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1)) |
359 | | fzdisj 12239 |
. . . . . . . 8
⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅) |
360 | 358, 359 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅) |
361 | | fzsplit 12238 |
. . . . . . . 8
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚))) |
362 | 67, 361 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚))) |
363 | 79 | recnd 9947 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ) |
364 | 360, 362,
10, 363 | fsumsplit 14318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)))) |
365 | 356, 364 | eqtr2d 2645 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
366 | 42 | rpcnd 11750 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) |
367 | 366 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ) |
368 | 367 | 2halvesd 11155 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) |
369 | 354, 365,
368 | 3brtr3d 4614 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
370 | 39, 41, 44, 45, 369 | lelttrd 10074 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
371 | 370 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
372 | | fveq2 6103 |
. . . 4
⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ≥‘𝑦) =
(ℤ≥‘(𝑠 + 𝑡))) |
373 | 372 | raleqdv 3121 |
. . 3
⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
374 | 373 | rspcev 3282 |
. 2
⊢ (((𝑠 + 𝑡) ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
375 | 9, 371, 374 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |