Metamath Proof Explorer

Theorem fsumharmonic

Description: Bound a finite sum based on the harmonic series, where the "strong" bound C only applies asymptotically, and there is a "weak" bound R for the remaining values. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses 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 fsumharmonic ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐵 / 𝑛 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 + ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 fsumharmonic.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 fsumharmonic.t ⊢ ( 𝜑 → ( 𝑇 ∈ ℝ ∧ 1 ≤ 𝑇 ) )
3 fsumharmonic.r ⊢ ( 𝜑 → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
4 fsumharmonic.b ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐵 ∈ ℂ )
5 fsumharmonic.c ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐶 ∈ ℝ )
6 fsumharmonic.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ≤ 𝐶 )
7 fsumharmonic.1 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑇 ≤ ( 𝐴 / 𝑛 ) ) → ( abs ‘ 𝐵 ) ≤ ( 𝐶 · 𝑛 ) )
8 fsumharmonic.2 ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ ( 𝐴 / 𝑛 ) < 𝑇 ) → ( abs ‘ 𝐵 ) ≤ 𝑅 )
9 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
10 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
12 11 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℂ )
13 11 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ≠ 0 )
14 4 12 13 divcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐵 / 𝑛 ) ∈ ℂ )
15 9 14 fsumcl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐵 / 𝑛 ) ∈ ℂ )
16 15 abscld ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐵 / 𝑛 ) ) ∈ ℝ )
17 4 abscld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( abs ‘ 𝐵 ) ∈ ℝ )
18 17 11 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( abs ‘ 𝐵 ) / 𝑛 ) ∈ ℝ )
19 9 18 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ∈ ℝ )
20 9 5 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 ∈ ℝ )
21 3 simpld ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
22 2 simpld ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
23 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
24 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
25 0lt1 ⊢ 0 < 1
26 25 a1i ⊢ ( 𝜑 → 0 < 1 )
27 2 simprd ⊢ ( 𝜑 → 1 ≤ 𝑇 )
28 23 24 22 26 27 ltletrd ⊢ ( 𝜑 → 0 < 𝑇 )
29 22 28 elrpd ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
30 29 relogcld ⊢ ( 𝜑 → ( log ‘ 𝑇 ) ∈ ℝ )
31 30 24 readdcld ⊢ ( 𝜑 → ( ( log ‘ 𝑇 ) + 1 ) ∈ ℝ )
32 21 31 remulcld ⊢ ( 𝜑 → ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) ∈ ℝ )
33 20 32 readdcld ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 + ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) ) ∈ ℝ )
34 9 14 fsumabs ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐵 / 𝑛 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( abs ‘ ( 𝐵 / 𝑛 ) ) )
35 4 12 13 absdivd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( abs ‘ ( 𝐵 / 𝑛 ) ) = ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝑛 ) ) )
36 11 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℝ+ )
37 36 rprege0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) )
38 absid ⊢ ( ( 𝑛 ∈ ℝ ∧ 0 ≤ 𝑛 ) → ( abs ‘ 𝑛 ) = 𝑛 )
39 37 38 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( abs ‘ 𝑛 ) = 𝑛 )
40 39 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( abs ‘ 𝐵 ) / ( abs ‘ 𝑛 ) ) = ( ( abs ‘ 𝐵 ) / 𝑛 ) )
41 35 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( abs ‘ ( 𝐵 / 𝑛 ) ) = ( ( abs ‘ 𝐵 ) / 𝑛 ) )
42 41 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( abs ‘ ( 𝐵 / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) )
43 34 42 breqtrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐵 / 𝑛 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) )
44 1 29 rpdivcld ⊢ ( 𝜑 → ( 𝐴 / 𝑇 ) ∈ ℝ+ )
45 44 rprege0d ⊢ ( 𝜑 → ( ( 𝐴 / 𝑇 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝑇 ) ) )
46 flge0nn0 ⊢ ( ( ( 𝐴 / 𝑇 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝑇 ) ) → ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ∈ ℕ0 )
47 45 46 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ∈ ℕ0 )
48 47 nn0red ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ∈ ℝ )
49 48 ltp1d ⊢ ( 𝜑 → ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) < ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) )
50 fzdisj ⊢ ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) < ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) → ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) = ∅ )
51 49 50 syl ⊢ ( 𝜑 → ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) = ∅ )
52 nn0p1nn ⊢ ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ∈ ℕ )
53 47 52 syl ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ∈ ℕ )
54 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
55 53 54 eleqtrdi ⊢ ( 𝜑 → ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
56 44 rpred ⊢ ( 𝜑 → ( 𝐴 / 𝑇 ) ∈ ℝ )
57 1 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
58 22 28 jca ⊢ ( 𝜑 → ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ) )
59 1 rpregt0d ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
60 lediv2 ⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 ≤ 𝑇 ↔ ( 𝐴 / 𝑇 ) ≤ ( 𝐴 / 1 ) ) )
61 24 26 58 59 60 syl211anc ⊢ ( 𝜑 → ( 1 ≤ 𝑇 ↔ ( 𝐴 / 𝑇 ) ≤ ( 𝐴 / 1 ) ) )
62 27 61 mpbid ⊢ ( 𝜑 → ( 𝐴 / 𝑇 ) ≤ ( 𝐴 / 1 ) )
63 57 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
64 63 div1d ⊢ ( 𝜑 → ( 𝐴 / 1 ) = 𝐴 )
65 62 64 breqtrd ⊢ ( 𝜑 → ( 𝐴 / 𝑇 ) ≤ 𝐴 )
66 flword2 ⊢ ( ( ( 𝐴 / 𝑇 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝐴 / 𝑇 ) ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) )
67 56 57 65 66 syl3anc ⊢ ( 𝜑 → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) )
68 fzsplit2 ⊢ ( ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ 𝐴 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) )
69 55 67 68 syl2anc ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) )
70 18 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( abs ‘ 𝐵 ) / 𝑛 ) ∈ ℂ )
71 51 69 9 70 fsumsplit ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ) )
72 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∈ Fin )
73 ssun1 ⊢ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ⊆ ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) )
74 73 69 sseqtrrid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
75 74 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
76 75 18 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( ( abs ‘ 𝐵 ) / 𝑛 ) ∈ ℝ )
77 72 76 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ∈ ℝ )
78 fzfid ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
79 ssun2 ⊢ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) )
80 79 69 sseqtrrid ⊢ ( 𝜑 → ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
81 80 sselda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
82 81 18 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( abs ‘ 𝐵 ) / 𝑛 ) ∈ ℝ )
83 78 82 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ∈ ℝ )
84 75 5 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝐶 ∈ ℝ )
85 72 84 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) 𝐶 ∈ ℝ )
86 fznnfl ⊢ ( ( 𝐴 / 𝑇 ) ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝐴 / 𝑇 ) ) ) )
87 56 86 syl ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ ( 𝐴 / 𝑇 ) ) ) )
88 87 simplbda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝑛 ≤ ( 𝐴 / 𝑇 ) )
89 36 rpred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℝ )
90 57 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
91 58 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ) )
92 lemuldiv2 ⊢ ( ( 𝑛 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 𝑇 ∈ ℝ ∧ 0 < 𝑇 ) ) → ( ( 𝑇 · 𝑛 ) ≤ 𝐴 ↔ 𝑛 ≤ ( 𝐴 / 𝑇 ) ) )
93 89 90 91 92 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑇 · 𝑛 ) ≤ 𝐴 ↔ 𝑛 ≤ ( 𝐴 / 𝑇 ) ) )
94 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑇 ∈ ℝ )
95 94 90 36 lemuldivd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑇 · 𝑛 ) ≤ 𝐴 ↔ 𝑇 ≤ ( 𝐴 / 𝑛 ) ) )
96 93 95 bitr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑛 ≤ ( 𝐴 / 𝑇 ) ↔ 𝑇 ≤ ( 𝐴 / 𝑛 ) ) )
97 75 96 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( 𝑛 ≤ ( 𝐴 / 𝑇 ) ↔ 𝑇 ≤ ( 𝐴 / 𝑛 ) ) )
98 88 97 mpbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝑇 ≤ ( 𝐴 / 𝑛 ) )
99 7 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑇 ≤ ( 𝐴 / 𝑛 ) → ( abs ‘ 𝐵 ) ≤ ( 𝐶 · 𝑛 ) ) )
100 75 99 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( 𝑇 ≤ ( 𝐴 / 𝑛 ) → ( abs ‘ 𝐵 ) ≤ ( 𝐶 · 𝑛 ) ) )
101 98 100 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( abs ‘ 𝐵 ) ≤ ( 𝐶 · 𝑛 ) )
102 75 4 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝐵 ∈ ℂ )
103 102 abscld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( abs ‘ 𝐵 ) ∈ ℝ )
104 75 10 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝑛 ∈ ℕ )
105 104 nnrpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝑛 ∈ ℝ+ )
106 103 84 105 ledivmul2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ 𝐶 ↔ ( abs ‘ 𝐵 ) ≤ ( 𝐶 · 𝑛 ) ) )
107 101 106 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ 𝐶 )
108 72 76 84 107 fsumle ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) 𝐶 )
109 9 5 6 74 fsumless ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) 𝐶 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 )
110 77 85 20 108 109 letrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 )
111 81 10 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
112 111 nnrecred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
113 78 112 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ∈ ℝ )
114 21 113 remulcld ⊢ ( 𝜑 → ( 𝑅 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ) ∈ ℝ )
115 21 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑅 ∈ ℝ )
116 115 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑅 ∈ ℂ )
117 111 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℂ )
118 111 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ≠ 0 )
119 116 117 118 divrecd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑅 / 𝑛 ) = ( 𝑅 · ( 1 / 𝑛 ) ) )
120 115 111 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑅 / 𝑛 ) ∈ ℝ )
121 119 120 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑅 · ( 1 / 𝑛 ) ) ∈ ℝ )
122 81 17 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( abs ‘ 𝐵 ) ∈ ℝ )
123 81 36 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℝ+ )
124 noel ⊢ ¬ 𝑛 ∈ ∅
125 elin ⊢ ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) )
126 51 eleq2d ⊢ ( 𝜑 → ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) ↔ 𝑛 ∈ ∅ ) )
127 125 126 bitr3id ⊢ ( 𝜑 → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) ↔ 𝑛 ∈ ∅ ) )
128 124 127 mtbiri ⊢ ( 𝜑 → ¬ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) )
129 imnan ⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) → ¬ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) ↔ ¬ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) )
130 128 129 sylibr ⊢ ( 𝜑 → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) → ¬ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) )
131 130 con2d ⊢ ( 𝜑 → ( 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) → ¬ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) )
132 131 imp ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ¬ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) )
133 86 baibd ⊢ ( ( ( 𝐴 / 𝑇 ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ↔ 𝑛 ≤ ( 𝐴 / 𝑇 ) ) )
134 56 10 133 syl2an ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ↔ 𝑛 ≤ ( 𝐴 / 𝑇 ) ) )
135 134 96 bitrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ↔ 𝑇 ≤ ( 𝐴 / 𝑛 ) ) )
136 81 135 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ↔ 𝑇 ≤ ( 𝐴 / 𝑛 ) ) )
137 132 136 mtbid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ¬ 𝑇 ≤ ( 𝐴 / 𝑛 ) )
138 57 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
139 138 111 nndivred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑛 ) ∈ ℝ )
140 22 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑇 ∈ ℝ )
141 139 140 ltnled ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 / 𝑛 ) < 𝑇 ↔ ¬ 𝑇 ≤ ( 𝐴 / 𝑛 ) ) )
142 137 141 mpbird ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑛 ) < 𝑇 )
143 8 ex ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 / 𝑛 ) < 𝑇 → ( abs ‘ 𝐵 ) ≤ 𝑅 ) )
144 81 143 syldan ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝐴 / 𝑛 ) < 𝑇 → ( abs ‘ 𝐵 ) ≤ 𝑅 ) )
145 142 144 mpd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( abs ‘ 𝐵 ) ≤ 𝑅 )
146 122 115 123 145 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ ( 𝑅 / 𝑛 ) )
147 146 119 breqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ ( 𝑅 · ( 1 / 𝑛 ) ) )
148 78 82 121 147 fsumle ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 𝑅 · ( 1 / 𝑛 ) ) )
149 21 recnd ⊢ ( 𝜑 → 𝑅 ∈ ℂ )
150 112 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
151 78 149 150 fsummulc2 ⊢ ( 𝜑 → ( 𝑅 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 𝑅 · ( 1 / 𝑛 ) ) )
152 148 151 breqtrrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ ( 𝑅 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ) )
153 104 nnrecred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
154 72 153 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ∈ ℝ )
155 154 recnd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ∈ ℂ )
156 113 recnd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ∈ ℂ )
157 11 nnrecred ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
158 157 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
159 51 69 9 158 fsumsplit ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ) )
160 155 156 159 mvrladdd ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) )
161 9 157 fsumrecl ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ∈ ℝ )
162 161 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ∈ ℝ )
163 154 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ∈ ℝ )
164 162 163 resubcld ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ∈ ℝ )
165 0red ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → 0 ∈ ℝ )
166 31 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( ( log ‘ 𝑇 ) + 1 ) ∈ ℝ )
167 fzfid ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ∈ Fin )
168 105 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐴 < 1 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 𝑛 ∈ ℝ+ )
169 168 rpreccld ⊢ ( ( ( 𝜑 ∧ 𝐴 < 1 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( 1 / 𝑛 ) ∈ ℝ+ )
170 169 rpred ⊢ ( ( ( 𝜑 ∧ 𝐴 < 1 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
171 169 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝐴 < 1 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ) → 0 ≤ ( 1 / 𝑛 ) )
172 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → 𝐴 ∈ ℝ+ )
173 172 rpge0d ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → 0 ≤ 𝐴 )
174 simpr ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → 𝐴 < 1 )
175 0p1e1 ⊢ ( 0 + 1 ) = 1
176 174 175 breqtrrdi ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → 𝐴 < ( 0 + 1 ) )
177 57 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → 𝐴 ∈ ℝ )
178 0z ⊢ 0 ∈ ℤ
179 flbi ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℤ ) → ( ( ⌊ ‘ 𝐴 ) = 0 ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < ( 0 + 1 ) ) ) )
180 177 178 179 sylancl ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( ( ⌊ ‘ 𝐴 ) = 0 ↔ ( 0 ≤ 𝐴 ∧ 𝐴 < ( 0 + 1 ) ) ) )
181 173 176 180 mpbir2and ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( ⌊ ‘ 𝐴 ) = 0 )
182 181 oveq2d ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ( 1 ... 0 ) )
183 fz10 ⊢ ( 1 ... 0 ) = ∅
184 182 183 eqtrdi ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) = ∅ )
185 0ss ⊢ ∅ ⊆ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) )
186 184 185 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) )
187 167 170 171 186 fsumless ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) )
188 162 163 suble0d ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ 0 ↔ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) )
189 187 188 mpbird ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ 0 )
190 22 27 logge0d ⊢ ( 𝜑 → 0 ≤ ( log ‘ 𝑇 ) )
191 0le1 ⊢ 0 ≤ 1
192 191 a1i ⊢ ( 𝜑 → 0 ≤ 1 )
193 30 24 190 192 addge0d ⊢ ( 𝜑 → 0 ≤ ( ( log ‘ 𝑇 ) + 1 ) )
194 193 adantr ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → 0 ≤ ( ( log ‘ 𝑇 ) + 1 ) )
195 164 165 166 189 194 letrd ⊢ ( ( 𝜑 ∧ 𝐴 < 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ ( ( log ‘ 𝑇 ) + 1 ) )
196 harmonicubnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) )
197 57 196 sylan ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐴 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) )
198 harmoniclbnd ⊢ ( ( 𝐴 / 𝑇 ) ∈ ℝ+ → ( log ‘ ( 𝐴 / 𝑇 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) )
199 44 198 syl ⊢ ( 𝜑 → ( log ‘ ( 𝐴 / 𝑇 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) )
200 199 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐴 ) → ( log ‘ ( 𝐴 / 𝑇 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) )
201 1 relogcld ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
202 peano2re ⊢ ( ( log ‘ 𝐴 ) ∈ ℝ → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ )
203 201 202 syl ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ )
204 44 relogcld ⊢ ( 𝜑 → ( log ‘ ( 𝐴 / 𝑇 ) ) ∈ ℝ )
205 le2sub ⊢ ( ( ( Σ 𝑛 ∈ ( 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 ⊢ ( 𝜑 → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) ∧ ( log ‘ ( 𝐴 / 𝑇 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ ( ( ( log ‘ 𝐴 ) + 1 ) − ( log ‘ ( 𝐴 / 𝑇 ) ) ) ) )
207 206 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐴 ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) ∧ ( log ‘ ( 𝐴 / 𝑇 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ ( ( ( log ‘ 𝐴 ) + 1 ) − ( log ‘ ( 𝐴 / 𝑇 ) ) ) ) )
208 197 200 207 mp2and ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐴 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ ( ( ( log ‘ 𝐴 ) + 1 ) − ( log ‘ ( 𝐴 / 𝑇 ) ) ) )
209 201 recnd ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
210 24 recnd ⊢ ( 𝜑 → 1 ∈ ℂ )
211 30 recnd ⊢ ( 𝜑 → ( log ‘ 𝑇 ) ∈ ℂ )
212 209 210 211 pnncand ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) + 1 ) − ( ( log ‘ 𝐴 ) − ( log ‘ 𝑇 ) ) ) = ( 1 + ( log ‘ 𝑇 ) ) )
213 1 29 relogdivd ⊢ ( 𝜑 → ( log ‘ ( 𝐴 / 𝑇 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝑇 ) ) )
214 213 oveq2d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) + 1 ) − ( log ‘ ( 𝐴 / 𝑇 ) ) ) = ( ( ( log ‘ 𝐴 ) + 1 ) − ( ( log ‘ 𝐴 ) − ( log ‘ 𝑇 ) ) ) )
215 ax-1cn ⊢ 1 ∈ ℂ
216 addcom ⊢ ( ( ( log ‘ 𝑇 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( log ‘ 𝑇 ) + 1 ) = ( 1 + ( log ‘ 𝑇 ) ) )
217 211 215 216 sylancl ⊢ ( 𝜑 → ( ( log ‘ 𝑇 ) + 1 ) = ( 1 + ( log ‘ 𝑇 ) ) )
218 212 214 217 3eqtr4d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) + 1 ) − ( log ‘ ( 𝐴 / 𝑇 ) ) ) = ( ( log ‘ 𝑇 ) + 1 ) )
219 218 adantr ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐴 ) → ( ( ( log ‘ 𝐴 ) + 1 ) − ( log ‘ ( 𝐴 / 𝑇 ) ) ) = ( ( log ‘ 𝑇 ) + 1 ) )
220 208 219 breqtrd ⊢ ( ( 𝜑 ∧ 1 ≤ 𝐴 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ ( ( log ‘ 𝑇 ) + 1 ) )
221 195 220 57 24 ltlecasei ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( 1 / 𝑛 ) ) ≤ ( ( log ‘ 𝑇 ) + 1 ) )
222 160 221 eqbrtrrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑇 ) + 1 ) )
223 lemul2a ⊢ ( ( ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ∈ ℝ ∧ ( ( log ‘ 𝑇 ) + 1 ) ∈ ℝ ∧ ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) ) ∧ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑇 ) + 1 ) ) → ( 𝑅 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ) ≤ ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) )
224 113 31 3 222 223 syl31anc ⊢ ( 𝜑 → ( 𝑅 · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑛 ) ) ≤ ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) )
225 83 114 32 152 224 letrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) )
226 77 83 20 32 110 225 le2addd ⊢ ( 𝜑 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝐴 / 𝑇 ) ) + 1 ) ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 + ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) ) )
227 71 226 eqbrtrd ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( abs ‘ 𝐵 ) / 𝑛 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 + ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) ) )
228 16 19 33 43 227 letrd ⊢ ( 𝜑 → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 𝐵 / 𝑛 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) 𝐶 + ( 𝑅 · ( ( log ‘ 𝑇 ) + 1 ) ) ) )