faclbnd4lem1

Description: Lemma for faclbnd4 . Prepare the induction step. (Contributed by NM, 20-Dec-2005)

	Ref	Expression
Hypotheses	faclbnd4lem1.1	$⊢ N \in ℕ$
	faclbnd4lem1.2	$⊢ K \in ℕ_{0}$
	faclbnd4lem1.3	$⊢ M \in ℕ_{0}$
Assertion	faclbnd4lem1	$⊢ {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)! \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$

Proof

Step	Hyp	Ref	Expression
1		faclbnd4lem1.1	$⊢ N \in ℕ$
2		faclbnd4lem1.2	$⊢ K \in ℕ_{0}$
3		faclbnd4lem1.3	$⊢ M \in ℕ_{0}$
4	1	nnrei	$⊢ N \in ℝ$
5		1re	$⊢ 1 \in ℝ$
6		lelttric	$⊢ (N \in ℝ \land 1 \in ℝ) \to (N \leq 1 \lor 1 < N)$
7	4 5 6	mp2an	$⊢ (N \leq 1 \lor 1 < N)$
8		nnge1	$⊢ N \in ℕ \to 1 \leq N$
9	1 8	ax-mp	$⊢ 1 \leq N$
10	4 5	letri3i	$⊢ N = 1 \leftrightarrow (N \leq 1 \land 1 \leq N)$
11	9 10	mpbiran2	$⊢ N = 1 \leftrightarrow N \leq 1$
12		0le1	$⊢ 0 \leq 1$
13	5 12	pm3.2i	$⊢ (1 \in ℝ \land 0 \leq 1)$
14		2re	$⊢ 2 \in ℝ$
15		1nn	$⊢ 1 \in ℕ$
16		nn0nnaddcl	$⊢ (K \in ℕ_{0} \land 1 \in ℕ) \to K + 1 \in ℕ$
17	2 15 16	mp2an	$⊢ K + 1 \in ℕ$
18	17	nnnn0i	$⊢ K + 1 \in ℕ_{0}$
19		2nn0	$⊢ 2 \in ℕ_{0}$
20	18 19	nn0expcli	$⊢ {(K + 1)}^{2} \in ℕ_{0}$
21		reexpcl	$⊢ (2 \in ℝ \land {(K + 1)}^{2} \in ℕ_{0}) \to 2^{{(K + 1)}^{2}} \in ℝ$
22	14 20 21	mp2an	$⊢ 2^{{(K + 1)}^{2}} \in ℝ$
23	13 22	pm3.2i	$⊢ ((1 \in ℝ \land 0 \leq 1) \land 2^{{(K + 1)}^{2}} \in ℝ)$
24	3	nn0rei	$⊢ M \in ℝ$
25	3	nn0ge0i	$⊢ 0 \leq M$
26	24 25	pm3.2i	$⊢ (M \in ℝ \land 0 \leq M)$
27		nn0nnaddcl	$⊢ (M \in ℕ_{0} \land K + 1 \in ℕ) \to M + K + 1 \in ℕ$
28	3 17 27	mp2an	$⊢ M + K + 1 \in ℕ$
29	28	nnnn0i	$⊢ M + K + 1 \in ℕ_{0}$
30	3 29	nn0expcli	$⊢ M^{M + K + 1} \in ℕ_{0}$
31	30	nn0rei	$⊢ M^{M + K + 1} \in ℝ$
32	26 31	pm3.2i	$⊢ ((M \in ℝ \land 0 \leq M) \land M^{M + K + 1} \in ℝ)$
33	23 32	pm3.2i	$⊢ (((1 \in ℝ \land 0 \leq 1) \land 2^{{(K + 1)}^{2}} \in ℝ) \land ((M \in ℝ \land 0 \leq M) \land M^{M + K + 1} \in ℝ))$
34		2cn	$⊢ 2 \in ℂ$
35		exp0	$⊢ 2 \in ℂ \to 2^{0} = 1$
36	34 35	ax-mp	$⊢ 2^{0} = 1$
37		1le2	$⊢ 1 \leq 2$
38		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
39	20 38	eleqtri	$⊢ {(K + 1)}^{2} \in ℤ_{\geq 0}$
40		leexp2a	$⊢ (2 \in ℝ \land 1 \leq 2 \land {(K + 1)}^{2} \in ℤ_{\geq 0}) \to 2^{0} \leq 2^{{(K + 1)}^{2}}$
41	14 37 39 40	mp3an	$⊢ 2^{0} \leq 2^{{(K + 1)}^{2}}$
42	36 41	eqbrtrri	$⊢ 1 \leq 2^{{(K + 1)}^{2}}$
43		elnn0	$⊢ M \in ℕ_{0} \leftrightarrow (M \in ℕ \lor M = 0)$
44		nncn	$⊢ M \in ℕ \to M \in ℂ$
45	44	exp1d	$⊢ M \in ℕ \to M^{1} = M$
46		nnge1	$⊢ M \in ℕ \to 1 \leq M$
47		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
48	28 47	eleqtri	$⊢ M + K + 1 \in ℤ_{\geq 1}$
49		leexp2a	$⊢ (M \in ℝ \land 1 \leq M \land M + K + 1 \in ℤ_{\geq 1}) \to M^{1} \leq M^{M + K + 1}$
50	24 48 49	mp3an13	$⊢ 1 \leq M \to M^{1} \leq M^{M + K + 1}$
51	46 50	syl	$⊢ M \in ℕ \to M^{1} \leq M^{M + K + 1}$
52	45 51	eqbrtrrd	$⊢ M \in ℕ \to M \leq M^{M + K + 1}$
53	30	nn0ge0i	$⊢ 0 \leq M^{M + K + 1}$
54		breq1	$⊢ M = 0 \to (M \leq M^{M + K + 1} \leftrightarrow 0 \leq M^{M + K + 1})$
55	53 54	mpbiri	$⊢ M = 0 \to M \leq M^{M + K + 1}$
56	52 55	jaoi	$⊢ (M \in ℕ \lor M = 0) \to M \leq M^{M + K + 1}$
57	43 56	sylbi	$⊢ M \in ℕ_{0} \to M \leq M^{M + K + 1}$
58	3 57	ax-mp	$⊢ M \leq M^{M + K + 1}$
59	42 58	pm3.2i	$⊢ (1 \leq 2^{{(K + 1)}^{2}} \land M \leq M^{M + K + 1})$
60		lemul12a	$⊢ (((1 \in ℝ \land 0 \leq 1) \land 2^{{(K + 1)}^{2}} \in ℝ) \land ((M \in ℝ \land 0 \leq M) \land M^{M + K + 1} \in ℝ)) \to ((1 \leq 2^{{(K + 1)}^{2}} \land M \leq M^{M + K + 1}) \to 1 \cdot M \leq 2^{{(K + 1)}^{2}} M^{M + K + 1})$
61	33 59 60	mp2	$⊢ 1 \cdot M \leq 2^{{(K + 1)}^{2}} M^{M + K + 1}$
62		oveq1	$⊢ N = 1 \to N^{K + 1} = 1^{K + 1}$
63	17	nnzi	$⊢ K + 1 \in ℤ$
64		1exp	$⊢ K + 1 \in ℤ \to 1^{K + 1} = 1$
65	63 64	ax-mp	$⊢ 1^{K + 1} = 1$
66	62 65	eqtrdi	$⊢ N = 1 \to N^{K + 1} = 1$
67		oveq2	$⊢ N = 1 \to M^{N} = M^{1}$
68	3	nn0cni	$⊢ M \in ℂ$
69		exp1	$⊢ M \in ℂ \to M^{1} = M$
70	68 69	ax-mp	$⊢ M^{1} = M$
71	67 70	eqtrdi	$⊢ N = 1 \to M^{N} = M$
72	66 71	oveq12d	$⊢ N = 1 \to N^{K + 1} M^{N} = 1 \cdot M$
73		fveq2	$⊢ N = 1 \to N! = 1!$
74		fac1	$⊢ 1! = 1$
75	73 74	eqtrdi	$⊢ N = 1 \to N! = 1$
76	75	oveq2d	$⊢ N = 1 \to 2^{{(K + 1)}^{2}} M^{M + K + 1} N! = 2^{{(K + 1)}^{2}} M^{M + K + 1} \cdot 1$
77	22	recni	$⊢ 2^{{(K + 1)}^{2}} \in ℂ$
78	30	nn0cni	$⊢ M^{M + K + 1} \in ℂ$
79	77 78	mulcli	$⊢ 2^{{(K + 1)}^{2}} M^{M + K + 1} \in ℂ$
80	79	mulid1i	$⊢ 2^{{(K + 1)}^{2}} M^{M + K + 1} \cdot 1 = 2^{{(K + 1)}^{2}} M^{M + K + 1}$
81	76 80	eqtrdi	$⊢ N = 1 \to 2^{{(K + 1)}^{2}} M^{M + K + 1} N! = 2^{{(K + 1)}^{2}} M^{M + K + 1}$
82	72 81	breq12d	$⊢ N = 1 \to (N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N! \leftrightarrow 1 \cdot M \leq 2^{{(K + 1)}^{2}} M^{M + K + 1})$
83	61 82	mpbiri	$⊢ N = 1 \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
84	11 83	sylbir	$⊢ N \leq 1 \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
85	84	adantr	$⊢ (N \leq 1 \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
86		reexpcl	$⊢ (N \in ℝ \land K + 1 \in ℕ_{0}) \to N^{K + 1} \in ℝ$
87	4 18 86	mp2an	$⊢ N^{K + 1} \in ℝ$
88	1	nnnn0i	$⊢ N \in ℕ_{0}$
89		reexpcl	$⊢ (M \in ℝ \land N \in ℕ_{0}) \to M^{N} \in ℝ$
90	24 88 89	mp2an	$⊢ M^{N} \in ℝ$
91	87 90	remulcli	$⊢ N^{K + 1} M^{N} \in ℝ$
92	91	a1i	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K + 1} M^{N} \in ℝ$
93	2 19	nn0expcli	$⊢ K^{2} \in ℕ_{0}$
94		reexpcl	$⊢ (2 \in ℝ \land K^{2} \in ℕ_{0}) \to 2^{K^{2}} \in ℝ$
95	14 93 94	mp2an	$⊢ 2^{K^{2}} \in ℝ$
96	19 2	nn0expcli	$⊢ 2^{K} \in ℕ_{0}$
97	96	nn0rei	$⊢ 2^{K} \in ℝ$
98	95 97	remulcli	$⊢ 2^{K^{2}} 2^{K} \in ℝ$
99		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
100	88 99	ax-mp	$⊢ N! \in ℕ$
101	100	nnnn0i	$⊢ N! \in ℕ_{0}$
102	30 101	nn0mulcli	$⊢ M^{M + K + 1} N! \in ℕ_{0}$
103	102	nn0rei	$⊢ M^{M + K + 1} N! \in ℝ$
104	98 103	remulcli	$⊢ 2^{K^{2}} 2^{K} M^{M + K + 1} N! \in ℝ$
105	104	a1i	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to 2^{K^{2}} 2^{K} M^{M + K + 1} N! \in ℝ$
106	22 103	remulcli	$⊢ 2^{{(K + 1)}^{2}} M^{M + K + 1} N! \in ℝ$
107	106	a1i	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to 2^{{(K + 1)}^{2}} M^{M + K + 1} N! \in ℝ$
108	1	nncni	$⊢ N \in ℂ$
109		expp1	$⊢ (N \in ℂ \land K \in ℕ_{0}) \to N^{K + 1} = N^{K} \cdot N$
110	108 2 109	mp2an	$⊢ N^{K + 1} = N^{K} \cdot N$
111		expm1t	$⊢ (M \in ℂ \land N \in ℕ) \to M^{N} = M^{N - 1} \cdot M$
112	68 1 111	mp2an	$⊢ M^{N} = M^{N - 1} \cdot M$
113	110 112	oveq12i	$⊢ N^{K + 1} M^{N} = N^{K} \cdot N M^{N - 1} \cdot M$
114		reexpcl	$⊢ (N \in ℝ \land K \in ℕ_{0}) \to N^{K} \in ℝ$
115	4 2 114	mp2an	$⊢ N^{K} \in ℝ$
116	115	recni	$⊢ N^{K} \in ℂ$
117		elnnnn0	$⊢ N \in ℕ \leftrightarrow (N \in ℂ \land N - 1 \in ℕ_{0})$
118	1 117	mpbi	$⊢ (N \in ℂ \land N - 1 \in ℕ_{0})$
119	118	simpri	$⊢ N - 1 \in ℕ_{0}$
120	3 119	nn0expcli	$⊢ M^{N - 1} \in ℕ_{0}$
121	120 3	nn0mulcli	$⊢ M^{N - 1} \cdot M \in ℕ_{0}$
122	121	nn0cni	$⊢ M^{N - 1} \cdot M \in ℂ$
123	116 108 122	mulassi	$⊢ N^{K} \cdot N M^{N - 1} \cdot M = N^{K} N M^{N - 1} \cdot M$
124	113 123	eqtri	$⊢ N^{K + 1} M^{N} = N^{K} N M^{N - 1} \cdot M$
125	88 121	nn0mulcli	$⊢ N M^{N - 1} \cdot M \in ℕ_{0}$
126	125	nn0rei	$⊢ N M^{N - 1} \cdot M \in ℝ$
127	115 126	remulcli	$⊢ N^{K} N M^{N - 1} \cdot M \in ℝ$
128	127	a1i	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K} N M^{N - 1} \cdot M \in ℝ$
129	119	nn0rei	$⊢ N - 1 \in ℝ$
130		reexpcl	$⊢ (N - 1 \in ℝ \land K \in ℕ_{0}) \to {(N - 1)}^{K} \in ℝ$
131	129 2 130	mp2an	$⊢ {(N - 1)}^{K} \in ℝ$
132	120	nn0rei	$⊢ M^{N - 1} \in ℝ$
133	131 132	remulcli	$⊢ {(N - 1)}^{K} M^{N - 1} \in ℝ$
134	96 88	nn0mulcli	$⊢ 2^{K} \cdot N \in ℕ_{0}$
135	134 3	nn0mulcli	$⊢ 2^{K} \cdot N \cdot M \in ℕ_{0}$
136	135	nn0rei	$⊢ 2^{K} \cdot N \cdot M \in ℝ$
137	133 136	remulcli	$⊢ {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M \in ℝ$
138	137	a1i	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M \in ℝ$
139	3 2	nn0addcli	$⊢ M + K \in ℕ_{0}$
140		reexpcl	$⊢ (M \in ℝ \land M + K \in ℕ_{0}) \to M^{M + K} \in ℝ$
141	24 139 140	mp2an	$⊢ M^{M + K} \in ℝ$
142	95 141	remulcli	$⊢ 2^{K^{2}} M^{M + K} \in ℝ$
143		faccl	$⊢ N - 1 \in ℕ_{0} \to (N - 1)! \in ℕ$
144	119 143	ax-mp	$⊢ (N - 1)! \in ℕ$
145	144	nnrei	$⊢ (N - 1)! \in ℝ$
146	142 145	remulcli	$⊢ 2^{K^{2}} M^{M + K} (N - 1)! \in ℝ$
147	146 136	remulcli	$⊢ 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M \in ℝ$
148	147	a1i	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M \in ℝ$
149	97 131	remulcli	$⊢ 2^{K} {(N - 1)}^{K} \in ℝ$
150	125	nn0ge0i	$⊢ 0 \leq N M^{N - 1} \cdot M$
151	126 150	pm3.2i	$⊢ (N M^{N - 1} \cdot M \in ℝ \land 0 \leq N M^{N - 1} \cdot M)$
152	115 149 151	3pm3.2i	$⊢ (N^{K} \in ℝ \land 2^{K} {(N - 1)}^{K} \in ℝ \land (N M^{N - 1} \cdot M \in ℝ \land 0 \leq N M^{N - 1} \cdot M))$
153		nnltp1le	$⊢ (1 \in ℕ \land N \in ℕ) \to (1 < N \leftrightarrow 1 + 1 \leq N)$
154	15 1 153	mp2an	$⊢ 1 < N \leftrightarrow 1 + 1 \leq N$
155		df-2	$⊢ 2 = 1 + 1$
156	155	breq1i	$⊢ 2 \leq N \leftrightarrow 1 + 1 \leq N$
157	154 156	bitr4i	$⊢ 1 < N \leftrightarrow 2 \leq N$
158		expubnd	$⊢ (N \in ℝ \land K \in ℕ_{0} \land 2 \leq N) \to N^{K} \leq 2^{K} {(N - 1)}^{K}$
159	4 2 158	mp3an12	$⊢ 2 \leq N \to N^{K} \leq 2^{K} {(N - 1)}^{K}$
160	157 159	sylbi	$⊢ 1 < N \to N^{K} \leq 2^{K} {(N - 1)}^{K}$
161		lemul1a	$⊢ ((N^{K} \in ℝ \land 2^{K} {(N - 1)}^{K} \in ℝ \land (N M^{N - 1} \cdot M \in ℝ \land 0 \leq N M^{N - 1} \cdot M)) \land N^{K} \leq 2^{K} {(N - 1)}^{K}) \to N^{K} N M^{N - 1} \cdot M \leq 2^{K} {(N - 1)}^{K} N M^{N - 1} \cdot M$
162	152 160 161	sylancr	$⊢ 1 < N \to N^{K} N M^{N - 1} \cdot M \leq 2^{K} {(N - 1)}^{K} N M^{N - 1} \cdot M$
163	96	nn0cni	$⊢ 2^{K} \in ℂ$
164	131	recni	$⊢ {(N - 1)}^{K} \in ℂ$
165	163 164 108 122	mul4i	$⊢ 2^{K} {(N - 1)}^{K} N M^{N - 1} \cdot M = 2^{K} \cdot N {(N - 1)}^{K} M^{N - 1} \cdot M$
166	120	nn0cni	$⊢ M^{N - 1} \in ℂ$
167	164 166 68	mulassi	$⊢ {(N - 1)}^{K} M^{N - 1} \cdot M = {(N - 1)}^{K} M^{N - 1} \cdot M$
168	167	oveq2i	$⊢ 2^{K} \cdot N {(N - 1)}^{K} M^{N - 1} \cdot M = 2^{K} \cdot N {(N - 1)}^{K} M^{N - 1} \cdot M$
169	134	nn0cni	$⊢ 2^{K} \cdot N \in ℂ$
170	133	recni	$⊢ {(N - 1)}^{K} M^{N - 1} \in ℂ$
171	169 170 68	mul12i	$⊢ 2^{K} \cdot N {(N - 1)}^{K} M^{N - 1} \cdot M = {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M$
172	165 168 171	3eqtr2i	$⊢ 2^{K} {(N - 1)}^{K} N M^{N - 1} \cdot M = {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M$
173	162 172	breqtrdi	$⊢ 1 < N \to N^{K} N M^{N - 1} \cdot M \leq {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M$
174	173	adantr	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K} N M^{N - 1} \cdot M \leq {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M$
175	135	nn0ge0i	$⊢ 0 \leq 2^{K} \cdot N \cdot M$
176	136 175	pm3.2i	$⊢ (2^{K} \cdot N \cdot M \in ℝ \land 0 \leq 2^{K} \cdot N \cdot M)$
177	133 146 176	3pm3.2i	$⊢ ({(N - 1)}^{K} M^{N - 1} \in ℝ \land 2^{K^{2}} M^{M + K} (N - 1)! \in ℝ \land (2^{K} \cdot N \cdot M \in ℝ \land 0 \leq 2^{K} \cdot N \cdot M))$
178		lemul1a	$⊢ (({(N - 1)}^{K} M^{N - 1} \in ℝ \land 2^{K^{2}} M^{M + K} (N - 1)! \in ℝ \land (2^{K} \cdot N \cdot M \in ℝ \land 0 \leq 2^{K} \cdot N \cdot M)) \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M \leq 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M$
179	177 178	mpan	$⊢ {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)! \to {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M \leq 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M$
180	179	adantl	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to {(N - 1)}^{K} M^{N - 1} 2^{K} \cdot N \cdot M \leq 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M$
181	128 138 148 174 180	letrd	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K} N M^{N - 1} \cdot M \leq 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M$
182	163 108 68	mul32i	$⊢ 2^{K} \cdot N \cdot M = 2^{K} \cdot M \cdot N$
183	182	oveq2i	$⊢ 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M = 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot M \cdot N$
184		expp1	$⊢ (M \in ℂ \land M + K \in ℕ_{0}) \to M^{M + K + 1} = M^{M + K} \cdot M$
185	68 139 184	mp2an	$⊢ M^{M + K + 1} = M^{M + K} \cdot M$
186	2	nn0cni	$⊢ K \in ℂ$
187		ax-1cn	$⊢ 1 \in ℂ$
188	68 186 187	addassi	$⊢ M + K + 1 = M + K + 1$
189	188	oveq2i	$⊢ M^{M + K + 1} = M^{M + K + 1}$
190	185 189	eqtr3i	$⊢ M^{M + K} \cdot M = M^{M + K + 1}$
191	190	oveq2i	$⊢ 2^{K^{2}} 2^{K} M^{M + K} \cdot M = 2^{K^{2}} 2^{K} M^{M + K + 1}$
192	95	recni	$⊢ 2^{K^{2}} \in ℂ$
193	141	recni	$⊢ M^{M + K} \in ℂ$
194	192 163 193 68	mul4i	$⊢ 2^{K^{2}} 2^{K} M^{M + K} \cdot M = 2^{K^{2}} M^{M + K} 2^{K} \cdot M$
195	191 194	eqtr3i	$⊢ 2^{K^{2}} 2^{K} M^{M + K + 1} = 2^{K^{2}} M^{M + K} 2^{K} \cdot M$
196		facnn2	$⊢ N \in ℕ \to N! = (N - 1)! \cdot N$
197	1 196	ax-mp	$⊢ N! = (N - 1)! \cdot N$
198	195 197	oveq12i	$⊢ 2^{K^{2}} 2^{K} M^{M + K + 1} N! = 2^{K^{2}} M^{M + K} 2^{K} \cdot M (N - 1)! \cdot N$
199	142	recni	$⊢ 2^{K^{2}} M^{M + K} \in ℂ$
200	144	nncni	$⊢ (N - 1)! \in ℂ$
201	163 68	mulcli	$⊢ 2^{K} \cdot M \in ℂ$
202	199 200 201 108	mul4i	$⊢ 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot M \cdot N = 2^{K^{2}} M^{M + K} 2^{K} \cdot M (N - 1)! \cdot N$
203	198 202	eqtr4i	$⊢ 2^{K^{2}} 2^{K} M^{M + K + 1} N! = 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot M \cdot N$
204	98	recni	$⊢ 2^{K^{2}} 2^{K} \in ℂ$
205	100	nncni	$⊢ N! \in ℂ$
206	204 78 205	mulassi	$⊢ 2^{K^{2}} 2^{K} M^{M + K + 1} N! = 2^{K^{2}} 2^{K} M^{M + K + 1} N!$
207	183 203 206	3eqtr2i	$⊢ 2^{K^{2}} M^{M + K} (N - 1)! 2^{K} \cdot N \cdot M = 2^{K^{2}} 2^{K} M^{M + K + 1} N!$
208	181 207	breqtrdi	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K} N M^{N - 1} \cdot M \leq 2^{K^{2}} 2^{K} M^{M + K + 1} N!$
209	124 208	eqbrtrid	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K + 1} M^{N} \leq 2^{K^{2}} 2^{K} M^{M + K + 1} N!$
210	102	nn0ge0i	$⊢ 0 \leq M^{M + K + 1} N!$
211	103 210	pm3.2i	$⊢ (M^{M + K + 1} N! \in ℝ \land 0 \leq M^{M + K + 1} N!)$
212	98 22 211	3pm3.2i	$⊢ (2^{K^{2}} 2^{K} \in ℝ \land 2^{{(K + 1)}^{2}} \in ℝ \land (M^{M + K + 1} N! \in ℝ \land 0 \leq M^{M + K + 1} N!))$
213		expadd	$⊢ (2 \in ℂ \land K^{2} \in ℕ_{0} \land K \in ℕ_{0}) \to 2^{K^{2} + K} = 2^{K^{2}} 2^{K}$
214	34 93 2 213	mp3an	$⊢ 2^{K^{2} + K} = 2^{K^{2}} 2^{K}$
215	20	nn0zi	$⊢ {(K + 1)}^{2} \in ℤ$
216	2	nn0rei	$⊢ K \in ℝ$
217	17	nnrei	$⊢ K + 1 \in ℝ$
218	18	nn0ge0i	$⊢ 0 \leq K + 1$
219	217 218	pm3.2i	$⊢ (K + 1 \in ℝ \land 0 \leq K + 1)$
220	216 217 219	3pm3.2i	$⊢ (K \in ℝ \land K + 1 \in ℝ \land (K + 1 \in ℝ \land 0 \leq K + 1))$
221	216	ltp1i	$⊢ K < K + 1$
222	216 217 221	ltleii	$⊢ K \leq K + 1$
223		lemul1a	$⊢ ((K \in ℝ \land K + 1 \in ℝ \land (K + 1 \in ℝ \land 0 \leq K + 1)) \land K \leq K + 1) \to K (K + 1) \leq (K + 1) (K + 1)$
224	220 222 223	mp2an	$⊢ K (K + 1) \leq (K + 1) (K + 1)$
225	186	sqvali	$⊢ K^{2} = K K$
226	186	mulid1i	$⊢ K \cdot 1 = K$
227	226	eqcomi	$⊢ K = K \cdot 1$
228	225 227	oveq12i	$⊢ K^{2} + K = K K + K \cdot 1$
229	186 186 187	adddii	$⊢ K (K + 1) = K K + K \cdot 1$
230	228 229	eqtr4i	$⊢ K^{2} + K = K (K + 1)$
231	17	nncni	$⊢ K + 1 \in ℂ$
232	231	sqvali	$⊢ {(K + 1)}^{2} = (K + 1) (K + 1)$
233	224 230 232	3brtr4i	$⊢ K^{2} + K \leq {(K + 1)}^{2}$
234	93 2	nn0addcli	$⊢ K^{2} + K \in ℕ_{0}$
235	234	nn0zi	$⊢ K^{2} + K \in ℤ$
236	235	eluz1i	$⊢ {(K + 1)}^{2} \in ℤ_{\geq (K^{2} + K)} \leftrightarrow ({(K + 1)}^{2} \in ℤ \land K^{2} + K \leq {(K + 1)}^{2})$
237	215 233 236	mpbir2an	$⊢ {(K + 1)}^{2} \in ℤ_{\geq (K^{2} + K)}$
238		leexp2a	$⊢ (2 \in ℝ \land 1 \leq 2 \land {(K + 1)}^{2} \in ℤ_{\geq (K^{2} + K)}) \to 2^{K^{2} + K} \leq 2^{{(K + 1)}^{2}}$
239	14 37 237 238	mp3an	$⊢ 2^{K^{2} + K} \leq 2^{{(K + 1)}^{2}}$
240	214 239	eqbrtrri	$⊢ 2^{K^{2}} 2^{K} \leq 2^{{(K + 1)}^{2}}$
241		lemul1a	$⊢ ((2^{K^{2}} 2^{K} \in ℝ \land 2^{{(K + 1)}^{2}} \in ℝ \land (M^{M + K + 1} N! \in ℝ \land 0 \leq M^{M + K + 1} N!)) \land 2^{K^{2}} 2^{K} \leq 2^{{(K + 1)}^{2}}) \to 2^{K^{2}} 2^{K} M^{M + K + 1} N! \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
242	212 240 241	mp2an	$⊢ 2^{K^{2}} 2^{K} M^{M + K + 1} N! \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
243	242	a1i	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to 2^{K^{2}} 2^{K} M^{M + K + 1} N! \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
244	92 105 107 209 243	letrd	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
245	77 78 205	mulassi	$⊢ 2^{{(K + 1)}^{2}} M^{M + K + 1} N! = 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
246	244 245	breqtrrdi	$⊢ (1 < N \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
247	85 246	jaoian	$⊢ ((N \leq 1 \lor 1 < N) \land {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)!) \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$
248	7 247	mpan	$⊢ {(N - 1)}^{K} M^{N - 1} \leq 2^{K^{2}} M^{M + K} (N - 1)! \to N^{K + 1} M^{N} \leq 2^{{(K + 1)}^{2}} M^{M + K + 1} N!$

Metamath Proof Explorer

Theorem faclbnd4lem1

Proof