Theorem faclbnd4

Description: Variant of faclbnd5 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005)

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

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
2		faclbnd4lem4	$$⊢\left(N\in \mathbb{N}\wedge K\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$
3	2	3com13	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\wedge N\in \mathbb{N}\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$
4	3	3expa	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\wedge N\in \mathbb{N}\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$
5		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!$$
6	4 5	jaodan	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\wedge \left(N\in \mathbb{N}\vee N=0\right)\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$
7	1 6	sylan2b	$$⊢\left(\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\wedge N\in {\mathbb{N}}_0\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$
8	7	3impa	$$⊢\left(M\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$
9	8	3com13	$$⊢\left(N\in {\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\wedge M\in {\mathbb{N}}_0\right)\to N^K{M}^N\le 2^{K^2}{M}^{M+K}N!$$