This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem faclbnd

Description: A lower bound for the factorial function. (Contributed by NM, 17-Dec-2005)

Ref Expression
Assertion faclbnd 
|- ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
2 oveq1 
 |-  ( j = 0 -> ( j + 1 ) = ( 0 + 1 ) )
3 2 oveq2d 
 |-  ( j = 0 -> ( M ^ ( j + 1 ) ) = ( M ^ ( 0 + 1 ) ) )
4 fveq2 
 |-  ( j = 0 -> ( ! ` j ) = ( ! ` 0 ) )
5 4 oveq2d 
 |-  ( j = 0 -> ( ( M ^ M ) x. ( ! ` j ) ) = ( ( M ^ M ) x. ( ! ` 0 ) ) )
6 3 5 breq12d 
 |-  ( j = 0 -> ( ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) <-> ( M ^ ( 0 + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` 0 ) ) ) )
7 6 imbi2d 
 |-  ( j = 0 -> ( ( M e. NN -> ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) ) <-> ( M e. NN -> ( M ^ ( 0 + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` 0 ) ) ) ) )
8 oveq1 
 |-  ( j = k -> ( j + 1 ) = ( k + 1 ) )
9 8 oveq2d 
 |-  ( j = k -> ( M ^ ( j + 1 ) ) = ( M ^ ( k + 1 ) ) )
10 fveq2 
 |-  ( j = k -> ( ! ` j ) = ( ! ` k ) )
11 10 oveq2d 
 |-  ( j = k -> ( ( M ^ M ) x. ( ! ` j ) ) = ( ( M ^ M ) x. ( ! ` k ) ) )
12 9 11 breq12d 
 |-  ( j = k -> ( ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) <-> ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) )
13 12 imbi2d 
 |-  ( j = k -> ( ( M e. NN -> ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) ) <-> ( M e. NN -> ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) ) )
14 oveq1 
 |-  ( j = ( k + 1 ) -> ( j + 1 ) = ( ( k + 1 ) + 1 ) )
15 14 oveq2d 
 |-  ( j = ( k + 1 ) -> ( M ^ ( j + 1 ) ) = ( M ^ ( ( k + 1 ) + 1 ) ) )
16 fveq2 
 |-  ( j = ( k + 1 ) -> ( ! ` j ) = ( ! ` ( k + 1 ) ) )
17 16 oveq2d 
 |-  ( j = ( k + 1 ) -> ( ( M ^ M ) x. ( ! ` j ) ) = ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) )
18 15 17 breq12d 
 |-  ( j = ( k + 1 ) -> ( ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) <-> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) )
19 18 imbi2d 
 |-  ( j = ( k + 1 ) -> ( ( M e. NN -> ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) ) <-> ( M e. NN -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) ) )
20 oveq1 
 |-  ( j = N -> ( j + 1 ) = ( N + 1 ) )
21 20 oveq2d 
 |-  ( j = N -> ( M ^ ( j + 1 ) ) = ( M ^ ( N + 1 ) ) )
22 fveq2 
 |-  ( j = N -> ( ! ` j ) = ( ! ` N ) )
23 22 oveq2d 
 |-  ( j = N -> ( ( M ^ M ) x. ( ! ` j ) ) = ( ( M ^ M ) x. ( ! ` N ) ) )
24 21 23 breq12d 
 |-  ( j = N -> ( ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) <-> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) )
25 24 imbi2d 
 |-  ( j = N -> ( ( M e. NN -> ( M ^ ( j + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` j ) ) ) <-> ( M e. NN -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) ) )
26 nnre 
 |-  ( M e. NN -> M e. RR )
27 nnge1 
 |-  ( M e. NN -> 1 <_ M )
28 elnnuz 
 |-  ( M e. NN <-> M e. ( ZZ>= ` 1 ) )
29 28 biimpi 
 |-  ( M e. NN -> M e. ( ZZ>= ` 1 ) )
30 26 27 29 leexp2ad 
 |-  ( M e. NN -> ( M ^ 1 ) <_ ( M ^ M ) )
31 0p1e1 
 |-  ( 0 + 1 ) = 1
32 31 oveq2i 
 |-  ( M ^ ( 0 + 1 ) ) = ( M ^ 1 )
33 32 a1i 
 |-  ( M e. NN -> ( M ^ ( 0 + 1 ) ) = ( M ^ 1 ) )
