Metamath Proof Explorer

Theorem mulog2sumlem1

Description: Asymptotic formula for sum_ n <_ x , log ( x / n ) / n = ( 1 / 2 ) log ^ 2 ( x ) + gamma x. log x - L + O ( log x / x ) , with explicit constants. Equation 10.2.7 of Shapiro, p. 407. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses logdivsum.1 ⊢ 𝐹 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
mulog2sumlem.1 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 )
mulog2sumlem1.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
mulog2sumlem1.3 ⊢ ( 𝜑 → e ≤ 𝐴 )
Assertion mulog2sumlem1 ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) ) ≤ ( 2 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 logdivsum.1 ⊢ 𝐹 = ( 𝑦 ∈ ℝ+ ↦ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) )
2 mulog2sumlem.1 ⊢ ( 𝜑 → 𝐹 ⇝𝑟 𝐿 )
3 mulog2sumlem1.2 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
4 mulog2sumlem1.3 ⊢ ( 𝜑 → e ≤ 𝐴 )
5 fzfid ⊢ ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
6 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℕ )
7 6 nnrpd ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑚 ∈ ℝ+ )
8 rpdivcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( 𝐴 / 𝑚 ) ∈ ℝ+ )
9 3 7 8 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑚 ) ∈ ℝ+ )
10 9 relogcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑚 ) ) ∈ ℝ )
11 6 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℕ )
12 10 11 nndivred ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) ∈ ℝ )
13 5 12 fsumrecl ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) ∈ ℝ )
14 3 relogcld ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
15 14 resqcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
16 15 rehalfcld ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ∈ ℝ )
17 emre ⊢ γ ∈ ℝ
18 remulcl ⊢ ( ( γ ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( γ · ( log ‘ 𝐴 ) ) ∈ ℝ )
19 17 14 18 sylancr ⊢ ( 𝜑 → ( γ · ( log ‘ 𝐴 ) ) ∈ ℝ )
20 rpsup ⊢ sup ( ℝ+ , ℝ* , < ) = +∞
21 20 a1i ⊢ ( 𝜑 → sup ( ℝ+ , ℝ* , < ) = +∞ )
22 1 logdivsum ⊢ ( 𝐹 : ℝ+ ⟶ ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
23 22 simp1i ⊢ 𝐹 : ℝ+ ⟶ ℝ
24 23 a1i ⊢ ( 𝜑 → 𝐹 : ℝ+ ⟶ ℝ )
25 24 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ℝ+ ↦ ( 𝐹 ‘ 𝑥 ) ) )
26 25 2 eqbrtrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 𝐹 ‘ 𝑥 ) ) ⇝𝑟 𝐿 )
27 23 ffvelcdmi ⊢ ( 𝑥 ∈ ℝ+ → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
29 21 26 28 rlimrecl ⊢ ( 𝜑 → 𝐿 ∈ ℝ )
30 19 29 resubcld ⊢ ( 𝜑 → ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ∈ ℝ )
31 16 30 readdcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ∈ ℝ )
32 13 31 resubcld ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) ∈ ℝ )
33 32 recnd ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) ∈ ℂ )
34 33 abscld ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) ) ∈ ℝ )
35 rerpdivcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ 𝑚 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) / 𝑚 ) ∈ ℝ )
36 14 7 35 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ 𝐴 ) / 𝑚 ) ∈ ℝ )
37 36 recnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ 𝐴 ) / 𝑚 ) ∈ ℂ )
38 5 37 fsumcl ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) ∈ ℂ )
39 14 recnd ⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
40 readdcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ γ ∈ ℝ ) → ( ( log ‘ 𝐴 ) + γ ) ∈ ℝ )
41 14 17 40 sylancl ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) + γ ) ∈ ℝ )
42 41 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) + γ ) ∈ ℂ )
43 39 42 mulcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ∈ ℂ )
44 38 43 subcld ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ∈ ℂ )
45 44 abscld ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) ∈ ℝ )
46 11 nnrpd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℝ+ )
47 46 relogcld ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
48 47 11 nndivred ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ 𝑚 ) / 𝑚 ) ∈ ℝ )
49 48 recnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ 𝑚 ) / 𝑚 ) ∈ ℂ )
50 5 49 fsumcl ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) ∈ ℂ )
51 16 recnd ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ∈ ℂ )
52 29 recnd ⊢ ( 𝜑 → 𝐿 ∈ ℂ )
53 51 52 addcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ∈ ℂ )
54 50 53 subcld ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ∈ ℂ )
55 54 abscld ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ∈ ℝ )
56 45 55 readdcld ⊢ ( 𝜑 → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) + ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ) ∈ ℝ )
57 2re ⊢ 2 ∈ ℝ
58 14 3 rerpdivcld ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℝ )
59 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℝ ) → ( 2 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) ∈ ℝ )
60 57 58 59 sylancr ⊢ ( 𝜑 → ( 2 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) ∈ ℝ )
61 relogdiv ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑚 ∈ ℝ+ ) → ( log ‘ ( 𝐴 / 𝑚 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝑚 ) ) )
62 3 7 61 syl2an ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑚 ) ) = ( ( log ‘ 𝐴 ) − ( log ‘ 𝑚 ) ) )
63 62 oveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) = ( ( ( log ‘ 𝐴 ) − ( log ‘ 𝑚 ) ) / 𝑚 ) )
64 39 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
65 47 recnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
66 46 rpcnne0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
67 divsubdir ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℂ ∧ ( log ‘ 𝑚 ) ∈ ℂ ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( ( log ‘ 𝐴 ) − ( log ‘ 𝑚 ) ) / 𝑚 ) = ( ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
68 64 65 66 67 syl3anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( log ‘ 𝐴 ) − ( log ‘ 𝑚 ) ) / 𝑚 ) = ( ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
69 63 68 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) = ( ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
70 69 sumeq2dv ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
71 5 37 49 fsumsub ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
72 70 71 eqtrd ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
73 remulcl ⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ ∧ γ ∈ ℝ ) → ( ( log ‘ 𝐴 ) · γ ) ∈ ℝ )
74 14 17 73 sylancl ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · γ ) ∈ ℝ )
75 16 74 readdcld ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) ∈ ℝ )
76 75 recnd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) ∈ ℂ )
77 76 51 pncand ⊢ ( 𝜑 → ( ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) = ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) )
78 17 recni ⊢ γ ∈ ℂ
79 78 a1i ⊢ ( 𝜑 → γ ∈ ℂ )
80 39 39 79 adddid ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) = ( ( ( log ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) + ( ( log ‘ 𝐴 ) · γ ) ) )
81 15 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
82 81 2halvesd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) = ( ( log ‘ 𝐴 ) ↑ 2 ) )
83 39 sqvald ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) ↑ 2 ) = ( ( log ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) )
84 82 83 eqtrd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) = ( ( log ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) )
85 84 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( log ‘ 𝐴 ) · γ ) ) = ( ( ( log ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) + ( ( log ‘ 𝐴 ) · γ ) ) )
86 74 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · γ ) ∈ ℂ )
87 51 51 86 add32d ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) + ( ( log ‘ 𝐴 ) · γ ) ) = ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) )
88 80 85 87 3eqtr2d ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) = ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) )
89 88 oveq1d ⊢ ( 𝜑 → ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) = ( ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) + ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) )
90 mulcom ⊢ ( ( γ ∈ ℂ ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → ( γ · ( log ‘ 𝐴 ) ) = ( ( log ‘ 𝐴 ) · γ ) )
91 78 39 90 sylancr ⊢ ( 𝜑 → ( γ · ( log ‘ 𝐴 ) ) = ( ( log ‘ 𝐴 ) · γ ) )
92 91 oveq2d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( γ · ( log ‘ 𝐴 ) ) ) = ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( log ‘ 𝐴 ) · γ ) ) )
93 77 89 92 3eqtr4rd ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( γ · ( log ‘ 𝐴 ) ) ) = ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) )
94 93 oveq1d ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( γ · ( log ‘ 𝐴 ) ) ) − 𝐿 ) = ( ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) − 𝐿 ) )
95 91 86 eqeltrd ⊢ ( 𝜑 → ( γ · ( log ‘ 𝐴 ) ) ∈ ℂ )
96 51 95 52 addsubassd ⊢ ( 𝜑 → ( ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( γ · ( log ‘ 𝐴 ) ) ) − 𝐿 ) = ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) )
97 43 51 52 subsub4d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) − 𝐿 ) = ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) )
98 94 96 97 3eqtr3d ⊢ ( 𝜑 → ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) = ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) )
99 72 98 oveq12d ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) ) − ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) )
100 38 50 43 53 sub4d ⊢ ( 𝜑 → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) ) − ( ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) )
101 99 100 eqtrd ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) )
102 101 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) ) = ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ) )
103 44 54 abs2dif2d ⊢ ( 𝜑 → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) − ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ) ≤ ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) + ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ) )
104 102 103 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) ) ≤ ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) + ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ) )
105 harmonicbnd4 ⊢ ( 𝐴 ∈ ℝ+ → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ≤ ( 1 / 𝐴 ) )
106 3 105 syl ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ≤ ( 1 / 𝐴 ) )
107 11 nnrecred ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
108 5 107 fsumrecl ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ∈ ℝ )
109 108 41 resubcld ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ∈ ℝ )
110 109 recnd ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ∈ ℂ )
111 110 abscld ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ∈ ℝ )
112 3 rprecred ⊢ ( 𝜑 → ( 1 / 𝐴 ) ∈ ℝ )
113 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
114 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
115 0lt1 ⊢ 0 < 1
116 115 a1i ⊢ ( 𝜑 → 0 < 1 )
117 loge ⊢ ( log ‘ e ) = 1
118 epr ⊢ e ∈ ℝ+
119 logleb ⊢ ( ( e ∈ ℝ+ ∧ 𝐴 ∈ ℝ+ ) → ( e ≤ 𝐴 ↔ ( log ‘ e ) ≤ ( log ‘ 𝐴 ) ) )
120 118 3 119 sylancr ⊢ ( 𝜑 → ( e ≤ 𝐴 ↔ ( log ‘ e ) ≤ ( log ‘ 𝐴 ) ) )
121 4 120 mpbid ⊢ ( 𝜑 → ( log ‘ e ) ≤ ( log ‘ 𝐴 ) )
122 117 121 eqbrtrrid ⊢ ( 𝜑 → 1 ≤ ( log ‘ 𝐴 ) )
123 113 114 14 116 122 ltletrd ⊢ ( 𝜑 → 0 < ( log ‘ 𝐴 ) )
124 lemul2 ⊢ ( ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ∈ ℝ ∧ ( 1 / 𝐴 ) ∈ ℝ ∧ ( ( log ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( log ‘ 𝐴 ) ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ≤ ( 1 / 𝐴 ) ↔ ( ( log ‘ 𝐴 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) ≤ ( ( log ‘ 𝐴 ) · ( 1 / 𝐴 ) ) ) )
125 111 112 14 123 124 syl112anc ⊢ ( 𝜑 → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ≤ ( 1 / 𝐴 ) ↔ ( ( log ‘ 𝐴 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) ≤ ( ( log ‘ 𝐴 ) · ( 1 / 𝐴 ) ) ) )
126 106 125 mpbid ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) ≤ ( ( log ‘ 𝐴 ) · ( 1 / 𝐴 ) ) )
127 46 rpcnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ∈ ℂ )
128 46 rpne0d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑚 ≠ 0 )
129 64 127 128 divrecd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( log ‘ 𝐴 ) / 𝑚 ) = ( ( log ‘ 𝐴 ) · ( 1 / 𝑚 ) ) )
130 129 sumeq2dv ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) · ( 1 / 𝑚 ) ) )
131 107 recnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 / 𝑚 ) ∈ ℂ )
132 5 39 131 fsummulc2 ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) · ( 1 / 𝑚 ) ) )
133 130 132 eqtr4d ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) = ( ( log ‘ 𝐴 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ) )
134 133 oveq1d ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) = ( ( ( log ‘ 𝐴 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) )
135 5 131 fsumcl ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ∈ ℂ )
136 39 135 42 subdid ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) = ( ( ( log ‘ 𝐴 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) )
137 134 136 eqtr4d ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) = ( ( log ‘ 𝐴 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) )
138 137 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) = ( abs ‘ ( ( log ‘ 𝐴 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) )
139 135 42 subcld ⊢ ( 𝜑 → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ∈ ℂ )
140 39 139 absmuld ⊢ ( 𝜑 → ( abs ‘ ( ( log ‘ 𝐴 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) = ( ( abs ‘ ( log ‘ 𝐴 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) )
141 113 14 123 ltled ⊢ ( 𝜑 → 0 ≤ ( log ‘ 𝐴 ) )
142 14 141 absidd ⊢ ( 𝜑 → ( abs ‘ ( log ‘ 𝐴 ) ) = ( log ‘ 𝐴 ) )
143 142 oveq1d ⊢ ( 𝜑 → ( ( abs ‘ ( log ‘ 𝐴 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) = ( ( log ‘ 𝐴 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) )
144 138 140 143 3eqtrd ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) = ( ( log ‘ 𝐴 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( 1 / 𝑚 ) − ( ( log ‘ 𝐴 ) + γ ) ) ) ) )
145 3 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
146 3 rpne0d ⊢ ( 𝜑 → 𝐴 ≠ 0 )
147 39 145 146 divrecd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) / 𝐴 ) = ( ( log ‘ 𝐴 ) · ( 1 / 𝐴 ) ) )
148 126 144 147 3brtr4d ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) )
149 fveq2 ⊢ ( 𝑖 = 𝑚 → ( log ‘ 𝑖 ) = ( log ‘ 𝑚 ) )
150 id ⊢ ( 𝑖 = 𝑚 → 𝑖 = 𝑚 )
151 149 150 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( log ‘ 𝑖 ) / 𝑖 ) = ( ( log ‘ 𝑚 ) / 𝑚 ) )
152 151 cbvsumv ⊢ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 )
153 fveq2 ⊢ ( 𝑦 = 𝐴 → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ 𝐴 ) )
154 153 oveq2d ⊢ ( 𝑦 = 𝐴 → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
155 154 sumeq1d ⊢ ( 𝑦 = 𝐴 → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) )
156 152 155 eqtrid ⊢ ( 𝑦 = 𝐴 → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) )
157 fveq2 ⊢ ( 𝑦 = 𝐴 → ( log ‘ 𝑦 ) = ( log ‘ 𝐴 ) )
158 157 oveq1d ⊢ ( 𝑦 = 𝐴 → ( ( log ‘ 𝑦 ) ↑ 2 ) = ( ( log ‘ 𝐴 ) ↑ 2 ) )
159 158 oveq1d ⊢ ( 𝑦 = 𝐴 → ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) = ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) )
160 156 159 oveq12d ⊢ ( 𝑦 = 𝐴 → ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( log ‘ 𝑖 ) / 𝑖 ) − ( ( ( log ‘ 𝑦 ) ↑ 2 ) / 2 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) )
161 ovex ⊢ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) ∈ V
162 160 1 161 fvmpt ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐹 ‘ 𝐴 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) )
163 3 162 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) )
164 163 oveq1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) − 𝐿 ) )
165 50 51 52 subsub4d ⊢ ( 𝜑 → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) ) − 𝐿 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) )
166 164 165 eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) )
167 166 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) = ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) )
168 22 simp3i ⊢ ( ( 𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤ 𝐴 ) → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) )
169 2 3 4 168 syl3anc ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐹 ‘ 𝐴 ) − 𝐿 ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) )
170 167 169 eqbrtrrd ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ≤ ( ( log ‘ 𝐴 ) / 𝐴 ) )
171 45 55 58 58 148 170 le2addd ⊢ ( 𝜑 → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) + ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ) ≤ ( ( ( log ‘ 𝐴 ) / 𝐴 ) + ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
172 58 recnd ⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) / 𝐴 ) ∈ ℂ )
173 172 2timesd ⊢ ( 𝜑 → ( 2 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) = ( ( ( log ‘ 𝐴 ) / 𝐴 ) + ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
174 171 173 breqtrrd ⊢ ( 𝜑 → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝐴 ) / 𝑚 ) − ( ( log ‘ 𝐴 ) · ( ( log ‘ 𝐴 ) + γ ) ) ) ) + ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ 𝑚 ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + 𝐿 ) ) ) ) ≤ ( 2 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) )
175 34 56 60 104 174 letrd ⊢ ( 𝜑 → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( log ‘ ( 𝐴 / 𝑚 ) ) / 𝑚 ) − ( ( ( ( log ‘ 𝐴 ) ↑ 2 ) / 2 ) + ( ( γ · ( log ‘ 𝐴 ) ) − 𝐿 ) ) ) ) ≤ ( 2 · ( ( log ‘ 𝐴 ) / 𝐴 ) ) )