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

Theorem faclbnd4lem1 12065
Description: Lemma for faclbnd4 12069. 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 10327 . . 3  |-  N  e.  RR
3 1re 9381 . . 3  |-  1  e.  RR
4 lelttric 9477 . . 3  |-  ( ( N  e.  RR  /\  1  e.  RR )  ->  ( N  <_  1  \/  1  <  N ) )
52, 3, 4mp2an 667 . 2  |-  ( N  <_  1  \/  1  <  N )
6 nnge1 10344 . . . . . . 7  |-  ( N  e.  NN  ->  1  <_  N )
71, 6ax-mp 5 . . . . . 6  |-  1  <_  N
82, 3letri3i 9486 . . . . . 6  |-  ( N  =  1  <->  ( N  <_  1  /\  1  <_  N ) )
97, 8mpbiran2 905 . . . . 5  |-  ( N  =  1  <->  N  <_  1 )
10 0le1 9859 . . . . . . . . . 10  |-  0  <_  1
113, 10pm3.2i 452 . . . . . . . . 9  |-  ( 1  e.  RR  /\  0  <_  1 )
12 2re 10387 . . . . . . . . . 10  |-  2  e.  RR
13 faclbnd4lem1.2 . . . . . . . . . . . . 13  |-  K  e. 
NN0
14 1nn 10329 . . . . . . . . . . . . 13  |-  1  e.  NN
15 nn0nnaddcl 10607 . . . . . . . . . . . . 13  |-  ( ( K  e.  NN0  /\  1  e.  NN )  ->  ( K  +  1 )  e.  NN )
1613, 14, 15mp2an 667 . . . . . . . . . . . 12  |-  ( K  +  1 )  e.  NN
1716nnnn0i 10583 . . . . . . . . . . 11  |-  ( K  +  1 )  e. 
NN0
18 2nn0 10592 . . . . . . . . . . 11  |-  2  e.  NN0
1917, 18nn0expcli 11887 . . . . . . . . . 10  |-  ( ( K  +  1 ) ^ 2 )  e. 
NN0
20 reexpcl 11878 . . . . . . . . . 10  |-  ( ( 2  e.  RR  /\  ( ( K  + 
1 ) ^ 2 )  e.  NN0 )  ->  ( 2 ^ (
( K  +  1 ) ^ 2 ) )  e.  RR )
2112, 19, 20mp2an 667 . . . . . . . . 9  |-  ( 2 ^ ( ( K  +  1 ) ^
2 ) )  e.  RR
2211, 21pm3.2i 452 . . . . . . . 8  |-  ( ( 1  e.  RR  /\  0  <_  1 )  /\  ( 2 ^ (
( K  +  1 ) ^ 2 ) )  e.  RR )
23 faclbnd4lem1.3 . . . . . . . . . . 11  |-  M  e. 
NN0
2423nn0rei 10586 . . . . . . . . . 10  |-  M  e.  RR
2523nn0ge0i 10603 . . . . . . . . . 10  |-  0  <_  M
2624, 25pm3.2i 452 . . . . . . . . 9  |-  ( M  e.  RR  /\  0  <_  M )
27 nn0nnaddcl 10607 . . . . . . . . . . . . 13  |-  ( ( M  e.  NN0  /\  ( K  +  1
)  e.  NN )  ->  ( M  +  ( K  +  1
) )  e.  NN )
2823, 16, 27mp2an 667 . . . . . . . . . . . 12  |-  ( M  +  ( K  + 
1 ) )  e.  NN
2928nnnn0i 10583 . . . . . . . . . . 11  |-  ( M  +  ( K  + 
1 ) )  e. 
NN0
3023, 29nn0expcli 11887 . . . . . . . . . 10  |-  ( M ^ ( M  +  ( K  +  1
) ) )  e. 
NN0
3130nn0rei 10586 . . . . . . . . 9  |-  ( M ^ ( M  +  ( K  +  1
) ) )  e.  RR
3226, 31pm3.2i 452 . . . . . . . 8  |-  ( ( M  e.  RR  /\  0  <_  M )  /\  ( M ^ ( M  +  ( K  + 
1 ) ) )  e.  RR )
3322, 32pm3.2i 452 . . . . . . 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 10388 . . . . . . . . . 10  |-  2  e.  CC
35 exp0 11865 . . . . . . . . . 10  |-  ( 2  e.  CC  ->  (
2 ^ 0 )  =  1 )
3634, 35ax-mp 5 . . . . . . . . 9  |-  ( 2 ^ 0 )  =  1
37 1le2 10531 . . . . . . . . . 10  |-  1  <_  2
38 nn0uz 10891 . . . . . . . . . . 11  |-  NN0  =  ( ZZ>= `  0 )
3919, 38eleqtri 2513 . . . . . . . . . 10  |-  ( ( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  0 )
40 leexp2a 11915 . . . . . . . . . 10  |-  ( ( 2  e.  RR  /\  1  <_  2  /\  (
( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  0
) )  ->  (
2 ^ 0 )  <_  ( 2 ^ ( ( K  + 
1 ) ^ 2 ) ) )
4112, 37, 39, 40mp3an 1309 . . . . . . . . 9  |-  ( 2 ^ 0 )  <_ 
( 2 ^ (
( K  +  1 ) ^ 2 ) )
4236, 41eqbrtrri 4310 . . . . . . . 8  |-  1  <_  ( 2 ^ (
( K  +  1 ) ^ 2 ) )
43 elnn0 10577 . . . . . . . . . 10  |-  ( M  e.  NN0  <->  ( M  e.  NN  \/  M  =  0 ) )
44 nncn 10326 . . . . . . . . . . . . 13  |-  ( M  e.  NN  ->  M  e.  CC )
4544exp1d 11999 . . . . . . . . . . . 12  |-  ( M  e.  NN  ->  ( M ^ 1 )  =  M )
46 nnge1 10344 . . . . . . . . . . . . 13  |-  ( M  e.  NN  ->  1  <_  M )
47 nnuz 10892 . . . . . . . . . . . . . . 15  |-  NN  =  ( ZZ>= `  1 )
4828, 47eleqtri 2513 . . . . . . . . . . . . . 14  |-  ( M  +  ( K  + 
1 ) )  e.  ( ZZ>= `  1 )
49 leexp2a 11915 . . . . . . . . . . . . . 14  |-  ( ( M  e.  RR  /\  1  <_  M  /\  ( M  +  ( K  +  1 ) )  e.  ( ZZ>= `  1
) )  ->  ( M ^ 1 )  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5024, 48, 49mp3an13 1300 . . . . . . . . . . . . 13  |-  ( 1  <_  M  ->  ( M ^ 1 )  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5146, 50syl 16 . . . . . . . . . . . 12  |-  ( M  e.  NN  ->  ( M ^ 1 )  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5245, 51eqbrtrrd 4311 . . . . . . . . . . 11  |-  ( M  e.  NN  ->  M  <_  ( M ^ ( M  +  ( K  +  1 ) ) ) )
5330nn0ge0i 10603 . . . . . . . . . . . 12  |-  0  <_  ( M ^ ( M  +  ( K  +  1 ) ) )
54 breq1 4292 . . . . . . . . . . . 12  |-  ( M  =  0  ->  ( M  <_  ( M ^
( M  +  ( K  +  1 ) ) )  <->  0  <_  ( M ^ ( M  +  ( K  + 
1 ) ) ) ) )
5553, 54mpbiri 233 . . . . . . . . . . 11  |-  ( M  =  0  ->  M  <_  ( M ^ ( M  +  ( K  +  1 ) ) ) )
5652, 55jaoi 379 . . . . . . . . . 10  |-  ( ( M  e.  NN  \/  M  =  0 )  ->  M  <_  ( M ^ ( M  +  ( K  +  1
) ) ) )
5743, 56sylbi 195 . . . . . . . . 9  |-  ( M  e.  NN0  ->  M  <_ 
( M ^ ( M  +  ( K  +  1 ) ) ) )
5823, 57ax-mp 5 . . . . . . . 8  |-  M  <_ 
( M ^ ( M  +  ( K  +  1 ) ) )
5942, 58pm3.2i 452 . . . . . . 7  |-  ( 1  <_  ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  /\  M  <_  ( M ^ ( M  +  ( K  +  1 ) ) ) )
60 lemul12a 10183 . . . . . . 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 6097 . . . . . . . . 9  |-  ( N  =  1  ->  ( N ^ ( K  + 
1 ) )  =  ( 1 ^ ( K  +  1 ) ) )
6316nnzi 10666 . . . . . . . . . 10  |-  ( K  +  1 )  e.  ZZ
64 1exp 11889 . . . . . . . . . 10  |-  ( ( K  +  1 )  e.  ZZ  ->  (
1 ^ ( K  +  1 ) )  =  1 )
6563, 64ax-mp 5 . . . . . . . . 9  |-  ( 1 ^ ( K  + 
1 ) )  =  1
6662, 65syl6eq 2489 . . . . . . . 8  |-  ( N  =  1  ->  ( N ^ ( K  + 
1 ) )  =  1 )
67 oveq2 6098 . . . . . . . . 9  |-  ( N  =  1  ->  ( M ^ N )  =  ( M ^ 1 ) )
6823nn0cni 10587 . . . . . . . . . 10  |-  M  e.  CC
69 exp1 11867 . . . . . . . . . 10  |-  ( M  e.  CC  ->  ( M ^ 1 )  =  M )
7068, 69ax-mp 5 . . . . . . . . 9  |-  ( M ^ 1 )  =  M
7167, 70syl6eq 2489 . . . . . . . 8  |-  ( N  =  1  ->  ( M ^ N )  =  M )
7266, 71oveq12d 6108 . . . . . . 7  |-  ( N  =  1  ->  (
( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  =  ( 1  x.  M ) )
73 fveq2 5688 . . . . . . . . . 10  |-  ( N  =  1  ->  ( ! `  N )  =  ( ! ` 
1 ) )
74 fac1 12051 . . . . . . . . . 10  |-  ( ! `
 1 )  =  1
7573, 74syl6eq 2489 . . . . . . . . 9  |-  ( N  =  1  ->  ( ! `  N )  =  1 )
7675oveq2d 6106 . . . . . . . 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 9394 . . . . . . . . . 10  |-  ( 2 ^ ( ( K  +  1 ) ^
2 ) )  e.  CC
7830nn0cni 10587 . . . . . . . . . 10  |-  ( M ^ ( M  +  ( K  +  1
) ) )  e.  CC
7977, 78mulcli 9387 . . . . . . . . 9  |-  ( ( 2 ^ ( ( K  +  1 ) ^ 2 ) )  x.  ( M ^
( M  +  ( K  +  1 ) ) ) )  e.  CC
8079mulid1i 9384 . . . . . . . 8  |-  ( ( ( 2 ^ (
( K  +  1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )  x.  1 )  =  ( ( 2 ^ ( ( K  + 
1 ) ^ 2 ) )  x.  ( M ^ ( M  +  ( K  +  1
) ) ) )
8176, 80syl6eq 2489 . . . . . . 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 4302 . . . . . 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 233 . . . . 5  |-  ( N  =  1  ->  (
( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  <_  ( ( ( 2 ^ ( ( K  +  1 ) ^ 2 ) )  x.  ( M ^
( M  +  ( K  +  1 ) ) ) )  x.  ( ! `  N
) ) )
849, 83sylbir 213 . . . 4  |-  ( N  <_  1  ->  (
( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  <_  ( ( ( 2 ^ ( ( K  +  1 ) ^ 2 ) )  x.  ( M ^
( M  +  ( K  +  1 ) ) ) )  x.  ( ! `  N
) ) )
8584adantr 462 . . 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 11878 . . . . . . . 8  |-  ( ( N  e.  RR  /\  ( K  +  1
)  e.  NN0 )  ->  ( N ^ ( K  +  1 ) )  e.  RR )
872, 17, 86mp2an 667 . . . . . . 7  |-  ( N ^ ( K  + 
1 ) )  e.  RR
881nnnn0i 10583 . . . . . . . 8  |-  N  e. 
NN0
89 reexpcl 11878 . . . . . . . 8  |-  ( ( M  e.  RR  /\  N  e.  NN0 )  -> 
( M ^ N
)  e.  RR )
9024, 88, 89mp2an 667 . . . . . . 7  |-  ( M ^ N )  e.  RR
9187, 90remulcli 9396 . . . . . 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 11887 . . . . . . . . 9  |-  ( K ^ 2 )  e. 
NN0
94 reexpcl 11878 . . . . . . . . 9  |-  ( ( 2  e.  RR  /\  ( K ^ 2 )  e.  NN0 )  -> 
( 2 ^ ( K ^ 2 ) )  e.  RR )
9512, 93, 94mp2an 667 . . . . . . . 8  |-  ( 2 ^ ( K ^
2 ) )  e.  RR
9618, 13nn0expcli 11887 . . . . . . . . 9  |-  ( 2 ^ K )  e. 
NN0
9796nn0rei 10586 . . . . . . . 8  |-  ( 2 ^ K )  e.  RR
9895, 97remulcli 9396 . . . . . . 7  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  e.  RR
99 faccl 12057 . . . . . . . . . . 11  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
10088, 99ax-mp 5 . . . . . . . . . 10  |-  ( ! `
 N )  e.  NN
101100nnnn0i 10583 . . . . . . . . 9  |-  ( ! `
 N )  e. 
NN0
10230, 101nn0mulcli 10614 . . . . . . . 8  |-  ( ( M ^ ( M  +  ( K  + 
1 ) ) )  x.  ( ! `  N ) )  e. 
NN0
103102nn0rei 10586 . . . . . . 7  |-  ( ( M ^ ( M  +  ( K  + 
1 ) ) )  x.  ( ! `  N ) )  e.  RR
10498, 103remulcli 9396 . . . . . 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 9396 . . . . . 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 10328 . . . . . . . . 9  |-  N  e.  CC
109 expp1 11868 . . . . . . . . 9  |-  ( ( N  e.  CC  /\  K  e.  NN0 )  -> 
( N ^ ( K  +  1 ) )  =  ( ( N ^ K )  x.  N ) )
110108, 13, 109mp2an 667 . . . . . . . 8  |-  ( N ^ ( K  + 
1 ) )  =  ( ( N ^ K )  x.  N
)
111 expm1t 11888 . . . . . . . . 9  |-  ( ( M  e.  CC  /\  N  e.  NN )  ->  ( M ^ N
)  =  ( ( M ^ ( N  -  1 ) )  x.  M ) )
11268, 1, 111mp2an 667 . . . . . . . 8  |-  ( M ^ N )  =  ( ( M ^
( N  -  1 ) )  x.  M
)
113110, 112oveq12i 6102 . . . . . . 7  |-  ( ( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  =  ( ( ( N ^ K )  x.  N )  x.  (
( M ^ ( N  -  1 ) )  x.  M ) )
114 reexpcl 11878 . . . . . . . . . 10  |-  ( ( N  e.  RR  /\  K  e.  NN0 )  -> 
( N ^ K
)  e.  RR )
1152, 13, 114mp2an 667 . . . . . . . . 9  |-  ( N ^ K )  e.  RR
116115recni 9394 . . . . . . . 8  |-  ( N ^ K )  e.  CC
117 elnnnn0 10619 . . . . . . . . . . . . 13  |-  ( N  e.  NN  <->  ( N  e.  CC  /\  ( N  -  1 )  e. 
NN0 ) )
1181, 117mpbi 208 . . . . . . . . . . . 12  |-  ( N  e.  CC  /\  ( N  -  1 )  e.  NN0 )
119118simpri 459 . . . . . . . . . . 11  |-  ( N  -  1 )  e. 
NN0
12023, 119nn0expcli 11887 . . . . . . . . . 10  |-  ( M ^ ( N  - 
1 ) )  e. 
NN0
121120, 23nn0mulcli 10614 . . . . . . . . 9  |-  ( ( M ^ ( N  -  1 ) )  x.  M )  e. 
NN0
122121nn0cni 10587 . . . . . . . 8  |-  ( ( M ^ ( N  -  1 ) )  x.  M )  e.  CC
123116, 108, 122mulassi 9391 . . . . . . 7  |-  ( ( ( N ^ K
)  x.  N )  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) )  =  ( ( N ^ K )  x.  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) ) )
124113, 123eqtri 2461 . . . . . 6  |-  ( ( N ^ ( K  +  1 ) )  x.  ( M ^ N ) )  =  ( ( N ^ K )  x.  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) ) )
12588, 121nn0mulcli 10614 . . . . . . . . . . 11  |-  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) )  e. 
NN0
126125nn0rei 10586 . . . . . . . . . 10  |-  ( N  x.  ( ( M ^ ( N  - 
1 ) )  x.  M ) )  e.  RR
127115, 126remulcli 9396 . . . . . . . . 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 10586 . . . . . . . . . . . 12  |-  ( N  -  1 )  e.  RR
130 reexpcl 11878 . . . . . . . . . . . 12  |-  ( ( ( N  -  1 )  e.  RR  /\  K  e.  NN0 )  -> 
( ( N  - 
1 ) ^ K
)  e.  RR )
131129, 13, 130mp2an 667 . . . . . . . . . . 11  |-  ( ( N  -  1 ) ^ K )  e.  RR
132120nn0rei 10586 . . . . . . . . . . 11  |-  ( M ^ ( N  - 
1 ) )  e.  RR
133131, 132remulcli 9396 . . . . . . . . . 10  |-  ( ( ( N  -  1 ) ^ K )  x.  ( M ^
( N  -  1 ) ) )  e.  RR
13496, 88nn0mulcli 10614 . . . . . . . . . . . 12  |-  ( ( 2 ^ K )  x.  N )  e. 
NN0
135134, 23nn0mulcli 10614 . . . . . . . . . . 11  |-  ( ( ( 2 ^ K
)  x.  N )  x.  M )  e. 
NN0
136135nn0rei 10586 . . . . . . . . . 10  |-  ( ( ( 2 ^ K
)  x.  N )  x.  M )  e.  RR
137133, 136remulcli 9396 . . . . . . . . 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 10613 . . . . . . . . . . . . 13  |-  ( M  +  K )  e. 
NN0
140 reexpcl 11878 . . . . . . . . . . . . 13  |-  ( ( M  e.  RR  /\  ( M  +  K
)  e.  NN0 )  ->  ( M ^ ( M  +  K )
)  e.  RR )
14124, 139, 140mp2an 667 . . . . . . . . . . . 12  |-  ( M ^ ( M  +  K ) )  e.  RR
14295, 141remulcli 9396 . . . . . . . . . . 11  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^
( M  +  K
) ) )  e.  RR
143 faccl 12057 . . . . . . . . . . . . 13  |-  ( ( N  -  1 )  e.  NN0  ->  ( ! `
 ( N  - 
1 ) )  e.  NN )
144119, 143ax-mp 5 . . . . . . . . . . . 12  |-  ( ! `
 ( N  - 
1 ) )  e.  NN
145144nnrei 10327 . . . . . . . . . . 11  |-  ( ! `
 ( N  - 
1 ) )  e.  RR
146142, 145remulcli 9396 . . . . . . . . . 10  |-  ( ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^
( M  +  K
) ) )  x.  ( ! `  ( N  -  1 ) ) )  e.  RR
147146, 136remulcli 9396 . . . . . . . . 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 9396 . . . . . . . . . . . 12  |-  ( ( 2 ^ K )  x.  ( ( N  -  1 ) ^ K ) )  e.  RR
150125nn0ge0i 10603 . . . . . . . . . . . . 13  |-  0  <_  ( N  x.  (
( M ^ ( N  -  1 ) )  x.  M ) )
151126, 150pm3.2i 452 . . . . . . . . . . . 12  |-  ( ( N  x.  ( ( M ^ ( N  -  1 ) )  x.  M ) )  e.  RR  /\  0  <_  ( N  x.  (
( M ^ ( N  -  1 ) )  x.  M ) ) )
152115, 149, 1513pm3.2i 1161 . . . . . . . . . . 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 10696 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  NN  /\  N  e.  NN )  ->  ( 1  <  N  <->  ( 1  +  1 )  <_  N ) )
15414, 1, 153mp2an 667 . . . . . . . . . . . . 13  |-  ( 1  <  N  <->  ( 1  +  1 )  <_  N )
155 df-2 10376 . . . . . . . . . . . . . 14  |-  2  =  ( 1  +  1 )
156155breq1i 4296 . . . . . . . . . . . . 13  |-  ( 2  <_  N  <->  ( 1  +  1 )  <_  N )
157154, 156bitr4i 252 . . . . . . . . . . . 12  |-  ( 1  <  N  <->  2  <_  N )
158 expubnd 11920 . . . . . . . . . . . . 13  |-  ( ( N  e.  RR  /\  K  e.  NN0  /\  2  <_  N )  ->  ( N ^ K )  <_ 
( ( 2 ^ K )  x.  (
( N  -  1 ) ^ K ) ) )
1592, 13, 158mp3an12 1299 . . . . . . . . . . . 12  |-  ( 2  <_  N  ->  ( N ^ K )  <_ 
( ( 2 ^ K )  x.  (
( N  -  1 ) ^ K ) ) )
160157, 159sylbi 195 . . . . . . . . . . 11  |-  ( 1  <  N  ->  ( N ^ K )  <_ 
( ( 2 ^ K )  x.  (
( N  -  1 ) ^ K ) ) )
161 lemul1a 10179 . . . . . . . . . . 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 658 . . . . . . . . . 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 10587 . . . . . . . . . . . 12  |-  ( 2 ^ K )  e.  CC
164131recni 9394 . . . . . . . . . . . 12  |-  ( ( N  -  1 ) ^ K )  e.  CC
165163, 164, 108, 122mul4i 9562 . . . . . . . . . . 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 10587 . . . . . . . . . . . . 13  |-  ( M ^ ( N  - 
1 ) )  e.  CC
167164, 166, 68mulassi 9391 . . . . . . . . . . . 12  |-  ( ( ( ( N  - 
1 ) ^ K
)  x.  ( M ^ ( N  - 
1 ) ) )  x.  M )  =  ( ( ( N  -  1 ) ^ K )  x.  (
( M ^ ( N  -  1 ) )  x.  M ) )
168167oveq2i 6101 . . . . . . . . . . 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 10587 . . . . . . . . . . . 12  |-  ( ( 2 ^ K )  x.  N )  e.  CC
170133recni 9394 . . . . . . . . . . . 12  |-  ( ( ( N  -  1 ) ^ K )  x.  ( M ^
( N  -  1 ) ) )  e.  CC
171169, 170, 68mul12i 9560 . . . . . . . . . . 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 2467 . . . . . . . . . 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 4328 . . . . . . . . 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 462 . . . . . . . 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 10603 . . . . . . . . . . . 12  |-  0  <_  ( ( ( 2 ^ K )  x.  N )  x.  M
)
176136, 175pm3.2i 452 . . . . . . . . . . 11  |-  ( ( ( ( 2 ^ K )  x.  N
)  x.  M )  e.  RR  /\  0  <_  ( ( ( 2 ^ K )  x.  N )  x.  M
) )
177133, 146, 1763pm3.2i 1161 . . . . . . . . . 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 10179 . . . . . . . . . 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 665 . . . . . . . . 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 463 . . . . . . . 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 9524 . . . . . . 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 9561 . . . . . . . . 9  |-  ( ( ( 2 ^ K
)  x.  N )  x.  M )  =  ( ( ( 2 ^ K )  x.  M )  x.  N
)
183182oveq2i 6101 . . . . . . . 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 11868 . . . . . . . . . . . . . 14  |-  ( ( M  e.  CC  /\  ( M  +  K
)  e.  NN0 )  ->  ( M ^ (
( M  +  K
)  +  1 ) )  =  ( ( M ^ ( M  +  K ) )  x.  M ) )
18568, 139, 184mp2an 667 . . . . . . . . . . . . 13  |-  ( M ^ ( ( M  +  K )  +  1 ) )  =  ( ( M ^
( M  +  K
) )  x.  M
)
18613nn0cni 10587 . . . . . . . . . . . . . . 15  |-  K  e.  CC
187 ax-1cn 9336 . . . . . . . . . . . . . . 15  |-  1  e.  CC
18868, 186, 187addassi 9390 . . . . . . . . . . . . . 14  |-  ( ( M  +  K )  +  1 )  =  ( M  +  ( K  +  1 ) )
189188oveq2i 6101 . . . . . . . . . . . . 13  |-  ( M ^ ( ( M  +  K )  +  1 ) )  =  ( M ^ ( M  +  ( K  +  1 ) ) )
190185, 189eqtr3i 2463 . . . . . . . . . . . 12  |-  ( ( M ^ ( M  +  K ) )  x.  M )  =  ( M ^ ( M  +  ( K  +  1 ) ) )
191190oveq2i 6101 . . . . . . . . . . 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 9394 . . . . . . . . . . . 12  |-  ( 2 ^ ( K ^
2 ) )  e.  CC
193141recni 9394 . . . . . . . . . . . 12  |-  ( M ^ ( M  +  K ) )  e.  CC
194192, 163, 193, 68mul4i 9562 . . . . . . . . . . 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 2463 . . . . . . . . . 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 12056 . . . . . . . . . . 11  |-  ( N  e.  NN  ->  ( ! `  N )  =  ( ( ! `
 ( N  - 
1 ) )  x.  N ) )
1971, 196ax-mp 5 . . . . . . . . . 10  |-  ( ! `
 N )  =  ( ( ! `  ( N  -  1
) )  x.  N
)
198195, 197oveq12i 6102 . . . . . . . . 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 9394 . . . . . . . . . 10  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( M ^
( M  +  K
) ) )  e.  CC
200144nncni 10328 . . . . . . . . . 10  |-  ( ! `
 ( N  - 
1 ) )  e.  CC
201163, 68mulcli 9387 . . . . . . . . . 10  |-  ( ( 2 ^ K )  x.  M )  e.  CC
202199, 200, 201, 108mul4i 9562 . . . . . . . . 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 2464 . . . . . . . 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 9394 . . . . . . . . 9  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  e.  CC
205100nncni 10328 . . . . . . . . 9  |-  ( ! `
 N )  e.  CC