34 fac0 
 |-  ( ! ` 0 ) = 1
35 34 oveq2i 
 |-  ( ( M ^ M ) x. ( ! ` 0 ) ) = ( ( M ^ M ) x. 1 )
36 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
37 26 36 reexpcld 
 |-  ( M e. NN -> ( M ^ M ) e. RR )
38 37 recnd 
 |-  ( M e. NN -> ( M ^ M ) e. CC )
39 38 mulridd 
 |-  ( M e. NN -> ( ( M ^ M ) x. 1 ) = ( M ^ M ) )
40 35 39 eqtrid 
 |-  ( M e. NN -> ( ( M ^ M ) x. ( ! ` 0 ) ) = ( M ^ M ) )
41 30 33 40 3brtr4d 
 |-  ( M e. NN -> ( M ^ ( 0 + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` 0 ) ) )
42 26 ad3antrrr 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> M e. RR )
43 simpllr 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> k e. NN0 )
44 peano2nn0 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN0 )
45 43 44 syl 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( k + 1 ) e. NN0 )
46 42 45 reexpcld 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( M ^ ( k + 1 ) ) e. RR )
47 36 ad3antrrr 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> M e. NN0 )
48 42 47 reexpcld 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( M ^ M ) e. RR )
49 43 faccld 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( ! ` k ) e. NN )
50 49 nnred 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( ! ` k ) e. RR )
51 48 50 remulcld 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( ( M ^ M ) x. ( ! ` k ) ) e. RR )
52 nn0re 
 |-  ( k e. NN0 -> k e. RR )
53 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
54 43 52 53 3syl 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( k + 1 ) e. RR )
55 nngt0 
 |-  ( M e. NN -> 0 < M )
56 55 ad3antrrr 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> 0 < M )
57 0re 
 |-  0 e. RR
58 ltle 
 |-  ( ( 0 e. RR /\ M e. RR ) -> ( 0 < M -> 0 <_ M ) )
59 57 58 mpan 
 |-  ( M e. RR -> ( 0 < M -> 0 <_ M ) )
60 42 56 59 sylc 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> 0 <_ M )
61 42 45 60 expge0d 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> 0 <_ ( M ^ ( k + 1 ) ) )
62 simplr 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) )
63 simprr 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> M <_ ( k + 1 ) )
64 46 51 42 54 61 60 62 63 lemul12ad 
 |-  ( ( ( ( M e. NN /\ k e. NN0 ) /\ ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) /\ ( ( M e. NN /\ k e. NN0 ) /\ M <_ ( k + 1 ) ) ) -> ( ( M ^ ( k + 1 ) ) x. M ) <_ ( ( ( M ^ M ) x. ( ! ` k ) ) x. ( k + 1 ) ) )
65 64 anandis 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) /\ M <_ ( k + 1 ) ) ) -> ( ( M ^ ( k + 1 ) ) x. M ) <_ ( ( ( M ^ M ) x. ( ! ` k ) ) x. ( k + 1 ) ) )
66 nncn 
 |-  ( M e. NN -> M e. CC )
67 expp1 
 |-  ( ( M e. CC /\ ( k + 1 ) e. NN0 ) -> ( M ^ ( ( k + 1 ) + 1 ) ) = ( ( M ^ ( k + 1 ) ) x. M ) )
68 66 44 67 syl2an 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M ^ ( ( k + 1 ) + 1 ) ) = ( ( M ^ ( k + 1 ) ) x. M ) )
69 68 adantr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) /\ M <_ ( k + 1 ) ) ) -> ( M ^ ( ( k + 1 ) + 1 ) ) = ( ( M ^ ( k + 1 ) ) x. M ) )
70 facp1 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
71 70 adantl 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
72 71 oveq2d 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) = ( ( M ^ M ) x. ( ( ! ` k ) x. ( k + 1 ) ) ) )
73 38 adantr 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M ^ M ) e. CC )
74 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
75 74 nncnd 
 |-  ( k e. NN0 -> ( ! ` k ) e. CC )
76 75 adantl 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ! ` k ) e. CC )
77 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
78 peano2cn 
 |-  ( k e. CC -> ( k + 1 ) e. CC )
79 77 78 syl 
 |-  ( k e. NN0 -> ( k + 1 ) e. CC )
