MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  faclbnd4lem1 Structured version   Unicode version

Theorem faclbnd4lem1 12475
Description: Lemma for faclbnd4 12479. Prepare the induction step. (Contributed by NM, 20-Dec-2005.)
Hypotheses
Ref Expression
faclbnd4lem1.1  |-  N  e.  NN
faclbnd4lem1.2  |-  K  e. 
NN0
faclbnd4lem1.3  |-  M  e. 
NN0
Assertion
Ref Expression
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 of Theorem faclbnd4lem1
StepHypRef Expression
1 faclbnd4lem1.1 . . . 4  |-  N  e.  NN
21nnrei 10618 . . 3  |-  N  e.  RR
3 1re 9641 . . 3  |-  1  e.  RR
4 lelttric 9740 . . 3  |-  ( ( N  e.  RR  /\  1  e.  RR )  ->  ( N  <_  1  \/  1  <  N ) )
52, 3, 4mp2an 676 . 2  |-  ( N  <_  1  \/  1  <  N )
6 nnge1 10635 . . . . . . 7  |-  ( N  e.  NN  ->  1  <_  N )
71, 6ax-mp 5 . . . . . 6  |-  1  <_  N
82, 3letri3i 9749 . . . . . 6  |-  ( N  =  1  <->  ( N  <_  1  /\  1  <_  N ) )
97, 8mpbiran2 927 . . . . 5  |-  ( N  =  1  <->  N  <_  1 )
10 0le1 10136 . . . . . . . . . 10  |-  0  <_  1
113, 10pm3.2i 456 . . . . . . . . 9  |-  ( 1  e.  RR  /\  0  <_  1 )
12 2re 10679 . . . . . . . . . 10  |-  2  e.  RR
13 faclbnd4lem1.2 . . . . . . . . . . . . 13  |-  K  e. 
NN0
14 1nn 10620 . . . . . . . . . . . . 13  |-  1  e.  NN
15 nn0nnaddcl 10901 . . . . . . . . . . . . 13  |-  ( ( K  e.  NN0  /\  1  e.  NN )  ->  ( K  +  1 )  e.  NN )
1613, 14, 15mp2an 676 . . . . . . . . . . . 12  |-  ( K  +  1 )  e.  NN
1716nnnn0i 10877 . . . . . . . . . . 11  |-  ( K  +  1 )  e. 
NN0
18 2nn0 10886 . . . . . . . . . . 11  |-  2  e.  NN0
1917, 18nn0expcli 12295 . . . . . . . . . 10  |-  ( ( K  +  1 ) ^ 2 )  e. 
NN0
20 reexpcl 12286 . . . . . . . . . 10  |-  ( ( 2  e.  RR  /\  ( ( K  + 
1 ) ^ 2 )  e.  NN0 )  ->  ( 2 ^ (
( K  +  1 ) ^ 2 ) )  e.  RR )
2112, 19, 20mp2an 676 . . . . . . . . 9  |-  ( 2 ^ ( ( K  +  1 ) ^
2 ) )  e.  RR
2211, 21pm3.2i 456 . . . . . . . 8  |-  ( ( 1  e.  RR  /\  0  <_  1 )  /\  ( 2 ^ (
( K  +  1 ) ^ 2 ) )  e.  RR )
23 faclbnd4lem1.3 . . . . . . . . . . 11  |-  M  e. 
NN0
2423nn0rei 10880 . . . . . . . . . 10  |-  M  e.  RR
2523nn0ge0i 10897 . . . . . . . . . 10  |-  0  <_  M
2624, 25pm3.2i 456 . . . . . . . . 9  |-  ( M  e.  RR  /\  0  <_  M )
27 nn0nnaddcl 10901 . . . . . . . . . . . . 13  |-  ( ( M  e.  NN0  /\  ( K  +  1
)  e.  NN )  ->  ( M  +  ( K  +  1
) )  e.  NN )
2823, 16, 27mp2an 676 . . . . . . . . . . . 12  |-  ( M  +  ( K  + 
1 ) )  e.  NN
2928nnnn0i 10877 . . . . . . . . . . 11  |-  ( M  +  ( K  + 
1 ) )  e. 
NN0
3023, 29nn0expcli 12295 . . . . . . . . . 10  |-  ( M ^ ( M  +  ( K  +  1
) ) )  e. 
NN0
3130nn0rei 10880 . . . . . . . . 9  |-  ( M ^ ( M  +  ( K  +  1
) ) )  e.  RR
3226, 31pm3.2i 456 . . . . . . . 8  |-  ( ( M  e.  RR  /\  0  <_  M )  /\  ( M ^ ( M  +  ( K  + 
1 ) ) )  e.  RR )
3322, 32pm3.2i 456 . . . . . . 7  |-  ( ( ( 1  e.  RR  /\  0  <_  1 )  /\  ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  e.  RR )  /\  ( ( M  e.  RR  /\  0  <_  M )  /\  ( M ^ ( M  +  ( K  +  1
) ) )  e.  RR ) )
34 2cn 10680 . . . . . . . . . 10  |-  2  e.  CC
35 exp0 12273 . . . . . . . . . 10  |-  ( 2  e.  CC  ->  (
2 ^ 0 )  =  1 )
3634, 35ax-mp 5 . . . . . . . . 9  |-  ( 2 ^ 0 )  =  1
37 1le2 10823 . . . . . . . . . 10  |-  1  <_  2
38 nn0uz 11193 . . . . . . . . . . 11  |-  NN0  =  ( ZZ>= `  0 )
3919, 38eleqtri 2515 . . . . . . . . . 10  |-  ( ( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  0 )
40 leexp2a 12325 . . . . . . . . . 10  |-  ( ( 2  e.  RR  /\  1  <_  2  /\  (
( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  0
) )  ->  (
2 ^ 0 )  <_  ( 2 ^ ( ( K  + 
1 ) ^ 2 ) ) )
4112, 37, 39, 40mp3an 1360 . . . . . . . . 9  |-  ( 2 ^ 0 )  <_ 
( 2 ^ (
( K  +  1 ) ^ 2 ) )
4236, 41eqbrtrri 4447 . . . . . . . 8  |-  1  <_  ( 2 ^ (
( K  +  1 ) ^ 2 ) )
43 elnn0 10871 . . . . . . . . . 10  |-  ( M  e.  NN0  <->  ( M  e.  NN  \/  M  =  0 ) )
44 nncn 10617 . . . . . . . . . . . . 13  |-  ( M  e.  NN  ->  M  e.  CC )
4544exp1d 12408 . . . . . . . . . . . 12  |-  ( M  e.  NN  ->  ( M ^ 1 )  =  M )
46 nnge1 10635 . . . . . . . . . . . . 13  |-  ( M  e.  NN  ->  1  <_  M )
47 nnuz 11194 . . . . . . . . . . . . . . 15  |-  NN  =  ( ZZ>= `  1 )
4828, 47eleqtri 2515 . . . . . . . . . . . . . 14  |-  ( M  +  ( K  + 
1 ) )  e.  ( ZZ>= `  1 )
49 leexp2a 12325 . . . . . . . . . . . . . 14  |-  ( ( M  e.  RR  /\  1  <_  M  /\  ( M  +  ( K  +  1 ) )  e.  ( ZZ>= `  1
) )  ->  ( M ^ 1 )  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5024, 48, 49mp3an13 1351 . . . . . . . . . . . . 13  |-  ( 1  <_  M  ->  ( M ^ 1 )  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5146, 50syl 17 . . . . . . . . . . . 12  |-  ( M  e.  NN  ->  ( M ^ 1 )  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5245, 51eqbrtrrd 4448 . . . . . . . . . . 11  |-  ( M  e.  NN  ->  M  <_  ( M ^ ( M  +  ( K  +  1 ) ) ) )
5330nn0ge0i 10897 . . . . . . . . . . . 12  |-  0  <_  ( M ^ ( M  +  ( K  +  1 ) ) )
54 breq1 4429 . . . . . . . . . . . 12  |-  ( M  =  0  ->  ( M  <_  ( M ^
( M  +  ( K  +  1 ) ) )  <->  0  <_  ( M ^ ( M  +  ( K  + 
1 ) ) ) ) )
5553, 54mpbiri 236 . . . . . . . . . . 11  |-  ( M  =  0  ->  M  <_  ( M ^ ( M  +  ( K  +  1 ) ) ) )
5652, 55jaoi 380 . . . . . . . . . 10  |-  ( ( M  e.  NN  \/  M  =  0 )  ->  M  <_  ( M ^ ( M  +  ( K  +  1
) ) ) )
5743, 56sylbi 198 . . . . . . . . 9  |-  ( M  e.  NN0  ->  M  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5823, 57ax-mp 5 . . . . . . . 8  |-  M  <_ 
( M ^ ( M  +  ( K  +  1 ) ) )
5942, 58pm3.2i 456 . . . . . . 7  |-  ( 1  <_  ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  /\  M  <_  ( M ^ ( M  +  ( K  +  1 ) ) ) )
60 lemul12a 10462 . . . . . . 7  |-  ( ( ( ( 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 ) ) ) ) ) )
6133, 59, 60mp2 9 . . . . . 6  |-  ( 1  x.  M )  <_ 
( ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )
62 oveq1 6312 . . . . . . . . 9  |-  ( N  =  1  ->  ( N ^ ( K  + 
1 ) )  =  ( 1 ^ ( K  +  1 ) ) )
6316nnzi 10961 . . . . . . . . . 10  |-  ( K  +  1 )  e.  ZZ
64 1exp 12298 . . . . . . . . . 10  |-  ( ( K  +  1 )  e.  ZZ  ->  (
1 ^ ( K  +  1 ) )  =  1 )
6563, 64ax-mp 5 . . . . . . . . 9  |-  ( 1 ^ ( K  + 
1 ) )  =  1
6662, 65syl6eq 2486 . . . . . . . 8  |-  ( N  =  1  ->  ( N ^ ( K  + 
1 ) )  =  1 )
67 oveq2 6313 . . . . . . . . 9  |-  ( N  =  1  ->  ( M ^ N )  =  ( M ^ 1 ) )
6823nn0cni 10881 . . . . . . . . . 10  |-  M  e.  CC
69 exp1 12275 . . . . . . . . . 10  |-  ( M  e.  CC  ->  ( M ^ 1 )  =  M )
7068, 69ax-mp 5 . . . . . . . . 9  |-  ( M ^ 1 )  =  M
7167, 70syl6eq 2486 . . . . . . . 8  |-  ( N  =  1  ->  ( M ^ N )  =  M )
7266, 71oveq12d 6323 . . . . . . 7  |-  ( N  =  1  ->  (
( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  =  ( 1  x.  M ) )
73 fveq2 5881 . . . . . . . . . 10  |-  ( N  =  1  ->  ( ! `  N )  =  ( ! ` 
1 ) )
74 fac1 12460 . . . . . . . . . 10  |-  ( ! `
 1 )  =  1
7573, 74syl6eq 2486 . . . . . . . . 9  |-  ( N  =  1  ->  ( ! `  N )  =  1 )
7675oveq2d 6321 . . . . . . . 8  |-  ( N  =  1  ->  (
( ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )  x.  ( ! `  N ) )  =  ( ( ( 2 ^ ( ( K  +  1 ) ^
2 ) )  x.  ( M ^ ( M  +  ( K  +  1 ) ) ) )  x.  1 ) )
7721recni 9654 . . . . . . . . . 10  |-  ( 2 ^ ( ( K  +  1 ) ^
2 ) )  e.  CC
7830nn0cni 10881 . . . . . . . . . 10  |-  ( M ^ ( M  +  ( K  +  1
) ) )  e.  CC
7977, 78mulcli 9647 . . . . . . . . 9  |-  ( ( 2 ^ ( ( K  +  1 ) ^ 2 ) )  x.  ( M ^
( M  +  ( K  +  1 ) ) ) )  e.  CC
8079mulid1i 9644 . . . . . . . 8  |-  ( ( ( 2 ^ (
( K  +  1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )  x.  1 )  =  ( ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )
8176, 80syl6eq 2486 . . . . . . 7  |-  ( N  =  1  ->  (
( ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )  x.  ( ! `  N ) )  =  ( ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) ) )
8272, 81breq12d 4439 . . . . . 6  |-  ( 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
) ) ) ) ) )
8361, 82mpbiri 236 . . . . 5  |-  ( N  =  1  ->  (
( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  <_  ( ( ( 2 ^ ( ( K  +  1 ) ^ 2 ) )  x.  ( M ^
( M  +  ( K  +  1 ) ) ) )  x.  ( ! `  N
) ) )
849, 83sylbir 216 . . . 4  |-  ( N  <_  1  ->  (
( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  <_  ( ( ( 2 ^ ( ( K  +  1 ) ^ 2 ) )  x.  ( M ^
( M  +  ( K  +  1 ) ) ) )  x.  ( ! `  N
) ) )
8584adantr 466 . . 3  |-  ( ( 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 12286 . . . . . . . 8  |-  ( ( N  e.  RR  /\  ( K  +  1
)  e.  NN0 )  ->  ( N ^ ( K  +  1 ) )  e.  RR )
872, 17, 86mp2an 676 . . . . . . 7  |-  ( N ^ ( K  + 
1 ) )  e.  RR
881nnnn0i 10877 . . . . . . . 8  |-  N  e. 
NN0
89 reexpcl 12286 . . . . . . . 8  |-  ( ( M  e.  RR  /\  N  e.  NN0 )  -> 
( M ^ N
)  e.  RR )
9024, 88, 89mp2an 676 . . . . . . 7  |-  ( M ^ N )  e.  RR
9187, 90remulcli 9656 . . . . . 6  |-  ( ( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  e.  RR
9291a1i 11 . . . . 5  |-  ( ( 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 )
9313, 18nn0expcli 12295 . . . . . . . . 9  |-  ( K ^ 2 )  e. 
NN0
94 reexpcl 12286 . . . . . . . . 9  |-  ( ( 2  e.  RR  /\  ( K ^ 2 )  e.  NN0 )  -> 
( 2 ^ ( K ^ 2 ) )  e.  RR )
9512, 93, 94mp2an 676 . . . . . . . 8  |-  ( 2 ^ ( K ^
2 ) )  e.  RR
9618, 13nn0expcli 12295 . . . . . . . . 9  |-  ( 2 ^ K )  e. 
NN0
9796nn0rei 10880 . . . . . . . 8  |-  ( 2 ^ K )  e.  RR
9895, 97remulcli 9656 . . . . . . 7  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  e.  RR
99 faccl 12466 . . . . . . . . . . 11  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
10088, 99ax-mp 5 . . . . . . . . . 10  |-  ( ! `
 N )  e.  NN
101100nnnn0i 10877 . . . . . . . . 9  |-  ( ! `
 N )  e. 
NN0
10230, 101nn0mulcli 10908 . . . . . . . 8  |-  ( ( M ^ ( M  +  ( K  + 
1 ) ) )  x.  ( ! `  N ) )  e. 
NN0
103102nn0rei 10880 . . . . . . 7  |-  ( ( M ^ ( M  +  ( K  + 
1 ) ) )  x.  ( ! `  N ) )  e.  RR
10498, 103remulcli 9656 . . . . . 6  |-  ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  x.  ( ( M ^
( M  +  ( K  +  1 ) ) )  x.  ( ! `  N )
) )  e.  RR
105104a1i 11 . . . . 5  |-  ( ( 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 )
10621, 103remulcli 9656 . . . . . 6  |-  ( ( 2 ^ ( ( K  +  1 ) ^ 2 ) )  x.  ( ( M ^ ( M  +  ( K  +  1
) ) )  x.  ( ! `  N
) ) )  e.  RR
107106a1i 11 . . . . 5  |-  ( ( 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 )
1081nncni 10619 . . . . . . . . 9  |-  N  e.  CC
109 expp1 12276 . . . . . . . . 9  |-  ( ( N  e.  CC  /\  K  e.  NN0 )  -> 
( N ^ ( K  +  1 ) )  =  ( ( N ^ K )  x.  N ) )
110108, 13, 109mp2an 676 . . . . . . . 8  |-  ( N ^ ( K  + 
1 ) )  =  ( ( N ^ K )  x.  N
)
111 expm1t 12297 . . . . . . . . 9  |-  ( ( M  e.  CC  /\  N  e.  NN )  ->  ( M ^ N
)  =  ( ( M ^ ( N  -  1 ) )  x.  M ) )
11268, 1, 111mp2an 676 . . . . . . . 8  |-  ( M ^ N )  =  ( ( M ^
( N  -  1 ) )  x.  M
)
113110, 112oveq12i 6317 . . . . . . 7  |-  ( ( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  =  ( ( ( N ^ K )  x.  N )  x.  (
( M ^ ( N  -  1 ) )  x.  M ) )
114 reexpcl 12286 . . . . . . . . . 10  |-  ( ( N  e.  RR  /\  K  e.  NN0 )  -> 
( N ^ K
)  e.  RR )
1152, 13, 114mp2an 676 . . . . . . . . 9  |-  ( N ^ K )  e.  RR
116115recni 9654 . . . . . . . 8  |-  ( N ^ K )  e.  CC
117 elnnnn0 10913 . . . . . . . . . . . . 13  |-  ( N  e.  NN  <->  ( N  e.  CC  /\  ( N  -  1 )  e. 
NN0 ) )
1181, 117mpbi 211 . . . . . . . . . . . 12  |-  ( N  e.  CC  /\  ( N  -  1 )  e.  NN0 )
119118simpri 463 . . . . . . . . . . 11  |-  ( N  -  1 )  e. 
NN0
12023, 119nn0expcli 12295 . . . . . . . . . 10  |-  ( M ^ ( N  - 
1 ) )  e. 
NN0
121120, 23nn0mulcli 10908 . . . . . . . . 9  |-  ( ( M ^ ( N  -  1 ) )  x.  M )  e. 
NN0
122121nn0cni 10881 . . . . . . . 8  |-  ( ( M ^ ( N  -  1 ) )  x.  M )  e.  CC
123116, 108, 122mulassi 9651 . . . . . . 7  |-  ( ( ( N ^ K
)  x.  N )  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) )  =  ( ( N ^ K )  x.  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) ) )
124113, 123eqtri 2458 . . . . . 6  |-  ( ( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  =  ( ( N ^ K )  x.  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) ) )
12588, 121nn0mulcli 10908 . . . . . . . . . . 11  |-  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) )  e. 
NN0
126125nn0rei 10880 . . . . . . . . . 10  |-  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) )  e.  RR
127115, 126remulcli 9656 . . . . . . . . 9  |-  ( ( N ^ K )  x.  ( N  x.  ( ( M ^
( N  -  1 ) )  x.  M
) ) )  e.  RR
128127a1i 11 . . . . . . . 8  |-  ( ( 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 )
129119nn0rei 10880 . . . . . . . . . . . 12  |-  ( N  -  1 )  e.  RR
130 reexpcl 12286 . . . . . . . . . . . 12  |-  ( ( ( N  -  1 )  e.  RR  /\  K  e.  NN0 )  -> 
( ( N  - 
1 ) ^ K
)  e.  RR )
131129, 13, 130mp2an 676 . . . . . . . . . . 11  |-  ( ( N  -  1 ) ^ K )  e.  RR
132120nn0rei 10880 . . . . . . . . . . 11  |-  ( M ^ ( N  - 
1 ) )  e.  RR
133131, 132remulcli 9656 . . . . . . . . . 10  |-  ( ( ( N  -  1 ) ^ K )  x.  ( M ^
( N  -  1 ) ) )  e.  RR
13496, 88nn0mulcli 10908 . . . . . . . . . . . 12  |-  ( ( 2 ^ K )  x.  N )  e. 
NN0
135134, 23nn0mulcli 10908 . . . . . . . . . . 11  |-  ( ( ( 2 ^ K
)  x.  N )  x.  M )  e. 
NN0
136135nn0rei 10880 . . . . . . . . . 10  |-  ( ( ( 2 ^ K
)  x.  N )  x.  M )  e.  RR
137133, 136remulcli 9656 . . . . . . . . 9  |-  ( ( ( ( N  - 
1 ) ^ K
)  x.  ( M ^ ( N  - 
1 ) ) )  x.  ( ( ( 2 ^ K )  x.  N )  x.  M ) )  e.  RR
138137a1i 11 . . . . . . . 8  |-  ( ( 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 )
13923, 13nn0addcli 10907 . . . . . . . . . . . . 13  |-  ( M  +  K )  e. 
NN0
140 reexpcl 12286 . . . . . . . . . . . . 13  |-  ( ( M  e.  RR  /\  ( M  +  K
)  e.  NN0 )  ->  ( M ^ ( M  +  K )
)  e.  RR )
14124, 139, 140mp2an 676 . . . . . . . . . . . 12  |-  ( M ^ ( M  +  K ) )  e.  RR
14295, 141remulcli 9656 . . . . . . . . . . 11  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^
( M  +  K
) ) )  e.  RR
143 faccl 12466 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  NN0  ->  ( ! `
 ( N  - 
1 ) )  e.  NN )
144119, 143ax-mp 5 . . . . . . . . . . . 12  |-  ( ! `
 ( N  - 
1 ) )  e.  NN
145144nnrei 10618 . . . . . . . . . . 11  |-  ( ! `
 ( N  - 
1 ) )  e.  RR
146142, 145remulcli 9656 . . . . . . . . . 10  |-  ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^
( M  +  K
) ) )  x.  ( ! `  ( N  -  1 ) ) )  e.  RR
147146, 136remulcli 9656 . . . . . . . . 9  |-  ( ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^ ( M  +  K ) ) )  x.  ( ! `  ( N  -  1
) ) )  x.  ( ( ( 2 ^ K )  x.  N )  x.  M
) )  e.  RR
148147a1i 11 . . . . . . . 8  |-  ( ( 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 )
14997, 131remulcli 9656 . . . . . . . . . . . 12  |-  ( ( 2 ^ K )  x.  ( ( N  -  1 ) ^ K ) )  e.  RR
150125nn0ge0i 10897 . . . . . . . . . . . . 13  |-  0  <_  ( N  x.  (
( M ^ ( N  -  1 ) )  x.  M ) )
151126, 150pm3.2i 456 . . . . . . . . . . . 12  |-  ( ( N  x.  ( ( M ^ ( N  -  1 ) )  x.  M ) )  e.  RR  /\  0  <_  ( N  x.  (
( M ^ ( N  -  1 ) )  x.  M ) ) )
152115, 149, 1513pm3.2i 1183 . . . . . . . . . . 11  |-  ( ( 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 10992 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  NN  /\  N  e.  NN )  ->  ( 1  <  N  <->  ( 1  +  1 )  <_  N ) )
15414, 1, 153mp2an 676 . . . . . . . . . . . . 13  |-  ( 1  <  N  <->  ( 1  +  1 )  <_  N )
155 df-2 10668 . . . . . . . . . . . . . 14  |-  2  =  ( 1  +  1 )
156155breq1i 4433 . . . . . . . . . . . . 13  |-  ( 2  <_  N  <->  ( 1  +  1 )  <_  N )
157154, 156bitr4i 255 . . . . . . . . . . . 12  |-  ( 1  <  N  <->  2  <_  N )
158 expubnd 12330 . . . . . . . . . . . . 13  |-  ( ( N  e.  RR  /\  K  e.  NN0  /\  2  <_  N )  ->  ( N ^ K )  <_ 
( ( 2 ^ K )  x.  (
( N  -  1 ) ^ K ) ) )
1592, 13, 158mp3an12 1350 . . . . . . . . . . . 12  |-  ( 2  <_  N  ->  ( N ^ K )  <_ 
( ( 2 ^ K )  x.  (
( N  -  1 ) ^ K ) ) )
160157, 159sylbi 198 . . . . . . . . . . 11  |-  ( 1  <  N  ->  ( N ^ K )  <_ 
( ( 2 ^ K )  x.  (
( N  -  1 ) ^ K ) ) )
161 lemul1a 10458 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) ) )
162152, 160, 161sylancr 667 . . . . . . . . . 10  |-  ( 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 ) ) ) )
16396nn0cni 10881 . . . . . . . . . . . 12  |-  ( 2 ^ K )  e.  CC
164131recni 9654 . . . . . . . . . . . 12  |-  ( ( N  -  1 ) ^ K )  e.  CC
165163, 164, 108, 122mul4i 9829 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
166120nn0cni 10881 . . . . . . . . . . . . 13  |-  ( M ^ ( N  - 
1 ) )  e.  CC
167164, 166, 68mulassi 9651 . . . . . . . . . . . 12  |-  ( ( ( ( N  - 
1 ) ^ K
)  x.  ( M ^ ( N  - 
1 ) ) )  x.  M )  =  ( ( ( N  -  1 ) ^ K )  x.  (
( M ^ ( N  -  1 ) )  x.  M ) )
168167oveq2i 6316 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
169134nn0cni 10881 . . . . . . . . . . . 12  |-  ( ( 2 ^ K )  x.  N )  e.  CC
170133recni 9654 . . . . . . . . . . . 12  |-  ( ( ( N  -  1 ) ^ K )  x.  ( M ^
( N  -  1 ) ) )  e.  CC
171169, 170, 68mul12i 9827 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
172165, 168, 1713eqtr2i 2464 . . . . . . . . . 10  |-  ( ( ( 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 ) )
173162, 172syl6breq 4465 . . . . . . . . 9  |-  ( 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
) ) )
174173adantr 466 . . . . . . . 8  |-  ( ( 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
) ) )
175135nn0ge0i 10897 . . . . . . . . . . . 12  |-  0  <_  ( ( ( 2 ^ K )  x.  N )  x.  M
)
176136, 175pm3.2i 456 . . . . . . . . . . 11  |-  ( ( ( ( 2 ^ K )  x.  N
)  x.  M )  e.  RR  /\  0  <_  ( ( ( 2 ^ K )  x.  N )  x.  M
) )
177133, 146, 1763pm3.2i 1183 . . . . . . . . . 10  |-  ( ( ( ( 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 10458 . . . . . . . . . 10  |-  ( ( ( ( ( ( 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 ) ) )
179177, 178mpan 674 . . . . . . . . 9  |-  ( ( ( ( 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 ) ) )
180179adantl 467 . . . . . . . 8  |-  ( ( 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
) ) )
181128, 138, 148, 174, 180letrd 9791 . . . . . . 7  |-  ( ( 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 ) ) )
182163, 108, 68mul32i 9828 . . . . . . . . 9  |-  ( ( ( 2 ^ K
)  x.  N )  x.  M )  =  ( ( ( 2 ^ K )  x.  M )  x.  N
)
183182oveq2i 6316 . . . . . . . 8  |-  ( ( ( ( 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 12276 . . . . . . . . . . . . . 14  |-  ( ( M  e.  CC  /\  ( M  +  K
)  e.  NN0 )  ->  ( M ^ (
( M  +  K
)  +  1 ) )  =  ( ( M ^ ( M  +  K ) )  x.  M ) )
18568, 139, 184mp2an 676 . . . . . . . . . . . . 13  |-  ( M ^ ( ( M  +  K )  +  1 ) )  =  ( ( M ^
( M  +  K
) )  x.  M
)
18613nn0cni 10881 . . . . . . . . . . . . . . 15  |-  K  e.  CC
187 ax-1cn 9596 . . . . . . . . . . . . . . 15  |-  1  e.  CC
18868, 186, 187addassi 9650 . . . . . . . . . . . . . 14  |-  ( ( M  +  K )  +  1 )  =  ( M  +  ( K  +  1 ) )
189188oveq2i 6316 . . . . . . . . . . . . 13  |-  ( M ^ ( ( M  +  K )  +  1 ) )  =  ( M ^ ( M  +  ( K  +  1 ) ) )
190185, 189eqtr3i 2460 . . . . . . . . . . . 12  |-  ( ( M ^ ( M  +  K ) )  x.  M )  =  ( M ^ ( M  +  ( K  +  1 ) ) )
191190oveq2i 6316 . . . . . . . . . . 11  |-  ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  x.  ( ( M ^
( M  +  K
) )  x.  M
) )  =  ( ( ( 2 ^ ( K ^ 2 ) )  x.  (
2 ^ K ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )
19295recni 9654 . . . . . . . . . . . 12  |-  ( 2 ^ ( K ^
2 ) )  e.  CC
193141recni 9654 . . . . . . . . . . . 12  |-  ( M ^ ( M  +  K ) )  e.  CC
194192, 163, 193, 68mul4i 9829 . . . . . . . . . . 11  |-  ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  x.  ( ( M ^
( M  +  K
) )  x.  M
) )  =  ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^ ( M  +  K ) ) )  x.  ( ( 2 ^ K )  x.  M ) )
195191, 194eqtr3i 2460 . . . . . . . . . 10  |-  ( ( ( 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 12465 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( ! `  N )  =  ( ( ! `
 ( N  - 
1 ) )  x.  N ) )
1971, 196ax-mp 5 . . . . . . . . . 10  |-  ( ! `
 N )  =  ( ( ! `  ( N  -  1
) )  x.  N
)
198195, 197oveq12i 6317 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
199142recni 9654 . . . . . . . . . 10  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^
( M  +  K
) ) )  e.  CC
200144nncni 10619 . . . . . . . . . 10  |-  ( ! `
 ( N  - 
1 ) )  e.  CC
201163, 68mulcli 9647 . . . . . . . . . 10  |-  ( ( 2 ^ K )  x.  M )  e.  CC
202199, 200, 201, 108mul4i 9829 . . . . . . . . 9  |-  ( ( ( ( 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 ) )
203198, 202eqtr4i 2461 . . . . . . . 8  |-  ( ( ( ( 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 ) )
20498recni 9654 . . . . . . . . 9  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  e.  CC
205100nncni 10619 . . . . . . . . 9  |-  ( ! `
 N )  e.  CC
206204, 78, 205mulassi 9651 . . . . . . . 8  |-  ( ( ( ( 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 ) ) )
207183, 203, 2063eqtr2i 2464 . . . . . . 7  |-  ( ( ( ( 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 ) ) )
208181, 207syl6breq 4465 . . . . . 6  |-  ( ( 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 )
) ) )
209124, 208syl5eqbr 4459 . . . . 5  |-  ( ( 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 )
) ) )
210102nn0ge0i 10897 . . . . . . . . 9  |-  0  <_  ( ( M ^
( M  +  ( K  +  1 ) ) )  x.  ( ! `  N )
)
211103, 210pm3.2i 456 . . . . . . . 8  |-  ( ( ( M ^ ( M  +  ( K  +  1 ) ) )  x.  ( ! `
 N ) )  e.  RR  /\  0  <_  ( ( M ^
( M  +  ( K  +  1 ) ) )  x.  ( ! `  N )
) )
21298, 21, 2113pm3.2i 1183 . . . . . . 7  |-  ( ( ( 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 12311 . . . . . . . . 9  |-  ( ( 2  e.  CC  /\  ( K ^ 2 )  e.  NN0  /\  K  e. 
NN0 )  ->  (
2 ^ ( ( K ^ 2 )  +  K ) )  =  ( ( 2 ^ ( K ^
2 ) )  x.  ( 2 ^ K
) ) )
21434, 93, 13, 213mp3an 1360 . . . . . . . 8  |-  ( 2 ^ ( ( K ^ 2 )  +  K ) )  =  ( ( 2 ^ ( K ^ 2 ) )  x.  (
2 ^ K ) )
21519nn0zi 10962 . . . . . . . . . 10  |-  ( ( K  +  1 ) ^ 2 )  e.  ZZ
21613nn0rei 10880 . . . . . . . . . . . . 13  |-  K  e.  RR
21716nnrei 10618 . . . . . . . . . . . . 13  |-  ( K  +  1 )  e.  RR
21817nn0ge0i 10897 . . . . . . . . . . . . . 14  |-  0  <_  ( K  +  1 )
219217, 218pm3.2i 456 . . . . . . . . . . . . 13  |-  ( ( K  +  1 )  e.  RR  /\  0  <_  ( K  +  1 ) )
220216, 217, 2193pm3.2i 1183 . . . . . . . . . . . 12  |-  ( K  e.  RR  /\  ( K  +  1 )  e.  RR  /\  (
( K  +  1 )  e.  RR  /\  0  <_  ( K  + 
1 ) ) )
221216ltp1i 10510 . . . . . . . . . . . . 13  |-  K  < 
( K  +  1 )
222216, 217, 221ltleii 9756 . . . . . . . . . . . 12  |-  K  <_ 
( K  +  1 )
223 lemul1a 10458 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
224220, 222, 223mp2an 676 . . . . . . . . . . 11  |-  ( K  x.  ( K  + 
1 ) )  <_ 
( ( K  + 
1 )  x.  ( K  +  1 ) )
225186sqvali 12351 . . . . . . . . . . . . 13  |-  ( K ^ 2 )  =  ( K  x.  K
)
226186mulid1i 9644 . . . . . . . . . . . . . 14  |-  ( K  x.  1 )  =  K
227226eqcomi 2442 . . . . . . . . . . . . 13  |-  K  =  ( K  x.  1 )
228225, 227oveq12i 6317 . . . . . . . . . . . 12  |-  ( ( K ^ 2 )  +  K )  =  ( ( K  x.  K )  +  ( K  x.  1 ) )
229186, 186, 187adddii 9652 . . . . . . . . . . . 12  |-  ( K  x.  ( K  + 
1 ) )  =  ( ( K  x.  K )  +  ( K  x.  1 ) )
230228, 229eqtr4i 2461 . . . . . . . . . . 11  |-  ( ( K ^ 2 )  +  K )  =  ( K  x.  ( K  +  1 ) )
23116nncni 10619 . . . . . . . . . . . 12  |-  ( K  +  1 )  e.  CC
232231sqvali 12351 . . . . . . . . . . 11  |-  ( ( K  +  1 ) ^ 2 )  =  ( ( K  + 
1 )  x.  ( K  +  1 ) )
233224, 230, 2323brtr4i 4454 . . . . . . . . . 10  |-  ( ( K ^ 2 )  +  K )  <_ 
( ( K  + 
1 ) ^ 2 )
23493, 13nn0addcli 10907 . . . . . . . . . . . 12  |-  ( ( K ^ 2 )  +  K )  e. 
NN0
235234nn0zi 10962 . . . . . . . . . . 11  |-  ( ( K ^ 2 )  +  K )  e.  ZZ
236235eluz1i 11166 . . . . . . . . . 10  |-  ( ( ( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  (
( K ^ 2 )  +  K ) )  <->  ( ( ( K  +  1 ) ^ 2 )  e.  ZZ  /\  ( ( K ^ 2 )  +  K )  <_ 
( ( K  + 
1 ) ^ 2 ) ) )
237215, 233, 236mpbir2an 928 . . . . . . . . 9  |-  ( ( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  ( ( K ^ 2 )  +  K ) )
238 leexp2a 12325 . . . . . . . . 9  |-  ( ( 2  e.  RR  /\  1  <_  2  /\  (
( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  (
( K ^ 2 )  +  K ) ) )  ->  (
2 ^ ( ( K ^ 2 )  +  K ) )  <_  ( 2 ^ ( ( K  + 
1 ) ^ 2 ) ) )
23912, 37, 237, 238mp3an 1360 . . . . . . . 8  |-  ( 2 ^ ( ( K ^ 2 )  +  K ) )  <_ 
( 2 ^ (
( K  +  1 ) ^ 2 ) )
240214, 239eqbrtrri 4447 . . . . . . 7  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  <_ 
( 2 ^ (
( K  +  1 ) ^ 2 ) )
241 lemul1a 10458 . . . . . . 7  |-  ( ( ( ( ( 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 ) ) ) )
242212, 240, 241mp2an 676 . . . . . 6  |-  ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  x.  ( ( M ^
( M  +  ( K  +  1 ) ) )  x.  ( ! `  N )
) )  <_  (
( 2 ^ (
( K  +  1 ) ^ 2 ) )  x.  ( ( M ^ ( M  +  ( K  + 
1 ) ) )  x.  ( ! `  N ) ) )
243242a1i 11 . . . . 5  |-  ( ( 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
) ) ) )
24492, 105, 107, 209, 243letrd 9791 . . . 4  |-  ( ( 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 )
) ) )
24577, 78, 205mulassi 9651 . . . 4  |-  ( ( ( 2 ^ (
( K  +  1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )  x.  ( ! `  N ) )  =  ( ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  x.  (
( M ^ ( M  +  ( K  +  1 ) ) )  x.  ( ! `
 N ) ) )
246244, 245syl6breqr 4466 . . 3  |-  ( ( 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
) ) )
24785, 246jaoian 791 . 2  |-  ( ( ( 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 ) ) )
2485, 247mpan 674 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
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437    e. wcel 1870   class class class wbr 4426   ` cfv 5601  (class class class)co 6305   CCcc 9536   RRcr 9537   0cc0 9538   1c1 9539    + caddc 9541    x. cmul 9543    < clt 9674    <_ cle 9675    - cmin 9859   NNcn 10609   2c2 10659   NN0cn0 10869   ZZcz 10937   ZZ>=cuz 11159   ^cexp 12269   !cfa 12456
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-er 7371  df-en 7578  df-dom 7579  df-sdom 7580  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-n0 10870  df-z 10938  df-uz 11160  df-rp 11303  df-seq 12211  df-exp 12270  df-fac 12457
This theorem is referenced by:  faclbnd4lem2  12476
  Copyright terms: Public domain W3C validator