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	$⊢ (A \in ℝ^{+} \land 1 \leq A) \to \|\log ⌊A⌋! - A (\log A - 1)\| \leq \log A + 1$

Proof

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

Metamath Proof Explorer

Theorem logfacbnd3

Proof