Metamath Proof Explorer

Theorem 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 mulid1i 
 |-  ( ( ( 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 mulid1i 
 |-  ( 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 ) ) )