Metamath Proof Explorer

Theorem faclbnd4lem4

Description: Lemma for faclbnd4 . Prove the 0 < N case by induction on K . (Contributed by NM, 19-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( n = m -> ( n ^ j ) = ( m ^ j ) )
2 oveq2 
 |-  ( n = m -> ( M ^ n ) = ( M ^ m ) )
3 1 2 oveq12d 
 |-  ( n = m -> ( ( n ^ j ) x. ( M ^ n ) ) = ( ( m ^ j ) x. ( M ^ m ) ) )
4 fveq2 
 |-  ( n = m -> ( ! ` n ) = ( ! ` m ) )
5 4 oveq2d 
 |-  ( n = m -> ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) = ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) )
6 3 5 breq12d 
 |-  ( n = m -> ( ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) <-> ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) ) )
7 6 cbvralvw 
 |-  ( A. n e. NN ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) <-> A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) )
8 nnre 
 |-  ( n e. NN -> n e. RR )
9 1re 
 |-  1 e. RR
10 lelttric 
 |-  ( ( n e. RR /\ 1 e. RR ) -> ( n <_ 1 \/ 1 < n ) )
11 8 9 10 sylancl 
 |-  ( n e. NN -> ( n <_ 1 \/ 1 < n ) )
12 11 ancli 
 |-  ( n e. NN -> ( n e. NN /\ ( n <_ 1 \/ 1 < n ) ) )
13 andi 
 |-  ( ( n e. NN /\ ( n <_ 1 \/ 1 < n ) ) <-> ( ( n e. NN /\ n <_ 1 ) \/ ( n e. NN /\ 1 < n ) ) )
14 12 13 sylib 
 |-  ( n e. NN -> ( ( n e. NN /\ n <_ 1 ) \/ ( n e. NN /\ 1 < n ) ) )
15 nnge1 
 |-  ( n e. NN -> 1 <_ n )
16 letri3 
 |-  ( ( n e. RR /\ 1 e. RR ) -> ( n = 1 <-> ( n <_ 1 /\ 1 <_ n ) ) )
17 8 9 16 sylancl 
 |-  ( n e. NN -> ( n = 1 <-> ( n <_ 1 /\ 1 <_ n ) ) )
18 17 biimpar 
 |-  ( ( n e. NN /\ ( n <_ 1 /\ 1 <_ n ) ) -> n = 1 )
19 18 anassrs 
 |-  ( ( ( n e. NN /\ n <_ 1 ) /\ 1 <_ n ) -> n = 1 )
20 15 19 mpidan 
 |-  ( ( n e. NN /\ n <_ 1 ) -> n = 1 )
21 oveq1 
 |-  ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
22 1m1e0 
 |-  ( 1 - 1 ) = 0
23 21 22 eqtrdi 
 |-  ( n = 1 -> ( n - 1 ) = 0 )
24 20 23 syl 
 |-  ( ( n e. NN /\ n <_ 1 ) -> ( n - 1 ) = 0 )
25 faclbnd4lem3 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ ( n - 1 ) = 0 ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) )
26 24 25 sylan2 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ ( n e. NN /\ n <_ 1 ) ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) )
27 26 a1d 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ ( n e. NN /\ n <_ 1 ) ) -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) ) )
28 1nn 
 |-  1 e. NN
29 nnsub 
 |-  ( ( 1 e. NN /\ n e. NN ) -> ( 1 < n <-> ( n - 1 ) e. NN ) )
30 28 29 mpan 
 |-  ( n e. NN -> ( 1 < n <-> ( n - 1 ) e. NN ) )
31 30 biimpa 
 |-  ( ( n e. NN /\ 1 < n ) -> ( n - 1 ) e. NN )
32 oveq1 
 |-  ( m = ( n - 1 ) -> ( m ^ j ) = ( ( n - 1 ) ^ j ) )
33 oveq2 
 |-  ( m = ( n - 1 ) -> ( M ^ m ) = ( M ^ ( n - 1 ) ) )
34 32 33 oveq12d 
 |-  ( m = ( n - 1 ) -> ( ( m ^ j ) x. ( M ^ m ) ) = ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) )
35 fveq2 
 |-  ( m = ( n - 1 ) -> ( ! ` m ) = ( ! ` ( n - 1 ) ) )
36 35 oveq2d 
 |-  ( m = ( n - 1 ) -> ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) = ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) )
37 34 36 breq12d 
 |-  ( m = ( n - 1 ) -> ( ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) <-> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) ) )
38 37 rspcv 
 |-  ( ( n - 1 ) e. NN -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) ) )
39 31 38 syl 
 |-  ( ( n e. NN /\ 1 < n ) -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) ) )
40 39 adantl 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ ( n e. NN /\ 1 < n ) ) -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) ) )
41 27 40 jaodan 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ ( ( n e. NN /\ n <_ 1 ) \/ ( n e. NN /\ 1 < n ) ) ) -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) ) )
42 14 41 sylan2 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ n e. NN ) -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) ) )
43 faclbnd4lem2 
 |-  ( ( M e. NN0 /\ j e. NN0 /\ n e. NN ) -> ( ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) -> ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) )
44 43 3expa 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ n e. NN ) -> ( ( ( ( n - 1 ) ^ j ) x. ( M ^ ( n - 1 ) ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` ( n - 1 ) ) ) -> ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) )
45 42 44 syld 
 |-  ( ( ( M e. NN0 /\ j e. NN0 ) /\ n e. NN ) -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) )
46 45 ralrimdva 
 |-  ( ( M e. NN0 /\ j e. NN0 ) -> ( A. m e. NN ( ( m ^ j ) x. ( M ^ m ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` m ) ) -> A. n e. NN ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) )
47 7 46 biimtrid 
 |-  ( ( M e. NN0 /\ j e. NN0 ) -> ( A. n e. NN ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) -> A. n e. NN ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) )
48 47 expcom 
 |-  ( j e. NN0 -> ( M e. NN0 -> ( A. n e. NN ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) -> A. n e. NN ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) ) )
49 48 a2d 
 |-  ( j e. NN0 -> ( ( M e. NN0 -> A. n e. NN ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) ) -> ( M e. NN0 -> A. n e. NN ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) ) )
50 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
51 faclbnd3 
 |-  ( ( M e. NN0 /\ n e. NN0 ) -> ( M ^ n ) <_ ( ( M ^ M ) x. ( ! ` n ) ) )
52 50 51 sylan2 
 |-  ( ( M e. NN0 /\ n e. NN ) -> ( M ^ n ) <_ ( ( M ^ M ) x. ( ! ` n ) ) )
53 nncn 
 |-  ( n e. NN -> n e. CC )
54 53 exp0d 
 |-  ( n e. NN -> ( n ^ 0 ) = 1 )
55 54 oveq1d 
 |-  ( n e. NN -> ( ( n ^ 0 ) x. ( M ^ n ) ) = ( 1 x. ( M ^ n ) ) )
56 55 adantl 
 |-  ( ( M e. NN0 /\ n e. NN ) -> ( ( n ^ 0 ) x. ( M ^ n ) ) = ( 1 x. ( M ^ n ) ) )
57 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
58 expcl 
 |-  ( ( M e. CC /\ n e. NN0 ) -> ( M ^ n ) e. CC )
59 57 50 58 syl2an 
 |-  ( ( M e. NN0 /\ n e. NN ) -> ( M ^ n ) e. CC )
60 59 mullidd 
 |-  ( ( M e. NN0 /\ n e. NN ) -> ( 1 x. ( M ^ n ) ) = ( M ^ n ) )
61 56 60 eqtrd 
 |-  ( ( M e. NN0 /\ n e. NN ) -> ( ( n ^ 0 ) x. ( M ^ n ) ) = ( M ^ n ) )
62 sq0 
 |-  ( 0 ^ 2 ) = 0
63 62 oveq2i 
 |-  ( 2 ^ ( 0 ^ 2 ) ) = ( 2 ^ 0 )
64 2cn 
 |-  2 e. CC
65 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
66 64 65 ax-mp 
 |-  ( 2 ^ 0 ) = 1
67 63 66 eqtri 
 |-  ( 2 ^ ( 0 ^ 2 ) ) = 1
68 67 a1i 
 |-  ( M e. NN0 -> ( 2 ^ ( 0 ^ 2 ) ) = 1 )
69 57 addridd 
 |-  ( M e. NN0 -> ( M + 0 ) = M )
70 69 oveq2d 
 |-  ( M e. NN0 -> ( M ^ ( M + 0 ) ) = ( M ^ M ) )
71 68 70 oveq12d 
 |-  ( M e. NN0 -> ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) = ( 1 x. ( M ^ M ) ) )
