Step | Hyp | Ref
| Expression |
1 | | nnuz 11723 |
. . 3
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 11408 |
. . 3
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | mertens.9 |
. . . . 5
⊢ (𝜑 → 𝐸 ∈
ℝ+) |
4 | 3 | rphalfcld 11884 |
. . . 4
⊢ (𝜑 → (𝐸 / 2) ∈
ℝ+) |
5 | | nn0uz 11722 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
6 | | 0zd 11389 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℤ) |
7 | | eqidd 2623 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (𝐾‘𝑗)) |
8 | | mertens.2 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) = (abs‘𝐴)) |
9 | | mertens.3 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈
ℂ) |
10 | 9 | abscld 14175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘𝐴) ∈
ℝ) |
11 | 8, 10 | eqeltrd 2701 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐾‘𝑗) ∈ ℝ) |
12 | | mertens.7 |
. . . . . 6
⊢ (𝜑 → seq0( + , 𝐾) ∈ dom ⇝
) |
13 | 5, 6, 7, 11, 12 | isumrecl 14496 |
. . . . 5
⊢ (𝜑 → Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) ∈ ℝ) |
14 | 9 | absge0d 14183 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(abs‘𝐴)) |
15 | 14, 8 | breqtrrd 4681 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 0 ≤
(𝐾‘𝑗)) |
16 | 5, 6, 7, 11, 12, 15 | isumge0 14497 |
. . . . 5
⊢ (𝜑 → 0 ≤ Σ𝑗 ∈ ℕ0
(𝐾‘𝑗)) |
17 | 13, 16 | ge0p1rpd 11902 |
. . . 4
⊢ (𝜑 → (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1) ∈
ℝ+) |
18 | 4, 17 | rpdivcld 11889 |
. . 3
⊢ (𝜑 → ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ∈
ℝ+) |
19 | | eqidd 2623 |
. . 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 14489 |
. . 3
⊢ (𝜑 → seq0( + , 𝐺) ⇝ Σ𝑘 ∈ ℕ0
𝐵) |
24 | 1, 2, 18, 19, 23 | climi2 14242 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
25 | | eluznn 11758 |
. . . . . . . 8
⊢ ((𝑠 ∈ ℕ ∧ 𝑚 ∈
(ℤ≥‘𝑠)) → 𝑚 ∈ ℕ) |
26 | 20, 21 | eqeltrd 2701 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
27 | 5, 6, 26 | serf 12829 |
. . . . . . . . . . . 12
⊢ (𝜑 → seq0( + , 𝐺):ℕ0⟶ℂ) |
28 | | nnnn0 11299 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℕ0) |
29 | | ffvelrn 6357 |
. . . . . . . . . . . 12
⊢ ((seq0( +
, 𝐺):ℕ0⟶ℂ ∧
𝑚 ∈
ℕ0) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ) |
30 | 27, 28, 29 | syl2an 494 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺)‘𝑚) ∈ ℂ) |
31 | 5, 6, 20, 21, 22 | isumcl 14492 |
. . . . . . . . . . . 12
⊢ (𝜑 → Σ𝑘 ∈ ℕ0 𝐵 ∈ ℂ) |
32 | 31 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0
𝐵 ∈
ℂ) |
33 | 30, 32 | abssubd 14192 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) =
(abs‘(Σ𝑘 ∈
ℕ0 𝐵
− (seq0( + , 𝐺)‘𝑚)))) |
34 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘(𝑚 + 1)) = (ℤ≥‘(𝑚 + 1)) |
35 | 28 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ0) |
36 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈
ℕ0) |
38 | 37 | nn0zd 11480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (𝑚 + 1) ∈ ℤ) |
39 | | simpll 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝜑) |
40 | | eluznn0 11757 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑚 + 1))) → 𝑘 ∈ ℕ0) |
41 | 37, 40 | sylan 488 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝑘 ∈
ℕ0) |
42 | 39, 41, 20 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → (𝐺‘𝑘) = 𝐵) |
43 | 39, 41, 21 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (ℤ≥‘(𝑚 + 1))) → 𝐵 ∈ ℂ) |
44 | 22 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → seq0( + , 𝐺) ∈ dom ⇝
) |
45 | 26 | adantlr 751 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
46 | 5, 37, 45 | iserex 14387 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝
)) |
47 | 44, 46 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → seq(𝑚 + 1)( + , 𝐺) ∈ dom ⇝ ) |
48 | 34, 38, 42, 43, 47 | isumcl 14492 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))𝐵 ∈ ℂ) |
49 | 30, 48 | pncan2d 10394 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) |
50 | 20 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) = 𝐵) |
51 | 21 | adantlr 751 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ ℕ0) → 𝐵 ∈
ℂ) |
52 | 5, 34, 37, 50, 51, 44 | isumsplit 14572 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0
𝐵 = (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)) |
53 | | nncn 11028 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℂ) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℂ) |
55 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℂ |
56 | | pncan 10287 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑚 + 1)
− 1) = 𝑚) |
57 | 54, 55, 56 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) − 1) = 𝑚) |
58 | 57 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (0...((𝑚 + 1) − 1)) = (0...𝑚)) |
59 | 58 | sumeq1d 14431 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = Σ𝑘 ∈ (0...𝑚)𝐵) |
60 | | simpl 473 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝜑) |
61 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (0...𝑚) → 𝑘 ∈ ℕ0) |
62 | 60, 61, 20 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑚)) → (𝐺‘𝑘) = 𝐵) |
63 | 35, 5 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → 𝑚 ∈
(ℤ≥‘0)) |
64 | 60, 61, 21 | syl2an 494 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ) ∧ 𝑘 ∈ (0...𝑚)) → 𝐵 ∈ ℂ) |
65 | 62, 63, 64 | fsumser 14461 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...𝑚)𝐵 = (seq0( + , 𝐺)‘𝑚)) |
66 | 59, 65 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 = (seq0( + , 𝐺)‘𝑚)) |
67 | 66 | oveq1d 6665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ (0...((𝑚 + 1) − 1))𝐵 + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)) |
68 | 52, 67 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈ ℕ0
𝐵 = ((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵)) |
69 | 68 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0
𝐵 − (seq0( + , 𝐺)‘𝑚)) = (((seq0( + , 𝐺)‘𝑚) + Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) − (seq0( + , 𝐺)‘𝑚))) |
70 | 42 | sumeq2dv 14433 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))𝐵) |
71 | 49, 69, 70 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (Σ𝑘 ∈ ℕ0
𝐵 − (seq0( + , 𝐺)‘𝑚)) = Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) |
72 | 71 | fveq2d 6195 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) →
(abs‘(Σ𝑘 ∈
ℕ0 𝐵
− (seq0( + , 𝐺)‘𝑚))) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘))) |
73 | 33, 72 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → (abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) =
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘))) |
74 | 73 | breq1d 4663 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ) → ((abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
75 | 25, 74 | sylan2 491 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ ℕ ∧ 𝑚 ∈ (ℤ≥‘𝑠))) → ((abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
76 | 75 | anassrs 680 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ) ∧ 𝑚 ∈ (ℤ≥‘𝑠)) → ((abs‘((seq0( +
, 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0
𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0
(𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
77 | 76 | ralbidva 2985 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
78 | | oveq1 6657 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑛 → (𝑚 + 1) = (𝑛 + 1)) |
79 | 78 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑚 = 𝑛 → (ℤ≥‘(𝑚 + 1)) =
(ℤ≥‘(𝑛 + 1))) |
80 | 79 | sumeq1d 14431 |
. . . . . . . 8
⊢ (𝑚 = 𝑛 → Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) |
81 | 80 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑚 = 𝑛 → (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
82 | 81 | breq1d 4663 |
. . . . . 6
⊢ (𝑚 = 𝑛 → ((abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
83 | 82 | cbvralv 3171 |
. . . . 5
⊢
(∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑚 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) |
84 | 77, 83 | syl6bb 276 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) ↔ ∀𝑛 ∈ (ℤ≥‘𝑠)(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
85 | | mertens.11 |
. . . . . 6
⊢ (𝜓 ↔ (𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)))) |
86 | | 0zd 11389 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℤ) |
87 | 4 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → (𝐸 / 2) ∈
ℝ+) |
88 | 85 | simplbi 476 |
. . . . . . . . . . . . 13
⊢ (𝜓 → 𝑠 ∈ ℕ) |
89 | 88 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑠 ∈ ℕ) |
90 | 89 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 𝑠 ∈ ℝ+) |
91 | 87, 90 | rpdivcld 11889 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → ((𝐸 / 2) / 𝑠) ∈
ℝ+) |
92 | | mertens.10 |
. . . . . . . . . . . . 13
⊢ 𝑇 = {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} |
93 | | eqid 2622 |
. . . . . . . . . . . . . . . . . 18
⊢
(ℤ≥‘(𝑛 + 1)) = (ℤ≥‘(𝑛 + 1)) |
94 | | elfznn0 12433 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ (0...(𝑠 − 1)) → 𝑛 ∈ ℕ0) |
95 | 94 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝑛 ∈ ℕ0) |
96 | | peano2nn0 11333 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0
→ (𝑛 + 1) ∈
ℕ0) |
97 | 95, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈
ℕ0) |
98 | 97 | nn0zd 11480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑛 + 1) ∈ ℤ) |
99 | | eqidd 2623 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) = (𝐺‘𝑘)) |
100 | | simplll 798 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝜑) |
101 | | eluznn0 11757 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑛 + 1) ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘(𝑛 + 1))) → 𝑘 ∈ ℕ0) |
102 | 97, 101 | sylan 488 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → 𝑘 ∈
ℕ0) |
103 | 100, 102,
26 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ (ℤ≥‘(𝑛 + 1))) → (𝐺‘𝑘) ∈ ℂ) |
104 | 22 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq0( + , 𝐺) ∈ dom ⇝
) |
105 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → 𝜑) |
106 | 105, 26 | sylan 488 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) ∧ 𝑘 ∈ ℕ0) → (𝐺‘𝑘) ∈ ℂ) |
107 | 5, 97, 106 | iserex 14387 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝
)) |
108 | 104, 107 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → seq(𝑛 + 1)( + , 𝐺) ∈ dom ⇝ ) |
109 | 93, 98, 99, 103, 108 | isumcl 14492 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) ∈ ℂ) |
110 | 109 | abscld 14175 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ∈ ℝ) |
111 | | eleq1a 2696 |
. . . . . . . . . . . . . . . 16
⊢
((abs‘Σ𝑘
∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ∈ ℝ → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ)) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑛 ∈ (0...(𝑠 − 1))) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ)) |
113 | 112 | rexlimdva 3031 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) → 𝑧 ∈ ℝ)) |
114 | 113 | abssdv 3676 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ⊆ ℝ) |
115 | 92, 114 | syl5eqss 3649 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ⊆ ℝ) |
116 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (0...(𝑠 − 1)) ∈ Fin) |
117 | | abrexfi 8266 |
. . . . . . . . . . . . . . 15
⊢
((0...(𝑠 − 1))
∈ Fin → {𝑧
∣ ∃𝑛 ∈
(0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ∈ Fin) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → {𝑧 ∣ ∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))} ∈ Fin) |
119 | 92, 118 | syl5eqel 2705 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ∈ Fin) |
120 | | nnm1nn0 11334 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 ∈ ℕ → (𝑠 − 1) ∈
ℕ0) |
121 | 89, 120 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (𝑠 − 1) ∈
ℕ0) |
122 | 121, 5 | syl6eleq 2711 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (𝑠 − 1) ∈
(ℤ≥‘0)) |
123 | | eluzfz1 12348 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑠 − 1))) |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 0 ∈ (0...(𝑠 − 1))) |
125 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
126 | 125, 20 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) = 𝐵) |
127 | 126 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → Σ𝑘 ∈ ℕ (𝐺‘𝑘) = Σ𝑘 ∈ ℕ 𝐵) |
128 | 127 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ ℕ (𝐺‘𝑘) = Σ𝑘 ∈ ℕ 𝐵) |
129 | 128 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ ℕ 𝐵)) |
130 | 129 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘))) |
131 | | oveq1 6657 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑛 = 0 → (𝑛 + 1) = (0 + 1)) |
132 | | 0p1e1 11132 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (0 + 1) =
1 |
133 | 131, 132 | syl6eq 2672 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 = 0 → (𝑛 + 1) = 1) |
134 | 133 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 0 →
(ℤ≥‘(𝑛 + 1)) =
(ℤ≥‘1)) |
135 | 134, 1 | syl6eqr 2674 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 0 →
(ℤ≥‘(𝑛 + 1)) = ℕ) |
136 | 135 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 0 → Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘) = Σ𝑘 ∈ ℕ (𝐺‘𝑘)) |
137 | 136 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 0 →
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘))) |
138 | 137 | eqeq2d 2632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 0 →
((abs‘Σ𝑘 ∈
ℕ 𝐵) =
(abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈ ℕ (𝐺‘𝑘)))) |
139 | 138 | rspcev 3309 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ (0...(𝑠 − 1))
∧ (abs‘Σ𝑘
∈ ℕ 𝐵) =
(abs‘Σ𝑘 ∈
ℕ (𝐺‘𝑘))) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
140 | 124, 130,
139 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
141 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
(abs‘Σ𝑘
∈ ℕ 𝐵) ∈
V |
142 | | eqeq1 2626 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ (abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
143 | 142 | rexbidv 3052 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (abs‘Σ𝑘 ∈ ℕ 𝐵) → (∃𝑛 ∈ (0...(𝑠 − 1))𝑧 = (abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)))) |
144 | 141, 143,
92 | elab2 3354 |
. . . . . . . . . . . . . . 15
⊢
((abs‘Σ𝑘
∈ ℕ 𝐵) ∈
𝑇 ↔ ∃𝑛 ∈ (0...(𝑠 − 1))(abs‘Σ𝑘 ∈ ℕ 𝐵) = (abs‘Σ𝑘 ∈
(ℤ≥‘(𝑛 + 1))(𝐺‘𝑘))) |
145 | 140, 144 | sylibr 224 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇) |
146 | | ne0i 3921 |
. . . . . . . . . . . . . 14
⊢
((abs‘Σ𝑘
∈ ℕ 𝐵) ∈
𝑇 → 𝑇 ≠ ∅) |
147 | 145, 146 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝑇 ≠ ∅) |
148 | | ltso 10118 |
. . . . . . . . . . . . . 14
⊢ < Or
ℝ |
149 | | fisupcl 8375 |
. . . . . . . . . . . . . 14
⊢ (( <
Or ℝ ∧ (𝑇 ∈
Fin ∧ 𝑇 ≠ ∅
∧ 𝑇 ⊆ ℝ))
→ sup(𝑇, ℝ, <
) ∈ 𝑇) |
150 | 148, 149 | mpan 706 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ∈ Fin ∧ 𝑇 ≠ ∅ ∧ 𝑇 ⊆ ℝ) →
sup(𝑇, ℝ, < )
∈ 𝑇) |
151 | 119, 147,
115, 150 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → sup(𝑇, ℝ, < ) ∈ 𝑇) |
152 | 115, 151 | sseldd 3604 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → sup(𝑇, ℝ, < ) ∈
ℝ) |
153 | | 0red 10041 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℝ) |
154 | 125, 21 | sylan2 491 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℂ) |
155 | | 1nn0 11308 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℕ0 |
156 | 155 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℕ0) |
157 | 5, 156, 26 | iserex 14387 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (seq0( + , 𝐺) ∈ dom ⇝ ↔
seq1( + , 𝐺) ∈ dom
⇝ )) |
158 | 22, 157 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → seq1( + , 𝐺) ∈ dom ⇝
) |
159 | 1, 2, 126, 154, 158 | isumcl 14492 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ) |
160 | 159 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ ℕ 𝐵 ∈ ℂ) |
161 | 160 | abscld 14175 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈
ℝ) |
162 | 160 | absge0d 14183 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → 0 ≤ (abs‘Σ𝑘 ∈ ℕ 𝐵)) |
163 | | fimaxre2 10969 |
. . . . . . . . . . . . . . 15
⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ∈ Fin) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) |
164 | 115, 119,
163 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) |
165 | 115, 147,
164 | 3jca 1242 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧)) |
166 | | suprub 10984 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧) ∧ (abs‘Σ𝑘 ∈ ℕ 𝐵) ∈ 𝑇) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ≤ sup(𝑇, ℝ, < )) |
167 | 165, 145,
166 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (abs‘Σ𝑘 ∈ ℕ 𝐵) ≤ sup(𝑇, ℝ, < )) |
168 | 153, 161,
152, 162, 167 | letrd 10194 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 0 ≤ sup(𝑇, ℝ, < )) |
169 | 152, 168 | ge0p1rpd 11902 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (sup(𝑇, ℝ, < ) + 1) ∈
ℝ+) |
170 | 91, 169 | rpdivcld 11889 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ∈
ℝ+) |
171 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (𝐾‘𝑛) = (𝐾‘𝑚)) |
172 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) |
173 | | fvex 6201 |
. . . . . . . . . . 11
⊢ (𝐾‘𝑚) ∈ V |
174 | 171, 172,
173 | fvmpt 6282 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐾‘𝑛))‘𝑚) = (𝐾‘𝑚)) |
175 | 174 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑚 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑚) = (𝐾‘𝑚)) |
176 | | nn0ex 11298 |
. . . . . . . . . . . . 13
⊢
ℕ0 ∈ V |
177 | 176 | mptex 6486 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛)) ∈ V |
178 | 177 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ∈ V) |
179 | | elnn0uz 11725 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ0
↔ 𝑗 ∈
(ℤ≥‘0)) |
180 | | fveq2 6191 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑗 → (𝐾‘𝑛) = (𝐾‘𝑗)) |
181 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾‘𝑗) ∈ V |
182 | 180, 172,
181 | fvmpt 6282 |
. . . . . . . . . . . . . . 15
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗)) |
183 | 182 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗)) |
184 | 179, 183 | sylan2br 493 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ≥‘0))
→ ((𝑛 ∈
ℕ0 ↦ (𝐾‘𝑛))‘𝑗) = (𝐾‘𝑗)) |
185 | 6, 184 | seqfeq 12826 |
. . . . . . . . . . . 12
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))) = seq0( + , 𝐾)) |
186 | 185, 12 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))) ∈ dom ⇝
) |
187 | 183, 8 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) = (abs‘𝐴)) |
188 | 187, 10 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) ∈ ℝ) |
189 | 188 | recnd 10068 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐾‘𝑛))‘𝑗) ∈ ℂ) |
190 | 5, 6, 178, 186, 189 | serf0 14411 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ⇝ 0) |
191 | 190 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑛 ∈ ℕ0 ↦ (𝐾‘𝑛)) ⇝ 0) |
192 | 5, 86, 170, 175, 191 | climi0 14243 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → ∃𝑡 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
193 | | simplll 798 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → 𝜑) |
194 | | eluznn0 11757 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℕ0
∧ 𝑚 ∈
(ℤ≥‘𝑡)) → 𝑚 ∈ ℕ0) |
195 | 194 | adantll 750 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → 𝑚 ∈ ℕ0) |
196 | 11, 15 | absidd 14161 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(abs‘(𝐾‘𝑗)) = (𝐾‘𝑗)) |
197 | 196 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑗 ∈ ℕ0 (abs‘(𝐾‘𝑗)) = (𝐾‘𝑗)) |
198 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑗 = 𝑚 → (𝐾‘𝑗) = (𝐾‘𝑚)) |
199 | 198 | fveq2d 6195 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 = 𝑚 → (abs‘(𝐾‘𝑗)) = (abs‘(𝐾‘𝑚))) |
200 | 199, 198 | eqeq12d 2637 |
. . . . . . . . . . . . . . . 16
⊢ (𝑗 = 𝑚 → ((abs‘(𝐾‘𝑗)) = (𝐾‘𝑗) ↔ (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚))) |
201 | 200 | rspccva 3308 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑗 ∈
ℕ0 (abs‘(𝐾‘𝑗)) = (𝐾‘𝑗) ∧ 𝑚 ∈ ℕ0) →
(abs‘(𝐾‘𝑚)) = (𝐾‘𝑚)) |
202 | 197, 201 | sylan 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) →
(abs‘(𝐾‘𝑚)) = (𝐾‘𝑚)) |
203 | 193, 195,
202 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → (abs‘(𝐾‘𝑚)) = (𝐾‘𝑚)) |
204 | 203 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) ∧ 𝑚 ∈
(ℤ≥‘𝑡)) → ((abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
205 | 204 | ralbidva 2985 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
206 | 171 | breq1d 4663 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ (𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
207 | 206 | cbvralv 3171 |
. . . . . . . . . . 11
⊢
(∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) |
208 | 205, 207 | syl6bbr 278 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) ↔ ∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
209 | | simpll 790 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → 𝜑) |
210 | | mertens.1 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐹‘𝑗) = 𝐴) |
211 | 209, 210 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0)
→ (𝐹‘𝑗) = 𝐴) |
212 | 209, 8 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0)
→ (𝐾‘𝑗) = (abs‘𝐴)) |
213 | 209, 9 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑗 ∈ ℕ0)
→ 𝐴 ∈
ℂ) |
214 | 209, 20 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0)
→ (𝐺‘𝑘) = 𝐵) |
215 | 209, 21 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0)
→ 𝐵 ∈
ℂ) |
216 | | mertens.6 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) |
217 | 209, 216 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ∧ 𝑘 ∈ ℕ0)
→ (𝐻‘𝑘) = Σ𝑗 ∈ (0...𝑘)(𝐴 · (𝐺‘(𝑘 − 𝑗)))) |
218 | 12 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → seq0( + ,
𝐾) ∈ dom ⇝
) |
219 | 22 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → seq0( + ,
𝐺) ∈ dom ⇝
) |
220 | 3 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → 𝐸 ∈
ℝ+) |
221 | 207 | anbi2i 730 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ ℕ0
∧ ∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))) ↔ (𝑡 ∈ ℕ0
∧ ∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) |
222 | 221 | anbi2i 730 |
. . . . . . . . . . . . . 14
⊢ ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) ↔ (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) |
223 | 222 | biimpi 206 |
. . . . . . . . . . . . 13
⊢ ((𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) |
224 | 223 | adantll 750 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (𝜓 ∧ (𝑡 ∈ ℕ0 ∧
∀𝑚 ∈
(ℤ≥‘𝑡)(𝐾‘𝑚) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1))))) |
225 | 168, 165 | jca 554 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (0 ≤ sup(𝑇, ℝ, < ) ∧ (𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑧 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) |
226 | 225 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) → (0 ≤
sup(𝑇, ℝ, < )
∧ (𝑇 ⊆ ℝ
∧ 𝑇 ≠ ∅ ∧
∃𝑧 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑤 ≤ 𝑧))) |
227 | 211, 212,
213, 214, 215, 217, 218, 219, 220, 92, 85, 224, 226 | mertenslem1 14616 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝜓) ∧ (𝑡 ∈ ℕ0 ∧
∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)))) →
∃𝑦 ∈
ℕ0 ∀𝑚 ∈ (ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
228 | 227 | expr 643 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑛 ∈
(ℤ≥‘𝑡)(𝐾‘𝑛) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0
∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
229 | 208, 228 | sylbid 230 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝜓) ∧ 𝑡 ∈ ℕ0) →
(∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0
∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
230 | 229 | rexlimdva 3031 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (∃𝑡 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑡)(abs‘(𝐾‘𝑚)) < (((𝐸 / 2) / 𝑠) / (sup(𝑇, ℝ, < ) + 1)) → ∃𝑦 ∈ ℕ0
∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
231 | 192, 230 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |
232 | 231 | ex 450 |
. . . . . 6
⊢ (𝜑 → (𝜓 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
233 | 85, 232 | syl5bir 233 |
. . . . 5
⊢ (𝜑 → ((𝑠 ∈ ℕ ∧ ∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1))) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
234 | 233 | expdimp 453 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑛 ∈
(ℤ≥‘𝑠)(abs‘Σ𝑘 ∈ (ℤ≥‘(𝑛 + 1))(𝐺‘𝑘)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
235 | 84, 234 | sylbid 230 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℕ) → (∀𝑚 ∈
(ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
236 | 235 | rexlimdva 3031 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ ℕ ∀𝑚 ∈ (ℤ≥‘𝑠)(abs‘((seq0( + , 𝐺)‘𝑚) − Σ𝑘 ∈ ℕ0 𝐵)) < ((𝐸 / 2) / (Σ𝑗 ∈ ℕ0 (𝐾‘𝑗) + 1)) → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸)) |
237 | 24, 236 | mpd 15 |
1
⊢ (𝜑 → ∃𝑦 ∈ ℕ0 ∀𝑚 ∈
(ℤ≥‘𝑦)(abs‘Σ𝑗 ∈ (0...𝑚)(𝐴 · Σ𝑘 ∈ (ℤ≥‘((𝑚 − 𝑗) + 1))𝐵)) < 𝐸) |