Proof of Theorem fsumharmonic
Step | Hyp | Ref
| Expression |
1 | | fzfid 12634 |
. . . 4
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
2 | | fsumharmonic.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ) |
3 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
4 | 3 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
5 | 4 | nncnd 10913 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℂ) |
6 | 4 | nnne0d 10942 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ≠ 0) |
7 | 2, 5, 6 | divcld 10680 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝐵 / 𝑛) ∈ ℂ) |
8 | 1, 7 | fsumcl 14311 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛) ∈ ℂ) |
9 | 8 | abscld 14023 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ∈ ℝ) |
10 | 2 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘𝐵) ∈ ℝ) |
11 | 10, 4 | nndivred 10946 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℝ) |
12 | 1, 11 | fsumrecl 14312 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ∈ ℝ) |
13 | | fsumharmonic.c |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐶 ∈ ℝ) |
14 | 1, 13 | fsumrecl 14312 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 ∈ ℝ) |
15 | | fsumharmonic.r |
. . . . 5
⊢ (𝜑 → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) |
16 | 15 | simpld 474 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ ℝ) |
17 | | fsumharmonic.t |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 1 ≤ 𝑇)) |
18 | 17 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℝ) |
19 | | 0red 9920 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
20 | | 1red 9934 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
21 | | 0lt1 10429 |
. . . . . . . . 9
⊢ 0 <
1 |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 < 1) |
23 | 17 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → 1 ≤ 𝑇) |
24 | 19, 20, 18, 22, 23 | ltletrd 10076 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑇) |
25 | 18, 24 | elrpd 11745 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
26 | 25 | relogcld 24173 |
. . . . 5
⊢ (𝜑 → (log‘𝑇) ∈
ℝ) |
27 | 26, 20 | readdcld 9948 |
. . . 4
⊢ (𝜑 → ((log‘𝑇) + 1) ∈
ℝ) |
28 | 16, 27 | remulcld 9949 |
. . 3
⊢ (𝜑 → (𝑅 · ((log‘𝑇) + 1)) ∈ ℝ) |
29 | 14, 28 | readdcld 9948 |
. 2
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))) ∈ ℝ) |
30 | 1, 7 | fsumabs 14374 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))(abs‘(𝐵 / 𝑛))) |
31 | 2, 5, 6 | absdivd 14042 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘(𝐵 / 𝑛)) = ((abs‘𝐵) / (abs‘𝑛))) |
32 | 4 | nnrpd 11746 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ+) |
33 | 32 | rprege0d 11755 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛)) |
34 | | absid 13884 |
. . . . . . 7
⊢ ((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) → (abs‘𝑛) = 𝑛) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘𝑛) = 𝑛) |
36 | 35 | oveq2d 6565 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / (abs‘𝑛)) = ((abs‘𝐵) / 𝑛)) |
37 | 31, 36 | eqtrd 2644 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘(𝐵 / 𝑛)) = ((abs‘𝐵) / 𝑛)) |
38 | 37 | sumeq2dv 14281 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(abs‘(𝐵 / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛)) |
39 | 30, 38 | breqtrd 4609 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛)) |
40 | | fsumharmonic.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
41 | 40, 25 | rpdivcld 11765 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / 𝑇) ∈
ℝ+) |
42 | 41 | rprege0d 11755 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 / 𝑇) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑇))) |
43 | | flge0nn0 12483 |
. . . . . . . 8
⊢ (((𝐴 / 𝑇) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑇)) → (⌊‘(𝐴 / 𝑇)) ∈
ℕ0) |
44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝐴 / 𝑇)) ∈
ℕ0) |
45 | 44 | nn0red 11229 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝐴 / 𝑇)) ∈ ℝ) |
46 | 45 | ltp1d 10833 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐴 / 𝑇)) < ((⌊‘(𝐴 / 𝑇)) + 1)) |
47 | | fzdisj 12239 |
. . . . 5
⊢
((⌊‘(𝐴 /
𝑇)) <
((⌊‘(𝐴 / 𝑇)) + 1) →
((1...(⌊‘(𝐴 /
𝑇))) ∩
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) = ∅) |
48 | 46, 47 | syl 17 |
. . . 4
⊢ (𝜑 →
((1...(⌊‘(𝐴 /
𝑇))) ∩
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) = ∅) |
49 | | nn0p1nn 11209 |
. . . . . . 7
⊢
((⌊‘(𝐴 /
𝑇)) ∈
ℕ0 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈ ℕ) |
50 | 44, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈ ℕ) |
51 | | nnuz 11599 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
52 | 50, 51 | syl6eleq 2698 |
. . . . 5
⊢ (𝜑 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈
(ℤ≥‘1)) |
53 | 41 | rpred 11748 |
. . . . . 6
⊢ (𝜑 → (𝐴 / 𝑇) ∈ ℝ) |
54 | 40 | rpred 11748 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
55 | 18, 24 | jca 553 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 0 < 𝑇)) |
56 | 40 | rpregt0d 11754 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
57 | | lediv2 10792 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 ≤ 𝑇 ↔ (𝐴 / 𝑇) ≤ (𝐴 / 1))) |
58 | 20, 22, 55, 56, 57 | syl211anc 1324 |
. . . . . . . 8
⊢ (𝜑 → (1 ≤ 𝑇 ↔ (𝐴 / 𝑇) ≤ (𝐴 / 1))) |
59 | 23, 58 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → (𝐴 / 𝑇) ≤ (𝐴 / 1)) |
60 | 54 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
61 | 60 | div1d 10672 |
. . . . . . 7
⊢ (𝜑 → (𝐴 / 1) = 𝐴) |
62 | 59, 61 | breqtrd 4609 |
. . . . . 6
⊢ (𝜑 → (𝐴 / 𝑇) ≤ 𝐴) |
63 | | flword2 12476 |
. . . . . 6
⊢ (((𝐴 / 𝑇) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝐴 / 𝑇) ≤ 𝐴) → (⌊‘𝐴) ∈
(ℤ≥‘(⌊‘(𝐴 / 𝑇)))) |
64 | 53, 54, 62, 63 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (⌊‘𝐴) ∈
(ℤ≥‘(⌊‘(𝐴 / 𝑇)))) |
65 | | fzsplit2 12237 |
. . . . 5
⊢
((((⌊‘(𝐴
/ 𝑇)) + 1) ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈
(ℤ≥‘(⌊‘(𝐴 / 𝑇)))) → (1...(⌊‘𝐴)) = ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
66 | 52, 64, 65 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (1...(⌊‘𝐴)) = ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
67 | 11 | recnd 9947 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℂ) |
68 | 48, 66, 1, 67 | fsumsplit 14318 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛))) |
69 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘(𝐴 / 𝑇))) ∈ Fin) |
70 | | ssun1 3738 |
. . . . . . . 8
⊢
(1...(⌊‘(𝐴 / 𝑇))) ⊆ ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) |
71 | 70, 66 | syl5sseqr 3617 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘(𝐴 / 𝑇))) ⊆ (1...(⌊‘𝐴))) |
72 | 71 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ (1...(⌊‘𝐴))) |
73 | 72, 11 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → ((abs‘𝐵) / 𝑛) ∈ ℝ) |
74 | 69, 73 | fsumrecl 14312 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ∈ ℝ) |
75 | | fzfid 12634 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) ∈ Fin) |
76 | | ssun2 3739 |
. . . . . . . 8
⊢
(((⌊‘(𝐴
/ 𝑇)) +
1)...(⌊‘𝐴))
⊆ ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) |
77 | 76, 66 | syl5sseqr 3617 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴))) |
78 | 77 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ (1...(⌊‘𝐴))) |
79 | 78, 11 | syldan 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℝ) |
80 | 75, 79 | fsumrecl 14312 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ∈ ℝ) |
81 | 72, 13 | syldan 486 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝐶 ∈ ℝ) |
82 | 69, 81 | fsumrecl 14312 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶 ∈ ℝ) |
83 | | fznnfl 12523 |
. . . . . . . . . . 11
⊢ ((𝐴 / 𝑇) ∈ ℝ → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑇)))) |
84 | 53, 83 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑇)))) |
85 | 84 | simplbda 652 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ≤ (𝐴 / 𝑇)) |
86 | 32 | rpred 11748 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ) |
87 | 54 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
88 | 55 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑇 ∈ ℝ ∧ 0 < 𝑇)) |
89 | | lemuldiv2 10783 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 <
𝑇)) → ((𝑇 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
90 | 86, 87, 88, 89 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑇 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
91 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑇 ∈ ℝ) |
92 | 91, 87, 32 | lemuldivd 11797 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑇 · 𝑛) ≤ 𝐴 ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
93 | 90, 92 | bitr3d 269 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ≤ (𝐴 / 𝑇) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
94 | 72, 93 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (𝑛 ≤ (𝐴 / 𝑇) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
95 | 85, 94 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑇 ≤ (𝐴 / 𝑛)) |
96 | | fsumharmonic.1 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑇 ≤ (𝐴 / 𝑛)) → (abs‘𝐵) ≤ (𝐶 · 𝑛)) |
97 | 96 | ex 449 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑇 ≤ (𝐴 / 𝑛) → (abs‘𝐵) ≤ (𝐶 · 𝑛))) |
98 | 72, 97 | syldan 486 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (𝑇 ≤ (𝐴 / 𝑛) → (abs‘𝐵) ≤ (𝐶 · 𝑛))) |
99 | 95, 98 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (abs‘𝐵) ≤ (𝐶 · 𝑛)) |
100 | 72, 2 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝐵 ∈ ℂ) |
101 | 100 | abscld 14023 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (abs‘𝐵) ∈ ℝ) |
102 | 72, 3 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℕ) |
103 | 102 | nnrpd 11746 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℝ+) |
104 | 101, 81, 103 | ledivmul2d 11802 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (((abs‘𝐵) / 𝑛) ≤ 𝐶 ↔ (abs‘𝐵) ≤ (𝐶 · 𝑛))) |
105 | 99, 104 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → ((abs‘𝐵) / 𝑛) ≤ 𝐶) |
106 | 69, 73, 81, 105 | fsumle 14372 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶) |
107 | | fsumharmonic.0 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 0 ≤ 𝐶) |
108 | 1, 13, 107, 71 | fsumless 14369 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶 ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶) |
109 | 74, 82, 14, 106, 108 | letrd 10073 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶) |
110 | 78, 3 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
111 | 110 | nnrecred 10943 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℝ) |
112 | 75, 111 | fsumrecl 14312 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ) |
113 | 16, 112 | remulcld 9949 |
. . . . 5
⊢ (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ∈ ℝ) |
114 | 16 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑅 ∈ ℝ) |
115 | 114 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑅 ∈ ℂ) |
116 | 110 | nncnd 10913 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℂ) |
117 | 110 | nnne0d 10942 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ≠ 0) |
118 | 115, 116,
117 | divrecd 10683 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 / 𝑛) = (𝑅 · (1 / 𝑛))) |
119 | 114, 110 | nndivred 10946 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 / 𝑛) ∈ ℝ) |
120 | 118, 119 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 · (1 / 𝑛)) ∈ ℝ) |
121 | 78, 10 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (abs‘𝐵) ∈ ℝ) |
122 | 78, 32 | syldan 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℝ+) |
123 | | noel 3878 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝑛 ∈
∅ |
124 | | elin 3758 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
((1...(⌊‘(𝐴 /
𝑇))) ∩
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
125 | 48 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑛 ∈ ((1...(⌊‘(𝐴 / 𝑇))) ∩ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ 𝑛 ∈ ∅)) |
126 | 124, 125 | syl5bbr 273 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ 𝑛 ∈ ∅)) |
127 | 123, 126 | mtbiri 316 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
128 | | imnan 437 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(1...(⌊‘(𝐴 /
𝑇))) → ¬ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ ¬ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
129 | 127, 128 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) → ¬ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
130 | 129 | con2d 128 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) → ¬ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))))) |
131 | 130 | imp 444 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ¬ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) |
132 | 83 | baibd 946 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 / 𝑇) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
133 | 53, 3, 132 | syl2an 493 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
134 | 133, 93 | bitrd 267 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
135 | 78, 134 | syldan 486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
136 | 131, 135 | mtbid 313 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ¬ 𝑇 ≤ (𝐴 / 𝑛)) |
137 | 54 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
138 | 137, 110 | nndivred 10946 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝐴 / 𝑛) ∈ ℝ) |
139 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑇 ∈ ℝ) |
140 | 138, 139 | ltnled 10063 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 ↔ ¬ 𝑇 ≤ (𝐴 / 𝑛))) |
141 | 136, 140 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝐴 / 𝑛) < 𝑇) |
142 | | fsumharmonic.2 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝐴 / 𝑛) < 𝑇) → (abs‘𝐵) ≤ 𝑅) |
143 | 142 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 → (abs‘𝐵) ≤ 𝑅)) |
144 | 78, 143 | syldan 486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 → (abs‘𝐵) ≤ 𝑅)) |
145 | 141, 144 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (abs‘𝐵) ≤ 𝑅) |
146 | 121, 114,
122, 145 | lediv1dd 11806 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ≤ (𝑅 / 𝑛)) |
147 | 146, 118 | breqtrd 4609 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ≤ (𝑅 · (1 / 𝑛))) |
148 | 75, 79, 120, 147 | fsumle 14372 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(𝑅 · (1 / 𝑛))) |
149 | 16 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℂ) |
150 | 111 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℂ) |
151 | 75, 149, 150 | fsummulc2 14358 |
. . . . . 6
⊢ (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) = Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(𝑅 · (1 / 𝑛))) |
152 | 148, 151 | breqtrrd 4611 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛))) |
153 | 4 | nnrecred 10943 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℝ) |
154 | 153 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℂ) |
155 | 48, 66, 1, 154 | fsumsplit 14318 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛))) |
156 | 155 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) = ((Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛))) |
157 | 102 | nnrecred 10943 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈ ℝ) |
158 | 69, 157 | fsumrecl 14312 |
. . . . . . . . . 10
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℝ) |
159 | 158 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℂ) |
160 | 112 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℂ) |
161 | 159, 160 | pncan2d 10273 |
. . . . . . . 8
⊢ (𝜑 → ((Σ𝑛 ∈
(1...(⌊‘(𝐴 /
𝑇)))(1 / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) = Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) |
162 | 156, 161 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) = Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) |
163 | 1, 153 | fsumrecl 14312 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ) |
164 | 163 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ) |
165 | 158 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℝ) |
166 | 164, 165 | resubcld 10337 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ∈ ℝ) |
167 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → 0 ∈
ℝ) |
168 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → ((log‘𝑇) + 1) ∈
ℝ) |
169 | | fzfid 12634 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘(𝐴 / 𝑇))) ∈ Fin) |
170 | 103 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℝ+) |
171 | 170 | rpreccld 11758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈
ℝ+) |
172 | 171 | rpred 11748 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈ ℝ) |
173 | 171 | rpge0d 11752 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 0 ≤ (1 / 𝑛)) |
174 | 40 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 ∈
ℝ+) |
175 | 174 | rpge0d 11752 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 < 1) → 0 ≤ 𝐴) |
176 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 < 1) |
177 | | 0p1e1 11009 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 1) =
1 |
178 | 176, 177 | syl6breqr 4625 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 < (0 + 1)) |
179 | 54 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 ∈ ℝ) |
180 | | 0z 11265 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
181 | | flbi 12479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℤ) → ((⌊‘𝐴) = 0 ↔ (0 ≤ 𝐴 ∧ 𝐴 < (0 + 1)))) |
182 | 179, 180,
181 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 < 1) → ((⌊‘𝐴) = 0 ↔ (0 ≤ 𝐴 ∧ 𝐴 < (0 + 1)))) |
183 | 175, 178,
182 | mpbir2and 959 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 < 1) → (⌊‘𝐴) = 0) |
184 | 183 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘𝐴)) = (1...0)) |
185 | | fz10 12233 |
. . . . . . . . . . . . 13
⊢ (1...0) =
∅ |
186 | 184, 185 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘𝐴)) = ∅) |
187 | | 0ss 3924 |
. . . . . . . . . . . 12
⊢ ∅
⊆ (1...(⌊‘(𝐴 / 𝑇))) |
188 | 186, 187 | syl6eqss 3618 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘𝐴)) ⊆
(1...(⌊‘(𝐴 /
𝑇)))) |
189 | 169, 172,
173, 188 | fsumless 14369 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) |
190 | 164, 165 | suble0d 10497 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ 0 ↔ Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛))) |
191 | 189, 190 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ 0) |
192 | 18, 23 | logge0d 24180 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (log‘𝑇)) |
193 | | 0le1 10430 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
194 | 193 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 1) |
195 | 26, 20, 192, 194 | addge0d 10482 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ ((log‘𝑇) + 1)) |
196 | 195 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → 0 ≤ ((log‘𝑇) + 1)) |
197 | 166, 167,
168, 191, 196 | letrd 10073 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1)) |
198 | | harmonicubnd 24536 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ≤ ((log‘𝐴) + 1)) |
199 | 54, 198 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1)) |
200 | | harmoniclbnd 24535 |
. . . . . . . . . . . 12
⊢ ((𝐴 / 𝑇) ∈ ℝ+ →
(log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈
(1...(⌊‘(𝐴 /
𝑇)))(1 / 𝑛)) |
201 | 41, 200 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) |
202 | 201 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) |
203 | 40 | relogcld 24173 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘𝐴) ∈
ℝ) |
204 | | peano2re 10088 |
. . . . . . . . . . . . 13
⊢
((log‘𝐴)
∈ ℝ → ((log‘𝐴) + 1) ∈ ℝ) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝐴) + 1) ∈
ℝ) |
206 | 41 | relogcld 24173 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐴 / 𝑇)) ∈ ℝ) |
207 | | le2sub 10406 |
. . . . . . . . . . . 12
⊢
(((Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ∈ ℝ ∧
Σ𝑛 ∈
(1...(⌊‘(𝐴 /
𝑇)))(1 / 𝑛) ∈ ℝ) ∧ (((log‘𝐴) + 1) ∈ ℝ ∧
(log‘(𝐴 / 𝑇)) ∈ ℝ)) →
((Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))))) |
208 | 163, 158,
205, 206, 207 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (𝜑 → ((Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))))) |
209 | 208 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))))) |
210 | 199, 202,
209 | mp2and 711 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇)))) |
211 | 203 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) |
212 | 20 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
213 | 26 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘𝑇) ∈
ℂ) |
214 | 211, 212,
213 | pnncand 10310 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘𝐴) + 1) − ((log‘𝐴) − (log‘𝑇))) = (1 + (log‘𝑇))) |
215 | 40, 25 | relogdivd 24176 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐴 / 𝑇)) = ((log‘𝐴) − (log‘𝑇))) |
216 | 215 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = (((log‘𝐴) + 1) − ((log‘𝐴) − (log‘𝑇)))) |
217 | | ax-1cn 9873 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
218 | | addcom 10101 |
. . . . . . . . . . . 12
⊢
(((log‘𝑇)
∈ ℂ ∧ 1 ∈ ℂ) → ((log‘𝑇) + 1) = (1 + (log‘𝑇))) |
219 | 213, 217,
218 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝑇) + 1) = (1 + (log‘𝑇))) |
220 | 214, 216,
219 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (𝜑 → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = ((log‘𝑇) + 1)) |
221 | 220 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = ((log‘𝑇) + 1)) |
222 | 210, 221 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1)) |
223 | 197, 222,
54, 20 | ltlecasei 10024 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1)) |
224 | 162, 223 | eqbrtrrd 4607 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝑇) + 1)) |
225 | | lemul2a 10757 |
. . . . . 6
⊢
(((Σ𝑛 ∈
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ ∧ ((log‘𝑇) + 1) ∈ ℝ ∧
(𝑅 ∈ ℝ ∧ 0
≤ 𝑅)) ∧ Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝑇) + 1)) → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ≤ (𝑅 · ((log‘𝑇) + 1))) |
226 | 112, 27, 15, 224, 225 | syl31anc 1321 |
. . . . 5
⊢ (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ≤ (𝑅 · ((log‘𝑇) + 1))) |
227 | 80, 113, 28, 152, 226 | letrd 10073 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (𝑅 · ((log‘𝑇) + 1))) |
228 | 74, 80, 14, 28, 109, 227 | le2addd 10525 |
. . 3
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) |
229 | 68, 228 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) |
230 | 9, 12, 29, 39, 229 | letrd 10073 |
1
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) |