Theorem faclbnd4lem3

Description: Lemma for faclbnd4 . The N = 0 case. (Contributed by NM, 23-Dec-2005)

	Ref	Expression
Assertion	faclbnd4lem3	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\wedge N=0\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢K\in {\mathbb{N}}_0\leftrightarrow \left(K\in \mathbb{N}\vee K=0\right)$$
2		0exp	$$⊢K\in \mathbb{N}\to 0^K=0$$
3	2	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in \mathbb{N}\right)\to 0^K=0$$
4		nnnn0	$$⊢K\in \mathbb{N}\to K\in {\mathbb{N}}_0$$
5		2nn0	$$⊢2\in {\mathbb{N}}_0$$
6		nn0sqcl	$$⊢K\in {\mathbb{N}}_0\to K^2\in {\mathbb{N}}_0$$
7		nn0expcl	$$⊢\left(2\in {\mathbb{N}}_0\wedge K^2\in {\mathbb{N}}_0\right)\to 2^{K^2}\in {\mathbb{N}}_0$$
8	5 6 7	sylancr	$$⊢K\in {\mathbb{N}}_0\to 2^{K^2}\in {\mathbb{N}}_0$$
9	8	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2^{K^2}\in {\mathbb{N}}_0$$
10		nn0addcl	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to M+K\in {\mathbb{N}}_0$$
11		nn0expcl	$$⊢\left(M\in {\mathbb{N}}_0\wedge M+K\in {\mathbb{N}}_0\right)\to M^{M+K}\in {\mathbb{N}}_0$$
12	10 11	syldan	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to M^{M+K}\in {\mathbb{N}}_0$$
13	9 12	nn0mulcld	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2^{K^2}{M}^{M+K}\in {\mathbb{N}}_0$$
14	4 13	sylan2	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in \mathbb{N}\right)\to 2^{K^2}{M}^{M+K}\in {\mathbb{N}}_0$$
15	14	nn0ge0d	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in \mathbb{N}\right)\to 0\le 2^{K^2}{M}^{M+K}$$
16	3 15	eqbrtrd	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in \mathbb{N}\right)\to 0^K\le 2^{K^2}{M}^{M+K}$$
17		1nn	$$⊢1\in \mathbb{N}$$
18		elnn0	$$⊢M\in {\mathbb{N}}_0\leftrightarrow \left(M\in \mathbb{N}\vee M=0\right)$$
19		nnnn0	$$⊢M\in \mathbb{N}\to M\in {\mathbb{N}}_0$$
20		0nn0	$$⊢0\in {\mathbb{N}}_0$$
21		nn0addcl	$$⊢\left(M\in {\mathbb{N}}_0\wedge 0\in {\mathbb{N}}_0\right)\to M+0\in {\mathbb{N}}_0$$
22	19 20 21	sylancl	$$⊢M\in \mathbb{N}\to M+0\in {\mathbb{N}}_0$$
23		nnexpcl	$$⊢\left(M\in \mathbb{N}\wedge M+0\in {\mathbb{N}}_0\right)\to M^{M+0}\in \mathbb{N}$$
24	22 23	mpdan	$$⊢M\in \mathbb{N}\to M^{M+0}\in \mathbb{N}$$
25		id	$$⊢M=0\to M=0$$
26		oveq1	$$⊢M=0\to M+0=0+0$$
27		00id	$$⊢0+0=0$$
28	26 27	eqtrdi	$$⊢M=0\to M+0=0$$
29	25 28	oveq12d	$$⊢M=0\to M^{M+0}=0^0$$
30		0exp0e1	$$⊢0^0=1$$
31	29 30	eqtrdi	$$⊢M=0\to M^{M+0}=1$$
32	31 17	eqeltrdi	$$⊢M=0\to M^{M+0}\in \mathbb{N}$$
33	24 32	jaoi	$$⊢\left(M\in \mathbb{N}\vee M=0\right)\to M^{M+0}\in \mathbb{N}$$
34	18 33	sylbi	$$⊢M\in {\mathbb{N}}_0\to M^{M+0}\in \mathbb{N}$$
35		nnmulcl	$$⊢\left(1\in \mathbb{N}\wedge M^{M+0}\in \mathbb{N}\right)\to 1M^{M+0}\in \mathbb{N}$$
36	17 34 35	sylancr	$$⊢M\in {\mathbb{N}}_0\to 1M^{M+0}\in \mathbb{N}$$
37	36	nnge1d	$$⊢M\in {\mathbb{N}}_0\to 1\le 1M^{M+0}$$
38	37	adantr	$$⊢\left(M\in {\mathbb{N}}_0\wedge K=0\right)\to 1\le 1M^{M+0}$$
39		oveq2	$$⊢K=0\to 0^K=0^0$$
40	39 30	eqtrdi	$$⊢K=0\to 0^K=1$$
41		sq0i	$$⊢K=0\to K^2=0$$
42	41	oveq2d	$$⊢K=0\to 2^{K^2}=2^0$$
43		2cn	$$⊢2\in ℂ$$
44		exp0	$$⊢2\in ℂ\to 2^0=1$$
45	43 44	ax-mp	$$⊢2^0=1$$
46	42 45	eqtrdi	$$⊢K=0\to 2^{K^2}=1$$
47		oveq2	$$⊢K=0\to M+K=M+0$$
48	47	oveq2d	$$⊢K=0\to M^{M+K}=M^{M+0}$$
49	46 48	oveq12d	$$⊢K=0\to 2^{K^2}{M}^{M+K}=1M^{M+0}$$
50	40 49	breq12d	$$⊢K=0\to \left(0^K\le 2^{K^2}{M}^{M+K}\leftrightarrow 1\le 1M^{M+0}\right)$$
51	50	adantl	$$⊢\left(M\in {\mathbb{N}}_0\wedge K=0\right)\to \left(0^K\le 2^{K^2}{M}^{M+K}\leftrightarrow 1\le 1M^{M+0}\right)$$
52	38 51	mpbird	$$⊢\left(M\in {\mathbb{N}}_0\wedge K=0\right)\to 0^K\le 2^{K^2}{M}^{M+K}$$
53	16 52	jaodan	$$⊢\left(M\in {\mathbb{N}}_0\wedge \left(K\in \mathbb{N}\vee K=0\right)\right)\to 0^K\le 2^{K^2}{M}^{M+K}$$
54	1 53	sylan2b	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 0^K\le 2^{K^2}{M}^{M+K}$$
55		nn0cn	$$⊢M\in {\mathbb{N}}_0\to M\in ℂ$$
56	55	exp0d	$$⊢M\in {\mathbb{N}}_0\to M^0=1$$
57	56	oveq2d	$$⊢M\in {\mathbb{N}}_0\to 0^K{M}^0=0^K\cdot 1$$
58		nn0expcl	$$⊢\left(0\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 0^K\in {\mathbb{N}}_0$$
59	20 58	mpan	$$⊢K\in {\mathbb{N}}_0\to 0^K\in {\mathbb{N}}_0$$
60	59	nn0cnd	$$⊢K\in {\mathbb{N}}_0\to 0^K\in ℂ$$
61	60	mulid1d	$$⊢K\in {\mathbb{N}}_0\to 0^K\cdot 1=0^K$$
62	57 61	sylan9eq	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 0^K{M}^0=0^K$$
63	13	nn0cnd	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2^{K^2}{M}^{M+K}\in ℂ$$
64	63	mulid1d	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 2^{K^2}{M}^{M+K}\cdot 1=2^{K^2}{M}^{M+K}$$
65	54 62 64	3brtr4d	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to 0^K{M}^0\le 2^{K^2}{M}^{M+K}\cdot 1$$
66	65	adantr	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\wedge N=0\right)\to 0^K{M}^0\le 2^{K^2}{M}^{M+K}\cdot 1$$
67		oveq1	$$⊢N=0\to N^K=0^K$$
68		oveq2	$$⊢N=0\to M^N=M^0$$
69	67 68	oveq12d	$$⊢N=0\to N^K{M}^N=0^K{M}^0$$
70		fveq2	$$⊢N=0\to N!=0!$$
71		fac0	$$⊢0!=1$$
72	70 71	eqtrdi	$$⊢N=0\to N!=1$$
73	72	oveq2d	$$⊢N=0\to 2^{K^2}{M}^{M+K}N!=2^{K^2}{M}^{M+K}\cdot 1$$
74	69 73	breq12d	$$⊢N=0\to \left(N^K{M}^N\le 2^{K^2}{M}^{M+K}N!\leftrightarrow 0^K{M}^0\le 2^{K^2}{M}^{M+K}\cdot 1\right)$$
75	74	adantl	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\wedge N=0\right)\to \left(N^K{M}^N\le 2^{K^2}{M}^{M+K}N!\leftrightarrow 0^K{M}^0\le 2^{K^2}{M}^{M+K}\cdot 1\right)$$
76	66 75	mpbird	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\wedge N=0\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$