Proof of Theorem mertenslem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mertens.12 | . . . . . . 7
⊢ (𝜑 → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) | 
| 2 | 1 | simpld 494 | . . . . . 6
⊢ (𝜑 → 𝜓) | 
| 3 |  | mertens.11 | . . . . . 6
⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 4 | 2, 3 | sylib 218 | . . . . 5
⊢ (𝜑 → (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 5 | 4 | simpld 494 | . . . 4
⊢ (𝜑 → 𝑠 ∈ ℕ) | 
| 6 | 5 | nnnn0d 12589 | . . 3
⊢ (𝜑 → 𝑠 ∈ ℕ0) | 
| 7 | 1 | simprd 495 | . . . 4
⊢ (𝜑 → (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 8 | 7 | simpld 494 | . . 3
⊢ (𝜑 → 𝑡 ∈ ℕ0) | 
| 9 | 6, 8 | nn0addcld 12593 | . 2
⊢ (𝜑 → (𝑠 + 𝑡) ∈
ℕ0) | 
| 10 |  | fzfid 14015 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...𝑚) ∈ Fin) | 
| 11 |  | simpl 482 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝜑) | 
| 12 |  | elfznn0 13661 | . . . . . . . 8
⊢ (𝑗 ∈ (0...𝑚) → 𝑗 ∈ ℕ0) | 
| 13 |  | mertens.3 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈
ℂ) | 
| 14 | 11, 12, 13 | syl2an 596 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝐴 ∈ ℂ) | 
| 15 |  | eqid 2736 | . . . . . . . 8
⊢
(ℤ≥‘((𝑚 − 𝑗) + 1)) =
(ℤ≥‘((𝑚 − 𝑗) + 1)) | 
| 16 |  | fznn0sub 13597 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0...𝑚) → (𝑚 − 𝑗) ∈
ℕ0) | 
| 17 | 16 | adantl 481 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝑚 − 𝑗) ∈
ℕ0) | 
| 18 |  | peano2nn0 12568 | . . . . . . . . . 10
⊢ ((𝑚 − 𝑗) ∈ ℕ0 → ((𝑚 − 𝑗) + 1) ∈
ℕ0) | 
| 19 | 17, 18 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) | 
| 20 | 19 | nn0zd 12641 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((𝑚 − 𝑗) + 1) ∈ ℤ) | 
| 21 |  | simplll 774 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) | 
| 22 |  | eluznn0 12960 | . . . . . . . . . 10
⊢ ((((𝑚 − 𝑗) + 1) ∈ ℕ0 ∧ 𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) | 
| 23 | 19, 22 | sylan 580 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) | 
| 24 |  | mertens.4 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) | 
| 25 | 21, 23, 24 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) | 
| 26 |  | mertens.5 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) | 
| 27 | 21, 23, 26 | syl2anc 584 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ) | 
| 28 |  | mertens.8 | . . . . . . . . . 10
⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝
) | 
| 29 | 28 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq0( + , 𝐺) ∈ dom ⇝ ) | 
| 30 |  | nn0uz 12921 | . . . . . . . . . 10
⊢
ℕ0 = (ℤ≥‘0) | 
| 31 |  | simpll 766 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 𝜑) | 
| 32 | 24, 26 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) | 
| 33 | 31, 32 | sylan 580 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) | 
| 34 | 30, 19, 33 | iserex 15694 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (seq0( + , 𝐺) ∈ dom ⇝ ↔ seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ )) | 
| 35 | 29, 34 | mpbid 232 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ) | 
| 36 | 15, 20, 25, 27, 35 | isumcl 15798 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ) | 
| 37 | 14, 36 | mulcld 11282 | . . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ) | 
| 38 | 10, 37 | fsumcl 15770 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℂ) | 
| 39 | 38 | abscld 15476 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 40 | 37 | abscld 15476 | . . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 41 | 10, 40 | fsumrecl 15771 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 42 |  | mertens.9 | . . . . . 6
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 43 | 42 | rpred 13078 | . . . . 5
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 44 | 43 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℝ) | 
| 45 | 10, 37 | fsumabs 15838 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) | 
| 46 |  | fzfid 14015 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ∈ Fin) | 
| 47 | 6 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℕ0) | 
| 48 | 47 | nn0ge0d 12592 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 0 ≤ 𝑠) | 
| 49 |  | eluzelz 12889 | . . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡)) → 𝑚 ∈ ℤ) | 
| 50 | 49 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℤ) | 
| 51 | 50 | zred 12724 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℝ) | 
| 52 | 47 | nn0red 12590 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℝ) | 
| 53 | 51, 52 | subge02d 11856 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0 ≤ 𝑠 ↔ (𝑚 − 𝑠) ≤ 𝑚)) | 
| 54 | 48, 53 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ≤ 𝑚) | 
| 55 | 47, 30 | eleqtrdi 2850 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈
(ℤ≥‘0)) | 
| 56 | 5 | nnzd 12642 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑠 ∈ ℤ) | 
| 57 |  | uzid 12894 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℤ → 𝑠 ∈
(ℤ≥‘𝑠)) | 
| 58 | 56, 57 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑠 ∈ (ℤ≥‘𝑠)) | 
| 59 |  | uzaddcl 12947 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∈
(ℤ≥‘𝑠) ∧ 𝑡 ∈ ℕ0) → (𝑠 + 𝑡) ∈ (ℤ≥‘𝑠)) | 
| 60 | 58, 8, 59 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑠 + 𝑡) ∈ (ℤ≥‘𝑠)) | 
| 61 |  | eqid 2736 | . . . . . . . . . . . . . . . . 17
⊢
(ℤ≥‘𝑠) = (ℤ≥‘𝑠) | 
| 62 | 61 | uztrn2 12898 | . . . . . . . . . . . . . . . 16
⊢ (((𝑠 + 𝑡) ∈ (ℤ≥‘𝑠) ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘𝑠)) | 
| 63 | 60, 62 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘𝑠)) | 
| 64 |  | elfzuzb 13559 | . . . . . . . . . . . . . . 15
⊢ (𝑠 ∈ (0...𝑚) ↔ (𝑠 ∈ (ℤ≥‘0)
∧ 𝑚 ∈
(ℤ≥‘𝑠))) | 
| 65 | 55, 63, 64 | sylanbrc 583 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ (0...𝑚)) | 
| 66 |  | fznn0sub2 13676 | . . . . . . . . . . . . . 14
⊢ (𝑠 ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ (0...𝑚)) | 
| 67 | 65, 66 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (0...𝑚)) | 
| 68 |  | elfzelz 13565 | . . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈ ℤ) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℤ) | 
| 70 |  | eluz 12893 | . . . . . . . . . . . 12
⊢ (((𝑚 − 𝑠) ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚)) | 
| 71 | 69, 50, 70 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠)) ↔ (𝑚 − 𝑠) ≤ 𝑚)) | 
| 72 | 54, 71 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ (ℤ≥‘(𝑚 − 𝑠))) | 
| 73 |  | fzss2 13605 | . . . . . . . . . 10
⊢ (𝑚 ∈
(ℤ≥‘(𝑚 − 𝑠)) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚)) | 
| 74 | 72, 73 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆ (0...𝑚)) | 
| 75 | 74 | sselda 3982 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ (0...𝑚)) | 
| 76 | 13 | abscld 15476 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) | 
| 77 | 11, 12, 76 | syl2an 596 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘𝐴) ∈ ℝ) | 
| 78 | 36 | abscld 15476 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) | 
| 79 | 77, 78 | remulcld 11292 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 80 | 75, 79 | syldan 591 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 81 | 46, 80 | fsumrecl 15771 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 82 |  | fzfid 14015 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) | 
| 83 |  | elfznn0 13661 | . . . . . . . . . . . . 13
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (𝑚 − 𝑠) ∈
ℕ0) | 
| 84 | 67, 83 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈
ℕ0) | 
| 85 |  | peano2nn0 12568 | . . . . . . . . . . . 12
⊢ ((𝑚 − 𝑠) ∈ ℕ0 → ((𝑚 − 𝑠) + 1) ∈
ℕ0) | 
| 86 | 84, 85 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
ℕ0) | 
| 87 | 86, 30 | eleqtrdi 2850 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘0)) | 
| 88 |  | fzss1 13604 | . . . . . . . . . 10
⊢ (((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘0) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚)) | 
| 89 | 87, 88 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝑚 − 𝑠) + 1)...𝑚) ⊆ (0...𝑚)) | 
| 90 | 89 | sselda 3982 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (0...𝑚)) | 
| 91 | 90, 79 | syldan 591 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 92 | 82, 91 | fsumrecl 15771 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℝ) | 
| 93 | 42 | rphalfcld 13090 | . . . . . . . 8
⊢ (𝜑 → (𝐸 / 2) ∈
ℝ+) | 
| 94 | 93 | rpred 13078 | . . . . . . 7
⊢ (𝜑 → (𝐸 / 2) ∈ ℝ) | 
| 95 | 94 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℝ) | 
| 96 |  | elfznn0 13661 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℕ0) | 
| 97 | 11, 96, 76 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℝ) | 
| 98 | 46, 97 | fsumrecl 15771 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ) | 
| 99 | 98, 95 | remulcld 11292 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ) | 
| 100 |  | 0zd 12627 | . . . . . . . . . . 11
⊢ (𝜑 → 0 ∈
ℤ) | 
| 101 |  | eqidd 2737 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (𝐾‘𝑗)) | 
| 102 |  | mertens.2 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) | 
| 103 | 102, 76 | eqeltrd 2840 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) ∈ ℝ) | 
| 104 |  | mertens.7 | . . . . . . . . . . 11
⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
) | 
| 105 | 30, 100, 101, 103, 104 | isumrecl 15802 | . . . . . . . . . 10
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) | 
| 106 | 13 | absge0d 15484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) | 
| 107 | 106, 102 | breqtrrd 5170 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(𝐾‘𝑗)) | 
| 108 | 30, 100, 101, 103, 104, 107 | isumge0 15803 | . . . . . . . . . 10
⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0
(𝐾‘𝑗)) | 
| 109 | 105, 108 | ge0p1rpd 13108 | . . . . . . . . 9
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) | 
| 110 | 109 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) | 
| 111 | 99, 110 | rerpdivcld 13109 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) | 
| 112 | 93, 109 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈
ℝ+) | 
| 113 | 112 | rpred 13078 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) | 
| 114 | 113 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ) | 
| 115 | 97, 114 | remulcld 11292 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) ∈ ℝ) | 
| 116 | 75, 20 | syldan 591 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈ ℤ) | 
| 117 |  | simplll 774 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) | 
| 118 | 75, 19 | syldan 591 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) | 
| 119 | 118, 22 | sylan 580 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) | 
| 120 | 117, 119,
24 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) | 
| 121 | 117, 119,
26 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝐵 ∈ ℂ) | 
| 122 | 75, 35 | syldan 591 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → seq((𝑚 − 𝑗) + 1)( + , 𝐺) ∈ dom ⇝ ) | 
| 123 | 15, 116, 120, 121, 122 | isumcl 15798 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 ∈ ℂ) | 
| 124 | 123 | abscld 15476 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) | 
| 125 | 76, 106 | jca 511 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) | 
| 126 | 11, 96, 125 | syl2an 596 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) | 
| 127 | 120 | sumeq2dv 15739 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) | 
| 128 | 127 | fveq2d 6909 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) | 
| 129 |  | fvoveq1 7455 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = (𝑚 − 𝑗) → (ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘((𝑚 − 𝑗) + 1))) | 
| 130 | 129 | sumeq1d 15737 | . . . . . . . . . . . . . . 15
⊢ (𝑛 = (𝑚 − 𝑗) → Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) | 
| 131 | 130 | fveq2d 6909 | . . . . . . . . . . . . . 14
⊢ (𝑛 = (𝑚 − 𝑗) → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) | 
| 132 | 131 | breq1d 5152 | . . . . . . . . . . . . 13
⊢ (𝑛 = (𝑚 − 𝑗) → ((abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 133 | 4 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 134 | 133 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 135 |  | elfzelz 13565 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ∈ ℤ) | 
| 136 | 135 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℤ) | 
| 137 | 136 | zred 12724 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ∈ ℝ) | 
| 138 | 49 | ad2antlr 727 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℤ) | 
| 139 | 138 | zred 12724 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑚 ∈ ℝ) | 
| 140 | 56 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℤ) | 
| 141 | 140 | zred 12724 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ∈ ℝ) | 
| 142 |  | elfzle2 13569 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → 𝑗 ≤ (𝑚 − 𝑠)) | 
| 143 | 142 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑗 ≤ (𝑚 − 𝑠)) | 
| 144 | 137, 139,
141, 143 | lesubd 11868 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → 𝑠 ≤ (𝑚 − 𝑗)) | 
| 145 | 138, 136 | zsubcld 12729 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ ℤ) | 
| 146 |  | eluz 12893 | . . . . . . . . . . . . . . 15
⊢ ((𝑠 ∈ ℤ ∧ (𝑚 − 𝑗) ∈ ℤ) → ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗))) | 
| 147 | 140, 145,
146 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((𝑚 − 𝑗) ∈ (ℤ≥‘𝑠) ↔ 𝑠 ≤ (𝑚 − 𝑗))) | 
| 148 | 144, 147 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (𝑚 − 𝑗) ∈ (ℤ≥‘𝑠)) | 
| 149 | 132, 134,
148 | rspcdva 3622 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 150 | 128, 149 | eqbrtrrd 5166 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 151 | 124, 114,
150 | ltled 11410 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 152 |  | lemul2a 12123 | . . . . . . . . . 10
⊢
((((abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈ ℝ ∧
((abs‘𝐴) ∈
ℝ ∧ 0 ≤ (abs‘𝐴))) ∧ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 153 | 124, 114,
126, 151, 152 | syl31anc 1374 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 154 | 46, 80, 115, 153 | fsumle 15836 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 155 | 98 | recnd 11290 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℂ) | 
| 156 | 93 | rpcnd 13080 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸 / 2) ∈ ℂ) | 
| 157 | 156 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝐸 / 2) ∈ ℂ) | 
| 158 |  | peano2re 11435 | . . . . . . . . . . . . 13
⊢
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) ∈ ℝ → (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ) | 
| 159 | 105, 158 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ) | 
| 160 | 159 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℂ) | 
| 161 | 160 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℂ) | 
| 162 | 109 | rpne0d 13083 | . . . . . . . . . . 11
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ≠ 0) | 
| 163 | 162 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ≠ 0) | 
| 164 | 155, 157,
161, 163 | divassd 12079 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 165 |  | fveq2 6905 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗)) | 
| 166 | 165 | cbvsumv 15733 | . . . . . . . . . . . . . . . 16
⊢
Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) = Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) | 
| 167 | 166 | oveq1i 7442 | . . . . . . . . . . . . . . 15
⊢
(Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) + 1) = (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) | 
| 168 | 167 | oveq2i 7443 | . . . . . . . . . . . . . 14
⊢ ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0
(𝐾‘𝑛) + 1)) = ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) | 
| 169 | 168, 112 | eqeltrid 2844 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈
ℝ+) | 
| 170 | 169 | rpcnd 13080 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈ ℂ) | 
| 171 | 170 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)) ∈ ℂ) | 
| 172 | 76 | recnd 11290 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℂ) | 
| 173 | 11, 96, 172 | syl2an 596 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...(𝑚 − 𝑠))) → (abs‘𝐴) ∈ ℂ) | 
| 174 | 46, 171, 173 | fsummulc1 15822 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1)))) | 
| 175 | 168 | oveq2i 7443 | . . . . . . . . . 10
⊢
(Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 176 | 168 | oveq2i 7443 | . . . . . . . . . . . 12
⊢
((abs‘𝐴)
· ((𝐸 / 2) /
(Σ𝑛 ∈
ℕ0 (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 177 | 176 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑗 ∈ (0...(𝑚 − 𝑠)) → ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = ((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 178 | 177 | sumeq2i 15735 | . . . . . . . . . 10
⊢
Σ𝑗 ∈
(0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑛 ∈ ℕ0 (𝐾‘𝑛) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 179 | 174, 175,
178 | 3eqtr3g 2799 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 180 | 164, 179 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) = Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 181 | 154, 180 | breqtrrd 5170 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 182 | 105 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) | 
| 183 | 159 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ) | 
| 184 |  | 0zd 12627 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 0 ∈ ℤ) | 
| 185 |  | fz0ssnn0 13663 | . . . . . . . . . . . . 13
⊢
(0...(𝑚 −
𝑠)) ⊆
ℕ0 | 
| 186 | 185 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...(𝑚 − 𝑠)) ⊆
ℕ0) | 
| 187 | 102 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) | 
| 188 | 76 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) | 
| 189 | 106 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) | 
| 190 | 104 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → seq0( + , 𝐾) ∈ dom ⇝ ) | 
| 191 | 30, 184, 46, 186, 187, 188, 189, 190 | isumless 15882 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (abs‘𝐴)) | 
| 192 | 102 | sumeq2dv 15739 | . . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴)) | 
| 193 | 192 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) = Σ𝑗 ∈ ℕ0 (abs‘𝐴)) | 
| 194 | 191, 193 | breqtrrd 5170 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) ≤ Σ𝑗 ∈ ℕ0 (𝐾‘𝑗)) | 
| 195 | 105 | ltp1d 12199 | . . . . . . . . . . 11
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) | 
| 196 | 195 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) | 
| 197 | 98, 182, 183, 194, 196 | lelttrd 11420 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) | 
| 198 | 93 | rpregt0d 13084 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) | 
| 199 | 198 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) ∈ ℝ ∧ 0 < (𝐸 / 2))) | 
| 200 |  | ltmul1 12118 | . . . . . . . . . 10
⊢
((Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) ∈ ℝ ∧ (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ ∧ ((𝐸 / 2) ∈ ℝ ∧ 0
< (𝐸 / 2))) →
(Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) | 
| 201 | 98, 183, 199, 200 | syl3anc 1372 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) < (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) | 
| 202 | 197, 201 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2))) | 
| 203 | 109 | rpregt0d 13084 | . . . . . . . . . 10
⊢ (𝜑 → ((Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) | 
| 204 | 203 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) | 
| 205 |  | ltdivmul 12144 | . . . . . . . . 9
⊢
(((Σ𝑗 ∈
(0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) ∈ ℝ ∧ (𝐸 / 2) ∈ ℝ ∧
((Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1) ∈ ℝ ∧ 0 <
(Σ𝑗 ∈
ℕ0 (𝐾‘𝑗) + 1))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) | 
| 206 | 99, 95, 204, 205 | syl3anc 1372 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2) ↔ (Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) < ((Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) · (𝐸 / 2)))) | 
| 207 | 202, 206 | mpbird 257 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((Σ𝑗 ∈ (0...(𝑚 − 𝑠))(abs‘𝐴) · (𝐸 / 2)) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) < (𝐸 / 2)) | 
| 208 | 81, 111, 95, 181, 207 | lelttrd 11420 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2)) | 
| 209 |  | mertens.13 | . . . . . . . . . . . 12
⊢ (𝜑 → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) | 
| 210 | 209 | simprd 495 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) | 
| 211 |  | suprcl 12229 | . . . . . . . . . . 11
⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) → sup(𝑇, ℝ, < ) ∈
ℝ) | 
| 212 | 210, 211 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈
ℝ) | 
| 213 | 94, 212 | remulcld 11292 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) ∈
ℝ) | 
| 214 | 209 | simpld 494 | . . . . . . . . . 10
⊢ (𝜑 → 0 ≤ sup(𝑇, ℝ, <
)) | 
| 215 | 212, 214 | ge0p1rpd 13108 | . . . . . . . . 9
⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ+) | 
| 216 | 213, 215 | rerpdivcld 13109 | . . . . . . . 8
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) | 
| 217 | 216 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) | 
| 218 | 5 | nnrpd 13076 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑠 ∈ ℝ+) | 
| 219 | 93, 218 | rpdivcld 13095 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈
ℝ+) | 
| 220 | 219, 215 | rpdivcld 13095 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ+) | 
| 221 | 220 | rpred 13078 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) | 
| 222 | 221, 212 | remulcld 11292 | . . . . . . . . . 10
⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℝ) | 
| 223 | 222 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℝ) | 
| 224 |  | simpll 766 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝜑) | 
| 225 | 90, 12 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℕ0) | 
| 226 | 224, 225,
76 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ∈ ℝ) | 
| 227 | 221 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ) | 
| 228 | 224, 225,
102 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) = (abs‘𝐴)) | 
| 229 |  | fveq2 6905 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝑗 → (𝐾‘𝑚) = (𝐾‘𝑗)) | 
| 230 | 229 | breq1d 5152 | . . . . . . . . . . . . 13
⊢ (𝑚 = 𝑗 → ((𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 231 | 7 | simprd 495 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) | 
| 232 | 231 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∀𝑚 ∈ (ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) | 
| 233 |  | elfzuz 13561 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → 𝑗 ∈ (ℤ≥‘((𝑚 − 𝑠) + 1))) | 
| 234 |  | eluzle 12892 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡)) → (𝑠 + 𝑡) ≤ 𝑚) | 
| 235 | 234 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 + 𝑡) ≤ 𝑚) | 
| 236 | 8 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑡 ∈ ℤ) | 
| 237 | 236 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℤ) | 
| 238 | 237 | zred 12724 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ∈ ℝ) | 
| 239 | 52, 238, 51 | leaddsub2d 11866 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑠 + 𝑡) ≤ 𝑚 ↔ 𝑡 ≤ (𝑚 − 𝑠))) | 
| 240 | 235, 239 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑡 ≤ (𝑚 − 𝑠)) | 
| 241 |  | eluz 12893 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ ℤ ∧ (𝑚 − 𝑠) ∈ ℤ) → ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠))) | 
| 242 | 237, 69, 241 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) ↔ 𝑡 ≤ (𝑚 − 𝑠))) | 
| 243 | 240, 242 | mpbird 257 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ (ℤ≥‘𝑡)) | 
| 244 |  | peano2uz 12944 | . . . . . . . . . . . . . . 15
⊢ ((𝑚 − 𝑠) ∈ (ℤ≥‘𝑡) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) | 
| 245 | 243, 244 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) | 
| 246 |  | uztrn 12897 | . . . . . . . . . . . . . 14
⊢ ((𝑗 ∈
(ℤ≥‘((𝑚 − 𝑠) + 1)) ∧ ((𝑚 − 𝑠) + 1) ∈
(ℤ≥‘𝑡)) → 𝑗 ∈ (ℤ≥‘𝑡)) | 
| 247 | 233, 245,
246 | syl2anr 597 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ (ℤ≥‘𝑡)) | 
| 248 | 230, 232,
247 | rspcdva 3622 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝐾‘𝑗) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) | 
| 249 | 228, 248 | eqbrtrrd 5166 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) | 
| 250 | 226, 227,
249 | ltled 11410 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) | 
| 251 | 210 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) | 
| 252 | 51 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑚 ∈ ℝ) | 
| 253 |  | peano2zm 12662 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑠 ∈ ℤ → (𝑠 − 1) ∈
ℤ) | 
| 254 | 56, 253 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑠 − 1) ∈ ℤ) | 
| 255 | 254 | zred 12724 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑠 − 1) ∈ ℝ) | 
| 256 | 255 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℝ) | 
| 257 | 225 | nn0red 12590 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 𝑗 ∈ ℝ) | 
| 258 | 50 | zcnd 12725 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑚 ∈ ℂ) | 
| 259 | 52 | recnd 11290 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℂ) | 
| 260 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 1 ∈ ℂ) | 
| 261 | 258, 259,
260 | subsubd 11649 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1)) | 
| 262 | 261 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) = ((𝑚 − 𝑠) + 1)) | 
| 263 |  | elfzle1 13568 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚) → ((𝑚 − 𝑠) + 1) ≤ 𝑗) | 
| 264 | 263 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑠) + 1) ≤ 𝑗) | 
| 265 | 262, 264 | eqbrtrd 5164 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − (𝑠 − 1)) ≤ 𝑗) | 
| 266 | 252, 256,
257, 265 | subled 11867 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ≤ (𝑠 − 1)) | 
| 267 | 90, 16 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈
ℕ0) | 
| 268 | 267, 30 | eleqtrdi 2850 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈
(ℤ≥‘0)) | 
| 269 | 254 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑠 − 1) ∈ ℤ) | 
| 270 |  | elfz5 13557 | . . . . . . . . . . . . . . 15
⊢ (((𝑚 − 𝑗) ∈ (ℤ≥‘0)
∧ (𝑠 − 1) ∈
ℤ) → ((𝑚 −
𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1))) | 
| 271 | 268, 269,
270 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ↔ (𝑚 − 𝑗) ≤ (𝑠 − 1))) | 
| 272 | 266, 271 | mpbird 257 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (𝑚 − 𝑗) ∈ (0...(𝑠 − 1))) | 
| 273 |  | simplll 774 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝜑) | 
| 274 | 90, 19 | syldan 591 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((𝑚 − 𝑗) + 1) ∈
ℕ0) | 
| 275 | 274, 22 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → 𝑘 ∈ ℕ0) | 
| 276 | 273, 275,
24 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) ∧ 𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))) → (𝐺‘𝑘) = 𝐵) | 
| 277 | 276 | sumeq2dv 15739 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) | 
| 278 | 277 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵 = Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘)) | 
| 279 | 278 | fveq2d 6909 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) | 
| 280 | 131 | rspceeqv 3644 | . . . . . . . . . . . . 13
⊢ (((𝑚 − 𝑗) ∈ (0...(𝑠 − 1)) ∧ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))(𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) | 
| 281 | 272, 279,
280 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) | 
| 282 |  | fvex 6918 | . . . . . . . . . . . . 13
⊢
(abs‘Σ𝑘
∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ V | 
| 283 |  | eqeq1 2740 | . . . . . . . . . . . . . 14
⊢ (𝑧 = (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) | 
| 284 | 283 | rexbidv 3178 | . . . . . . . . . . . . 13
⊢ (𝑧 = (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) | 
| 285 |  | mertens.10 | . . . . . . . . . . . . 13
⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} | 
| 286 | 282, 284,
285 | elab2 3681 | . . . . . . . . . . . 12
⊢
((abs‘Σ𝑘
∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) | 
| 287 | 281, 286 | sylibr 234 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) | 
| 288 |  | suprub 12230 | . . . . . . . . . . 11
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) | 
| 289 | 251, 287,
288 | syl2anc 584 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) | 
| 290 | 224, 225,
125 | syl2anc 584 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) ∈ ℝ ∧ 0 ≤
(abs‘𝐴))) | 
| 291 | 90, 78 | syldan 591 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ) | 
| 292 | 36 | absge0d 15484 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) | 
| 293 | 90, 292 | syldan 591 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → 0 ≤ (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) | 
| 294 | 291, 293 | jca 511 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ∈ ℝ ∧ 0 ≤
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) | 
| 295 | 212 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → sup(𝑇, ℝ, < ) ∈
ℝ) | 
| 296 |  | lemul12a 12126 | . . . . . . . . . . 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(𝑇, ℝ, <
)))) | 
| 297 | 290, 227,
294, 295, 296 | syl22anc 838 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → (((abs‘𝐴) ≤ (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∧
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵) ≤ sup(𝑇, ℝ, < )) → ((abs‘𝐴) ·
(abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) | 
| 298 | 250, 289,
297 | mp2and 699 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) | 
| 299 | 82, 91, 223, 298 | fsumle 15836 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) | 
| 300 | 222 | recnd 11290 | . . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) | 
| 301 | 300 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) | 
| 302 |  | fsumconst 15827 | . . . . . . . . . 10
⊢
(((((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin ∧ ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) ∈
ℂ) → Σ𝑗
∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) =
((♯‘(((𝑚
− 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) | 
| 303 | 82, 301, 302 | syl2anc 584 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) =
((♯‘(((𝑚
− 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) | 
| 304 |  | 1zzd 12650 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 1 ∈ ℤ) | 
| 305 | 56 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝑠 ∈ ℤ) | 
| 306 |  | fzen 13582 | . . . . . . . . . . . . . 14
⊢ ((1
∈ ℤ ∧ 𝑠
∈ ℤ ∧ (𝑚
− 𝑠) ∈ ℤ)
→ (1...𝑠) ≈ ((1
+ (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠)))) | 
| 307 | 304, 305,
69, 306 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠)))) | 
| 308 |  | ax-1cn 11214 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℂ | 
| 309 | 69 | zcnd 12725 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℂ) | 
| 310 |  | addcom 11448 | . . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ (𝑚
− 𝑠) ∈ ℂ)
→ (1 + (𝑚 −
𝑠)) = ((𝑚 − 𝑠) + 1)) | 
| 311 | 308, 309,
310 | sylancr 587 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1 + (𝑚 − 𝑠)) = ((𝑚 − 𝑠) + 1)) | 
| 312 | 259, 258 | pncan3d 11624 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 + (𝑚 − 𝑠)) = 𝑚) | 
| 313 | 311, 312 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((1 + (𝑚 − 𝑠))...(𝑠 + (𝑚 − 𝑠))) = (((𝑚 − 𝑠) + 1)...𝑚)) | 
| 314 | 307, 313 | breqtrd 5168 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚)) | 
| 315 |  | fzfid 14015 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (1...𝑠) ∈ Fin) | 
| 316 |  | hashen 14387 | . . . . . . . . . . . . 13
⊢
(((1...𝑠) ∈ Fin
∧ (((𝑚 − 𝑠) + 1)...𝑚) ∈ Fin) →
((♯‘(1...𝑠)) =
(♯‘(((𝑚 −
𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))) | 
| 317 | 315, 82, 316 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) ↔ (1...𝑠) ≈ (((𝑚 − 𝑠) + 1)...𝑚))) | 
| 318 | 314, 317 | mpbird 257 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = (♯‘(((𝑚 − 𝑠) + 1)...𝑚))) | 
| 319 |  | hashfz1 14386 | . . . . . . . . . . . 12
⊢ (𝑠 ∈ ℕ0
→ (♯‘(1...𝑠)) = 𝑠) | 
| 320 | 47, 319 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (♯‘(1...𝑠)) = 𝑠) | 
| 321 | 318, 320 | eqtr3d 2778 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (♯‘(((𝑚 − 𝑠) + 1)...𝑚)) = 𝑠) | 
| 322 | 321 | oveq1d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((♯‘(((𝑚 − 𝑠) + 1)...𝑚)) · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) | 
| 323 | 212 | recnd 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → sup(𝑇, ℝ, < ) ∈
ℂ) | 
| 324 | 215 | rpcnne0d 13087 | . . . . . . . . . . . 12
⊢ (𝜑 → ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧
(sup(𝑇, ℝ, < ) +
1) ≠ 0)) | 
| 325 |  | div23 11942 | . . . . . . . . . . . 12
⊢ (((𝐸 / 2) ∈ ℂ ∧
sup(𝑇, ℝ, < )
∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈ ℂ ∧
(sup(𝑇, ℝ, < ) +
1) ≠ 0)) → (((𝐸 /
2) · sup(𝑇, ℝ,
< )) / (sup(𝑇, ℝ,
< ) + 1)) = (((𝐸 / 2) /
(sup(𝑇, ℝ, < ) +
1)) · sup(𝑇,
ℝ, < ))) | 
| 326 | 156, 323,
324, 325 | syl3anc 1372 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) | 
| 327 | 56 | zcnd 12725 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑠 ∈ ℂ) | 
| 328 | 219 | rpcnd 13080 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸 / 2) / 𝑠) ∈ ℂ) | 
| 329 |  | divass 11941 | . . . . . . . . . . . . . 14
⊢ ((𝑠 ∈ ℂ ∧ ((𝐸 / 2) / 𝑠) ∈ ℂ ∧ ((sup(𝑇, ℝ, < ) + 1) ∈
ℂ ∧ (sup(𝑇,
ℝ, < ) + 1) ≠ 0)) → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 330 | 327, 328,
324, 329 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 331 | 5 | nnne0d 12317 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑠 ≠ 0) | 
| 332 | 156, 327,
331 | divcan2d 12046 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑠 · ((𝐸 / 2) / 𝑠)) = (𝐸 / 2)) | 
| 333 | 332 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑠 · ((𝐸 / 2) / 𝑠)) / (sup(𝑇, ℝ, < ) + 1)) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1))) | 
| 334 | 330, 333 | eqtr3d 2778 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) = ((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1))) | 
| 335 | 334 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
))) | 
| 336 | 220 | rpcnd 13080 | . . . . . . . . . . . 12
⊢ (𝜑 → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℂ) | 
| 337 | 327, 336,
323 | mulassd 11285 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝑠 · (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) · sup(𝑇, ℝ, < )) = (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, <
)))) | 
| 338 | 326, 335,
337 | 3eqtr2rd 2783 | . . . . . . . . . 10
⊢ (𝜑 → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) | 
| 339 | 338 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑠 · ((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < ))) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) | 
| 340 | 303, 322,
339 | 3eqtrd 2780 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) · sup(𝑇, ℝ, < )) = (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) +
1))) | 
| 341 | 299, 340 | breqtrd 5168 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ≤ (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1))) | 
| 342 |  | peano2re 11435 | . . . . . . . . . . 11
⊢
(sup(𝑇, ℝ,
< ) ∈ ℝ → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ) | 
| 343 | 212, 342 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ) | 
| 344 | 212 | ltp1d 12199 | . . . . . . . . . 10
⊢ (𝜑 → sup(𝑇, ℝ, < ) < (sup(𝑇, ℝ, < ) +
1)) | 
| 345 | 212, 343,
93, 344 | ltmul2dd 13134 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1))) | 
| 346 | 213, 94, 215 | ltdivmul2d 13130 | . . . . . . . . 9
⊢ (𝜑 → ((((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2) ↔ ((𝐸 / 2) · sup(𝑇, ℝ, < )) < ((𝐸 / 2) · (sup(𝑇, ℝ, < ) + 1)))) | 
| 347 | 345, 346 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2)) | 
| 348 | 347 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (((𝐸 / 2) · sup(𝑇, ℝ, < )) / (sup(𝑇, ℝ, < ) + 1)) < (𝐸 / 2)) | 
| 349 | 92, 217, 95, 341, 348 | lelttrd 11420 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < (𝐸 / 2)) | 
| 350 | 81, 92, 95, 95, 208, 349 | lt2addd 11887 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) < ((𝐸 / 2) + (𝐸 / 2))) | 
| 351 | 14, 36 | absmuld 15494 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → (abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) | 
| 352 | 351 | sumeq2dv 15739 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) | 
| 353 | 69 | zred 12724 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) ∈ ℝ) | 
| 354 | 353 | ltp1d 12199 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1)) | 
| 355 |  | fzdisj 13592 | . . . . . . . 8
⊢ ((𝑚 − 𝑠) < ((𝑚 − 𝑠) + 1) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅) | 
| 356 | 354, 355 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((0...(𝑚 − 𝑠)) ∩ (((𝑚 − 𝑠) + 1)...𝑚)) = ∅) | 
| 357 |  | fzsplit 13591 | . . . . . . . 8
⊢ ((𝑚 − 𝑠) ∈ (0...𝑚) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚))) | 
| 358 | 67, 357 | syl 17 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (0...𝑚) = ((0...(𝑚 − 𝑠)) ∪ (((𝑚 − 𝑠) + 1)...𝑚))) | 
| 359 | 79 | recnd 11290 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) ∧ 𝑗 ∈ (0...𝑚)) → ((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) ∈ ℂ) | 
| 360 | 356, 358,
10, 359 | fsumsplit 15778 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) = (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)))) | 
| 361 | 352, 360 | eqtr2d 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (Σ𝑗 ∈ (0...(𝑚 − 𝑠))((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) + Σ𝑗 ∈ (((𝑚 − 𝑠) + 1)...𝑚)((abs‘𝐴) · (abs‘Σ𝑘 ∈
(ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) = Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵))) | 
| 362 | 42 | rpcnd 13080 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 363 | 362 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → 𝐸 ∈ ℂ) | 
| 364 | 363 | 2halvesd 12514 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → ((𝐸 / 2) + (𝐸 / 2)) = 𝐸) | 
| 365 | 350, 361,
364 | 3brtr3d 5173 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → Σ𝑗 ∈ (0...𝑚)(abs‘(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | 
| 366 | 39, 41, 44, 45, 365 | lelttrd 11420 | . . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))) → (abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | 
| 367 | 366 | ralrimiva 3145 | . 2
⊢ (𝜑 → ∀𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | 
| 368 |  | fveq2 6905 | . . . 4
⊢ (𝑦 = (𝑠 + 𝑡) → (ℤ≥‘𝑦) =
(ℤ≥‘(𝑠 + 𝑡))) | 
| 369 | 368 | raleqdv 3325 | . . 3
⊢ (𝑦 = (𝑠 + 𝑡) → (∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸 ↔ ∀𝑚 ∈ (ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 370 | 369 | rspcev 3621 | . 2
⊢ (((𝑠 + 𝑡) ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘(𝑠 + 𝑡))(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | 
| 371 | 9, 367, 370 | syl2anc 584 | 1
⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |