Metamath Proof Explorer

Theorem faclbnd4lem3

Description: Lemma for faclbnd4 . The N = 0 case. (Contributed by NM, 23-Dec-2005)

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

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( K e. NN0 <-> ( K e. NN \/ K = 0 ) )
2 0exp 
 |-  ( K e. NN -> ( 0 ^ K ) = 0 )
3 2 adantl 
 |-  ( ( M e. NN0 /\ K e. NN ) -> ( 0 ^ K ) = 0 )
4 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
5 2nn0 
 |-  2 e. NN0
6 nn0sqcl 
 |-  ( K e. NN0 -> ( K ^ 2 ) e. NN0 )
7 nn0expcl 
 |-  ( ( 2 e. NN0 /\ ( K ^ 2 ) e. NN0 ) -> ( 2 ^ ( K ^ 2 ) ) e. NN0 )
8 5 6 7 sylancr 
 |-  ( K e. NN0 -> ( 2 ^ ( K ^ 2 ) ) e. NN0 )
9 8 adantl 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( 2 ^ ( K ^ 2 ) ) e. NN0 )
10 nn0addcl 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( M + K ) e. NN0 )
11 nn0expcl 
 |-  ( ( M e. NN0 /\ ( M + K ) e. NN0 ) -> ( M ^ ( M + K ) ) e. NN0 )
12 10 11 syldan 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( M ^ ( M + K ) ) e. NN0 )
13 9 12 nn0mulcld 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) e. NN0 )
14 4 13 sylan2 
 |-  ( ( M e. NN0 /\ K e. NN ) -> ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) e. NN0 )
15 14 nn0ge0d 
 |-  ( ( M e. NN0 /\ K e. NN ) -> 0 <_ ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) )
16 3 15 eqbrtrd 
 |-  ( ( M e. NN0 /\ K e. NN ) -> ( 0 ^ K ) <_ ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) )
17 1nn 
 |-  1 e. NN
18 elnn0 
 |-  ( M e. NN0 <-> ( M e. NN \/ M = 0 ) )
19 nnnn0 
 |-  ( M e. NN -> M e. NN0 )
20 0nn0 
 |-  0 e. NN0
21 nn0addcl 
 |-  ( ( M e. NN0 /\ 0 e. NN0 ) -> ( M + 0 ) e. NN0 )
22 19 20 21 sylancl 
 |-  ( M e. NN -> ( M + 0 ) e. NN0 )
23 nnexpcl 
 |-  ( ( M e. NN /\ ( M + 0 ) e. NN0 ) -> ( M ^ ( M + 0 ) ) e. NN )
24 22 23 mpdan 
 |-  ( M e. NN -> ( M ^ ( M + 0 ) ) e. NN )
25 id 
 |-  ( M = 0 -> M = 0 )
26 oveq1 
 |-  ( M = 0 -> ( M + 0 ) = ( 0 + 0 ) )
27 00id 
 |-  ( 0 + 0 ) = 0
28 26 27 eqtrdi 
 |-  ( M = 0 -> ( M + 0 ) = 0 )
29 25 28 oveq12d 
 |-  ( M = 0 -> ( M ^ ( M + 0 ) ) = ( 0 ^ 0 ) )
30 0exp0e1 
 |-  ( 0 ^ 0 ) = 1
31 29 30 eqtrdi 
 |-  ( M = 0 -> ( M ^ ( M + 0 ) ) = 1 )
32 31 17 eqeltrdi 
 |-  ( M = 0 -> ( M ^ ( M + 0 ) ) e. NN )
33 24 32 jaoi 
 |-  ( ( M e. NN \/ M = 0 ) -> ( M ^ ( M + 0 ) ) e. NN )
34 18 33 sylbi 
 |-  ( M e. NN0 -> ( M ^ ( M + 0 ) ) e. NN )
35 nnmulcl 
 |-  ( ( 1 e. NN /\ ( M ^ ( M + 0 ) ) e. NN ) -> ( 1 x. ( M ^ ( M + 0 ) ) ) e. NN )
36 17 34 35 sylancr 
 |-  ( M e. NN0 -> ( 1 x. ( M ^ ( M + 0 ) ) ) e. NN )
37 36 nnge1d 
 |-  ( M e. NN0 -> 1 <_ ( 1 x. ( M ^ ( M + 0 ) ) ) )
38 37 adantr 
 |-  ( ( M e. NN0 /\ K = 0 ) -> 1 <_ ( 1 x. ( M ^ ( M + 0 ) ) ) )
39 oveq2 
 |-  ( K = 0 -> ( 0 ^ K ) = ( 0 ^ 0 ) )
