Theorem faclbnd2

Description: A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005)

	Ref	Expression
Assertion	faclbnd2	$$⊢N\in {\mathbb{N}}_0\to \frac{2^N}{2}\le N!$$

Proof

Step	Hyp	Ref	Expression
1		sq2	$$⊢2^2=4$$
2		2t2e4	$$⊢2\cdot 2=4$$
3	1 2	eqtr4i	$$⊢2^2=2\cdot 2$$
4	3	oveq2i	$$⊢\frac{2^{N+1}}{2^2}=\frac{2^{N+1}}{2\cdot 2}$$
5		2cn	$$⊢2\in ℂ$$
6		expp1	$$⊢\left(2\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to 2^{N+1}=2^N\cdot 2$$
7	5 6	mpan	$$⊢N\in {\mathbb{N}}_0\to 2^{N+1}=2^N\cdot 2$$
8	7	oveq1d	$$⊢N\in {\mathbb{N}}_0\to \frac{2^{N+1}}{2\cdot 2}=\frac{2^N\cdot 2}{2\cdot 2}$$
9	4 8	syl5eq	$$⊢N\in {\mathbb{N}}_0\to \frac{2^{N+1}}{2^2}=\frac{2^N\cdot 2}{2\cdot 2}$$
10		expcl	$$⊢\left(2\in ℂ\wedge N\in {\mathbb{N}}_0\right)\to 2^N\in ℂ$$
11	5 10	mpan	$$⊢N\in {\mathbb{N}}_0\to 2^N\in ℂ$$
12		2cnne0	$$⊢\left(2\in ℂ\wedge 2\ne 0\right)$$
13		divmuldiv	$$⊢\left(\left(2^N\in ℂ\wedge 2\in ℂ\right)\wedge \left(\left(2\in ℂ\wedge 2\ne 0\right)\wedge \left(2\in ℂ\wedge 2\ne 0\right)\right)\right)\to \left(\frac{2^N}{2}\right)\left(\frac{2}{2}\right)=\frac{2^N\cdot 2}{2\cdot 2}$$
14	12 12 13	mpanr12	$$⊢\left(2^N\in ℂ\wedge 2\in ℂ\right)\to \left(\frac{2^N}{2}\right)\left(\frac{2}{2}\right)=\frac{2^N\cdot 2}{2\cdot 2}$$
15	11 5 14	sylancl	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{2^N}{2}\right)\left(\frac{2}{2}\right)=\frac{2^N\cdot 2}{2\cdot 2}$$
16		2div2e1	$$⊢\frac{2}{2}=1$$
17	16	oveq2i	$$⊢\left(\frac{2^N}{2}\right)\left(\frac{2}{2}\right)=\left(\frac{2^N}{2}\right)\cdot 1$$
18	11	halfcld	$$⊢N\in {\mathbb{N}}_0\to \frac{2^N}{2}\in ℂ$$
19	18	mulid1d	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{2^N}{2}\right)\cdot 1=\frac{2^N}{2}$$
20	17 19	syl5eq	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{2^N}{2}\right)\left(\frac{2}{2}\right)=\frac{2^N}{2}$$
21	9 15 20	3eqtr2rd	$$⊢N\in {\mathbb{N}}_0\to \frac{2^N}{2}=\frac{2^{N+1}}{2^2}$$
22		2nn0	$$⊢2\in {\mathbb{N}}_0$$
23		faclbnd	$$⊢\left(2\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to 2^{N+1}\le 2^{2}N!$$
24	22 23	mpan	$$⊢N\in {\mathbb{N}}_0\to 2^{N+1}\le 2^{2}N!$$
25		2re	$$⊢2\in ℝ$$
26		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
27		reexpcl	$$⊢\left(2\in ℝ\wedge N+1\in {\mathbb{N}}_0\right)\to 2^{N+1}\in ℝ$$
28	25 26 27	sylancr	$$⊢N\in {\mathbb{N}}_0\to 2^{N+1}\in ℝ$$
29		faccl	$$⊢N\in {\mathbb{N}}_0\to N!\in \mathbb{N}$$
30	29	nnred	$$⊢N\in {\mathbb{N}}_0\to N!\in ℝ$$
31		4re	$$⊢4\in ℝ$$
32	1 31	eqeltri	$$⊢2^2\in ℝ$$
33		4pos	$$⊢0<4$$
34	33 1	breqtrri	$$⊢0<2^2$$
35	32 34	pm3.2i	$$⊢\left(2^2\in ℝ\wedge 0<2^2\right)$$
36		ledivmul	$$⊢\left(2^{N+1}\in ℝ\wedge N!\in ℝ\wedge \left(2^2\in ℝ\wedge 0<2^2\right)\right)\to \left(\frac{2^{N+1}}{2^2}\le N!\leftrightarrow 2^{N+1}\le 2^{2}N!\right)$$
37	35 36	mp3an3	$$⊢\left(2^{N+1}\in ℝ\wedge N!\in ℝ\right)\to \left(\frac{2^{N+1}}{2^2}\le N!\leftrightarrow 2^{N+1}\le 2^{2}N!\right)$$
38	28 30 37	syl2anc	$$⊢N\in {\mathbb{N}}_0\to \left(\frac{2^{N+1}}{2^2}\le N!\leftrightarrow 2^{N+1}\le 2^{2}N!\right)$$
39	24 38	mpbird	$$⊢N\in {\mathbb{N}}_0\to \frac{2^{N+1}}{2^2}\le N!$$
40	21 39	eqbrtrd	$$⊢N\in {\mathbb{N}}_0\to \frac{2^N}{2}\le N!$$