Proof of Theorem fsumharmonic
Step | Hyp | Ref
| Expression |
1 | | fzfid 13693 |
. . . 4
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
2 | | fsumharmonic.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ) |
3 | | elfznn 13285 |
. . . . . . 7
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
4 | 3 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
5 | 4 | nncnd 11989 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℂ) |
6 | 4 | nnne0d 12023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ≠ 0) |
7 | 2, 5, 6 | divcld 11751 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝐵 / 𝑛) ∈ ℂ) |
8 | 1, 7 | fsumcl 15445 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛) ∈ ℂ) |
9 | 8 | abscld 15148 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ∈ ℝ) |
10 | 2 | abscld 15148 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘𝐵) ∈ ℝ) |
11 | 10, 4 | nndivred 12027 |
. . 3
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℝ) |
12 | 1, 11 | fsumrecl 15446 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ∈ ℝ) |
13 | | fsumharmonic.c |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐶 ∈ ℝ) |
14 | 1, 13 | fsumrecl 15446 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 ∈ ℝ) |
15 | | fsumharmonic.r |
. . . . 5
⊢ (𝜑 → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) |
16 | 15 | simpld 495 |
. . . 4
⊢ (𝜑 → 𝑅 ∈ ℝ) |
17 | | fsumharmonic.t |
. . . . . . . 8
⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 1 ≤ 𝑇)) |
18 | 17 | simpld 495 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ ℝ) |
19 | | 0red 10978 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
20 | | 1red 10976 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
21 | | 0lt1 11497 |
. . . . . . . . 9
⊢ 0 <
1 |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 < 1) |
23 | 17 | simprd 496 |
. . . . . . . 8
⊢ (𝜑 → 1 ≤ 𝑇) |
24 | 19, 20, 18, 22, 23 | ltletrd 11135 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑇) |
25 | 18, 24 | elrpd 12769 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈
ℝ+) |
26 | 25 | relogcld 25778 |
. . . . 5
⊢ (𝜑 → (log‘𝑇) ∈
ℝ) |
27 | 26, 20 | readdcld 11004 |
. . . 4
⊢ (𝜑 → ((log‘𝑇) + 1) ∈
ℝ) |
28 | 16, 27 | remulcld 11005 |
. . 3
⊢ (𝜑 → (𝑅 · ((log‘𝑇) + 1)) ∈ ℝ) |
29 | 14, 28 | readdcld 11004 |
. 2
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))) ∈ ℝ) |
30 | 1, 7 | fsumabs 15513 |
. . 3
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))(abs‘(𝐵 / 𝑛))) |
31 | 2, 5, 6 | absdivd 15167 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘(𝐵 / 𝑛)) = ((abs‘𝐵) / (abs‘𝑛))) |
32 | 4 | nnrpd 12770 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ+) |
33 | 32 | rprege0d 12779 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛)) |
34 | | absid 15008 |
. . . . . . 7
⊢ ((𝑛 ∈ ℝ ∧ 0 ≤
𝑛) → (abs‘𝑛) = 𝑛) |
35 | 33, 34 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘𝑛) = 𝑛) |
36 | 35 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / (abs‘𝑛)) = ((abs‘𝐵) / 𝑛)) |
37 | 31, 36 | eqtrd 2778 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘(𝐵 / 𝑛)) = ((abs‘𝐵) / 𝑛)) |
38 | 37 | sumeq2dv 15415 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(abs‘(𝐵 / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛)) |
39 | 30, 38 | breqtrd 5100 |
. 2
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛)) |
40 | | fsumharmonic.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
41 | 40, 25 | rpdivcld 12789 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 / 𝑇) ∈
ℝ+) |
42 | 41 | rprege0d 12779 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 / 𝑇) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑇))) |
43 | | flge0nn0 13540 |
. . . . . . . 8
⊢ (((𝐴 / 𝑇) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑇)) → (⌊‘(𝐴 / 𝑇)) ∈
ℕ0) |
44 | 42, 43 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (⌊‘(𝐴 / 𝑇)) ∈
ℕ0) |
45 | 44 | nn0red 12294 |
. . . . . 6
⊢ (𝜑 → (⌊‘(𝐴 / 𝑇)) ∈ ℝ) |
46 | 45 | ltp1d 11905 |
. . . . 5
⊢ (𝜑 → (⌊‘(𝐴 / 𝑇)) < ((⌊‘(𝐴 / 𝑇)) + 1)) |
47 | | fzdisj 13283 |
. . . . 5
⊢
((⌊‘(𝐴 /
𝑇)) <
((⌊‘(𝐴 / 𝑇)) + 1) →
((1...(⌊‘(𝐴 /
𝑇))) ∩
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) = ∅) |
48 | 46, 47 | syl 17 |
. . . 4
⊢ (𝜑 →
((1...(⌊‘(𝐴 /
𝑇))) ∩
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) = ∅) |
49 | | nn0p1nn 12272 |
. . . . . . 7
⊢
((⌊‘(𝐴 /
𝑇)) ∈
ℕ0 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈ ℕ) |
50 | 44, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈ ℕ) |
51 | | nnuz 12621 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
52 | 50, 51 | eleqtrdi 2849 |
. . . . 5
⊢ (𝜑 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈
(ℤ≥‘1)) |
53 | 41 | rpred 12772 |
. . . . . 6
⊢ (𝜑 → (𝐴 / 𝑇) ∈ ℝ) |
54 | 40 | rpred 12772 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
55 | 18, 24 | jca 512 |
. . . . . . . . 9
⊢ (𝜑 → (𝑇 ∈ ℝ ∧ 0 < 𝑇)) |
56 | 40 | rpregt0d 12778 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
57 | | lediv2 11865 |
. . . . . . . . 9
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 ≤ 𝑇 ↔ (𝐴 / 𝑇) ≤ (𝐴 / 1))) |
58 | 20, 22, 55, 56, 57 | syl211anc 1375 |
. . . . . . . 8
⊢ (𝜑 → (1 ≤ 𝑇 ↔ (𝐴 / 𝑇) ≤ (𝐴 / 1))) |
59 | 23, 58 | mpbid 231 |
. . . . . . 7
⊢ (𝜑 → (𝐴 / 𝑇) ≤ (𝐴 / 1)) |
60 | 54 | recnd 11003 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
61 | 60 | div1d 11743 |
. . . . . . 7
⊢ (𝜑 → (𝐴 / 1) = 𝐴) |
62 | 59, 61 | breqtrd 5100 |
. . . . . 6
⊢ (𝜑 → (𝐴 / 𝑇) ≤ 𝐴) |
63 | | flword2 13533 |
. . . . . 6
⊢ (((𝐴 / 𝑇) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝐴 / 𝑇) ≤ 𝐴) → (⌊‘𝐴) ∈
(ℤ≥‘(⌊‘(𝐴 / 𝑇)))) |
64 | 53, 54, 62, 63 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (⌊‘𝐴) ∈
(ℤ≥‘(⌊‘(𝐴 / 𝑇)))) |
65 | | fzsplit2 13281 |
. . . . 5
⊢
((((⌊‘(𝐴
/ 𝑇)) + 1) ∈
(ℤ≥‘1) ∧ (⌊‘𝐴) ∈
(ℤ≥‘(⌊‘(𝐴 / 𝑇)))) → (1...(⌊‘𝐴)) = ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
66 | 52, 64, 65 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (1...(⌊‘𝐴)) = ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
67 | 11 | recnd 11003 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℂ) |
68 | 48, 66, 1, 67 | fsumsplit 15453 |
. . 3
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛))) |
69 | | fzfid 13693 |
. . . . 5
⊢ (𝜑 → (1...(⌊‘(𝐴 / 𝑇))) ∈ Fin) |
70 | | ssun1 4106 |
. . . . . . . 8
⊢
(1...(⌊‘(𝐴 / 𝑇))) ⊆ ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) |
71 | 70, 66 | sseqtrrid 3974 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘(𝐴 / 𝑇))) ⊆ (1...(⌊‘𝐴))) |
72 | 71 | sselda 3921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ (1...(⌊‘𝐴))) |
73 | 72, 11 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → ((abs‘𝐵) / 𝑛) ∈ ℝ) |
74 | 69, 73 | fsumrecl 15446 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ∈ ℝ) |
75 | | fzfid 13693 |
. . . . 5
⊢ (𝜑 → (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) ∈ Fin) |
76 | | ssun2 4107 |
. . . . . . . 8
⊢
(((⌊‘(𝐴
/ 𝑇)) +
1)...(⌊‘𝐴))
⊆ ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) |
77 | 76, 66 | sseqtrrid 3974 |
. . . . . . 7
⊢ (𝜑 → (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴))) |
78 | 77 | sselda 3921 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ (1...(⌊‘𝐴))) |
79 | 78, 11 | syldan 591 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℝ) |
80 | 75, 79 | fsumrecl 15446 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ∈ ℝ) |
81 | 72, 13 | syldan 591 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝐶 ∈ ℝ) |
82 | 69, 81 | fsumrecl 15446 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶 ∈ ℝ) |
83 | | fznnfl 13582 |
. . . . . . . . . . 11
⊢ ((𝐴 / 𝑇) ∈ ℝ → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑇)))) |
84 | 53, 83 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑇)))) |
85 | 84 | simplbda 500 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ≤ (𝐴 / 𝑇)) |
86 | 32 | rpred 12772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ) |
87 | 54 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
88 | 55 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑇 ∈ ℝ ∧ 0 < 𝑇)) |
89 | | lemuldiv2 11856 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 <
𝑇)) → ((𝑇 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
90 | 86, 87, 88, 89 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑇 · 𝑛) ≤ 𝐴 ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
91 | 18 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 𝑇 ∈ ℝ) |
92 | 91, 87, 32 | lemuldivd 12821 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑇 · 𝑛) ≤ 𝐴 ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
93 | 90, 92 | bitr3d 280 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ≤ (𝐴 / 𝑇) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
94 | 72, 93 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (𝑛 ≤ (𝐴 / 𝑇) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
95 | 85, 94 | mpbid 231 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑇 ≤ (𝐴 / 𝑛)) |
96 | | fsumharmonic.1 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑇 ≤ (𝐴 / 𝑛)) → (abs‘𝐵) ≤ (𝐶 · 𝑛)) |
97 | 96 | ex 413 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑇 ≤ (𝐴 / 𝑛) → (abs‘𝐵) ≤ (𝐶 · 𝑛))) |
98 | 72, 97 | syldan 591 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (𝑇 ≤ (𝐴 / 𝑛) → (abs‘𝐵) ≤ (𝐶 · 𝑛))) |
99 | 95, 98 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (abs‘𝐵) ≤ (𝐶 · 𝑛)) |
100 | 72, 2 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝐵 ∈ ℂ) |
101 | 100 | abscld 15148 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (abs‘𝐵) ∈ ℝ) |
102 | 72, 3 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℕ) |
103 | 102 | nnrpd 12770 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℝ+) |
104 | 101, 81, 103 | ledivmul2d 12826 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (((abs‘𝐵) / 𝑛) ≤ 𝐶 ↔ (abs‘𝐵) ≤ (𝐶 · 𝑛))) |
105 | 99, 104 | mpbird 256 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → ((abs‘𝐵) / 𝑛) ≤ 𝐶) |
106 | 69, 73, 81, 105 | fsumle 15511 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶) |
107 | | fsumharmonic.0 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → 0 ≤ 𝐶) |
108 | 1, 13, 107, 71 | fsumless 15508 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶 ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶) |
109 | 74, 82, 14, 106, 108 | letrd 11132 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶) |
110 | 78, 3 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℕ) |
111 | 110 | nnrecred 12024 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℝ) |
112 | 75, 111 | fsumrecl 15446 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ) |
113 | 16, 112 | remulcld 11005 |
. . . . 5
⊢ (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ∈ ℝ) |
114 | 16 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑅 ∈ ℝ) |
115 | 114 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑅 ∈ ℂ) |
116 | 110 | nncnd 11989 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℂ) |
117 | 110 | nnne0d 12023 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ≠ 0) |
118 | 115, 116,
117 | divrecd 11754 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 / 𝑛) = (𝑅 · (1 / 𝑛))) |
119 | 114, 110 | nndivred 12027 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 / 𝑛) ∈ ℝ) |
120 | 118, 119 | eqeltrrd 2840 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 · (1 / 𝑛)) ∈ ℝ) |
121 | 78, 10 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (abs‘𝐵) ∈ ℝ) |
122 | 78, 32 | syldan 591 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℝ+) |
123 | | noel 4264 |
. . . . . . . . . . . . . . . 16
⊢ ¬
𝑛 ∈
∅ |
124 | | elin 3903 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
((1...(⌊‘(𝐴 /
𝑇))) ∩
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
125 | 48 | eleq2d 2824 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑛 ∈ ((1...(⌊‘(𝐴 / 𝑇))) ∩ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ 𝑛 ∈ ∅)) |
126 | 124, 125 | bitr3id 285 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ 𝑛 ∈ ∅)) |
127 | 123, 126 | mtbiri 327 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ¬ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
128 | | imnan 400 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 ∈
(1...(⌊‘(𝐴 /
𝑇))) → ¬ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ ¬ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
129 | 127, 128 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) → ¬ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))) |
130 | 129 | con2d 134 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) → ¬ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))))) |
131 | 130 | imp 407 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ¬ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) |
132 | 83 | baibd 540 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 / 𝑇) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
133 | 53, 3, 132 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑛 ≤ (𝐴 / 𝑇))) |
134 | 133, 93 | bitrd 278 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
135 | 78, 134 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑇 ≤ (𝐴 / 𝑛))) |
136 | 131, 135 | mtbid 324 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ¬ 𝑇 ≤ (𝐴 / 𝑛)) |
137 | 54 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝐴 ∈ ℝ) |
138 | 137, 110 | nndivred 12027 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝐴 / 𝑛) ∈ ℝ) |
139 | 18 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑇 ∈ ℝ) |
140 | 138, 139 | ltnled 11122 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 ↔ ¬ 𝑇 ≤ (𝐴 / 𝑛))) |
141 | 136, 140 | mpbird 256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝐴 / 𝑛) < 𝑇) |
142 | | fsumharmonic.2 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝐴 / 𝑛) < 𝑇) → (abs‘𝐵) ≤ 𝑅) |
143 | 142 | ex 413 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 → (abs‘𝐵) ≤ 𝑅)) |
144 | 78, 143 | syldan 591 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 → (abs‘𝐵) ≤ 𝑅)) |
145 | 141, 144 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (abs‘𝐵) ≤ 𝑅) |
146 | 121, 114,
122, 145 | lediv1dd 12830 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ≤ (𝑅 / 𝑛)) |
147 | 146, 118 | breqtrd 5100 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ≤ (𝑅 · (1 / 𝑛))) |
148 | 75, 79, 120, 147 | fsumle 15511 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(𝑅 · (1 / 𝑛))) |
149 | 16 | recnd 11003 |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ ℂ) |
150 | 111 | recnd 11003 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℂ) |
151 | 75, 149, 150 | fsummulc2 15496 |
. . . . . 6
⊢ (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) = Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(𝑅 · (1 / 𝑛))) |
152 | 148, 151 | breqtrrd 5102 |
. . . . 5
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛))) |
153 | 102 | nnrecred 12024 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈ ℝ) |
154 | 69, 153 | fsumrecl 15446 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℝ) |
155 | 154 | recnd 11003 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℂ) |
156 | 112 | recnd 11003 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℂ) |
157 | 4 | nnrecred 12024 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℝ) |
158 | 157 | recnd 11003 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ (1...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℂ) |
159 | 48, 66, 1, 158 | fsumsplit 15453 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛))) |
160 | 155, 156,
159 | mvrladdd 11388 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) = Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) |
161 | 1, 157 | fsumrecl 15446 |
. . . . . . . . . . 11
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ) |
162 | 161 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ) |
163 | 154 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℝ) |
164 | 162, 163 | resubcld 11403 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ∈ ℝ) |
165 | | 0red 10978 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → 0 ∈
ℝ) |
166 | 27 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → ((log‘𝑇) + 1) ∈
ℝ) |
167 | | fzfid 13693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘(𝐴 / 𝑇))) ∈ Fin) |
168 | 103 | adantlr 712 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℝ+) |
169 | 168 | rpreccld 12782 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈
ℝ+) |
170 | 169 | rpred 12772 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈ ℝ) |
171 | 169 | rpge0d 12776 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 0 ≤ (1 / 𝑛)) |
172 | 40 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 ∈
ℝ+) |
173 | 172 | rpge0d 12776 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 < 1) → 0 ≤ 𝐴) |
174 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 < 1) |
175 | | 0p1e1 12095 |
. . . . . . . . . . . . . . . 16
⊢ (0 + 1) =
1 |
176 | 174, 175 | breqtrrdi 5116 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 < (0 + 1)) |
177 | 54 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐴 < 1) → 𝐴 ∈ ℝ) |
178 | | 0z 12330 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℤ |
179 | | flbi 13536 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 0 ∈
ℤ) → ((⌊‘𝐴) = 0 ↔ (0 ≤ 𝐴 ∧ 𝐴 < (0 + 1)))) |
180 | 177, 178,
179 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐴 < 1) → ((⌊‘𝐴) = 0 ↔ (0 ≤ 𝐴 ∧ 𝐴 < (0 + 1)))) |
181 | 173, 176,
180 | mpbir2and 710 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐴 < 1) → (⌊‘𝐴) = 0) |
182 | 181 | oveq2d 7291 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘𝐴)) = (1...0)) |
183 | | fz10 13277 |
. . . . . . . . . . . . 13
⊢ (1...0) =
∅ |
184 | 182, 183 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘𝐴)) = ∅) |
185 | | 0ss 4330 |
. . . . . . . . . . . 12
⊢ ∅
⊆ (1...(⌊‘(𝐴 / 𝑇))) |
186 | 184, 185 | eqsstrdi 3975 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐴 < 1) → (1...(⌊‘𝐴)) ⊆
(1...(⌊‘(𝐴 /
𝑇)))) |
187 | 167, 170,
171, 186 | fsumless 15508 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) |
188 | 162, 163 | suble0d 11566 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐴 < 1) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ 0 ↔ Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛))) |
189 | 187, 188 | mpbird 256 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ 0) |
190 | 18, 23 | logge0d 25785 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ (log‘𝑇)) |
191 | | 0le1 11498 |
. . . . . . . . . . . 12
⊢ 0 ≤
1 |
192 | 191 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 1) |
193 | 26, 20, 190, 192 | addge0d 11551 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ ((log‘𝑇) + 1)) |
194 | 193 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐴 < 1) → 0 ≤ ((log‘𝑇) + 1)) |
195 | 164, 165,
166, 189, 194 | letrd 11132 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1)) |
196 | | harmonicubnd 26159 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ≤ ((log‘𝐴) + 1)) |
197 | 54, 196 | sylan 580 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1)) |
198 | | harmoniclbnd 26158 |
. . . . . . . . . . . 12
⊢ ((𝐴 / 𝑇) ∈ ℝ+ →
(log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈
(1...(⌊‘(𝐴 /
𝑇)))(1 / 𝑛)) |
199 | 41, 198 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) |
200 | 199 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) |
201 | 40 | relogcld 25778 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (log‘𝐴) ∈
ℝ) |
202 | | peano2re 11148 |
. . . . . . . . . . . . 13
⊢
((log‘𝐴)
∈ ℝ → ((log‘𝐴) + 1) ∈ ℝ) |
203 | 201, 202 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((log‘𝐴) + 1) ∈
ℝ) |
204 | 41 | relogcld 25778 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐴 / 𝑇)) ∈ ℝ) |
205 | | le2sub 11474 |
. . . . . . . . . . . 12
⊢
(((Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ∈ ℝ ∧
Σ𝑛 ∈
(1...(⌊‘(𝐴 /
𝑇)))(1 / 𝑛) ∈ ℝ) ∧ (((log‘𝐴) + 1) ∈ ℝ ∧
(log‘(𝐴 / 𝑇)) ∈ ℝ)) →
((Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))))) |
206 | 161, 154,
203, 204, 205 | syl22anc 836 |
. . . . . . . . . . 11
⊢ (𝜑 → ((Σ𝑛 ∈
(1...(⌊‘𝐴))(1 /
𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))))) |
207 | 206 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))))) |
208 | 197, 200,
207 | mp2and 696 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇)))) |
209 | 201 | recnd 11003 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘𝐴) ∈
ℂ) |
210 | 20 | recnd 11003 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ∈
ℂ) |
211 | 26 | recnd 11003 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘𝑇) ∈
ℂ) |
212 | 209, 210,
211 | pnncand 11371 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘𝐴) + 1) − ((log‘𝐴) − (log‘𝑇))) = (1 + (log‘𝑇))) |
213 | 40, 25 | relogdivd 25781 |
. . . . . . . . . . . 12
⊢ (𝜑 → (log‘(𝐴 / 𝑇)) = ((log‘𝐴) − (log‘𝑇))) |
214 | 213 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (𝜑 → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = (((log‘𝐴) + 1) − ((log‘𝐴) − (log‘𝑇)))) |
215 | | ax-1cn 10929 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
216 | | addcom 11161 |
. . . . . . . . . . . 12
⊢
(((log‘𝑇)
∈ ℂ ∧ 1 ∈ ℂ) → ((log‘𝑇) + 1) = (1 + (log‘𝑇))) |
217 | 211, 215,
216 | sylancl 586 |
. . . . . . . . . . 11
⊢ (𝜑 → ((log‘𝑇) + 1) = (1 + (log‘𝑇))) |
218 | 212, 214,
217 | 3eqtr4d 2788 |
. . . . . . . . . 10
⊢ (𝜑 → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = ((log‘𝑇) + 1)) |
219 | 218 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = ((log‘𝑇) + 1)) |
220 | 208, 219 | breqtrd 5100 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1)) |
221 | 195, 220,
54, 20 | ltlecasei 11083 |
. . . . . . 7
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1)) |
222 | 160, 221 | eqbrtrrd 5098 |
. . . . . 6
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝑇) + 1)) |
223 | | lemul2a 11830 |
. . . . . 6
⊢
(((Σ𝑛 ∈
(((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ ∧ ((log‘𝑇) + 1) ∈ ℝ ∧
(𝑅 ∈ ℝ ∧ 0
≤ 𝑅)) ∧ Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝑇) + 1)) → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ≤ (𝑅 · ((log‘𝑇) + 1))) |
224 | 112, 27, 15, 222, 223 | syl31anc 1372 |
. . . . 5
⊢ (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ≤ (𝑅 · ((log‘𝑇) + 1))) |
225 | 80, 113, 28, 152, 224 | letrd 11132 |
. . . 4
⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (𝑅 · ((log‘𝑇) + 1))) |
226 | 74, 80, 14, 28, 109, 225 | le2addd 11594 |
. . 3
⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) |
227 | 68, 226 | eqbrtrd 5096 |
. 2
⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) |
228 | 9, 12, 29, 39, 227 | letrd 11132 |
1
⊢ (𝜑 → (abs‘Σ𝑛 ∈
(1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1)))) |