40 39 30 eqtrdi 
 |-  ( K = 0 -> ( 0 ^ K ) = 1 )
41 sq0i 
 |-  ( K = 0 -> ( K ^ 2 ) = 0 )
42 41 oveq2d 
 |-  ( K = 0 -> ( 2 ^ ( K ^ 2 ) ) = ( 2 ^ 0 ) )
43 2cn 
 |-  2 e. CC
44 exp0 
 |-  ( 2 e. CC -> ( 2 ^ 0 ) = 1 )
45 43 44 ax-mp 
 |-  ( 2 ^ 0 ) = 1
46 42 45 eqtrdi 
 |-  ( K = 0 -> ( 2 ^ ( K ^ 2 ) ) = 1 )
47 oveq2 
 |-  ( K = 0 -> ( M + K ) = ( M + 0 ) )
48 47 oveq2d 
 |-  ( K = 0 -> ( M ^ ( M + K ) ) = ( M ^ ( M + 0 ) ) )
49 46 48 oveq12d 
 |-  ( K = 0 -> ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) = ( 1 x. ( M ^ ( M + 0 ) ) ) )
50 40 49 breq12d 
 |-  ( K = 0 -> ( ( 0 ^ K ) <_ ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) <-> 1 <_ ( 1 x. ( M ^ ( M + 0 ) ) ) ) )
51 50 adantl 
 |-  ( ( M e. NN0 /\ K = 0 ) -> ( ( 0 ^ K ) <_ ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) <-> 1 <_ ( 1 x. ( M ^ ( M + 0 ) ) ) ) )
52 38 51 mpbird 
 |-  ( ( M e. NN0 /\ K = 0 ) -> ( 0 ^ K ) <_ ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) )
53 16 52 jaodan 
 |-  ( ( M e. NN0 /\ ( K e. NN \/ K = 0 ) ) -> ( 0 ^ K ) <_ ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) )
54 1 53 sylan2b 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( 0 ^ K ) <_ ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) )
55 nn0cn 
 |-  ( M e. NN0 -> M e. CC )
56 55 exp0d 
 |-  ( M e. NN0 -> ( M ^ 0 ) = 1 )
57 56 oveq2d 
 |-  ( M e. NN0 -> ( ( 0 ^ K ) x. ( M ^ 0 ) ) = ( ( 0 ^ K ) x. 1 ) )
58 nn0expcl 
 |-  ( ( 0 e. NN0 /\ K e. NN0 ) -> ( 0 ^ K ) e. NN0 )
59 20 58 mpan 
 |-  ( K e. NN0 -> ( 0 ^ K ) e. NN0 )
60 59 nn0cnd 
 |-  ( K e. NN0 -> ( 0 ^ K ) e. CC )
61 60 mulid1d 
 |-  ( K e. NN0 -> ( ( 0 ^ K ) x. 1 ) = ( 0 ^ K ) )
62 57 61 sylan9eq 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( ( 0 ^ K ) x. ( M ^ 0 ) ) = ( 0 ^ K ) )
63 13 nn0cnd 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) e. CC )
64 63 mulid1d 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. 1 ) = ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) )
65 54 62 64 3brtr4d 
 |-  ( ( M e. NN0 /\ K e. NN0 ) -> ( ( 0 ^ K ) x. ( M ^ 0 ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. 1 ) )
66 65 adantr 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ N = 0 ) -> ( ( 0 ^ K ) x. ( M ^ 0 ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. 1 ) )
67 oveq1 
 |-  ( N = 0 -> ( N ^ K ) = ( 0 ^ K ) )
68 oveq2 
 |-  ( N = 0 -> ( M ^ N ) = ( M ^ 0 ) )
69 67 68 oveq12d 
 |-  ( N = 0 -> ( ( N ^ K ) x. ( M ^ N ) ) = ( ( 0 ^ K ) x. ( M ^ 0 ) ) )
70 fveq2 
 |-  ( N = 0 -> ( ! ` N ) = ( ! ` 0 ) )
71 fac0 
 |-  ( ! ` 0 ) = 1
72 70 71 eqtrdi 
 |-  ( N = 0 -> ( ! ` N ) = 1 )
73 72 oveq2d 
 |-  ( N = 0 -> ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) = ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. 1 ) )
74 69 73 breq12d 
 |-  ( N = 0 -> ( ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) <-> ( ( 0 ^ K ) x. ( M ^ 0 ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. 1 ) ) )
75 74 adantl 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ N = 0 ) -> ( ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) <-> ( ( 0 ^ K ) x. ( M ^ 0 ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. 1 ) ) )
76 66 75 mpbird 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ N = 0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )