Theorem logfacbnd3

Description: Show the stronger statement log ( x ! ) = x log x - x + O ( log x ) alluded to in logfacrlim . (Contributed by Mario Carneiro, 20-May-2016)

	Ref	Expression
Assertion	logfacbnd3	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|\le \log A+1$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\in {ℝ}^{+}$$
2	1	rprege0d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(A\in ℝ\wedge 0\le A\right)$$
3		flge0nn0	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to ⌊A⌋\in {\mathbb{N}}_0$$
4	2 3	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\in {\mathbb{N}}_0$$
5	4	faccld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋!\in \mathbb{N}$$
6	5	nnrpd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋!\in {ℝ}^{+}$$
7		relogcl	$$⊢⌊A⌋!\in {ℝ}^{+}\to \log ⌊A⌋!\in ℝ$$
8	6 7	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!\in ℝ$$
9		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
10	9	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\in ℝ$$
11		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
12	11	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log A\in ℝ$$
13		peano2rem	$$⊢\log A\in ℝ\to \log A-1\in ℝ$$
14	12 13	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log A-1\in ℝ$$
15	10 14	remulcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\left(\log A-1\right)\in ℝ$$
16	8 15	resubcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!-A\left(\log A-1\right)\in ℝ$$
17	16	recnd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!-A\left(\log A-1\right)\in ℂ$$
18	17	abscld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|\in ℝ$$
19		peano2rem	$$⊢\left|\log ⌊A⌋!-A\left(\log A-1\right)\right|\in ℝ\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-1\in ℝ$$
20	18 19	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-1\in ℝ$$
21		ax-1cn	$$⊢1\in ℂ$$
22		subcl	$$⊢\left(\log ⌊A⌋!-A\left(\log A-1\right)\in ℂ\wedge 1\in ℂ\right)\to \log ⌊A⌋!-A\left(\log A-1\right)-1\in ℂ$$
23	17 21 22	sylancl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!-A\left(\log A-1\right)-1\in ℂ$$
24	23	abscld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)-1\right|\in ℝ$$
25		abs1	$$⊢\left|1\right|=1$$
26	25	oveq2i	$$⊢\left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-\left|1\right|=\left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-1$$
27		abs2dif	$$⊢\left(\log ⌊A⌋!-A\left(\log A-1\right)\in ℂ\wedge 1\in ℂ\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-\left|1\right|\le \left|\log ⌊A⌋!-A\left(\log A-1\right)-1\right|$$
28	17 21 27	sylancl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-\left|1\right|\le \left|\log ⌊A⌋!-A\left(\log A-1\right)-1\right|$$
29	26 28	eqbrtrrid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-1\le \left|\log ⌊A⌋!-A\left(\log A-1\right)-1\right|$$
30		fveq2	$$⊢x=A\to ⌊x⌋=⌊A⌋$$
31	30	oveq2d	$$⊢x=A\to \left(1\dots ⌊x⌋\right)=\left(1\dots ⌊A⌋\right)$$
32	31	sumeq1d	$$⊢x=A\to \sum _{n=1}^{⌊x⌋}\log n=\sum _{n=1}^{⌊A⌋}\log n$$
33		id	$$⊢x=A\to x=A$$
34		fveq2	$$⊢x=A\to \log x=\log A$$
35	34	oveq1d	$$⊢x=A\to \log x-1=\log A-1$$
36	33 35	oveq12d	$$⊢x=A\to x\left(\log x-1\right)=A\left(\log A-1\right)$$
37	32 36	oveq12d	$$⊢x=A\to \sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)=\sum _{n=1}^{⌊A⌋}\log n-A\left(\log A-1\right)$$
38		eqid	$$⊢\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)=\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)$$
39		ovex	$$⊢\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\in \mathrm{V}$$
40	37 38 39	fvmpt3i	$$⊢A\in {ℝ}^{+}\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(A\right)=\sum _{n=1}^{⌊A⌋}\log n-A\left(\log A-1\right)$$
41	40	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(A\right)=\sum _{n=1}^{⌊A⌋}\log n-A\left(\log A-1\right)$$
42		logfac	$$⊢⌊A⌋\in {\mathbb{N}}_0\to \log ⌊A⌋!=\sum _{n=1}^{⌊A⌋}\log n$$
43	4 42	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!=\sum _{n=1}^{⌊A⌋}\log n$$
44	43	oveq1d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!-A\left(\log A-1\right)=\sum _{n=1}^{⌊A⌋}\log n-A\left(\log A-1\right)$$
45	41 44	eqtr4d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(A\right)=\log ⌊A⌋!-A\left(\log A-1\right)$$
46		1rp	$$⊢1\in {ℝ}^{+}$$
47		fveq2	$$⊢x=1\to ⌊x⌋=⌊1⌋$$
48		1z	$$⊢1\in \mathbb{Z}$$
49		flid	$$⊢1\in \mathbb{Z}\to ⌊1⌋=1$$
50	48 49	ax-mp	$$⊢⌊1⌋=1$$
51	47 50	eqtrdi	$$⊢x=1\to ⌊x⌋=1$$
52	51	oveq2d	$$⊢x=1\to \left(1\dots ⌊x⌋\right)=\left(1\dots 1\right)$$
53	52	sumeq1d	$$⊢x=1\to \sum _{n=1}^{⌊x⌋}\log n=\sum _{n=1}^1\log n$$
54		0cn	$$⊢0\in ℂ$$
55		fveq2	$$⊢n=1\to \log n=\log 1$$
56		log1	$$⊢\log 1=0$$
57	55 56	eqtrdi	$$⊢n=1\to \log n=0$$
58	57	fsum1	$$⊢\left(1\in \mathbb{Z}\wedge 0\in ℂ\right)\to \sum _{n=1}^1\log n=0$$
59	48 54 58	mp2an	$$⊢\sum _{n=1}^1\log n=0$$
60	53 59	eqtrdi	$$⊢x=1\to \sum _{n=1}^{⌊x⌋}\log n=0$$
61		id	$$⊢x=1\to x=1$$
62		fveq2	$$⊢x=1\to \log x=\log 1$$
63	62 56	eqtrdi	$$⊢x=1\to \log x=0$$
64	63	oveq1d	$$⊢x=1\to \log x-1=0-1$$
65	61 64	oveq12d	$$⊢x=1\to x\left(\log x-1\right)=1\left(0-1\right)$$
66	54 21	subcli	$$⊢0-1\in ℂ$$
67	66	mullidi	$$⊢1\left(0-1\right)=0-1$$
68	65 67	eqtrdi	$$⊢x=1\to x\left(\log x-1\right)=0-1$$
69	60 68	oveq12d	$$⊢x=1\to \sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)=0-\left(0-1\right)$$
70		nncan	$$⊢\left(0\in ℂ\wedge 1\in ℂ\right)\to 0-\left(0-1\right)=1$$
71	54 21 70	mp2an	$$⊢0-\left(0-1\right)=1$$
72	69 71	eqtrdi	$$⊢x=1\to \sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)=1$$
73	72 38 39	fvmpt3i	$$⊢1\in {ℝ}^{+}\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(1\right)=1$$
74	46 73	mp1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(1\right)=1$$
75	45 74	oveq12d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(A\right)-\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(1\right)=\log ⌊A⌋!-A\left(\log A-1\right)-1$$
76	75	fveq2d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(A\right)-\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(1\right)\right|=\left|\log ⌊A⌋!-A\left(\log A-1\right)-1\right|$$
77		ioorp	$$⊢\left(0,\mathrm{+\infty }\right)={ℝ}^{+}$$
78	77	eqcomi	$$⊢{ℝ}^{+}=\left(0,\mathrm{+\infty }\right)$$
79		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
80	48	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\in \mathbb{Z}$$
81		1re	$$⊢1\in ℝ$$
82	81	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\in ℝ$$
83		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
84	83	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
85		1nn0	$$⊢1\in {\mathbb{N}}_0$$
86	81 85	nn0addge1i	$$⊢1\le 1+1$$
87	86	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\le 1+1$$
88		0red	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 0\in ℝ$$
89		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
90	89	adantl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to x\in ℝ$$
91		relogcl	$$⊢x\in {ℝ}^{+}\to \log x\in ℝ$$
92	91	adantl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to \log x\in ℝ$$
93		peano2rem	$$⊢\log x\in ℝ\to \log x-1\in ℝ$$
94	92 93	syl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to \log x-1\in ℝ$$
95	90 94	remulcld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in {ℝ}^{+}\right)\to x\left(\log x-1\right)\in ℝ$$
96		nnrp	$$⊢x\in \mathbb{N}\to x\in {ℝ}^{+}$$
97	96 92	sylan2	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge x\in \mathbb{N}\right)\to \log x\in ℝ$$
98		advlog	$$⊢\frac{d\left(x\in {ℝ}^{+}⟼x\left(\log x-1\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\log x\right)$$
99	98	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \frac{d\left(x\in {ℝ}^{+}⟼x\left(\log x-1\right)\right)}{d_{ℝ}x}=\left(x\in {ℝ}^{+}⟼\log x\right)$$
100		fveq2	$$⊢x=n\to \log x=\log n$$
101		simp32	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\wedge \left(1\le x\wedge x\le n\wedge n\le \mathrm{+\infty }\right)\right)\to x\le n$$
102		logleb	$$⊢\left(x\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\to \left(x\le n\leftrightarrow \log x\le \log n\right)$$
103	102	3ad2ant2	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\wedge \left(1\le x\wedge x\le n\wedge n\le \mathrm{+\infty }\right)\right)\to \left(x\le n\leftrightarrow \log x\le \log n\right)$$
104	101 103	mpbid	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\wedge \left(1\le x\wedge x\le n\wedge n\le \mathrm{+\infty }\right)\right)\to \log x\le \log n$$
105		simprr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge 1\le x\right)\right)\to 1\le x$$
106		simprl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge 1\le x\right)\right)\to x\in {ℝ}^{+}$$
107		logleb	$$⊢\left(1\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to \left(1\le x\leftrightarrow \log 1\le \log x\right)$$
108	46 106 107	sylancr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge 1\le x\right)\right)\to \left(1\le x\leftrightarrow \log 1\le \log x\right)$$
109	105 108	mpbid	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge 1\le x\right)\right)\to \log 1\le \log x$$
110	56 109	eqbrtrrid	$$⊢\left(\left(A\in {ℝ}^{+}\wedge 1\le A\right)\wedge \left(x\in {ℝ}^{+}\wedge 1\le x\right)\right)\to 0\le \log x$$
111	46	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\in {ℝ}^{+}$$
112		1le1	$$⊢1\le 1$$
113	112	a1i	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\le 1$$
114		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\le A$$
115	10	rexrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\in {ℝ}^{*}$$
116		pnfge	$$⊢A\in {ℝ}^{*}\to A\le \mathrm{+\infty }$$
117	115 116	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\le \mathrm{+\infty }$$
118	78 79 80 82 84 87 88 95 92 97 99 100 104 38 110 111 1 113 114 117 34	dvfsum2	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(A\right)-\left(x\in {ℝ}^{+}⟼\sum _{n=1}^{⌊x⌋}\log n-x\left(\log x-1\right)\right)\left(1\right)\right|\le \log A$$
119	76 118	eqbrtrrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)-1\right|\le \log A$$
120	20 24 12 29 119	letrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-1\le \log A$$
121	18 82 12	lesubaddd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(\left|\log ⌊A⌋!-A\left(\log A-1\right)\right|-1\le \log A\leftrightarrow \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|\le \log A+1\right)$$
122	120 121	mpbid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left|\log ⌊A⌋!-A\left(\log A-1\right)\right|\le \log A+1$$