Metamath Proof Explorer

Theorem dchrvmasumlem2

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 4-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
dchrvmasum.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝐹 ∈ ℂ )
dchrvmasum.g ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → 𝐹 = 𝐾 )
dchrvmasum.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
dchrvmasum.t ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
dchrvmasum.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
dchrvmasum.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
dchrvmasum.2 ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 1 [,) 3 ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 )
Assertion dchrvmasumlem2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrvmasum.f ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝐹 ∈ ℂ )
10 dchrvmasum.g ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → 𝐹 = 𝐾 )
11 dchrvmasum.c ⊢ ( 𝜑 → 𝐶 ∈ ( 0 [,) +∞ ) )
12 dchrvmasum.t ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
13 dchrvmasum.1 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 3 [,) +∞ ) ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
14 dchrvmasum.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ )
15 dchrvmasum.2 ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 1 [,) 3 ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 )
16 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
17 elrege0 ⊢ ( 𝐶 ∈ ( 0 [,) +∞ ) ↔ ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
18 11 17 sylib ⊢ ( 𝜑 → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
19 18 simpld ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ℝ )
21 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
22 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
23 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
24 23 nnrpd ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℝ+ )
25 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
26 22 24 25 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ+ )
27 26 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑑 ) ) ∈ ℝ )
28 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
29 27 28 rerpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ∈ ℝ )
30 21 29 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ∈ ℝ )
31 20 30 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ∈ ℝ )
32 3nn ⊢ 3 ∈ ℕ
33 nnrp ⊢ ( 3 ∈ ℕ → 3 ∈ ℝ+ )
34 relogcl ⊢ ( 3 ∈ ℝ+ → ( log ‘ 3 ) ∈ ℝ )
35 32 33 34 mp2b ⊢ ( log ‘ 3 ) ∈ ℝ
36 1re ⊢ 1 ∈ ℝ
37 35 36 readdcli ⊢ ( ( log ‘ 3 ) + 1 ) ∈ ℝ
38 remulcl ⊢ ( ( 𝑅 ∈ ℝ ∧ ( ( log ‘ 3 ) + 1 ) ∈ ℝ ) → ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ∈ ℝ )
39 14 37 38 sylancl ⊢ ( 𝜑 → ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ∈ ℝ )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ∈ ℝ )
41 rpssre ⊢ ℝ+ ⊆ ℝ
42 19 recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
43 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ 𝐶 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 𝐶 ) ∈ 𝑂(1) )
44 41 42 43 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ 𝐶 ) ∈ 𝑂(1) )
45 logfacrlim2 ⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ⇝𝑟 1
46 rlimo1 ⊢ ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ⇝𝑟 1 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ∈ 𝑂(1) )
47 45 46 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ∈ 𝑂(1) )
48 20 30 44 47 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ) ∈ 𝑂(1) )
49 39 recnd ⊢ ( 𝜑 → ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ∈ ℂ )
50 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ∈ 𝑂(1) )
51 41 49 50 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ∈ 𝑂(1) )
52 31 40 48 51 o1add2 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ) ∈ 𝑂(1) )
53 31 40 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ∈ ℝ )
54 10 eleq1d ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( 𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ ) )
55 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℝ+ 𝐹 ∈ ℂ )
56 55 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑚 ∈ ℝ+ 𝐹 ∈ ℂ )
57 54 56 26 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐾 ∈ ℂ )
58 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑇 ∈ ℂ )
59 57 58 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐾 − 𝑇 ) ∈ ℂ )
60 59 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ∈ ℝ )
61 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℕ )
62 60 61 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℝ )
63 21 62 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℝ )
64 63 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ∈ ℂ )
65 61 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℝ+ )
66 59 absge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝐾 − 𝑇 ) ) )
67 60 65 66 divge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
68 21 62 67 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
69 63 68 absidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) )
70 69 63 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ∈ ℝ )
71 53 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ∈ ℂ )
72 71 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ) ∈ ℝ )
73 3re ⊢ 3 ∈ ℝ
74 73 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 3 ∈ ℝ )
75 1le3 ⊢ 1 ≤ 3
76 74 75 jctir ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 3 ∈ ℝ ∧ 1 ≤ 3 ) )
77 14 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑅 ∈ ℝ )
78 36 rexri ⊢ 1 ∈ ℝ*
79 73 rexri ⊢ 3 ∈ ℝ*
80 1lt3 ⊢ 1 < 3
81 lbico1 ⊢ ( ( 1 ∈ ℝ* ∧ 3 ∈ ℝ* ∧ 1 < 3 ) → 1 ∈ ( 1 [,) 3 ) )
82 78 79 80 81 mp3an ⊢ 1 ∈ ( 1 [,) 3 )
83 0red ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 0 ∈ ℝ )
84 elico2 ⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℝ* ) → ( 𝑚 ∈ ( 1 [,) 3 ) ↔ ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3 ) ) )
85 36 79 84 mp2an ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) ↔ ( 𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3 ) )
86 85 simp1bi ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 𝑚 ∈ ℝ )
87 0red ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 0 ∈ ℝ )
88 1red ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 1 ∈ ℝ )
89 0lt1 ⊢ 0 < 1
90 89 a1i ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 0 < 1 )
91 85 simp2bi ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 1 ≤ 𝑚 )
92 87 88 86 90 91 ltletrd ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 0 < 𝑚 )
93 86 92 elrpd ⊢ ( 𝑚 ∈ ( 1 [,) 3 ) → 𝑚 ∈ ℝ+ )
94 12 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 𝑇 ∈ ℂ )
95 9 94 subcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( 𝐹 − 𝑇 ) ∈ ℂ )
96 95 abscld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ∈ ℝ )
97 93 96 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ∈ ℝ )
98 14 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 𝑅 ∈ ℝ )
99 95 absge0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℝ+ ) → 0 ≤ ( abs ‘ ( 𝐹 − 𝑇 ) ) )
100 93 99 sylan2 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 0 ≤ ( abs ‘ ( 𝐹 − 𝑇 ) ) )
101 15 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 )
102 83 97 98 100 101 letrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 [,) 3 ) ) → 0 ≤ 𝑅 )
103 102 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 1 [,) 3 ) 0 ≤ 𝑅 )
104 biidd ⊢ ( 𝑚 = 1 → ( 0 ≤ 𝑅 ↔ 0 ≤ 𝑅 ) )
105 104 rspcv ⊢ ( 1 ∈ ( 1 [,) 3 ) → ( ∀ 𝑚 ∈ ( 1 [,) 3 ) 0 ≤ 𝑅 → 0 ≤ 𝑅 ) )
106 82 103 105 mpsyl ⊢ ( 𝜑 → 0 ≤ 𝑅 )
107 106 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ 𝑅 )
108 77 107 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑅 ∈ ℝ ∧ 0 ≤ 𝑅 ) )
109 60 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ∈ ℂ )
110 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐶 ∈ ℝ )
111 110 29 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ∈ ℝ )
112 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) )
113 log1 ⊢ ( log ‘ 1 ) = 0
114 61 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ∈ ℂ )
115 114 mulid2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑑 ) = 𝑑 )
116 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
117 116 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
118 fznnfl ⊢ ( 𝑥 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥 ) ) )
119 117 118 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝑥 ) ) )
120 119 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑑 ≤ 𝑥 )
121 115 120 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑑 ) ≤ 𝑥 )
122 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
123 116 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
124 122 123 65 lemuldivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · 𝑑 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑑 ) ) )
125 121 124 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( 𝑥 / 𝑑 ) )
126 1rp ⊢ 1 ∈ ℝ+
127 126 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ+ )
128 127 26 logled ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ≤ ( 𝑥 / 𝑑 ) ↔ ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑑 ) ) ) )
129 125 128 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 1 ) ≤ ( log ‘ ( 𝑥 / 𝑑 ) ) )
130 113 129 eqbrtrrid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( log ‘ ( 𝑥 / 𝑑 ) ) )
131 rpregt0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
132 131 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
133 divge0 ⊢ ( ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) ∈ ℝ ∧ 0 ≤ ( log ‘ ( 𝑥 / 𝑑 ) ) ) ∧ ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ) → 0 ≤ ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) )
134 27 130 132 133 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) )
135 mulge0 ⊢ ( ( ( 𝐶 ∈ ℝ ∧ 0 ≤ 𝐶 ) ∧ ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ∈ ℝ ∧ 0 ≤ ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) ) → 0 ≤ ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) )
136 112 29 134 135 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) )
137 absidm ⊢ ( ( 𝐾 − 𝑇 ) ∈ ℂ → ( abs ‘ ( abs ‘ ( 𝐾 − 𝑇 ) ) ) = ( abs ‘ ( 𝐾 − 𝑇 ) ) )
138 59 137 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( abs ‘ ( 𝐾 − 𝑇 ) ) ) = ( abs ‘ ( 𝐾 − 𝑇 ) ) )
139 138 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ( abs ‘ ( abs ‘ ( 𝐾 − 𝑇 ) ) ) = ( abs ‘ ( 𝐾 − 𝑇 ) ) )
140 10 fvoveq1d ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( abs ‘ ( 𝐹 − 𝑇 ) ) = ( abs ‘ ( 𝐾 − 𝑇 ) ) )
141 fveq2 ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( log ‘ 𝑚 ) = ( log ‘ ( 𝑥 / 𝑑 ) ) )
142 id ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → 𝑚 = ( 𝑥 / 𝑑 ) )
143 141 142 oveq12d ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( ( log ‘ 𝑚 ) / 𝑚 ) = ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) )
144 143 oveq2d ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) ) )
145 140 144 breq12d ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ↔ ( abs ‘ ( 𝐾 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) ) ) )
146 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ( 3 [,) +∞ ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
147 146 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ∀ 𝑚 ∈ ( 3 [,) +∞ ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
148 nndivre ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑑 ∈ ℕ ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
149 117 23 148 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
150 149 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
151 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → 3 ≤ ( 𝑥 / 𝑑 ) )
152 elicopnf ⊢ ( 3 ∈ ℝ → ( ( 𝑥 / 𝑑 ) ∈ ( 3 [,) +∞ ) ↔ ( ( 𝑥 / 𝑑 ) ∈ ℝ ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) ) )
153 73 152 ax-mp ⊢ ( ( 𝑥 / 𝑑 ) ∈ ( 3 [,) +∞ ) ↔ ( ( 𝑥 / 𝑑 ) ∈ ℝ ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) )
154 150 151 153 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ( 𝑥 / 𝑑 ) ∈ ( 3 [,) +∞ ) )
155 145 147 154 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ≤ ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) ) )
156 27 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑑 ) ) ∈ ℂ )
157 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
158 157 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
159 65 rpcnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
160 divdiv2 ⊢ ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ) → ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) = ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) · 𝑑 ) / 𝑥 ) )
161 156 158 159 160 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) = ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) · 𝑑 ) / 𝑥 ) )
162 div23 ⊢ ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) ∈ ℂ ∧ 𝑑 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) · 𝑑 ) / 𝑥 ) = ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) · 𝑑 ) )
163 156 114 158 162 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) · 𝑑 ) / 𝑥 ) = ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) · 𝑑 ) )
164 161 163 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) = ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) · 𝑑 ) )
165 164 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) ) = ( 𝐶 · ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) · 𝑑 ) ) )
166 42 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐶 ∈ ℂ )
167 29 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ∈ ℂ )
168 166 167 114 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) · 𝑑 ) = ( 𝐶 · ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) · 𝑑 ) ) )
169 165 168 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) ) = ( ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) · 𝑑 ) )
170 169 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / ( 𝑥 / 𝑑 ) ) ) = ( ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) · 𝑑 ) )
171 155 170 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ≤ ( ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) · 𝑑 ) )
172 139 171 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 3 ≤ ( 𝑥 / 𝑑 ) ) → ( abs ‘ ( abs ‘ ( 𝐾 − 𝑇 ) ) ) ≤ ( ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) · 𝑑 ) )
173 138 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → ( abs ‘ ( abs ‘ ( 𝐾 − 𝑇 ) ) ) = ( abs ‘ ( 𝐾 − 𝑇 ) ) )
174 140 breq1d ⊢ ( 𝑚 = ( 𝑥 / 𝑑 ) → ( ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 ↔ ( abs ‘ ( 𝐾 − 𝑇 ) ) ≤ 𝑅 ) )
175 15 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → ∀ 𝑚 ∈ ( 1 [,) 3 ) ( abs ‘ ( 𝐹 − 𝑇 ) ) ≤ 𝑅 )
176 149 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → ( 𝑥 / 𝑑 ) ∈ ℝ )
177 125 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → 1 ≤ ( 𝑥 / 𝑑 ) )
178 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → ( 𝑥 / 𝑑 ) < 3 )
179 elico2 ⊢ ( ( 1 ∈ ℝ ∧ 3 ∈ ℝ* ) → ( ( 𝑥 / 𝑑 ) ∈ ( 1 [,) 3 ) ↔ ( ( 𝑥 / 𝑑 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑑 ) ∧ ( 𝑥 / 𝑑 ) < 3 ) ) )
180 36 79 179 mp2an ⊢ ( ( 𝑥 / 𝑑 ) ∈ ( 1 [,) 3 ) ↔ ( ( 𝑥 / 𝑑 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑑 ) ∧ ( 𝑥 / 𝑑 ) < 3 ) )
181 176 177 178 180 syl3anbrc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → ( 𝑥 / 𝑑 ) ∈ ( 1 [,) 3 ) )
182 174 175 181 rspcdva ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → ( abs ‘ ( 𝐾 − 𝑇 ) ) ≤ 𝑅 )
183 173 182 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ ( 𝑥 / 𝑑 ) < 3 ) → ( abs ‘ ( abs ‘ ( 𝐾 − 𝑇 ) ) ) ≤ 𝑅 )
184 22 76 108 109 111 136 172 183 fsumharmonic ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ≤ ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) )
185 42 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐶 ∈ ℂ )
186 21 185 167 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) )
187 186 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐶 · ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) )
188 184 187 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ≤ ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) )
189 53 leabsd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ≤ ( abs ‘ ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ) )
190 70 53 72 188 189 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ≤ ( abs ‘ ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ) )
191 190 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ≤ ( abs ‘ ( ( 𝐶 · Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑑 ) ) / 𝑥 ) ) + ( 𝑅 · ( ( log ‘ 3 ) + 1 ) ) ) ) )
192 16 52 53 64 191 o1le ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝐾 − 𝑇 ) ) / 𝑑 ) ) ∈ 𝑂(1) )