72 expcl 
 |-  ( ( M e. CC /\ M e. NN0 ) -> ( M ^ M ) e. CC )
73 57 72 mpancom 
 |-  ( M e. NN0 -> ( M ^ M ) e. CC )
74 73 mullidd 
 |-  ( M e. NN0 -> ( 1 x. ( M ^ M ) ) = ( M ^ M ) )
75 71 74 eqtrd 
 |-  ( M e. NN0 -> ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) = ( M ^ M ) )
76 75 oveq1d 
 |-  ( M e. NN0 -> ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) = ( ( M ^ M ) x. ( ! ` n ) ) )
77 76 adantr 
 |-  ( ( M e. NN0 /\ n e. NN ) -> ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) = ( ( M ^ M ) x. ( ! ` n ) ) )
78 52 61 77 3brtr4d 
 |-  ( ( M e. NN0 /\ n e. NN ) -> ( ( n ^ 0 ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) )
79 78 ralrimiva 
 |-  ( M e. NN0 -> A. n e. NN ( ( n ^ 0 ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) )
80 oveq2 
 |-  ( m = 0 -> ( n ^ m ) = ( n ^ 0 ) )
81 80 oveq1d 
 |-  ( m = 0 -> ( ( n ^ m ) x. ( M ^ n ) ) = ( ( n ^ 0 ) x. ( M ^ n ) ) )
82 oveq1 
 |-  ( m = 0 -> ( m ^ 2 ) = ( 0 ^ 2 ) )
83 82 oveq2d 
 |-  ( m = 0 -> ( 2 ^ ( m ^ 2 ) ) = ( 2 ^ ( 0 ^ 2 ) ) )
84 oveq2 
 |-  ( m = 0 -> ( M + m ) = ( M + 0 ) )
85 84 oveq2d 
 |-  ( m = 0 -> ( M ^ ( M + m ) ) = ( M ^ ( M + 0 ) ) )
86 83 85 oveq12d 
 |-  ( m = 0 -> ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) = ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) )
87 86 oveq1d 
 |-  ( m = 0 -> ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) = ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) )
88 81 87 breq12d 
 |-  ( m = 0 -> ( ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> ( ( n ^ 0 ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) ) )
89 88 ralbidv 
 |-  ( m = 0 -> ( A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> A. n e. NN ( ( n ^ 0 ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) ) )
90 89 imbi2d 
 |-  ( m = 0 -> ( ( M e. NN0 -> A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) ) <-> ( M e. NN0 -> A. n e. NN ( ( n ^ 0 ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( 0 ^ 2 ) ) x. ( M ^ ( M + 0 ) ) ) x. ( ! ` n ) ) ) ) )
91 oveq2 
 |-  ( m = j -> ( n ^ m ) = ( n ^ j ) )
92 91 oveq1d 
 |-  ( m = j -> ( ( n ^ m ) x. ( M ^ n ) ) = ( ( n ^ j ) x. ( M ^ n ) ) )
93 oveq1 
 |-  ( m = j -> ( m ^ 2 ) = ( j ^ 2 ) )
94 93 oveq2d 
 |-  ( m = j -> ( 2 ^ ( m ^ 2 ) ) = ( 2 ^ ( j ^ 2 ) ) )
95 oveq2 
 |-  ( m = j -> ( M + m ) = ( M + j ) )
96 95 oveq2d 
 |-  ( m = j -> ( M ^ ( M + m ) ) = ( M ^ ( M + j ) ) )
97 94 96 oveq12d 
 |-  ( m = j -> ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) = ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) )
98 97 oveq1d 
 |-  ( m = j -> ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) = ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) )
99 92 98 breq12d 
 |-  ( m = j -> ( ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) ) )
100 99 ralbidv 
 |-  ( m = j -> ( A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> A. n e. NN ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) ) )
101 100 imbi2d 
 |-  ( m = j -> ( ( M e. NN0 -> A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) ) <-> ( M e. NN0 -> A. n e. NN ( ( n ^ j ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( j ^ 2 ) ) x. ( M ^ ( M + j ) ) ) x. ( ! ` n ) ) ) ) )
102 oveq2 
 |-  ( m = ( j + 1 ) -> ( n ^ m ) = ( n ^ ( j + 1 ) ) )
