Theorem logfacubnd

Description: A simple upper bound on the logarithm of a factorial. (Contributed by Mario Carneiro, 16-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
2		flge1nn	$$⊢\left(A\in ℝ\wedge 1\le A\right)\to ⌊A⌋\in \mathbb{N}$$
3	1 2	sylan	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\in \mathbb{N}$$
4	3	nnnn0d	$$⊢\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	6	relogcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!\in ℝ$$
8	1	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\in ℝ$$
9		reflcl	$$⊢A\in ℝ\to ⌊A⌋\in ℝ$$
10	8 9	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\in ℝ$$
11	3	nnrpd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\in {ℝ}^{+}$$
12	11	relogcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋\in ℝ$$
13	10 12	remulcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\log ⌊A⌋\in ℝ$$
14		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
15	14	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log A\in ℝ$$
16	8 15	remulcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\log A\in ℝ$$
17		facubnd	$$⊢⌊A⌋\in {\mathbb{N}}_0\to ⌊A⌋!\le {⌊A⌋}^{⌊A⌋}$$
18	4 17	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋!\le {⌊A⌋}^{⌊A⌋}$$
19	3 4	nnexpcld	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to {⌊A⌋}^{⌊A⌋}\in \mathbb{N}$$
20	19	nnrpd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to {⌊A⌋}^{⌊A⌋}\in {ℝ}^{+}$$
21	6 20	logled	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(⌊A⌋!\le {⌊A⌋}^{⌊A⌋}\leftrightarrow \log ⌊A⌋!\le \log {⌊A⌋}^{⌊A⌋}\right)$$
22	18 21	mpbid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!\le \log {⌊A⌋}^{⌊A⌋}$$
23	3	nnzd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\in \mathbb{Z}$$
24		relogexp	$$⊢\left(⌊A⌋\in {ℝ}^{+}\wedge ⌊A⌋\in \mathbb{Z}\right)\to \log {⌊A⌋}^{⌊A⌋}=⌊A⌋\log ⌊A⌋$$
25	11 23 24	syl2anc	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log {⌊A⌋}^{⌊A⌋}=⌊A⌋\log ⌊A⌋$$
26	22 25	breqtrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!\le ⌊A⌋\log ⌊A⌋$$
27		flle	$$⊢A\in ℝ\to ⌊A⌋\le A$$
28	8 27	syl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\le A$$
29		simpl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to A\in {ℝ}^{+}$$
30	11 29	logled	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(⌊A⌋\le A\leftrightarrow \log ⌊A⌋\le \log A\right)$$
31	28 30	mpbid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋\le \log A$$
32	11	rprege0d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(⌊A⌋\in ℝ\wedge 0\le ⌊A⌋\right)$$
33		log1	$$⊢\log 1=0$$
34	3	nnge1d	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 1\le ⌊A⌋$$
35		1rp	$$⊢1\in {ℝ}^{+}$$
36		logleb	$$⊢\left(1\in {ℝ}^{+}\wedge ⌊A⌋\in {ℝ}^{+}\right)\to \left(1\le ⌊A⌋\leftrightarrow \log 1\le \log ⌊A⌋\right)$$
37	35 11 36	sylancr	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(1\le ⌊A⌋\leftrightarrow \log 1\le \log ⌊A⌋\right)$$
38	34 37	mpbid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log 1\le \log ⌊A⌋$$
39	33 38	eqbrtrrid	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to 0\le \log ⌊A⌋$$
40	12 39	jca	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(\log ⌊A⌋\in ℝ\wedge 0\le \log ⌊A⌋\right)$$
41		lemul12a	$$⊢\left(\left(\left(⌊A⌋\in ℝ\wedge 0\le ⌊A⌋\right)\wedge A\in ℝ\right)\wedge \left(\left(\log ⌊A⌋\in ℝ\wedge 0\le \log ⌊A⌋\right)\wedge \log A\in ℝ\right)\right)\to \left(\left(⌊A⌋\le A\wedge \log ⌊A⌋\le \log A\right)\to ⌊A⌋\log ⌊A⌋\le A\log A\right)$$
42	32 8 40 15 41	syl22anc	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \left(\left(⌊A⌋\le A\wedge \log ⌊A⌋\le \log A\right)\to ⌊A⌋\log ⌊A⌋\le A\log A\right)$$
43	28 31 42	mp2and	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to ⌊A⌋\log ⌊A⌋\le A\log A$$
44	7 13 16 26 43	letrd	$$⊢\left(A\in {ℝ}^{+}\wedge 1\le A\right)\to \log ⌊A⌋!\le A\log A$$