| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nnuz 12921 | . . 3
⊢ ℕ =
(ℤ≥‘1) | 
| 2 |  | 1zzd 12648 | . . 3
⊢ (𝜑 → 1 ∈
ℤ) | 
| 3 |  | mertens.9 | . . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) | 
| 4 | 3 | rphalfcld 13089 | . . . 4
⊢ (𝜑 → (𝐸 / 2) ∈
ℝ+) | 
| 5 |  | nn0uz 12920 | . . . . . 6
⊢
ℕ0 = (ℤ≥‘0) | 
| 6 |  | 0zd 12625 | . . . . . 6
⊢ (𝜑 → 0 ∈
ℤ) | 
| 7 |  | eqidd 2738 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (𝐾‘𝑗)) | 
| 8 |  | mertens.2 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) | 
| 9 |  | mertens.3 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈
ℂ) | 
| 10 | 9 | abscld 15475 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) | 
| 11 | 8, 10 | eqeltrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) ∈ ℝ) | 
| 12 |  | mertens.7 | . . . . . 6
⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
) | 
| 13 | 5, 6, 7, 11, 12 | isumrecl 15801 | . . . . 5
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) | 
| 14 | 9 | absge0d 15483 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) | 
| 15 | 14, 8 | breqtrrd 5171 | . . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(𝐾‘𝑗)) | 
| 16 | 5, 6, 7, 11, 12, 15 | isumge0 15802 | . . . . 5
⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0
(𝐾‘𝑗)) | 
| 17 | 13, 16 | ge0p1rpd 13107 | . . . 4
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) | 
| 18 | 4, 17 | rpdivcld 13094 | . . 3
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈
ℝ+) | 
| 19 |  | eqidd 2738 | . . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) = (seq0( + , 𝐺)‘𝑚)) | 
| 20 |  | mertens.4 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) | 
| 21 |  | mertens.5 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) | 
| 22 |  | mertens.8 | . . . 4
⊢ (𝜑 → seq0( + , 𝐺) ∈ dom ⇝
) | 
| 23 | 5, 6, 20, 21, 22 | isumclim2 15794 | . . 3
⊢ (𝜑 → seq0( + , 𝐺) ⇝ Σ𝑘 ∈ ℕ0
𝐵) | 
| 24 | 1, 2, 18, 19, 23 | climi2 15547 | . 2
⊢ (𝜑 → ∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 25 |  | eluznn 12960 | . . . . . . . 8
⊢ ((𝑠 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘𝑠)) → 𝑚 ∈ ℕ) | 
| 26 | 20, 21 | eqeltrd 2841 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) | 
| 27 | 5, 6, 26 | serf 14071 | . . . . . . . . . . . 12
⊢ (𝜑 → seq0( + , 𝐺):ℕ0⟶ℂ) | 
| 28 |  | nnnn0 12533 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) | 
| 29 |  | ffvelcdm 7101 | . . . . . . . . . . . 12
⊢ ((seq0( +
, 𝐺):ℕ0⟶ℂ ∧
𝑚 ∈
ℕ0) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ) | 
| 30 | 27, 28, 29 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ) | 
| 31 | 5, 6, 20, 21, 22 | isumcl 15797 | . . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ) | 
| 32 | 31 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0
𝐵 ∈
ℂ) | 
| 33 | 30, 32 | abssubd 15492 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) =
(abs‘(Σ𝑘 ∈
ℕ0 𝐵
− (seq0( + , 𝐺)‘𝑚)))) | 
| 34 |  | eqid 2737 | . . . . . . . . . . . . . 14
⊢
(ℤ≥‘(𝑚 + 1)) = (ℤ≥‘(𝑚 + 1)) | 
| 35 | 28 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0) | 
| 36 |  | peano2nn0 12566 | . . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) | 
| 37 | 35, 36 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈
ℕ0) | 
| 38 | 37 | nn0zd 12639 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℤ) | 
| 39 |  | simpll 767 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝜑) | 
| 40 |  | eluznn0 12959 | . . . . . . . . . . . . . . . 16
⊢ (((𝑚 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑚 + 1))) → 𝑘 ∈ ℕ0) | 
| 41 | 37, 40 | sylan 580 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝑘 ∈
ℕ0) | 
| 42 | 39, 41, 20 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → (𝐺‘𝑘) = 𝐵) | 
| 43 | 39, 41, 21 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝐵 ∈ ℂ) | 
| 44 | 22 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → seq0( + , 𝐺) ∈ dom ⇝
) | 
| 45 | 26 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) | 
| 46 | 5, 37, 45 | iserex 15693 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝
)) | 
| 47 | 44, 46 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ ) | 
| 48 | 34, 38, 42, 43, 47 | isumcl 15797 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))𝐵 ∈ ℂ) | 
| 49 | 30, 48 | pncan2d 11622 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) | 
| 50 | 20 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) | 
| 51 | 21 | adantlr 715 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) | 
| 52 | 5, 34, 37, 50, 51, 44 | isumsplit 15876 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0
𝐵 = (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)) | 
| 53 |  | nncn 12274 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) | 
| 54 | 53 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) | 
| 55 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ | 
| 56 |  | pncan 11514 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑚 + 1)
− 1) = 𝑚) | 
| 57 | 54, 55, 56 | sylancl 586 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) − 1) = 𝑚) | 
| 58 | 57 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...((𝑚 + 1) − 1)) = (0...𝑚)) | 
| 59 | 58 | sumeq1d 15736 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = Σ𝑘 ∈ (0...𝑚)𝐵) | 
| 60 |  | simpl 482 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝜑) | 
| 61 |  | elfznn0 13660 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ0) | 
| 62 | 60, 61, 20 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑚)) → (𝐺‘𝑘) = 𝐵) | 
| 63 | 35, 5 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
(ℤ≥‘0)) | 
| 64 | 60, 61, 21 | syl2an 596 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑚)) → 𝐵 ∈ ℂ) | 
| 65 | 62, 63, 64 | fsumser 15766 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑚)𝐵 = (seq0( + , 𝐺)‘𝑚)) | 
| 66 | 59, 65 | eqtrd 2777 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = (seq0( + , 𝐺)‘𝑚)) | 
| 67 | 66 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)) | 
| 68 | 52, 67 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0
𝐵 = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)) | 
| 69 | 68 | oveq1d 7446 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0
𝐵 − (seq0( + , 𝐺)‘𝑚)) = (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚))) | 
| 70 | 42 | sumeq2dv 15738 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) | 
| 71 | 49, 69, 70 | 3eqtr4d 2787 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0
𝐵 − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) | 
| 72 | 71 | fveq2d 6910 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(abs‘(Σ𝑘 ∈
ℕ0 𝐵
− (seq0( + , 𝐺)‘𝑚))) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘))) | 
| 73 | 33, 72 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) =
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘))) | 
| 74 | 73 | breq1d 5153 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 75 | 25, 74 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑠))) → ((abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 76 | 75 | anassrs 467 | . . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑠)) → ((abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 77 | 76 | ralbidva 3176 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 78 |  | fvoveq1 7454 | . . . . . . . . 9
⊢ (𝑚 = 𝑛 → (ℤ≥‘(𝑚 + 1)) =
(ℤ≥‘(𝑛 + 1))) | 
| 79 | 78 | sumeq1d 15736 | . . . . . . . 8
⊢ (𝑚 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) | 
| 80 | 79 | fveq2d 6910 | . . . . . . 7
⊢ (𝑚 = 𝑛 → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) | 
| 81 | 80 | breq1d 5153 | . . . . . 6
⊢ (𝑚 = 𝑛 → ((abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 82 | 81 | cbvralvw 3237 | . . . . 5
⊢
(∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) | 
| 83 | 77, 82 | bitrdi 287 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 84 |  | mertens.11 | . . . . . 6
⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) | 
| 85 |  | 0zd 12625 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℤ) | 
| 86 | 4 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝐸 / 2) ∈
ℝ+) | 
| 87 | 84 | simplbi 497 | . . . . . . . . . . . . 13
⊢ (𝜓 → 𝑠 ∈ ℕ) | 
| 88 | 87 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑠 ∈ ℕ) | 
| 89 | 88 | nnrpd 13075 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑠 ∈ ℝ+) | 
| 90 | 86, 89 | rpdivcld 13094 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝐸 / 2) / 𝑠) ∈
ℝ+) | 
| 91 |  | mertens.10 | . . . . . . . . . . . . 13
⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} | 
| 92 |  | eqid 2737 | . . . . . . . . . . . . . . . . . 18
⊢
(ℤ≥‘(𝑛 + 1)) = (ℤ≥‘(𝑛 + 1)) | 
| 93 |  | elfznn0 13660 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (0...(𝑠 − 1)) → 𝑛 ∈ ℕ0) | 
| 94 | 93 | adantl 481 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝑛 ∈ ℕ0) | 
| 95 |  | peano2nn0 12566 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ0) | 
| 96 | 94, 95 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈
ℕ0) | 
| 97 | 96 | nn0zd 12639 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℤ) | 
| 98 |  | eqidd 2738 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) = (𝐺‘𝑘)) | 
| 99 |  | simplll 775 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝜑) | 
| 100 |  | eluznn0 12959 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑘 ∈ ℕ0) | 
| 101 | 96, 100 | sylan 580 | . . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑘 ∈
ℕ0) | 
| 102 | 99, 101, 26 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) ∈ ℂ) | 
| 103 | 22 | ad2antrr 726 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq0( + , 𝐺) ∈ dom ⇝
) | 
| 104 | 26 | ad4ant14 752 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) | 
| 105 | 5, 96, 104 | iserex 15693 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝
)) | 
| 106 | 103, 105 | mpbid 232 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ ) | 
| 107 | 92, 97, 98, 102, 106 | isumcl 15797 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) ∈ ℂ) | 
| 108 | 107 | abscld 15475 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ∈ ℝ) | 
| 109 |  | eleq1a 2836 | . . . . . . . . . . . . . . . 16
⊢
((abs‘Σ𝑘
∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ∈ ℝ → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ)) | 
| 110 | 108, 109 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ)) | 
| 111 | 110 | rexlimdva 3155 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ)) | 
| 112 | 111 | abssdv 4068 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ⊆ ℝ) | 
| 113 | 91, 112 | eqsstrid 4022 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ ℝ) | 
| 114 |  | fzfid 14014 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (0...(𝑠 − 1)) ∈ Fin) | 
| 115 |  | abrexfi 9392 | . . . . . . . . . . . . . . 15
⊢
((0...(𝑠 − 1))
∈ Fin → {𝑧
∣ ∃𝑛 ∈
(0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ∈ Fin) | 
| 116 | 114, 115 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ∈ Fin) | 
| 117 | 91, 116 | eqeltrid 2845 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ Fin) | 
| 118 |  | nnm1nn0 12567 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ ℕ → (𝑠 − 1) ∈
ℕ0) | 
| 119 | 88, 118 | syl 17 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (𝑠 − 1) ∈
ℕ0) | 
| 120 | 119, 5 | eleqtrdi 2851 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (𝑠 − 1) ∈
(ℤ≥‘0)) | 
| 121 |  | eluzfz1 13571 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑠 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑠 − 1))) | 
| 122 | 120, 121 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 0 ∈ (0...(𝑠 − 1))) | 
| 123 |  | nnnn0 12533 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) | 
| 124 | 123, 20 | sylan2 593 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = 𝐵) | 
| 125 | 124 | sumeq2dv 15738 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐺‘𝑘) = Σ𝑘 ∈ ℕ 𝐵) | 
| 126 | 125 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ ℕ (𝐺‘𝑘) = Σ𝑘 ∈ ℕ 𝐵) | 
| 127 | 126 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ ℕ 𝐵)) | 
| 128 | 127 | eqcomd 2743 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘))) | 
| 129 |  | fv0p1e1 12389 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 0 →
(ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘1)) | 
| 130 | 129, 1 | eqtr4di 2795 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 0 →
(ℤ≥‘(𝑛 + 1)) = ℕ) | 
| 131 | 130 | sumeq1d 15736 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 → Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ ℕ (𝐺‘𝑘)) | 
| 132 | 131 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 →
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘))) | 
| 133 | 132 | rspceeqv 3645 | . . . . . . . . . . . . . . . 16
⊢ ((0
∈ (0...(𝑠 − 1))
∧ (abs‘Σ𝑘
∈ ℕ 𝐵) =
(abs‘Σ𝑘 ∈
ℕ (𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) | 
| 134 | 122, 128,
133 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) | 
| 135 |  | fvex 6919 | . . . . . . . . . . . . . . . 16
⊢
(abs‘Σ𝑘
∈ ℕ 𝐵) ∈
V | 
| 136 |  | eqeq1 2741 | . . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) | 
| 137 | 136 | rexbidv 3179 | . . . . . . . . . . . . . . . 16
⊢ (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) | 
| 138 | 135, 137,
91 | elab2 3682 | . . . . . . . . . . . . . . 15
⊢
((abs‘Σ𝑘
∈ ℕ 𝐵) ∈
𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) | 
| 139 | 134, 138 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇) | 
| 140 | 139 | ne0d 4342 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ≠ ∅) | 
| 141 |  | ltso 11341 | . . . . . . . . . . . . . 14
⊢  < Or
ℝ | 
| 142 |  | fisupcl 9509 | . . . . . . . . . . . . . 14
⊢ (( <
Or ℝ ∧ (𝑇 ∈
Fin ∧ 𝑇 ≠ ∅
∧ 𝑇 ⊆ ℝ))
→ sup(𝑇, ℝ, <
) ∈ 𝑇) | 
| 143 | 141, 142 | mpan 690 | . . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ) →
sup(𝑇, ℝ, < )
∈ 𝑇) | 
| 144 | 117, 140,
113, 143 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → sup(𝑇, ℝ, < ) ∈ 𝑇) | 
| 145 | 113, 144 | sseldd 3984 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → sup(𝑇, ℝ, < ) ∈
ℝ) | 
| 146 |  | 0red 11264 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℝ) | 
| 147 | 123, 21 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ) | 
| 148 |  | 1nn0 12542 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ0 | 
| 149 | 148 | a1i 11 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℕ0) | 
| 150 | 5, 149, 26 | iserex 15693 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq1( + , 𝐺) ∈ dom
⇝ )) | 
| 151 | 22, 150 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝
) | 
| 152 | 1, 2, 124, 147, 151 | isumcl 15797 | . . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ) | 
| 153 | 152 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ) | 
| 154 | 153 | abscld 15475 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈
ℝ) | 
| 155 | 153 | absge0d 15483 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 0 ≤ (abs‘Σ𝑘 ∈ ℕ 𝐵)) | 
| 156 |  | fimaxre2 12213 | . . . . . . . . . . . . . 14
⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) | 
| 157 | 113, 117,
156 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) | 
| 158 | 113, 140,
157, 139 | suprubd 12230 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ≤ sup(𝑇, ℝ, < )) | 
| 159 | 146, 154,
145, 155, 158 | letrd 11418 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 0 ≤ sup(𝑇, ℝ, < )) | 
| 160 | 145, 159 | ge0p1rpd 13107 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ+) | 
| 161 | 90, 160 | rpdivcld 13094 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ+) | 
| 162 |  | fveq2 6906 | . . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚)) | 
| 163 |  | eqid 2737 | . . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) | 
| 164 |  | fvex 6919 | . . . . . . . . . . 11
⊢ (𝐾‘𝑚) ∈ V | 
| 165 | 162, 163,
164 | fvmpt 7016 | . . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐾‘𝑛))‘𝑚) = (𝐾‘𝑚)) | 
| 166 | 165 | adantl 481 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑚) = (𝐾‘𝑚)) | 
| 167 |  | nn0ex 12532 | . . . . . . . . . . . . 13
⊢
ℕ0 ∈ V | 
| 168 | 167 | mptex 7243 | . . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛)) ∈ V | 
| 169 | 168 | a1i 11 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ∈ V) | 
| 170 |  | elnn0uz 12923 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
↔ 𝑗 ∈
(ℤ≥‘0)) | 
| 171 |  | fveq2 6906 | . . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗)) | 
| 172 |  | fvex 6919 | . . . . . . . . . . . . . . . 16
⊢ (𝐾‘𝑗) ∈ V | 
| 173 | 171, 163,
172 | fvmpt 7016 | . . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗)) | 
| 174 | 173 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗)) | 
| 175 | 170, 174 | sylan2br 595 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘0))
→ ((𝑛 ∈
ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗)) | 
| 176 | 6, 175 | seqfeq 14068 | . . . . . . . . . . . 12
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))) = seq0( + , 𝐾)) | 
| 177 | 176, 12 | eqeltrd 2841 | . . . . . . . . . . 11
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))) ∈ dom ⇝
) | 
| 178 | 174, 8 | eqtrd 2777 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) = (abs‘𝐴)) | 
| 179 | 178, 10 | eqeltrd 2841 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) ∈ ℝ) | 
| 180 | 179 | recnd 11289 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) ∈ ℂ) | 
| 181 | 5, 6, 169, 177, 180 | serf0 15717 | . . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ⇝ 0) | 
| 182 | 181 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ⇝ 0) | 
| 183 | 5, 85, 161, 166, 182 | climi0 15548 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ∃𝑡 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) | 
| 184 |  | simplll 775 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → 𝜑) | 
| 185 |  | eluznn0 12959 | . . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑡)) → 𝑚 ∈ ℕ0) | 
| 186 | 185 | adantll 714 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → 𝑚 ∈ ℕ0) | 
| 187 | 11, 15 | absidd 15461 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘(𝐾‘𝑗)) = (𝐾‘𝑗)) | 
| 188 | 187 | ralrimiva 3146 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑗 ∈ ℕ0 (abs‘(𝐾‘𝑗)) = (𝐾‘𝑗)) | 
| 189 |  | fveq2 6906 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚)) | 
| 190 | 189 | fveq2d 6910 | . . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑚 → (abs‘(𝐾‘𝑗)) = (abs‘(𝐾‘𝑚))) | 
| 191 | 190, 189 | eqeq12d 2753 | . . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑚 → ((abs‘(𝐾‘𝑗)) = (𝐾‘𝑗) ↔ (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚))) | 
| 192 | 191 | rspccva 3621 | . . . . . . . . . . . . . . 15
⊢
((∀𝑗 ∈
ℕ0 (abs‘(𝐾‘𝑗)) = (𝐾‘𝑗) ∧ 𝑚 ∈ ℕ0) →
(abs‘(𝐾‘𝑚)) = (𝐾‘𝑚)) | 
| 193 | 188, 192 | sylan 580 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(abs‘(𝐾‘𝑚)) = (𝐾‘𝑚)) | 
| 194 | 184, 186,
193 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚)) | 
| 195 | 194 | breq1d 5153 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → ((abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 196 | 195 | ralbidva 3176 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 197 | 162 | breq1d 5153 | . . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 198 | 197 | cbvralvw 3237 | . . . . . . . . . . 11
⊢
(∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) | 
| 199 | 196, 198 | bitr4di 289 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 200 |  | mertens.1 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴) | 
| 201 | 200 | ad4ant14 752 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0)
→ (𝐹‘𝑗) = 𝐴) | 
| 202 | 8 | ad4ant14 752 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0)
→ (𝐾‘𝑗) = (abs‘𝐴)) | 
| 203 | 9 | ad4ant14 752 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0)
→ 𝐴 ∈
ℂ) | 
| 204 | 20 | ad4ant14 752 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0)
→ (𝐺‘𝑘) = 𝐵) | 
| 205 | 21 | ad4ant14 752 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0)
→ 𝐵 ∈
ℂ) | 
| 206 |  | mertens.6 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) | 
| 207 | 206 | ad4ant14 752 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0)
→ (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) | 
| 208 | 12 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → seq0( + ,
𝐾) ∈ dom ⇝
) | 
| 209 | 22 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → seq0( + ,
𝐺) ∈ dom ⇝
) | 
| 210 | 3 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → 𝐸 ∈
ℝ+) | 
| 211 | 198 | anbi2i 623 | . . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℕ0
∧ ∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) ↔ (𝑡 ∈ ℕ0
∧ ∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) | 
| 212 | 211 | anbi2i 623 | . . . . . . . . . . . . . 14
⊢ ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ↔ (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) | 
| 213 | 212 | biimpi 216 | . . . . . . . . . . . . 13
⊢ ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) | 
| 214 | 213 | adantll 714 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) | 
| 215 | 113, 140,
157 | 3jca 1129 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) | 
| 216 | 159, 215 | jca 511 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) | 
| 217 | 216 | adantr 480 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (0 ≤
sup(𝑇, ℝ, < )
∧ (𝑇 ⊆ ℝ
∧ 𝑇 ≠ ∅ ∧
∃𝑧 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) | 
| 218 | 201, 202,
203, 204, 205, 207, 208, 209, 210, 91, 84, 214, 217 | mertenslem1 15920 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) →
∃𝑦 ∈
ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | 
| 219 | 218 | expr 456 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0
∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 220 | 199, 219 | sylbid 240 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0
∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 221 | 220 | rexlimdva 3155 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (∃𝑡 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0
∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 222 | 183, 221 | mpd 15 | . . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) | 
| 223 | 222 | ex 412 | . . . . . 6
⊢ (𝜑 → (𝜓 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 224 | 84, 223 | biimtrrid 243 | . . . . 5
⊢ (𝜑 → ((𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 225 | 224 | expdimp 452 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 226 | 83, 225 | sylbid 240 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 227 | 226 | rexlimdva 3155 | . 2
⊢ (𝜑 → (∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) | 
| 228 | 24, 227 | mpd 15 | 1
⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |