faclbnd4lem1

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

	Ref	Expression
Hypotheses	faclbnd4lem1.1	\|- N e. NN
	faclbnd4lem1.2	\|- K e. NN0
	faclbnd4lem1.3	\|- M e. NN0
Assertion	faclbnd4lem1	\|- ( ( ( ( N - 1 ) ^ K ) x. ( M ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` ( N - 1 ) ) ) -> ( ( N ^ ( K + 1 ) ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( K + 1 ) ) ) ) x. ( ! ` N ) ) )

Proof

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

Metamath Proof Explorer

Theorem faclbnd4lem1

Proof