80 79 adantl 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( k + 1 ) e. CC )
81 73 76 80 mulassd 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( ( M ^ M ) x. ( ! ` k ) ) x. ( k + 1 ) ) = ( ( M ^ M ) x. ( ( ! ` k ) x. ( k + 1 ) ) ) )
82 72 81 eqtr4d 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) = ( ( ( M ^ M ) x. ( ! ` k ) ) x. ( k + 1 ) ) )
83 82 adantr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) /\ M <_ ( k + 1 ) ) ) -> ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) = ( ( ( M ^ M ) x. ( ! ` k ) ) x. ( k + 1 ) ) )
84 65 69 83 3brtr4d 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) /\ M <_ ( k + 1 ) ) ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) )
85 84 exp32 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) -> ( M <_ ( k + 1 ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) ) )
86 85 com23 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M <_ ( k + 1 ) -> ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) ) )
87 nn0ltp1le 
 |-  ( ( ( k + 1 ) e. NN0 /\ M e. NN0 ) -> ( ( k + 1 ) < M <-> ( ( k + 1 ) + 1 ) <_ M ) )
88 44 36 87 syl2anr 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( k + 1 ) < M <-> ( ( k + 1 ) + 1 ) <_ M ) )
89 peano2nn0 
 |-  ( ( k + 1 ) e. NN0 -> ( ( k + 1 ) + 1 ) e. NN0 )
90 44 89 syl 
 |-  ( k e. NN0 -> ( ( k + 1 ) + 1 ) e. NN0 )
91 reexpcl 
 |-  ( ( M e. RR /\ ( ( k + 1 ) + 1 ) e. NN0 ) -> ( M ^ ( ( k + 1 ) + 1 ) ) e. RR )
92 26 90 91 syl2an 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M ^ ( ( k + 1 ) + 1 ) ) e. RR )
93 92 adantr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( M ^ ( ( k + 1 ) + 1 ) ) e. RR )
94 37 ad2antrr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( M ^ M ) e. RR )
95 44 faccld 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) e. NN )
96 95 nnred 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) e. RR )
97 remulcl 
 |-  ( ( ( M ^ M ) e. RR /\ ( ! ` ( k + 1 ) ) e. RR ) -> ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) e. RR )
98 37 96 97 syl2an 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) e. RR )
99 98 adantr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) e. RR )
100 26 ad2antrr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> M e. RR )
101 27 ad2antrr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> 1 <_ M )
102 simpr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( ( k + 1 ) + 1 ) <_ M )
103 90 ad2antlr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( ( k + 1 ) + 1 ) e. NN0 )
104 103 nn0zd 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( ( k + 1 ) + 1 ) e. ZZ )
105 nnz 
 |-  ( M e. NN -> M e. ZZ )
106 105 ad2antrr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> M e. ZZ )
107 eluz 
 |-  ( ( ( ( k + 1 ) + 1 ) e. ZZ /\ M e. ZZ ) -> ( M e. ( ZZ>= ` ( ( k + 1 ) + 1 ) ) <-> ( ( k + 1 ) + 1 ) <_ M ) )
108 104 106 107 syl2anc 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( M e. ( ZZ>= ` ( ( k + 1 ) + 1 ) ) <-> ( ( k + 1 ) + 1 ) <_ M ) )
109 102 108 mpbird 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> M e. ( ZZ>= ` ( ( k + 1 ) + 1 ) ) )
110 100 101 109 leexp2ad 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( M ^ M ) )
111 37 96 anim12i 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( M ^ M ) e. RR /\ ( ! ` ( k + 1 ) ) e. RR ) )
112 nn0re 
 |-  ( M e. NN0 -> M e. RR )
113 id 
 |-  ( M e. NN0 -> M e. NN0 )
114 nn0ge0 
 |-  ( M e. NN0 -> 0 <_ M )
115 112 113 114 expge0d 
 |-  ( M e. NN0 -> 0 <_ ( M ^ M ) )
116 36 115 syl 
 |-  ( M e. NN -> 0 <_ ( M ^ M ) )
117 95 nnge1d 
 |-  ( k e. NN0 -> 1 <_ ( ! ` ( k + 1 ) ) )
