MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumharmonic Structured version   Visualization version   GIF version

Theorem fsumharmonic 26957
Description: Bound a finite sum based on the harmonic series, where the "strong" bound 𝐶 only applies asymptotically, and there is a "weak" bound 𝑅 for the remaining values. (Contributed by Mario Carneiro, 18-May-2016.)
Hypotheses
Ref Expression
fsumharmonic.a (𝜑𝐴 ∈ ℝ+)
fsumharmonic.t (𝜑 → (𝑇 ∈ ℝ ∧ 1 ≤ 𝑇))
fsumharmonic.r (𝜑 → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
fsumharmonic.b ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ)
fsumharmonic.c ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝐶 ∈ ℝ)
fsumharmonic.0 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 0 ≤ 𝐶)
fsumharmonic.1 (((𝜑𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑇 ≤ (𝐴 / 𝑛)) → (abs‘𝐵) ≤ (𝐶 · 𝑛))
fsumharmonic.2 (((𝜑𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝐴 / 𝑛) < 𝑇) → (abs‘𝐵) ≤ 𝑅)
Assertion
Ref Expression
fsumharmonic (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))))
Distinct variable groups:   𝐴,𝑛   𝜑,𝑛   𝑅,𝑛   𝑇,𝑛
Allowed substitution hints:   𝐵(𝑛)   𝐶(𝑛)