206204, 78, 205mulassi 9391 . . . . . . . 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 2467 . . . . . . 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 4328 . . . . . 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 4322 . . . . 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 10603 . . . . . . . . 9  |-  0  <_  ( ( M ^
( M  +  ( K  +  1 ) ) )  x.  ( ! `  N )
)
211103, 210pm3.2i 452 . . . . . . . 8  |-  ( ( ( M ^ ( M  +  ( K  +  1 ) ) )  x.  ( ! `
 N ) )  e.  RR  /\  0  <_  ( ( M ^
( M  +  ( K  +  1 ) ) )  x.  ( ! `  N )
) )
21298, 21, 2113pm3.2i 1161 . . . . . . 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 11902 . . . . . . . . 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 1309 . . . . . . . 8  |-  ( 2 ^ ( ( K ^ 2 )  +  K ) )  =  ( ( 2 ^ ( K ^ 2 ) )  x.  (
2 ^ K ) )
21519nn0zi 10667 . . . . . . . . . 10  |-  ( ( K  +  1 ) ^ 2 )  e.  ZZ
21613nn0rei 10586 . . . . . . . . . . . . 13  |-  K  e.  RR
21716nnrei 10327 . . . . . . . . . . . . 13  |-  ( K  +  1 )  e.  RR
21817nn0ge0i 10603 . . . . . . . . . . . . . 14  |-  0  <_  ( K  +  1 )
219217, 218pm3.2i 452 . . . . . . . . . . . . 13  |-  ( ( K  +  1 )  e.  RR  /\  0  <_  ( K  +  1 ) )
220216, 217, 2193pm3.2i 1161 . . . . . . . . . . . 12  |-  ( K  e.  RR  /\  ( K  +  1 )  e.  RR  /\  (
( K  +  1 )  e.  RR  /\  0  <_  ( K  + 
1 ) ) )
221216ltp1i 10232 . . . . . . . . . . . . 13  |-  K  < 
( K  +  1 )
222216, 217, 221ltleii 9493 . . . . . . . . . . . 12  |-  K  <_ 
( K  +  1 )
223 lemul1a 10179 . . . . . . . . . . . 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 667 . . . . . . . . . . 11  |-  ( K  x.  ( K  + 
1 ) )  <_ 
( ( K  + 
1 )  x.  ( K  +  1 ) )
225186sqvali 11941 . . . . . . . . . . . . 13  |-  ( K ^ 2 )  =  ( K  x.  K
)
226186mulid1i 9384 . . . . . . . . . . . . . 14  |-  ( K  x.  1 )  =  K
227226eqcomi 2445 . . . . . . . . . . . . 13  |-  K  =  ( K  x.  1 )
228225, 227oveq12i 6102 . . . . . . . . . . . 12  |-  ( ( K ^ 2 )  +  K )  =  ( ( K  x.  K )  +  ( K  x.  1 ) )
229186, 186, 187adddii 9392 . . . . . . . . . . . 12  |-  ( K  x.  ( K  + 
1 ) )  =  ( ( K  x.  K )  +  ( K  x.  1 ) )
230228, 229eqtr4i 2464 . . . . . . . . . . 11  |-  ( ( K ^ 2 )  +  K )  =  ( K  x.  ( K  +  1 ) )
23116nncni 10328 . . . . . . . . . . . 12  |-  ( K  +  1 )  e.  CC
232231sqvali 11941 . . . . . . . . . . 11  |-  ( ( K  +  1 ) ^ 2 )  =  ( ( K  + 
1 )  x.  ( K  +  1 ) )
233224, 230, 2323brtr4i 4317 . . . . . . . . . 10  |-  ( ( K ^ 2 )  +  K )  <_ 
( ( K  + 
1 ) ^ 2 )
23493, 13nn0addcli 10613 . . . . . . . . . . . 12  |-  ( ( K ^ 2 )  +  K )  e. 
NN0
235234nn0zi 10667 . . . . . . . . . . 11  |-  ( ( K ^ 2 )  +  K )  e.  ZZ
236235eluz1i 10864 . . . . . . . . . 10  |-  ( ( ( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  (
( K ^ 2 )  +  K ) )  <->  ( ( ( K  +  1 ) ^ 2 )  e.  ZZ  /\  ( ( K ^ 2 )  +  K )  <_ 
( ( K  + 
1 ) ^ 2 ) ) )
237215, 233, 236mpbir2an 906 . . . . . . . . 9  |-  ( ( K  +  1 ) ^ 2 )  e.  ( ZZ>= `  ( ( K ^ 2 )  +  K ) )
238 leexp2a 11915 . . . . . . . . 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 1309 . . . . . . . 8  |-  ( 2 ^ ( ( K ^ 2 )  +  K ) )  <_ 
( 2 ^ (
( K  +  1 ) ^ 2 ) )
240214, 239eqbrtrri 4310 . . . . . . 7  |-  ( ( 2 ^ ( K ^ 2 ) )  x.  ( 2 ^ K ) )  <_ 
( 2 ^ (
( K  +  1 ) ^ 2 ) )
241 lemul1a 10179 . . . . . . 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 667 . . . . . 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 9524 . . . 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 9391 . . . 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 4329 . . 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 777 . 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 665 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 184    \/ wo 368    /\ wa 369    /\ w3a 960    = wceq 1364    e. wcel 1761   class class class wbr 4289   ` cfv 5415  (class class class)co 6090   CCcc 9276   RRcr 9277   0cc0 9278   1c1 9279    + caddc 9281    x. cmul 9283    < clt 9414    <_ cle 9415    - cmin 9591   NNcn 10318   2c2 10367   NN0cn0 10575   ZZcz 10642   ZZ>=cuz 10857   ^cexp 11861   !cfa 12047
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-2nd 6577  df-recs 6828  df-rdg 6862  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-div 9990  df-nn 10319  df-2 10376  df-n0 10576  df-z 10643  df-uz 10858  df-rp 10988  df-seq 11803  df-exp 11862  df-fac 12048
This theorem is referenced by:  faclbnd4lem2  12066
  Copyright terms: Public domain W3C validator