logfacrlim

Description: Combine the estimates logfacubnd and logfaclbnd , to get log ( x ! ) = x log x + O ( x ) . Equation 9.2.9 of Shapiro, p. 329. This is a weak form of the even stronger statement, log ( x ! ) = x log x - x + O ( log x ) . (Contributed by Mario Carneiro, 16-Apr-2016) (Revised by Mario Carneiro, 21-May-2016)

		Ref	Expression
	Assertion	logfacrlim	$⊢ (x \in ℝ^{+} ⟼ \log x - (\frac{\log ⌊x⌋!}{x})) \underset{ℝ}{⇝} 1$

Proof

Step	Hyp	Ref	Expression
1		1red	$⊢ ⊤ \to 1 \in ℝ$
2		1cnd	$⊢ ⊤ \to 1 \in ℂ$
3		relogcl	$⊢ x \in ℝ^{+} \to \log x \in ℝ$
4	3	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x \in ℝ$
5	4	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x \in ℂ$
6		1cnd	$⊢ (⊤ \land x \in ℝ^{+}) \to 1 \in ℂ$
7		rpcnne0	$⊢ x \in ℝ^{+} \to (x \in ℂ \land x \neq 0)$
8	7	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to (x \in ℂ \land x \neq 0)$
9		divdir	$⊢ (\log x \in ℂ \land 1 \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{\log x + 1}{x} = (\frac{\log x}{x}) + (\frac{1}{x})$
10	5 6 8 9	syl3anc	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\log x + 1}{x} = (\frac{\log x}{x}) + (\frac{1}{x})$
11	10	mpteq2dva	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\log x + 1}{x}) = (x \in ℝ^{+} ⟼ (\frac{\log x}{x}) + (\frac{1}{x}))$
12		simpr	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
13	4 12	rerpdivcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\log x}{x} \in ℝ$
14		rpreccl	$⊢ x \in ℝ^{+} \to \frac{1}{x} \in ℝ^{+}$
15	14	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ^{+}$
16	15	rpred	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{1}{x} \in ℝ$
17	8	simpld	$⊢ (⊤ \land x \in ℝ^{+}) \to x \in ℂ$
18	17	cxp1d	$⊢ (⊤ \land x \in ℝ^{+}) \to x^{1} = x$
19	18	oveq2d	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\log x}{x^{1}} = \frac{\log x}{x}$
20	19	mpteq2dva	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\log x}{x^{1}}) = (x \in ℝ^{+} ⟼ \frac{\log x}{x})$
21		1rp	$⊢ 1 \in ℝ^{+}$
22		cxploglim	$⊢ 1 \in ℝ^{+} \to (x \in ℝ^{+} ⟼ \frac{\log x}{x^{1}}) \underset{ℝ}{⇝} 0$
23	21 22	mp1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\log x}{x^{1}}) \underset{ℝ}{⇝} 0$
24	20 23	eqbrtrrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\log x}{x}) \underset{ℝ}{⇝} 0$
25		ax-1cn	$⊢ 1 \in ℂ$
26		divrcnv	$⊢ 1 \in ℂ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
27	25 26	mp1i	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{1}{x}) \underset{ℝ}{⇝} 0$
28	13 16 24 27	rlimadd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ (\frac{\log x}{x}) + (\frac{1}{x})) \underset{ℝ}{⇝} (0 + 0)$
29	11 28	eqbrtrd	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\log x + 1}{x}) \underset{ℝ}{⇝} (0 + 0)$
30		00id	$⊢ 0 + 0 = 0$
31	29 30	breqtrdi	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \frac{\log x + 1}{x}) \underset{ℝ}{⇝} 0$
32		peano2re	$⊢ \log x \in ℝ \to \log x + 1 \in ℝ$
33	4 32	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x + 1 \in ℝ$
34	33 12	rerpdivcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\log x + 1}{x} \in ℝ$
35	34	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\log x + 1}{x} \in ℂ$
36		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
37	36	adantl	$⊢ (⊤ \land x \in ℝ^{+}) \to (x \in ℝ \land 0 \leq x)$
38		flge0nn0	$⊢ (x \in ℝ \land 0 \leq x) \to ⌊x⌋ \in ℕ_{0}$
39		faccl	$⊢ ⌊x⌋ \in ℕ_{0} \to ⌊x⌋! \in ℕ$
40	37 38 39	3syl	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋! \in ℕ$
41	40	nnrpd	$⊢ (⊤ \land x \in ℝ^{+}) \to ⌊x⌋! \in ℝ^{+}$
42		relogcl	$⊢ ⌊x⌋! \in ℝ^{+} \to \log ⌊x⌋! \in ℝ$
43	41 42	syl	$⊢ (⊤ \land x \in ℝ^{+}) \to \log ⌊x⌋! \in ℝ$
44	43 12	rerpdivcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\log ⌊x⌋!}{x} \in ℝ$
45	44	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \frac{\log ⌊x⌋!}{x} \in ℂ$
46	5 45	subcld	$⊢ (⊤ \land x \in ℝ^{+}) \to \log x - (\frac{\log ⌊x⌋!}{x}) \in ℂ$
47		logfacbnd3	$⊢ (x \in ℝ^{+} \land 1 \leq x) \to \|\log ⌊x⌋! - x (\log x - 1)\| \leq \log x + 1$
48	47	adantl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\log ⌊x⌋! - x (\log x - 1)\| \leq \log x + 1$
49	43	recnd	$⊢ (⊤ \land x \in ℝ^{+}) \to \log ⌊x⌋! \in ℂ$
50	49	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log ⌊x⌋! \in ℂ$
51	7	ad2antrl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℂ \land x \neq 0)$
52	51	simpld	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℂ$
53	5	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \in ℂ$
54		subcl	$⊢ (\log x \in ℂ \land 1 \in ℂ) \to \log x - 1 \in ℂ$
55	53 25 54	sylancl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x - 1 \in ℂ$
56	52 55	mulcld	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to x (\log x - 1) \in ℂ$
57	50 56	subcld	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log ⌊x⌋! - x (\log x - 1) \in ℂ$
58	57	abscld	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\log ⌊x⌋! - x (\log x - 1)\| \in ℝ$
59	4	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x \in ℝ$
60	59 32	syl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x + 1 \in ℝ$
61		rpregt0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 < x)$
62	61	ad2antrl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℝ \land 0 < x)$
63		lediv1	$⊢ (\|\log ⌊x⌋! - x (\log x - 1)\| \in ℝ \land \log x + 1 \in ℝ \land (x \in ℝ \land 0 < x)) \to (\|\log ⌊x⌋! - x (\log x - 1)\| \leq \log x + 1 \leftrightarrow \frac{\|\log ⌊x⌋! - x (\log x - 1)\|}{x} \leq \frac{\log x + 1}{x})$
64	58 60 62 63	syl3anc	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (\|\log ⌊x⌋! - x (\log x - 1)\| \leq \log x + 1 \leftrightarrow \frac{\|\log ⌊x⌋! - x (\log x - 1)\|}{x} \leq \frac{\log x + 1}{x})$
65	48 64	mpbid	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\|\log ⌊x⌋! - x (\log x - 1)\|}{x} \leq \frac{\log x + 1}{x}$
66	51	simprd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \neq 0$
67	55 52 66	divcan3d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{x (\log x - 1)}{x} = \log x - 1$
68	67	oveq1d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (\frac{x (\log x - 1)}{x}) - (\frac{\log ⌊x⌋!}{x}) = \log x - 1 - (\frac{\log ⌊x⌋!}{x})$
69		divsubdir	$⊢ (x (\log x - 1) \in ℂ \land \log ⌊x⌋! \in ℂ \land (x \in ℂ \land x \neq 0)) \to \frac{x (\log x - 1) - \log ⌊x⌋!}{x} = (\frac{x (\log x - 1)}{x}) - (\frac{\log ⌊x⌋!}{x})$
70	56 50 51 69	syl3anc	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{x (\log x - 1) - \log ⌊x⌋!}{x} = (\frac{x (\log x - 1)}{x}) - (\frac{\log ⌊x⌋!}{x})$
71	45	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log ⌊x⌋!}{x} \in ℂ$
72		1cnd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \in ℂ$
73	53 71 72	sub32d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x - (\frac{\log ⌊x⌋!}{x}) - 1 = \log x - 1 - (\frac{\log ⌊x⌋!}{x})$
74	68 70 73	3eqtr4rd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x - (\frac{\log ⌊x⌋!}{x}) - 1 = \frac{x (\log x - 1) - \log ⌊x⌋!}{x}$
75	74	fveq2d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\log x - (\frac{\log ⌊x⌋!}{x}) - 1\| = \|\frac{x (\log x - 1) - \log ⌊x⌋!}{x}\|$
76	56 50	subcld	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to x (\log x - 1) - \log ⌊x⌋! \in ℂ$
77	76 52 66	absdivd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\frac{x (\log x - 1) - \log ⌊x⌋!}{x}\| = \frac{\|x (\log x - 1) - \log ⌊x⌋!\|}{\|x\|}$
78	56 50	abssubd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|x (\log x - 1) - \log ⌊x⌋!\| = \|\log ⌊x⌋! - x (\log x - 1)\|$
79	36	ad2antrl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (x \in ℝ \land 0 \leq x)$
80		absid	$⊢ (x \in ℝ \land 0 \leq x) \to \|x\| = x$
81	79 80	syl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|x\| = x$
82	78 81	oveq12d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\|x (\log x - 1) - \log ⌊x⌋!\|}{\|x\|} = \frac{\|\log ⌊x⌋! - x (\log x - 1)\|}{x}$
83	75 77 82	3eqtrd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\log x - (\frac{\log ⌊x⌋!}{x}) - 1\| = \frac{\|\log ⌊x⌋! - x (\log x - 1)\|}{x}$
84	35	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log x + 1}{x} \in ℂ$
85	84	subid1d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (\frac{\log x + 1}{x}) - 0 = \frac{\log x + 1}{x}$
86	85	fveq2d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\log x + 1}{x}) - 0\| = \|\frac{\log x + 1}{x}\|$
87		log1	$⊢ \log 1 = 0$
88		simprr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to 1 \leq x$
89	12	adantrr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to x \in ℝ^{+}$
90		logleb	$⊢ (1 \in ℝ^{+} \land x \in ℝ^{+}) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
91	21 89 90	sylancr	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to (1 \leq x \leftrightarrow \log 1 \leq \log x)$
92	88 91	mpbid	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log 1 \leq \log x$
93	87 92	eqbrtrrid	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to 0 \leq \log x$
94	59 93	ge0p1rpd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \log x + 1 \in ℝ^{+}$
95	94 89	rpdivcld	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \frac{\log x + 1}{x} \in ℝ^{+}$
96		rprege0	$⊢ \frac{\log x + 1}{x} \in ℝ^{+} \to (\frac{\log x + 1}{x} \in ℝ \land 0 \leq \frac{\log x + 1}{x})$
97		absid	$⊢ (\frac{\log x + 1}{x} \in ℝ \land 0 \leq \frac{\log x + 1}{x}) \to \|\frac{\log x + 1}{x}\| = \frac{\log x + 1}{x}$
98	95 96 97	3syl	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\frac{\log x + 1}{x}\| = \frac{\log x + 1}{x}$
99	86 98	eqtrd	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|(\frac{\log x + 1}{x}) - 0\| = \frac{\log x + 1}{x}$
100	65 83 99	3brtr4d	$⊢ (⊤ \land (x \in ℝ^{+} \land 1 \leq x)) \to \|\log x - (\frac{\log ⌊x⌋!}{x}) - 1\| \leq \|(\frac{\log x + 1}{x}) - 0\|$
101	1 2 31 35 46 100	rlimsqzlem	$⊢ ⊤ \to (x \in ℝ^{+} ⟼ \log x - (\frac{\log ⌊x⌋!}{x})) \underset{ℝ}{⇝} 1$
102	101	mptru	$⊢ (x \in ℝ^{+} ⟼ \log x - (\frac{\log ⌊x⌋!}{x})) \underset{ℝ}{⇝} 1$

Metamath Proof Explorer

Theorem logfacrlim

Proof