Proof of Theorem fsumharmonic
StepHypRef Expression
1 fzfid 13971 . . . 4 (𝜑 → (1...(⌊‘𝐴)) ∈ Fin)
2 fsumharmonic.b . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ)
3 elfznn 13563 . . . . . . 7 (𝑛 ∈ (1...(⌊‘𝐴)) → 𝑛 ∈ ℕ)
43adantl 481 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
54nncnd 12259 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℂ)
64nnne0d 12293 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ≠ 0)
72, 5, 6divcld 12021 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝐵 / 𝑛) ∈ ℂ)
81, 7fsumcl 15712 . . 3 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛) ∈ ℂ)
98abscld 15416 . 2 (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ∈ ℝ)
102abscld 15416 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘𝐵) ∈ ℝ)
1110, 4nndivred 12297 . . 3 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℝ)
121, 11fsumrecl 15713 . 2 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ∈ ℝ)
13 fsumharmonic.c . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝐶 ∈ ℝ)
141, 13fsumrecl 15713 . . 3 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 ∈ ℝ)
15 fsumharmonic.r . . . . 5 (𝜑 → (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅))
1615simpld 494 . . . 4 (𝜑𝑅 ∈ ℝ)
17 fsumharmonic.t . . . . . . . 8 (𝜑 → (𝑇 ∈ ℝ ∧ 1 ≤ 𝑇))
1817simpld 494 . . . . . . 7 (𝜑𝑇 ∈ ℝ)
19 0red 11248 . . . . . . . 8 (𝜑 → 0 ∈ ℝ)
20 1red 11246 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
21 0lt1 11767 . . . . . . . . 9 0 < 1
2221a1i 11 . . . . . . . 8 (𝜑 → 0 < 1)
2317simprd 495 . . . . . . . 8 (𝜑 → 1 ≤ 𝑇)
2419, 20, 18, 22, 23ltletrd 11405 . . . . . . 7 (𝜑 → 0 < 𝑇)
2518, 24elrpd 13046 . . . . . 6 (𝜑𝑇 ∈ ℝ+)
2625relogcld 26570 . . . . 5 (𝜑 → (log‘𝑇) ∈ ℝ)
2726, 20readdcld 11274 . . . 4 (𝜑 → ((log‘𝑇) + 1) ∈ ℝ)
2816, 27remulcld 11275 . . 3 (𝜑 → (𝑅 · ((log‘𝑇) + 1)) ∈ ℝ)
2914, 28readdcld 11274 . 2 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))) ∈ ℝ)
301, 7fsumabs 15780 . . 3 (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))(abs‘(𝐵 / 𝑛)))
312, 5, 6absdivd 15435 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘(𝐵 / 𝑛)) = ((abs‘𝐵) / (abs‘𝑛)))
324nnrpd 13047 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ+)
3332rprege0d 13056 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ ℝ ∧ 0 ≤ 𝑛))
34 absid 15276 . . . . . . 7 ((𝑛 ∈ ℝ ∧ 0 ≤ 𝑛) → (abs‘𝑛) = 𝑛)
3533, 34syl 17 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘𝑛) = 𝑛)
3635oveq2d 7436 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / (abs‘𝑛)) = ((abs‘𝐵) / 𝑛))
3731, 36eqtrd 2768 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (abs‘(𝐵 / 𝑛)) = ((abs‘𝐵) / 𝑛))
3837sumeq2dv 15682 . . 3 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(abs‘(𝐵 / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛))
3930, 38breqtrd 5174 . 2 (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛))
40 fsumharmonic.a . . . . . . . . . 10 (𝜑𝐴 ∈ ℝ+)
4140, 25rpdivcld 13066 . . . . . . . . 9 (𝜑 → (𝐴 / 𝑇) ∈ ℝ+)
4241rprege0d 13056 . . . . . . . 8 (𝜑 → ((𝐴 / 𝑇) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑇)))
43 flge0nn0 13818 . . . . . . . 8 (((𝐴 / 𝑇) ∈ ℝ ∧ 0 ≤ (𝐴 / 𝑇)) → (⌊‘(𝐴 / 𝑇)) ∈ ℕ0)
4442, 43syl 17 . . . . . . 7 (𝜑 → (⌊‘(𝐴 / 𝑇)) ∈ ℕ0)
4544nn0red 12564 . . . . . 6 (𝜑 → (⌊‘(𝐴 / 𝑇)) ∈ ℝ)
4645ltp1d 12175 . . . . 5 (𝜑 → (⌊‘(𝐴 / 𝑇)) < ((⌊‘(𝐴 / 𝑇)) + 1))
47 fzdisj 13561 . . . . 5 ((⌊‘(𝐴 / 𝑇)) < ((⌊‘(𝐴 / 𝑇)) + 1) → ((1...(⌊‘(𝐴 / 𝑇))) ∩ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) = ∅)
4846, 47syl 17 . . . 4 (𝜑 → ((1...(⌊‘(𝐴 / 𝑇))) ∩ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) = ∅)
49 nn0p1nn 12542 . . . . . . 7 ((⌊‘(𝐴 / 𝑇)) ∈ ℕ0 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈ ℕ)
5044, 49syl 17 . . . . . 6 (𝜑 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈ ℕ)
51 nnuz 12896 . . . . . 6 ℕ = (ℤ‘1)
5250, 51eleqtrdi 2839 . . . . 5 (𝜑 → ((⌊‘(𝐴 / 𝑇)) + 1) ∈ (ℤ‘1))
5341rpred 13049 . . . . . 6 (𝜑 → (𝐴 / 𝑇) ∈ ℝ)
5440rpred 13049 . . . . . 6 (𝜑𝐴 ∈ ℝ)
5518, 24jca 511 . . . . . . . . 9 (𝜑 → (𝑇 ∈ ℝ ∧ 0 < 𝑇))
5640rpregt0d 13055 . . . . . . . . 9 (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
57 lediv2 12135 . . . . . . . . 9 (((1 ∈ ℝ ∧ 0 < 1) ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇) ∧ (𝐴 ∈ ℝ ∧ 0 < 𝐴)) → (1 ≤ 𝑇 ↔ (𝐴 / 𝑇) ≤ (𝐴 / 1)))
5820, 22, 55, 56, 57syl211anc 1374 . . . . . . . 8 (𝜑 → (1 ≤ 𝑇 ↔ (𝐴 / 𝑇) ≤ (𝐴 / 1)))
5923, 58mpbid 231 . . . . . . 7 (𝜑 → (𝐴 / 𝑇) ≤ (𝐴 / 1))
6054recnd 11273 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
6160div1d 12013 . . . . . . 7 (𝜑 → (𝐴 / 1) = 𝐴)
6259, 61breqtrd 5174 . . . . . 6 (𝜑 → (𝐴 / 𝑇) ≤ 𝐴)
63 flword2 13811 . . . . . 6 (((𝐴 / 𝑇) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝐴 / 𝑇) ≤ 𝐴) → (⌊‘𝐴) ∈ (ℤ‘(⌊‘(𝐴 / 𝑇))))
6453, 54, 62, 63syl3anc 1369 . . . . 5 (𝜑 → (⌊‘𝐴) ∈ (ℤ‘(⌊‘(𝐴 / 𝑇))))
65 fzsplit2 13559 . . . . 5 ((((⌊‘(𝐴 / 𝑇)) + 1) ∈ (ℤ‘1) ∧ (⌊‘𝐴) ∈ (ℤ‘(⌊‘(𝐴 / 𝑇)))) → (1...(⌊‘𝐴)) = ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))))
6652, 64, 65syl2anc 583 . . . 4 (𝜑 → (1...(⌊‘𝐴)) = ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))))
6711recnd 11273 . . . 4 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℂ)
6848, 66, 1, 67fsumsplit 15720 . . 3 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛)))
69 fzfid 13971 . . . . 5 (𝜑 → (1...(⌊‘(𝐴 / 𝑇))) ∈ Fin)
70 ssun1 4172 . . . . . . . 8 (1...(⌊‘(𝐴 / 𝑇))) ⊆ ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))
7170, 66sseqtrrid 4033 . . . . . . 7 (𝜑 → (1...(⌊‘(𝐴 / 𝑇))) ⊆ (1...(⌊‘𝐴)))
7271sselda 3980 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ (1...(⌊‘𝐴)))
7372, 11syldan 590 . . . . 5 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → ((abs‘𝐵) / 𝑛) ∈ ℝ)
7469, 73fsumrecl 15713 . . . 4 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ∈ ℝ)
75 fzfid 13971 . . . . 5 (𝜑 → (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) ∈ Fin)
76 ssun2 4173 . . . . . . . 8 (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) ⊆ ((1...(⌊‘(𝐴 / 𝑇))) ∪ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)))
7776, 66sseqtrrid 4033 . . . . . . 7 (𝜑 → (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) ⊆ (1...(⌊‘𝐴)))
7877sselda 3980 . . . . . 6 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ (1...(⌊‘𝐴)))
7978, 11syldan 590 . . . . 5 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ∈ ℝ)
8075, 79fsumrecl 15713 . . . 4 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ∈ ℝ)
8172, 13syldan 590 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝐶 ∈ ℝ)
8269, 81fsumrecl 15713 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶 ∈ ℝ)
83 fznnfl 13860 . . . . . . . . . . 11 ((𝐴 / 𝑇) ∈ ℝ → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑇))))
8453, 83syl 17 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ (𝐴 / 𝑇))))
8584simplbda 499 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ≤ (𝐴 / 𝑇))
8632rpred 13049 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑛 ∈ ℝ)
8754adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝐴 ∈ ℝ)
8855adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝑇 ∈ ℝ ∧ 0 < 𝑇))
89 lemuldiv2 12126 . . . . . . . . . . . 12 ((𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ (𝑇 ∈ ℝ ∧ 0 < 𝑇)) → ((𝑇 · 𝑛) ≤ 𝐴𝑛 ≤ (𝐴 / 𝑇)))
9086, 87, 88, 89syl3anc 1369 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑇 · 𝑛) ≤ 𝐴𝑛 ≤ (𝐴 / 𝑇)))
9118adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 𝑇 ∈ ℝ)
9291, 87, 32lemuldivd 13098 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → ((𝑇 · 𝑛) ≤ 𝐴𝑇 ≤ (𝐴 / 𝑛)))
9390, 92bitr3d 281 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ≤ (𝐴 / 𝑇) ↔ 𝑇 ≤ (𝐴 / 𝑛)))
9472, 93syldan 590 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (𝑛 ≤ (𝐴 / 𝑇) ↔ 𝑇 ≤ (𝐴 / 𝑛)))
9585, 94mpbid 231 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑇 ≤ (𝐴 / 𝑛))
96 fsumharmonic.1 . . . . . . . . . 10 (((𝜑𝑛 ∈ (1...(⌊‘𝐴))) ∧ 𝑇 ≤ (𝐴 / 𝑛)) → (abs‘𝐵) ≤ (𝐶 · 𝑛))
9796ex 412 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝑇 ≤ (𝐴 / 𝑛) → (abs‘𝐵) ≤ (𝐶 · 𝑛)))
9872, 97syldan 590 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (𝑇 ≤ (𝐴 / 𝑛) → (abs‘𝐵) ≤ (𝐶 · 𝑛)))
9995, 98mpd 15 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (abs‘𝐵) ≤ (𝐶 · 𝑛))
10072, 2syldan 590 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝐵 ∈ ℂ)
101100abscld 15416 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (abs‘𝐵) ∈ ℝ)
10272, 3syl 17 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℕ)
103102nnrpd 13047 . . . . . . . 8 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℝ+)
104101, 81, 103ledivmul2d 13103 . . . . . . 7 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (((abs‘𝐵) / 𝑛) ≤ 𝐶 ↔ (abs‘𝐵) ≤ (𝐶 · 𝑛)))
10599, 104mpbird 257 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → ((abs‘𝐵) / 𝑛) ≤ 𝐶)
10669, 73, 81, 105fsumle 15778 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶)
107 fsumharmonic.0 . . . . . 6 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → 0 ≤ 𝐶)
1081, 13, 107, 71fsumless 15775 . . . . 5 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))𝐶 ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶)
10974, 82, 14, 106, 108letrd 11402 . . . 4 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶)
11078, 3syl 17 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℕ)
111110nnrecred 12294 . . . . . . 7 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℝ)
11275, 111fsumrecl 15713 . . . . . 6 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ)
11316, 112remulcld 11275 . . . . 5 (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ∈ ℝ)
11416adantr 480 . . . . . . . . . 10 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑅 ∈ ℝ)
115114recnd 11273 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑅 ∈ ℂ)
116110nncnd 12259 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℂ)
117110nnne0d 12293 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ≠ 0)
118115, 116, 117divrecd 12024 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 / 𝑛) = (𝑅 · (1 / 𝑛)))
119114, 110nndivred 12297 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 / 𝑛) ∈ ℝ)
120118, 119eqeltrrd 2830 . . . . . . 7 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑅 · (1 / 𝑛)) ∈ ℝ)
12178, 10syldan 590 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (abs‘𝐵) ∈ ℝ)
12278, 32syldan 590 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑛 ∈ ℝ+)
123 noel 4331 . . . . . . . . . . . . . . . 16 ¬ 𝑛 ∈ ∅
124 elin 3963 . . . . . . . . . . . . . . . . 17 (𝑛 ∈ ((1...(⌊‘(𝐴 / 𝑇))) ∩ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))))
12548eleq2d 2815 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑛 ∈ ((1...(⌊‘(𝐴 / 𝑇))) ∩ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ 𝑛 ∈ ∅))
126124, 125bitr3id 285 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ 𝑛 ∈ ∅))
127123, 126mtbiri 327 . . . . . . . . . . . . . . 15 (𝜑 → ¬ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))))
128 imnan 399 . . . . . . . . . . . . . . 15 ((𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) → ¬ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) ↔ ¬ (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ∧ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))))
129127, 128sylibr 233 . . . . . . . . . . . . . 14 (𝜑 → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) → ¬ 𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))))
130129con2d 134 . . . . . . . . . . . . 13 (𝜑 → (𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴)) → ¬ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))))
131130imp 406 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ¬ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))))
13283baibd 539 . . . . . . . . . . . . . . 15 (((𝐴 / 𝑇) ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑛 ≤ (𝐴 / 𝑇)))
13353, 3, 132syl2an 595 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑛 ≤ (𝐴 / 𝑇)))
134133, 93bitrd 279 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑇 ≤ (𝐴 / 𝑛)))
13578, 134syldan 590 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇))) ↔ 𝑇 ≤ (𝐴 / 𝑛)))
136131, 135mtbid 324 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ¬ 𝑇 ≤ (𝐴 / 𝑛))
13754adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝐴 ∈ ℝ)
138137, 110nndivred 12297 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝐴 / 𝑛) ∈ ℝ)
13918adantr 480 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → 𝑇 ∈ ℝ)
140138, 139ltnled 11392 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 ↔ ¬ 𝑇 ≤ (𝐴 / 𝑛)))
141136, 140mpbird 257 . . . . . . . . . 10 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (𝐴 / 𝑛) < 𝑇)
142 fsumharmonic.2 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ (1...(⌊‘𝐴))) ∧ (𝐴 / 𝑛) < 𝑇) → (abs‘𝐵) ≤ 𝑅)
143142ex 412 . . . . . . . . . . 11 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 → (abs‘𝐵) ≤ 𝑅))
14478, 143syldan 590 . . . . . . . . . 10 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((𝐴 / 𝑛) < 𝑇 → (abs‘𝐵) ≤ 𝑅))
145141, 144mpd 15 . . . . . . . . 9 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (abs‘𝐵) ≤ 𝑅)
146121, 114, 122, 145lediv1dd 13107 . . . . . . . 8 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ≤ (𝑅 / 𝑛))
147146, 118breqtrd 5174 . . . . . . 7 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → ((abs‘𝐵) / 𝑛) ≤ (𝑅 · (1 / 𝑛)))
14875, 79, 120, 147fsumle 15778 . . . . . 6 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(𝑅 · (1 / 𝑛)))
14916recnd 11273 . . . . . . 7 (𝜑𝑅 ∈ ℂ)
150111recnd 11273 . . . . . . 7 ((𝜑𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℂ)
15175, 149, 150fsummulc2 15763 . . . . . 6 (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) = Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(𝑅 · (1 / 𝑛)))
152148, 151breqtrrd 5176 . . . . 5 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)))
153102nnrecred 12294 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈ ℝ)
15469, 153fsumrecl 15713 . . . . . . . . 9 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℝ)
155154recnd 11273 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℂ)
156112recnd 11273 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℂ)
1574nnrecred 12294 . . . . . . . . . 10 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℝ)
158157recnd 11273 . . . . . . . . 9 ((𝜑𝑛 ∈ (1...(⌊‘𝐴))) → (1 / 𝑛) ∈ ℂ)
15948, 66, 1, 158fsumsplit 15720 . . . . . . . 8 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)))
160155, 156, 159mvrladdd 11658 . . . . . . 7 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) = Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛))
1611, 157fsumrecl 15713 . . . . . . . . . . 11 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ)
162161adantr 480 . . . . . . . . . 10 ((𝜑𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ)
163154adantr 480 . . . . . . . . . 10 ((𝜑𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℝ)
164162, 163resubcld 11673 . . . . . . . . 9 ((𝜑𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ∈ ℝ)
165 0red 11248 . . . . . . . . 9 ((𝜑𝐴 < 1) → 0 ∈ ℝ)
16627adantr 480 . . . . . . . . 9 ((𝜑𝐴 < 1) → ((log‘𝑇) + 1) ∈ ℝ)
167 fzfid 13971 . . . . . . . . . . 11 ((𝜑𝐴 < 1) → (1...(⌊‘(𝐴 / 𝑇))) ∈ Fin)
168103adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 𝑛 ∈ ℝ+)
169168rpreccld 13059 . . . . . . . . . . . 12 (((𝜑𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈ ℝ+)
170169rpred 13049 . . . . . . . . . . 11 (((𝜑𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → (1 / 𝑛) ∈ ℝ)
171169rpge0d 13053 . . . . . . . . . . 11 (((𝜑𝐴 < 1) ∧ 𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))) → 0 ≤ (1 / 𝑛))
17240adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 < 1) → 𝐴 ∈ ℝ+)
173172rpge0d 13053 . . . . . . . . . . . . . . 15 ((𝜑𝐴 < 1) → 0 ≤ 𝐴)
174 simpr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 < 1) → 𝐴 < 1)
175 0p1e1 12365 . . . . . . . . . . . . . . . 16 (0 + 1) = 1
176174, 175breqtrrdi 5190 . . . . . . . . . . . . . . 15 ((𝜑𝐴 < 1) → 𝐴 < (0 + 1))
17754adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝐴 < 1) → 𝐴 ∈ ℝ)
178 0z 12600 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
179 flbi 13814 . . . . . . . . . . . . . . . 16 ((𝐴 ∈ ℝ ∧ 0 ∈ ℤ) → ((⌊‘𝐴) = 0 ↔ (0 ≤ 𝐴𝐴 < (0 + 1))))
180177, 178, 179sylancl 585 . . . . . . . . . . . . . . 15 ((𝜑𝐴 < 1) → ((⌊‘𝐴) = 0 ↔ (0 ≤ 𝐴𝐴 < (0 + 1))))
181173, 176, 180mpbir2and 712 . . . . . . . . . . . . . 14 ((𝜑𝐴 < 1) → (⌊‘𝐴) = 0)
182181oveq2d 7436 . . . . . . . . . . . . 13 ((𝜑𝐴 < 1) → (1...(⌊‘𝐴)) = (1...0))
183 fz10 13555 . . . . . . . . . . . . 13 (1...0) = ∅
184182, 183eqtrdi 2784 . . . . . . . . . . . 12 ((𝜑𝐴 < 1) → (1...(⌊‘𝐴)) = ∅)
185 0ss 4397 . . . . . . . . . . . 12 ∅ ⊆ (1...(⌊‘(𝐴 / 𝑇)))
186184, 185eqsstrdi 4034 . . . . . . . . . . 11 ((𝜑𝐴 < 1) → (1...(⌊‘𝐴)) ⊆ (1...(⌊‘(𝐴 / 𝑇))))
187167, 170, 171, 186fsumless 15775 . . . . . . . . . 10 ((𝜑𝐴 < 1) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛))
188162, 163suble0d 11836 . . . . . . . . . 10 ((𝜑𝐴 < 1) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ 0 ↔ Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)))
189187, 188mpbird 257 . . . . . . . . 9 ((𝜑𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ 0)
19018, 23logge0d 26577 . . . . . . . . . . 11 (𝜑 → 0 ≤ (log‘𝑇))
191 0le1 11768 . . . . . . . . . . . 12 0 ≤ 1
192191a1i 11 . . . . . . . . . . 11 (𝜑 → 0 ≤ 1)
19326, 20, 190, 192addge0d 11821 . . . . . . . . . 10 (𝜑 → 0 ≤ ((log‘𝑇) + 1))
194193adantr 480 . . . . . . . . 9 ((𝜑𝐴 < 1) → 0 ≤ ((log‘𝑇) + 1))
195164, 165, 166, 189, 194letrd 11402 . . . . . . . 8 ((𝜑𝐴 < 1) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1))
196 harmonicubnd 26955 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1))
19754, 196sylan 579 . . . . . . . . . 10 ((𝜑 ∧ 1 ≤ 𝐴) → Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1))
198 harmoniclbnd 26954 . . . . . . . . . . . 12 ((𝐴 / 𝑇) ∈ ℝ+ → (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛))
19941, 198syl 17 . . . . . . . . . . 11 (𝜑 → (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛))
200199adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 1 ≤ 𝐴) → (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛))
20140relogcld 26570 . . . . . . . . . . . . 13 (𝜑 → (log‘𝐴) ∈ ℝ)
202 peano2re 11418 . . . . . . . . . . . . 13 ((log‘𝐴) ∈ ℝ → ((log‘𝐴) + 1) ∈ ℝ)
203201, 202syl 17 . . . . . . . . . . . 12 (𝜑 → ((log‘𝐴) + 1) ∈ ℝ)
20441relogcld 26570 . . . . . . . . . . . 12 (𝜑 → (log‘(𝐴 / 𝑇)) ∈ ℝ)
205 le2sub 11744 . . . . . . . . . . . 12 (((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛) ∈ ℝ) ∧ (((log‘𝐴) + 1) ∈ ℝ ∧ (log‘(𝐴 / 𝑇)) ∈ ℝ)) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇)))))
206161, 154, 203, 204, 205syl22anc 838 . . . . . . . . . . 11 (𝜑 → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇)))))
207206adantr 480 . . . . . . . . . 10 ((𝜑 ∧ 1 ≤ 𝐴) → ((Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝐴) + 1) ∧ (log‘(𝐴 / 𝑇)) ≤ Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇)))))
208197, 200, 207mp2and 698 . . . . . . . . 9 ((𝜑 ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))))
209201recnd 11273 . . . . . . . . . . . 12 (𝜑 → (log‘𝐴) ∈ ℂ)
21020recnd 11273 . . . . . . . . . . . 12 (𝜑 → 1 ∈ ℂ)
21126recnd 11273 . . . . . . . . . . . 12 (𝜑 → (log‘𝑇) ∈ ℂ)
212209, 210, 211pnncand 11641 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴) + 1) − ((log‘𝐴) − (log‘𝑇))) = (1 + (log‘𝑇)))
21340, 25relogdivd 26573 . . . . . . . . . . . 12 (𝜑 → (log‘(𝐴 / 𝑇)) = ((log‘𝐴) − (log‘𝑇)))
214213oveq2d 7436 . . . . . . . . . . 11 (𝜑 → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = (((log‘𝐴) + 1) − ((log‘𝐴) − (log‘𝑇))))
215 ax-1cn 11197 . . . . . . . . . . . 12 1 ∈ ℂ
216 addcom 11431 . . . . . . . . . . . 12 (((log‘𝑇) ∈ ℂ ∧ 1 ∈ ℂ) → ((log‘𝑇) + 1) = (1 + (log‘𝑇)))
217211, 215, 216sylancl 585 . . . . . . . . . . 11 (𝜑 → ((log‘𝑇) + 1) = (1 + (log‘𝑇)))
218212, 214, 2173eqtr4d 2778 . . . . . . . . . 10 (𝜑 → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = ((log‘𝑇) + 1))
219218adantr 480 . . . . . . . . 9 ((𝜑 ∧ 1 ≤ 𝐴) → (((log‘𝐴) + 1) − (log‘(𝐴 / 𝑇))) = ((log‘𝑇) + 1))
220208, 219breqtrd 5174 . . . . . . . 8 ((𝜑 ∧ 1 ≤ 𝐴) → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1))
221195, 220, 54, 20ltlecasei 11353 . . . . . . 7 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))(1 / 𝑛) − Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))(1 / 𝑛)) ≤ ((log‘𝑇) + 1))
222160, 221eqbrtrrd 5172 . . . . . 6 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝑇) + 1))
223 lemul2a 12100 . . . . . 6 (((Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ∈ ℝ ∧ ((log‘𝑇) + 1) ∈ ℝ ∧ (𝑅 ∈ ℝ ∧ 0 ≤ 𝑅)) ∧ Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛) ≤ ((log‘𝑇) + 1)) → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ≤ (𝑅 · ((log‘𝑇) + 1)))
224112, 27, 15, 222, 223syl31anc 1371 . . . . 5 (𝜑 → (𝑅 · Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))(1 / 𝑛)) ≤ (𝑅 · ((log‘𝑇) + 1)))
22580, 113, 28, 152, 224letrd 11402 . . . 4 (𝜑 → Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (𝑅 · ((log‘𝑇) + 1)))
22674, 80, 14, 28, 109, 225le2addd 11864 . . 3 (𝜑 → (Σ𝑛 ∈ (1...(⌊‘(𝐴 / 𝑇)))((abs‘𝐵) / 𝑛) + Σ𝑛 ∈ (((⌊‘(𝐴 / 𝑇)) + 1)...(⌊‘𝐴))((abs‘𝐵) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))))
22768, 226eqbrtrd 5170 . 2 (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((abs‘𝐵) / 𝑛) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))))
2289, 12, 29, 39, 227letrd 11402 1 (𝜑 → (abs‘Σ𝑛 ∈ (1...(⌊‘𝐴))(𝐵 / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝐴))𝐶 + (𝑅 · ((log‘𝑇) + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1534  wcel 2099  cun 3945  cin 3946  c0 4323   class class class wbr 5148  cfv 6548  (class class class)co 7420  cc 11137  cr 11138  0cc0 11139  1c1 11140   + caddc 11142   · cmul 11144   < clt 11279  cle 11280  cmin 11475   / cdiv 11902  cn 12243  0cn0 12503  cz 12589  cuz 12853  +crp 13007  ...cfz 13517  cfl 13788  abscabs 15214  Σcsu 15665  logclog 26501
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5365  ax-pr 5429  ax-un 7740  ax-inf2 9665  ax-cnex 11195  ax-resscn 11196  ax-1cn 11197  ax-icn 11198  ax-addcl 11199  ax-addrcl 11200  ax-mulcl 11201  ax-mulrcl 11202  ax-mulcom 11203  ax-addass 11204  ax-mulass 11205  ax-distr 11206  ax-i2m1 11207  ax-1ne0 11208  ax-1rid 11209  ax-rnegex 11210  ax-rrecex 11211  ax-cnre 11212  ax-pre-lttri 11213  ax-pre-lttrn 11214  ax-pre-ltadd 11215  ax-pre-mulgt0 11216  ax-pre-sup 11217  ax-addf 11218
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3373  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4909  df-int 4950  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-isom 6557  df-riota 7376  df-ov 7423  df-oprab 7424  df-mpo 7425  df-of 7685  df-om 7871  df-1st 7993  df-2nd 7994  df-supp 8166  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-2o 8488  df-oadd 8491  df-er 8725  df-map 8847  df-pm 8848  df-ixp 8917  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-fsupp 9387  df-fi 9435  df-sup 9466  df-inf 9467  df-oi 9534  df-card 9963  df-pnf 11281  df-mnf 11282  df-xr 11283  df-ltxr 11284  df-le 11285  df-sub 11477  df-neg 11478  df-div 11903  df-nn 12244  df-2 12306  df-3 12307  df-4 12308  df-5 12309  df-6 12310  df-7 12311  df-8 12312  df-9 12313  df-n0 12504  df-xnn0 12576  df-z 12590  df-dec 12709  df-uz 12854  df-q 12964  df-rp 13008  df-xneg 13125  df-xadd 13126  df-xmul 13127  df-ioo 13361  df-ioc 13362  df-ico 13363  df-icc 13364  df-fz 13518  df-fzo 13661  df-fl 13790  df-mod 13868  df-seq 14000  df-exp 14060  df-fac 14266  df-bc 14295  df-hash 14323  df-shft 15047  df-cj 15079  df-re 15080  df-im 15081  df-sqrt 15215  df-abs 15216  df-limsup 15448  df-clim 15465  df-rlim 15466  df-sum 15666  df-ef 16044  df-e 16045  df-sin 16046  df-cos 16047  df-tan 16048  df-pi 16049  df-dvds 16232  df-struct 17116  df-sets 17133  df-slot 17151  df-ndx 17163  df-base 17181  df-ress 17210  df-plusg 17246  df-mulr 17247  df-starv 17248  df-sca 17249  df-vsca 17250  df-ip 17251  df-tset 17252  df-ple 17253  df-ds 17255  df-unif 17256  df-hom 17257  df-cco 17258  df-rest 17404  df-topn 17405  df-0g 17423  df-gsum 17424  df-topgen 17425  df-pt 17426  df-prds 17429  df-xrs 17484  df-qtop 17489  df-imas 17490  df-xps 17492  df-mre 17566  df-mrc 17567  df-acs 17569  df-mgm 18600  df-sgrp 18679  df-mnd 18695  df-submnd 18741  df-mulg 19024  df-cntz 19268  df-cmn 19737  df-psmet 21271  df-xmet 21272  df-met 21273  df-bl 21274  df-mopn 21275  df-fbas 21276  df-fg 21277  df-cnfld 21280  df-top 22809  df-topon 22826  df-topsp 22848  df-bases 22862  df-cld 22936  df-ntr 22937  df-cls 22938  df-nei 23015  df-lp 23053  df-perf 23054  df-cn 23144  df-cnp 23145  df-haus 23232  df-cmp 23304  df-tx 23479  df-hmeo 23672  df-fil 23763  df-fm 23855  df-flim 23856  df-flf 23857  df-xms 24239  df-ms 24240  df-tms 24241  df-cncf 24811  df-limc 25808  df-dv 25809  df-ulm 26326  df-log 26503  df-atan 26812  df-em 26938
This theorem is referenced by:  dchrvmasumlem2  27444  mulog2sumlem2  27481
  Copyright terms: Public domain W3C validator