Theorem faclbnd4lem2

Description: Lemma for faclbnd4 . Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 to antecedents. (Contributed by NM, 23-Dec-2005)

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

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to M^{N-1}={if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}$$
2	1	oveq2d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to {\left(N-1\right)}^K{M}^{N-1}={\left(N-1\right)}^K{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}$$
3		id	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to M=if\left(M\in {\mathbb{N}}_0,M,1\right)$$
4		oveq1	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to M+K=if\left(M\in {\mathbb{N}}_0,M,1\right)+K$$
5	3 4	oveq12d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to M^{M+K}={if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}$$
6	5	oveq2d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to 2^{K^2}{M}^{M+K}=2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}$$
7	6	oveq1d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to 2^{K^2}{M}^{M+K}\left(N-1\right)!=2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}\left(N-1\right)!$$
8	2 7	breq12d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to \left({\left(N-1\right)}^K{M}^{N-1}\le 2^{K^2}{M}^{M+K}\left(N-1\right)!\leftrightarrow {\left(N-1\right)}^K{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}\left(N-1\right)!\right)$$
9		oveq1	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to M^N={if\left(M\in {\mathbb{N}}_0,M,1\right)}^N$$
10	9	oveq2d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to N^{K+1}{M}^N=N^{K+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N$$
11		oveq1	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to M+K+1=if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1$$
12	3 11	oveq12d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to M^{M+K+1}={if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}$$
13	12	oveq2d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to 2^{{\left(K+1\right)}^2}{M}^{M+K+1}=2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}$$
14	13	oveq1d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to 2^{{\left(K+1\right)}^2}{M}^{M+K+1}N!=2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}N!$$
15	10 14	breq12d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to \left(N^{K+1}{M}^N\le 2^{{\left(K+1\right)}^2}{M}^{M+K+1}N!\leftrightarrow N^{K+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}N!\right)$$
16	8 15	imbi12d	$$⊢M=if\left(M\in {\mathbb{N}}_0,M,1\right)\to \left(\left({\left(N-1\right)}^K{M}^{N-1}\le 2^{K^2}{M}^{M+K}\left(N-1\right)!\to N^{K+1}{M}^N\le 2^{{\left(K+1\right)}^2}{M}^{M+K+1}N!\right)\leftrightarrow \left({\left(N-1\right)}^K{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}\left(N-1\right)!\to N^{K+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}N!\right)\right)$$
17		oveq2	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to {\left(N-1\right)}^K={\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}$$
18	17	oveq1d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to {\left(N-1\right)}^K{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}={\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}$$
19		oveq1	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to K^2={if\left(K\in {\mathbb{N}}_0,K,1\right)}^2$$
20	19	oveq2d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to 2^{K^2}=2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}$$
21		oveq2	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to if\left(M\in {\mathbb{N}}_0,M,1\right)+K=if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)$$
22	21	oveq2d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to {if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}={if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}$$
23	20 22	oveq12d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to 2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}=2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}$$
24	23	oveq1d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to 2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}\left(N-1\right)!=2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(N-1\right)!$$
25	18 24	breq12d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to \left({\left(N-1\right)}^K{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}\left(N-1\right)!\leftrightarrow {\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(N-1\right)!\right)$$
26		oveq1	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to K+1=if\left(K\in {\mathbb{N}}_0,K,1\right)+1$$
27	26	oveq2d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to N^{K+1}=N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}$$
28	27	oveq1d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to N^{K+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N=N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N$$
29	26	oveq1d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to {\left(K+1\right)}^2={\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2$$
30	29	oveq2d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to 2^{{\left(K+1\right)}^2}=2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}$$
31	26	oveq2d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1=if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1$$
32	31	oveq2d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to {if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}={if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}$$
33	30 32	oveq12d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to 2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}=2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}$$
34	33	oveq1d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to 2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}N!=2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}N!$$
35	28 34	breq12d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to \left(N^{K+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}N!\leftrightarrow N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}N!\right)$$
36	25 35	imbi12d	$$⊢K=if\left(K\in {\mathbb{N}}_0,K,1\right)\to \left(\left({\left(N-1\right)}^K{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{K^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K}\left(N-1\right)!\to N^{K+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(K+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+K+1}N!\right)\leftrightarrow \left({\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(N-1\right)!\to N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}N!\right)\right)$$
37		oveq1	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to N-1=if\left(N\in \mathbb{N},N,1\right)-1$$
38	37	oveq1d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to {\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}={\left(if\left(N\in \mathbb{N},N,1\right)-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}$$
39	37	oveq2d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to {if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}={if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)-1}$$
40	38 39	oveq12d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to {\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}={\left(if\left(N\in \mathbb{N},N,1\right)-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)-1}$$
41		fvoveq1	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to \left(N-1\right)!=\left(if\left(N\in \mathbb{N},N,1\right)-1\right)!$$
42	41	oveq2d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(N-1\right)!=2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(if\left(N\in \mathbb{N},N,1\right)-1\right)!$$
43	40 42	breq12d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to \left({\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(N-1\right)!\leftrightarrow {\left(if\left(N\in \mathbb{N},N,1\right)-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)-1}\le 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(if\left(N\in \mathbb{N},N,1\right)-1\right)!\right)$$
44		oveq1	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}={if\left(N\in \mathbb{N},N,1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}$$
45		oveq2	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to {if\left(M\in {\mathbb{N}}_0,M,1\right)}^N={if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)}$$
46	44 45	oveq12d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N={if\left(N\in \mathbb{N},N,1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)}$$
47		fveq2	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to N!=if\left(N\in \mathbb{N},N,1\right)!$$
48	47	oveq2d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}N!=2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}if\left(N\in \mathbb{N},N,1\right)!$$
49	46 48	breq12d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to \left(N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}N!\leftrightarrow {if\left(N\in \mathbb{N},N,1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)}\le 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}if\left(N\in \mathbb{N},N,1\right)!\right)$$
50	43 49	imbi12d	$$⊢N=if\left(N\in \mathbb{N},N,1\right)\to \left(\left({\left(N-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{N-1}\le 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(N-1\right)!\to N^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^N\le 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}N!\right)\leftrightarrow \left({\left(if\left(N\in \mathbb{N},N,1\right)-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)-1}\le 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(if\left(N\in \mathbb{N},N,1\right)-1\right)!\to {if\left(N\in \mathbb{N},N,1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)}\le 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}if\left(N\in \mathbb{N},N,1\right)!\right)\right)$$
51		1nn	$$⊢1\in \mathbb{N}$$
52	51	elimel	$$⊢if\left(N\in \mathbb{N},N,1\right)\in \mathbb{N}$$
53		1nn0	$$⊢1\in {\mathbb{N}}_0$$
54	53	elimel	$$⊢if\left(K\in {\mathbb{N}}_0,K,1\right)\in {\mathbb{N}}_0$$
55	53	elimel	$$⊢if\left(M\in {\mathbb{N}}_0,M,1\right)\in {\mathbb{N}}_0$$
56	52 54 55	faclbnd4lem1	$$⊢{\left(if\left(N\in \mathbb{N},N,1\right)-1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)-1}\le 2^{{if\left(K\in {\mathbb{N}}_0,K,1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)}\left(if\left(N\in \mathbb{N},N,1\right)-1\right)!\to {if\left(N\in \mathbb{N},N,1\right)}^{if\left(K\in {\mathbb{N}}_0,K,1\right)+1}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(N\in \mathbb{N},N,1\right)}\le 2^{{\left(if\left(K\in {\mathbb{N}}_0,K,1\right)+1\right)}^2}{if\left(M\in {\mathbb{N}}_0,M,1\right)}^{if\left(M\in {\mathbb{N}}_0,M,1\right)+if\left(K\in {\mathbb{N}}_0,K,1\right)+1}if\left(N\in \mathbb{N},N,1\right)!$$
57	16 36 50 56	dedth3h	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\wedge N\in \mathbb{N}\right)\to \left({\left(N-1\right)}^K{M}^{N-1}\le 2^{K^2}{M}^{M+K}\left(N-1\right)!\to N^{K+1}{M}^N\le 2^{{\left(K+1\right)}^2}{M}^{M+K+1}N!\right)$$