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 ‘ 𝐴 ) / 𝐴 ) ) )