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	$⊢ F = (y \in ℝ^{+} ⟼ \sum_{i = 1}^{⌊y⌋} (\frac{\log i}{i}) - (\frac{{\log y}^{2}}{2}))$
	mulog2sumlem.1	$⊢ φ \to F \underset{ℝ}{⇝} L$
	mulog2sumlem1.2	$⊢ φ \to A \in ℝ^{+}$
	mulog2sumlem1.3	$⊢ φ \to e \leq A$
Assertion	mulog2sumlem1	$⊢ φ \to \|\sum_{m = 1}^{⌊A⌋} (\frac{\log (\frac{A}{m})}{m}) - ((\frac{{\log A}^{2}}{2}) + γ \log A - L)\| \leq 2 (\frac{\log A}{A})$

Proof

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

Metamath Proof Explorer

Theorem mulog2sumlem1

Proof