118 116 117 anim12i 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( 0 <_ ( M ^ M ) /\ 1 <_ ( ! ` ( k + 1 ) ) ) )
119 lemulge11 
 |-  ( ( ( ( M ^ M ) e. RR /\ ( ! ` ( k + 1 ) ) e. RR ) /\ ( 0 <_ ( M ^ M ) /\ 1 <_ ( ! ` ( k + 1 ) ) ) ) -> ( M ^ M ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) )
120 111 118 119 syl2anc 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M ^ M ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) )
121 120 adantr 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( M ^ M ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) )
122 93 94 99 110 121 letrd 
 |-  ( ( ( M e. NN /\ k e. NN0 ) /\ ( ( k + 1 ) + 1 ) <_ M ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) )
123 122 ex 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( ( k + 1 ) + 1 ) <_ M -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) )
124 88 123 sylbid 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( k + 1 ) < M -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) )
125 124 a1dd 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( k + 1 ) < M -> ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) ) )
126 52 53 syl 
 |-  ( k e. NN0 -> ( k + 1 ) e. RR )
127 lelttric 
 |-  ( ( M e. RR /\ ( k + 1 ) e. RR ) -> ( M <_ ( k + 1 ) \/ ( k + 1 ) < M ) )
128 26 126 127 syl2an 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( M <_ ( k + 1 ) \/ ( k + 1 ) < M ) )
129 86 125 128 mpjaod 
 |-  ( ( M e. NN /\ k e. NN0 ) -> ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) )
130 129 expcom 
 |-  ( k e. NN0 -> ( M e. NN -> ( ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) ) )
131 130 a2d 
 |-  ( k e. NN0 -> ( ( M e. NN -> ( M ^ ( k + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` k ) ) ) -> ( M e. NN -> ( M ^ ( ( k + 1 ) + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` ( k + 1 ) ) ) ) ) )
132 7 13 19 25 41 131 nn0ind 
 |-  ( N e. NN0 -> ( M e. NN -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) )
133 132 impcom 
 |-  ( ( M e. NN /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
134 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
135 134 nnnn0d 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN0 )
136 135 nn0ge0d 
 |-  ( N e. NN0 -> 0 <_ ( ! ` N ) )
137 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
138 137 0expd 
 |-  ( N e. NN0 -> ( 0 ^ ( N + 1 ) ) = 0 )
139 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
140 139 oveq1i 
 |-  ( ( 0 ^ 0 ) x. ( ! ` N ) ) = ( 1 x. ( ! ` N ) )
141 134 nncnd 
 |-  ( N e. NN0 -> ( ! ` N ) e. CC )
142 141 mullidd 
 |-  ( N e. NN0 -> ( 1 x. ( ! ` N ) ) = ( ! ` N ) )
143 140 142 eqtrid 
 |-  ( N e. NN0 -> ( ( 0 ^ 0 ) x. ( ! ` N ) ) = ( ! ` N ) )
144 136 138 143 3brtr4d 
 |-  ( N e. NN0 -> ( 0 ^ ( N + 1 ) ) <_ ( ( 0 ^ 0 ) x. ( ! ` N ) ) )
145 oveq1 
 |-  ( M = 0 -> ( M ^ ( N + 1 ) ) = ( 0 ^ ( N + 1 ) ) )
146 oveq12 
 |-  ( ( M = 0 /\ M = 0 ) -> ( M ^ M ) = ( 0 ^ 0 ) )
147 146 anidms 
 |-  ( M = 0 -> ( M ^ M ) = ( 0 ^ 0 ) )
148 147 oveq1d 
 |-  ( M = 0 -> ( ( M ^ M ) x. ( ! ` N ) ) = ( ( 0 ^ 0 ) x. ( ! ` N ) ) )
149 145 148 breq12d 
 |-  ( M = 0 -> ( ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) <-> ( 0 ^ ( N + 1 ) ) <_ ( ( 0 ^ 0 ) x. ( ! ` N ) ) ) )
150 144 149 imbitrrid 
 |-  ( M = 0 -> ( N e. NN0 -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) ) )
151 150 imp 
 |-  ( ( M = 0 /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
152 133 151 jaoian 
 |-  ( ( ( M e. NN \/ M = 0 ) /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )
153 1 152 sylanb 
 |-  ( ( M e. NN0 /\ N e. NN0 ) -> ( M ^ ( N + 1 ) ) <_ ( ( M ^ M ) x. ( ! ` N ) ) )