Proof of Theorem mertenslem1
Step | Hyp | Ref
| Expression |
1 | | mertens.12 |
. . . . . . 7
⊢ (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) |
2 | 1 | simpld 475 |
. . . . . 6
⊢ (𝜑 → 𝜓) |
3 | | mertens.11 |
. . . . . 6
⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
4 | 2, 3 | sylib 208 |
. . . . 5
⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
5 | 4 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝑠 ∈ ℕ) |
6 | 5 | nnnn0d 11351 |
. . 3
⊢ (𝜑 → 𝑠 ∈ ℕ0) |
7 | 1 | simprd 479 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
8 | 7 | simpld 475 |
. . 3
⊢ (𝜑 → 𝑡 ∈ ℕ0) |
9 | 6, 8 | nn0addcld 11355 |
. 2
⊢ (𝜑 → (𝑠 + 𝑡) ∈
ℕ0) |
10 | | fzfid 12772 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin) |
11 | | simpl 473 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝜑) |
12 | | elfznn0 12433 |
. . . . . . . 8
⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0) |
13 | | mertens.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈
ℂ) |
14 | 11, 12, 13 | syl2an 494 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ) |
15 | | eqid 2622 |
. . . . . . . 8
⊢
(ℤ≥‘((𝑚 − 𝑗) + 1)) =
(ℤ≥‘((𝑚 − 𝑗) + 1)) |
16 | | fznn0sub 12373 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈
ℕ0) |
17 | 16 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈
ℕ0) |
18 | | peano2nn0 11333 |
. . . . . . . . . 10
⊢ ((𝑚 − 𝑗) ∈ ℕ0 → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
20 | 19 | nn0zd 11480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ) |
21 | | simplll 798 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) |
22 | | eluznn0 11757 |
. . . . . . . . . 10
⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ0 ∧ 𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
23 | 19, 22 | sylan 488 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
24 | | mertens.4 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) |
25 | 21, 23, 24 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) |
26 | | mertens.5 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) |
27 | 21, 23, 26 | syl2anc 693 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ) |
28 | | mertens.8 |
. . . . . . . . . 10
⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝
) |
29 | 28 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ ) |
30 | | nn0uz 11722 |
. . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) |
31 | | simpll 790 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑) |
32 | 24, 26 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
33 | 31, 32 | sylan 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
34 | 30, 19, 33 | iserex 14387 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )) |
35 | 29, 34 | mpbid 222 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ) |
36 | 15, 20, 25, 27, 35 | isumcl 14492 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ) |
37 | 14, 36 | mulcld 10060 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ) |
38 | 10, 37 | fsumcl 14464 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ) |
39 | 38 | abscld 14175 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
40 | 37 | abscld 14175 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
41 | 10, 40 | fsumrecl 14465 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
42 | | mertens.9 |
. . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
43 | 42 | rpred 11872 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) |
44 | 43 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ) |
45 | 10, 37 | fsumabs 14533 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
46 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin) |
47 | 6 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ0) |
48 | 47 | nn0ge0d 11354 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠) |
49 | | eluzelz 11697 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ) |
50 | 49 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ) |
51 | 50 | zred 11482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ) |
52 | 47 | nn0red 11352 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ) |
53 | 51, 52 | subge02d 10619 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚)) |
54 | 48, 53 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚) |
55 | 47, 30 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈
(ℤ≥‘0)) |
56 | 5 | nnzd 11481 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑠 ∈ ℤ) |
57 | | uzid 11702 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℤ → 𝑠 ∈
(ℤ≥‘𝑠)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑠 ∈ (ℤ≥‘𝑠)) |
59 | | uzaddcl 11744 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈
(ℤ≥‘𝑠) ∧ 𝑡 ∈ ℕ0) → (𝑠 + 𝑡) ∈ (ℤ≥‘𝑠)) |
60 | 58, 8, 59 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ≥‘𝑠)) |
61 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑠) = (ℤ≥‘𝑠) |
62 | 61 | uztrn2 11705 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑠 + 𝑡) ∈ (ℤ≥‘𝑠) ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘𝑠)) |
63 | 60, 62 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘𝑠)) |
64 | | elfzuzb 12336 |
. . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ≥‘0)
∧ 𝑚 ∈
(ℤ≥‘𝑠))) |
65 | 55, 63, 64 | sylanbrc 698 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚)) |
66 | | fznn0sub2 12446 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚)) |
68 | | elfzelz 12342 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ) |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ) |
70 | | eluz 11701 |
. . . . . . . . . . . 12
⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚)) |
71 | 69, 50, 70 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚)) |
72 | 54, 71 | mpbird 247 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠))) |
73 | | fzss2 12381 |
. . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚)) |
74 | 72, 73 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚)) |
75 | 74 | sselda 3603 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚)) |
76 | 13 | abscld 14175 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) |
77 | 11, 12, 76 | syl2an 494 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ) |
78 | 36 | abscld 14175 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) |
79 | 77, 78 | remulcld 10070 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
80 | 75, 79 | syldan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
81 | 46, 80 | fsumrecl 14465 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
82 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) |
83 | | elfznn0 12433 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈
ℕ0) |
84 | 67, 83 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈
ℕ0) |
85 | | peano2nn0 11333 |
. . . . . . . . . . . 12
⊢ ((𝑚 − 𝑠) ∈ ℕ0 → ((𝑚 − 𝑠) + 1) ∈
ℕ0) |
86 | 84, 85 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
ℕ0) |
87 | 86, 30 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘0)) |
88 | | fzss1 12380 |
. . . . . . . . . 10
⊢ (((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚)) |
89 | 87, 88 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚)) |
90 | 89 | sselda 3603 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚)) |
91 | 90, 79 | syldan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
92 | 82, 91 | fsumrecl 14465 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) |
93 | 42 | rphalfcld 11884 |
. . . . . . . 8
⊢ (𝜑 → (𝐸 / 2) ∈
ℝ+) |
94 | 93 | rpred 11872 |
. . . . . . 7
⊢ (𝜑 → (𝐸 / 2) ∈ ℝ) |
95 | 94 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ) |
96 | | elfznn0 12433 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ0) |
97 | 11, 96, 76 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ) |
98 | 46, 97 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ) |
99 | 98, 95 | remulcld 10070 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ) |
100 | | 0zd 11389 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) |
101 | | eqidd 2623 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (𝐾‘𝑗)) |
102 | | mertens.2 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) |
103 | 102, 76 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) ∈ ℝ) |
104 | | mertens.7 |
. . . . . . . . . . 11
⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
) |
105 | 30, 100, 101, 103, 104 | isumrecl 14496 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) |
106 | 13 | absge0d 14183 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) |
107 | 106, 102 | breqtrrd 4681 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(𝐾‘𝑗)) |
108 | 30, 100, 101, 103, 104, 107 | isumge0 14497 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0
(𝐾‘𝑗)) |
109 | 105, 108 | ge0p1rpd 11902 |
. . . . . . . . 9
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) |
110 | 109 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) |
111 | 99, 110 | rerpdivcld 11903 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) |
112 | 93, 109 | rpdivcld 11889 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈
ℝ+) |
113 | 112 | rpred 11872 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) |
114 | 113 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) |
115 | 97, 114 | remulcld 10070 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) ∈ ℝ) |
116 | 75, 20 | syldan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ) |
117 | | simplll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) |
118 | 75, 19 | syldan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
119 | 118, 22 | sylan 488 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
120 | 117, 119,
24 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) |
121 | 117, 119,
26 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ) |
122 | 75, 35 | syldan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ) |
123 | 15, 116, 120, 121, 122 | isumcl 14492 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ) |
124 | 123 | abscld 14175 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) |
125 | 76, 106 | jca 554 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) |
126 | 11, 96, 125 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) |
127 | 120 | sumeq2dv 14433 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) |
128 | 127 | fveq2d 6195 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) |
129 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ) |
130 | 129 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ) |
131 | 130 | zred 11482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ) |
132 | 49 | ad2antlr 763 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ) |
133 | 132 | zred 11482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ) |
134 | 56 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ) |
135 | 134 | zred 11482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ) |
136 | | elfzle2 12345 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠)) |
137 | 136 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠)) |
138 | 131, 133,
135, 137 | lesubd 10631 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗)) |
139 | 132, 130 | zsubcld 11487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ) |
140 | | eluz 11701 |
. . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗))) |
141 | 134, 139,
140 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗))) |
142 | 138, 141 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ≥‘𝑠)) |
143 | 4 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
144 | 143 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
145 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑚 − 𝑗) → (𝑛 + 1) = ((𝑚 − 𝑗) + 1)) |
146 | 145 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘((𝑚 − 𝑗) + 1))) |
147 | 146 | sumeq1d 14431 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) |
148 | 147 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) |
149 | 148 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
150 | 149 | rspcv 3305 |
. . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) → (∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
151 | 142, 144,
150 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
152 | 128, 151 | eqbrtrrd 4677 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
153 | 124, 114,
152 | ltled 10185 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
154 | | lemul2a 10878 |
. . . . . . . . . 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 1329 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
156 | 46, 80, 115, 155 | fsumle 14531 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
157 | 98 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ) |
158 | 93 | rpcnd 11874 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / 2) ∈ ℂ) |
159 | 158 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ) |
160 | | peano2re 10209 |
. . . . . . . . . . . . 13
⊢
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ) |
161 | 105, 160 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ) |
162 | 161 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℂ) |
163 | 162 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℂ) |
164 | 109 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ≠ 0) |
165 | 164 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ≠ 0) |
166 | 157, 159,
163, 165 | divassd 10836 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
167 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗)) |
168 | 167 | cbvsumv 14426 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) = Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) |
169 | 168 | oveq1i 6660 |
. . . . . . . . . . . . . . 15
⊢
(Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) |
170 | 169 | oveq2i 6661 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0
(𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
171 | 170, 112 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈
ℝ+) |
172 | 171 | rpcnd 11874 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈ ℂ) |
173 | 172 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈ ℂ) |
174 | 76 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℂ) |
175 | 11, 96, 174 | syl2an 494 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ) |
176 | 46, 173, 175 | fsummulc1 14517 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)))) |
177 | 170 | oveq2i 6661 |
. . . . . . . . . 10
⊢
(Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
178 | 170 | oveq2i 6661 |
. . . . . . . . . . . 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 14429 |
. . . . . . . . . 10
⊢
Σ𝑗 ∈
(0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
181 | 176, 177,
180 | 3eqtr3g 2679 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
182 | 166, 181 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
183 | 156, 182 | breqtrrd 4681 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
184 | 105 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) |
185 | 161 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ) |
186 | | 0zd 11389 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ) |
187 | | fz0ssnn0 12435 |
. . . . . . . . . . . . 13
⊢
(0...(𝑚 −
𝑠)) ⊆
ℕ0 |
188 | 187 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆
ℕ0) |
189 | 102 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) |
190 | 76 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) |
191 | 106 | adantlr 751 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) |
192 | 104 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ ) |
193 | 30, 186, 46, 188, 189, 190, 191, 192 | isumless 14577 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (abs‘𝐴)) |
194 | 102 | sumeq2dv 14433 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴)) |
195 | 194 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴)) |
196 | 193, 195 | breqtrrd 4681 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (𝐾‘𝑗)) |
197 | 105 | ltp1d 10954 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
198 | 197 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
199 | 98, 184, 185, 196, 198 | lelttrd 10195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) |
200 | 93 | rpregt0d 11878 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) |
201 | 200 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) |
202 | | ltmul1 10873 |
. . . . . . . . . 10
⊢
((Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0
< (𝐸 / 2))) →
(Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) |
203 | 98, 185, 201, 202 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) |
204 | 199, 203 | mpbid 222 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2))) |
205 | 109 | rpregt0d 11878 |
. . . . . . . . . 10
⊢ (𝜑 → ((Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) |
206 | 205 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) |
207 | | ltdivmul 10898 |
. . . . . . . . 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 1326 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) |
209 | 204, 208 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2)) |
210 | 81, 111, 95, 183, 209 | lelttrd 10195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2)) |
211 | | mertens.13 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) |
212 | 211 | simprd 479 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) |
213 | | suprcl 10983 |
. . . . . . . . . . 11
⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈
ℝ) |
214 | 212, 213 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈
ℝ) |
215 | 94, 214 | remulcld 10070 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈
ℝ) |
216 | 211 | simpld 475 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, <
)) |
217 | 214, 216 | ge0p1rpd 11902 |
. . . . . . . . 9
⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ+) |
218 | 215, 217 | rerpdivcld 11903 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
219 | 218 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
220 | 5 | nnrpd 11870 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑠 ∈ ℝ+) |
221 | 93, 220 | rpdivcld 11889 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈
ℝ+) |
222 | 221, 217 | rpdivcld 11889 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ+) |
223 | 222 | rpred 11872 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
224 | 223, 214 | remulcld 10070 |
. . . . . . . . . 10
⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℝ) |
225 | 224 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℝ) |
226 | | simpll 790 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑) |
227 | 90, 12 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ0) |
228 | 226, 227,
76 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ) |
229 | 223 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) |
230 | 226, 227,
102 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴)) |
231 | | elfzuz 12338 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ≥‘((𝑚 − 𝑠) + 1))) |
232 | | eluzle 11700 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚) |
233 | 232 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚) |
234 | 8 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑡 ∈ ℤ) |
235 | 234 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ) |
236 | 235 | zred 11482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ) |
237 | 52, 236, 51 | leaddsub2d 10629 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠))) |
238 | 233, 237 | mpbid 222 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠)) |
239 | | eluz 11701 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠))) |
240 | 235, 69, 239 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠))) |
241 | 238, 240 | mpbird 247 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ≥‘𝑡)) |
242 | | peano2uz 11741 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) |
243 | 241, 242 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) |
244 | | uztrn 11704 |
. . . . . . . . . . . . . 14
⊢ ((𝑗 ∈
(ℤ≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) → 𝑗 ∈ (ℤ≥‘𝑡)) |
245 | 231, 243,
244 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ≥‘𝑡)) |
246 | 7 | simprd 479 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
247 | 246 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
248 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗)) |
249 | 248 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
250 | 249 | rspcv 3305 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈
(ℤ≥‘𝑡) → (∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
251 | 245, 247,
250 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
252 | 230, 251 | eqbrtrrd 4677 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
253 | 228, 229,
252 | ltled 10185 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
254 | 212 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) |
255 | 51 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ) |
256 | | peano2zm 11420 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈
ℤ) |
257 | 56, 256 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑠 − 1) ∈ ℤ) |
258 | 257 | zred 11482 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑠 − 1) ∈ ℝ) |
259 | 258 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ) |
260 | 227 | nn0red 11352 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ) |
261 | 50 | zcnd 11483 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ) |
262 | 52 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ) |
263 | | 1cnd 10056 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ) |
264 | 261, 262,
263 | subsubd 10420 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1)) |
265 | 264 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1)) |
266 | | elfzle1 12344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗) |
267 | 266 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗) |
268 | 265, 267 | eqbrtrd 4675 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗) |
269 | 255, 259,
260, 268 | subled 10630 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1)) |
270 | 90, 16 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈
ℕ0) |
271 | 270, 30 | syl6eleq 2711 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈
(ℤ≥‘0)) |
272 | 257 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ) |
273 | | elfz5 12334 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 − 𝑗) ∈ (ℤ≥‘0)
∧ (𝑠 − 1) ∈
ℤ) → ((𝑚 −
𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1))) |
274 | 271, 272,
273 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1))) |
275 | 269, 274 | mpbird 247 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1))) |
276 | | simplll 798 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) |
277 | 90, 19 | syldan 487 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) |
278 | 277, 22 | sylan 488 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) |
279 | 276, 278,
24 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) |
280 | 279 | sumeq2dv 14433 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) |
281 | 280 | eqcomd 2628 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) |
282 | 281 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) |
283 | 148 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)))) |
284 | 283 | rspcev 3309 |
. . . . . . . . . . . . 13
⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
285 | 275, 282,
284 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
286 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
(abs‘Σ𝑘
∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V |
287 | | eqeq1 2626 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
288 | 287 | rexbidv 3052 |
. . . . . . . . . . . . 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 3354 |
. . . . . . . . . . . 12
⊢
((abs‘Σ𝑘
∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
291 | 285, 290 | sylibr 224 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) |
292 | | suprub 10984 |
. . . . . . . . . . 11
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) |
293 | 254, 291,
292 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) |
294 | 226, 227,
125 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) |
295 | 90, 78 | syldan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) |
296 | 36 | absge0d 14183 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) |
297 | 90, 296 | syldan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) |
298 | 295, 297 | jca 554 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
299 | 214 | ad2antrr 762 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈
ℝ) |
300 | | lemul12a 10881 |
. . . . . . . . . . 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 1327 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) ·
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
302 | 253, 293,
301 | mp2and 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
303 | 82, 91, 225, 302 | fsumle 14531 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
304 | 224 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) |
305 | 304 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) |
306 | | fsumconst 14522 |
. . . . . . . . . 10
⊢
(((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) → Σ𝑗
∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) =
((#‘(((𝑚 −
𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
307 | 82, 305, 306 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) =
((#‘(((𝑚 −
𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
308 | | 1zzd 11408 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ) |
309 | 56 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ) |
310 | | fzen 12358 |
. . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ (𝑚
− 𝑠) ∈ ℤ)
→ (1...𝑠) ≈ ((1
+ (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠)))) |
311 | 308, 309,
69, 310 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠)))) |
312 | | ax-1cn 9994 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ |
313 | 69 | zcnd 11483 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ) |
314 | | addcom 10222 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ (𝑚
− 𝑠) ∈ ℂ)
→ (1 + (𝑚 −
𝑠)) = ((𝑚 − 𝑠) + 1)) |
315 | 312, 313,
314 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1)) |
316 | 262, 261 | pncan3d 10395 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚) |
317 | 315, 316 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚)) |
318 | 311, 317 | breqtrd 4679 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)) |
319 | | fzfid 12772 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin) |
320 | | hashen 13135 |
. . . . . . . . . . . . 13
⊢
(((1...𝑠) ∈ Fin
∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) → ((#‘(1...𝑠)) = (#‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))) |
321 | 319, 82, 320 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((#‘(1...𝑠)) = (#‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))) |
322 | 318, 321 | mpbird 247 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (#‘(1...𝑠)) = (#‘(((𝑚 − 𝑠) + 1)...𝑚))) |
323 | | hashfz1 13134 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ0
→ (#‘(1...𝑠)) =
𝑠) |
324 | 47, 323 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (#‘(1...𝑠)) = 𝑠) |
325 | 322, 324 | eqtr3d 2658 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (#‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠) |
326 | 325 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((#‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
327 | 214 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈
ℂ) |
328 | 217 | rpcnne0d 11881 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧
(sup(𝑇, ℝ, < ) +
1) ≠ 0)) |
329 | | div23 10704 |
. . . . . . . . . . . 12
⊢ (((𝐸 / 2) ∈ ℂ ∧
sup(𝑇, ℝ, < )
∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧
(sup(𝑇, ℝ, < ) +
1) ≠ 0)) → (((𝐸 /
2) · sup(𝑇, ℝ,
< )) / (sup(𝑇, ℝ,
< ) + 1)) = (((𝐸 / 2) /
(sup(𝑇, ℝ, < ) +
1)) · sup(𝑇,
ℝ, < ))) |
330 | 158, 327,
328, 329 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
331 | 56 | zcnd 11483 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑠 ∈ ℂ) |
332 | 221 | rpcnd 11874 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ) |
333 | | divass 10703 |
. . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈
ℂ ∧ (sup(𝑇,
ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
334 | 331, 332,
328, 333 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
335 | 5 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑠 ≠ 0) |
336 | 158, 331,
335 | divcan2d 10803 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2)) |
337 | 336 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1))) |
338 | 334, 337 | eqtr3d 2658 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1))) |
339 | 338 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) |
340 | 222 | rpcnd 11874 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℂ) |
341 | 331, 340,
327 | mulassd 10063 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) |
342 | 330, 339,
341 | 3eqtr2rd 2663 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) |
343 | 342 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) |
344 | 307, 326,
343 | 3eqtrd 2660 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) |
345 | 303, 344 | breqtrd 4679 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1))) |
346 | | peano2re 10209 |
. . . . . . . . . . 11
⊢
(sup(𝑇, ℝ,
< ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ) |
347 | 214, 346 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ) |
348 | 214 | ltp1d 10954 |
. . . . . . . . . 10
⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1)) |
349 | 214, 347,
93, 348 | ltmul2dd 11928 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))) |
350 | 215, 94, 217 | ltdivmul2d 11924 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))) |
351 | 349, 350 | mpbird 247 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2)) |
352 | 351 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2)) |
353 | 92, 219, 95, 345, 352 | lelttrd 10195 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2)) |
354 | 81, 92, 95, 95, 210, 353 | lt2addd 10650 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2))) |
355 | 14, 36 | absmuld 14193 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
356 | 355 | sumeq2dv 14433 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
357 | 69 | zred 11482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ) |
358 | 357 | ltp1d 10954 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1)) |
359 | | fzdisj 12368 |
. . . . . . . 8
⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅) |
360 | 358, 359 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅) |
361 | | fzsplit 12367 |
. . . . . . . 8
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚))) |
362 | 67, 361 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚))) |
363 | 79 | recnd 10068 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ) |
364 | 360, 362,
10, 363 | fsumsplit 14471 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)))) |
365 | 356, 364 | eqtr2d 2657 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) |
366 | 42 | rpcnd 11874 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) |
367 | 366 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ) |
368 | 367 | 2halvesd 11278 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) |
369 | 354, 365,
368 | 3brtr3d 4684 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
370 | 39, 41, 44, 45, 369 | lelttrd 10195 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
371 | 370 | ralrimiva 2966 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
372 | | fveq2 6191 |
. . . 4
⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ≥‘𝑦) =
(ℤ≥‘(𝑠 + 𝑡))) |
373 | 372 | raleqdv 3144 |
. . 3
⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
374 | 373 | rspcev 3309 |
. 2
⊢ (((𝑠 + 𝑡) ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
375 | 9, 371, 374 | syl2anc 693 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |