Metamath Proof Explorer

Theorem faclbnd4

Description: Variant of faclbnd5 providing a non-strict lower bound. (Contributed by NM, 23-Dec-2005)

Ref Expression
Assertion faclbnd4 
|- ( ( N e. NN0 /\ 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 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 faclbnd4lem4 
 |-  ( ( N e. NN /\ K e. NN0 /\ M e. NN0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
3 2 3com13 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ N e. NN ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
4 3 3expa 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ N e. NN ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
5 faclbnd4lem3 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ N = 0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
6 4 5 jaodan 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ ( N e. NN \/ N = 0 ) ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
7 1 6 sylan2b 
 |-  ( ( ( M e. NN0 /\ K e. NN0 ) /\ N e. NN0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
8 7 3impa 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ N e. NN0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )
9 8 3com13 
 |-  ( ( N e. NN0 /\ K e. NN0 /\ M e. NN0 ) -> ( ( N ^ K ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` N ) ) )