103 102 oveq1d 
 |-  ( m = ( j + 1 ) -> ( ( n ^ m ) x. ( M ^ n ) ) = ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) )
104 oveq1 
 |-  ( m = ( j + 1 ) -> ( m ^ 2 ) = ( ( j + 1 ) ^ 2 ) )
105 104 oveq2d 
 |-  ( m = ( j + 1 ) -> ( 2 ^ ( m ^ 2 ) ) = ( 2 ^ ( ( j + 1 ) ^ 2 ) ) )
106 oveq2 
 |-  ( m = ( j + 1 ) -> ( M + m ) = ( M + ( j + 1 ) ) )
107 106 oveq2d 
 |-  ( m = ( j + 1 ) -> ( M ^ ( M + m ) ) = ( M ^ ( M + ( j + 1 ) ) ) )
108 105 107 oveq12d 
 |-  ( m = ( j + 1 ) -> ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) = ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) )
109 108 oveq1d 
 |-  ( m = ( j + 1 ) -> ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) = ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) )
110 103 109 breq12d 
 |-  ( m = ( j + 1 ) -> ( ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) )
111 110 ralbidv 
 |-  ( m = ( j + 1 ) -> ( A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> A. n e. NN ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) )
112 111 imbi2d 
 |-  ( m = ( j + 1 ) -> ( ( M e. NN0 -> A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) ) <-> ( M e. NN0 -> A. n e. NN ( ( n ^ ( j + 1 ) ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( ( j + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( j + 1 ) ) ) ) x. ( ! ` n ) ) ) ) )
113 oveq2 
 |-  ( m = K -> ( n ^ m ) = ( n ^ K ) )
114 113 oveq1d 
 |-  ( m = K -> ( ( n ^ m ) x. ( M ^ n ) ) = ( ( n ^ K ) x. ( M ^ n ) ) )
115 oveq1 
 |-  ( m = K -> ( m ^ 2 ) = ( K ^ 2 ) )
116 115 oveq2d 
 |-  ( m = K -> ( 2 ^ ( m ^ 2 ) ) = ( 2 ^ ( K ^ 2 ) ) )
117 oveq2 
 |-  ( m = K -> ( M + m ) = ( M + K ) )
118 117 oveq2d 
 |-  ( m = K -> ( M ^ ( M + m ) ) = ( M ^ ( M + K ) ) )
119 116 118 oveq12d 
 |-  ( m = K -> ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) = ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) )
120 119 oveq1d 
 |-  ( m = K -> ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) = ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) )
121 114 120 breq12d 
 |-  ( m = K -> ( ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> ( ( n ^ K ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) ) )
122 121 ralbidv 
 |-  ( m = K -> ( A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) <-> A. n e. NN ( ( n ^ K ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) ) )
123 122 imbi2d 
 |-  ( m = K -> ( ( M e. NN0 -> A. n e. NN ( ( n ^ m ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( m ^ 2 ) ) x. ( M ^ ( M + m ) ) ) x. ( ! ` n ) ) ) <-> ( M e. NN0 -> A. n e. NN ( ( n ^ K ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) ) ) )
124 49 79 90 101 112 123 nn0indALT 
 |-  ( K e. NN0 -> ( M e. NN0 -> A. n e. NN ( ( n ^ K ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) ) )
125 124 imp 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> A. n e. NN ( ( n ^ K ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) )
126 oveq1 
 |-  ( n = N -> ( n ^ K ) = ( N ^ K ) )
127 oveq2 
 |-  ( n = N -> ( M ^ n ) = ( M ^ N ) )
128 126 127 oveq12d 
 |-  ( n = N -> ( ( n ^ K ) x. ( M ^ n ) ) = ( ( N ^ K ) x. ( M ^ N ) ) )
129 fveq2 
 |-  ( n = N -> ( ! ` n ) = ( ! ` N ) )
130 129 oveq2d 
 |-  ( n = N -> ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) = ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
131 128 130 breq12d 
 |-  ( n = N -> ( ( ( n ^ K ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) <-> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) ) )
132 131 rspcva 
 |-  ( ( N e. NN /\ A. n e. NN ( ( n ^ K ) x. ( M ^ n ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` n ) ) ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
133 125 132 sylan2 
 |-  ( ( N e. NN /\ ( K e. NN0 /\ M e. NN0 ) ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
134 133 3impb 
 |-  ( ( N e. NN /\ K e. NN0 /\ M e. NN0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )