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

Metamath Proof Explorer

Theorem faclbnd4lem2

Description: Lemma for faclbnd4 . Use the weak deduction theorem to convert the hypotheses of faclbnd4lem1 to antecedents. (Contributed by NM, 23-Dec-2005)

Ref Expression
Assertion faclbnd4lem2 
|- ( ( M e. NN0 /\ K e. NN0 /\ N e. NN ) -> ( ( ( ( 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

Step Hyp Ref Expression
1 oveq1 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( M ^ ( N - 1 ) ) = ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) )
2 1 oveq2d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( ( N - 1 ) ^ K ) x. ( M ^ ( N - 1 ) ) ) = ( ( ( N - 1 ) ^ K ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) )
3 id 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> M = if ( M e. NN0 , M , 1 ) )
4 oveq1 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( M + K ) = ( if ( M e. NN0 , M , 1 ) + K ) )
5 3 4 oveq12d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( M ^ ( M + K ) ) = ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) )
6 5 oveq2d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) = ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) )
7 6 oveq1d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` ( N - 1 ) ) ) = ( ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) x. ( ! ` ( N - 1 ) ) ) )
8 2 7 breq12d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( ( ( N - 1 ) ^ K ) x. ( M ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( M ^ ( M + K ) ) ) x. ( ! ` ( N - 1 ) ) ) <-> ( ( ( N - 1 ) ^ K ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) x. ( ! ` ( N - 1 ) ) ) ) )
9 oveq1 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( M ^ N ) = ( if ( M e. NN0 , M , 1 ) ^ N ) )
10 9 oveq2d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( N ^ ( K + 1 ) ) x. ( M ^ N ) ) = ( ( N ^ ( K + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) )
11 oveq1 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( M + ( K + 1 ) ) = ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) )
12 3 11 oveq12d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( M ^ ( M + ( K + 1 ) ) ) = ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) )
13 12 oveq2d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( K + 1 ) ) ) ) = ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) )
14 13 oveq1d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( K + 1 ) ) ) ) x. ( ! ` N ) ) = ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) x. ( ! ` N ) ) )
15 10 14 breq12d 
 |-  ( M = if ( M e. NN0 , M , 1 ) -> ( ( ( N ^ ( K + 1 ) ) x. ( M ^ N ) ) <_ ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( M ^ ( M + ( K + 1 ) ) ) ) x. ( ! ` N ) ) <-> ( ( N ^ ( K + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) x. ( ! ` N ) ) ) )
16 8 15 imbi12d 
 |-  ( M = if ( M e. NN0 , M , 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 ) ) ) <-> ( ( ( ( N - 1 ) ^ K ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) x. ( ! ` ( N - 1 ) ) ) -> ( ( N ^ ( K + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) x. ( ! ` N ) ) ) ) )
17 oveq2 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( N - 1 ) ^ K ) = ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) )
18 17 oveq1d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( ( N - 1 ) ^ K ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) = ( ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) )
19 oveq1 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( K ^ 2 ) = ( if ( K e. NN0 , K , 1 ) ^ 2 ) )
20 19 oveq2d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( 2 ^ ( K ^ 2 ) ) = ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) )
21 oveq2 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( if ( M e. NN0 , M , 1 ) + K ) = ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) )
22 21 oveq2d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) = ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) )
23 20 22 oveq12d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) = ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) )
24 23 oveq1d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) x. ( ! ` ( N - 1 ) ) ) = ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( N - 1 ) ) ) )
25 18 24 breq12d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( ( ( N - 1 ) ^ K ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) x. ( ! ` ( N - 1 ) ) ) <-> ( ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( N - 1 ) ) ) ) )
26 oveq1 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( K + 1 ) = ( if ( K e. NN0 , K , 1 ) + 1 ) )
27 26 oveq2d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( N ^ ( K + 1 ) ) = ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) )
28 27 oveq1d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( N ^ ( K + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) = ( ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) )
29 26 oveq1d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( K + 1 ) ^ 2 ) = ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) )
30 29 oveq2d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( 2 ^ ( ( K + 1 ) ^ 2 ) ) = ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) )
31 26 oveq2d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) = ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) )
32 31 oveq2d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) = ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) )
33 30 32 oveq12d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) = ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) )
34 33 oveq1d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) x. ( ! ` N ) ) = ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` N ) ) )
35 28 34 breq12d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( ( N ^ ( K + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) x. ( ! ` N ) ) <-> ( ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` N ) ) ) )
36 25 35 imbi12d 
 |-  ( K = if ( K e. NN0 , K , 1 ) -> ( ( ( ( ( N - 1 ) ^ K ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( K ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + K ) ) ) x. ( ! ` ( N - 1 ) ) ) -> ( ( N ^ ( K + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( K + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( K + 1 ) ) ) ) x. ( ! ` N ) ) ) <-> ( ( ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( N - 1 ) ) ) -> ( ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` N ) ) ) ) )
37 oveq1 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( N - 1 ) = ( if ( N e. NN , N , 1 ) - 1 ) )
38 37 oveq1d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) = ( ( if ( N e. NN , N , 1 ) - 1 ) ^ if ( K e. NN0 , K , 1 ) ) )
39 37 oveq2d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) = ( if ( M e. NN0 , M , 1 ) ^ ( if ( N e. NN , N , 1 ) - 1 ) ) )
40 38 39 oveq12d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) = ( ( ( if ( N e. NN , N , 1 ) - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( N e. NN , N , 1 ) - 1 ) ) ) )
41 fvoveq1 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ! ` ( N - 1 ) ) = ( ! ` ( if ( N e. NN , N , 1 ) - 1 ) ) )
42 41 oveq2d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( N - 1 ) ) ) = ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( if ( N e. NN , N , 1 ) - 1 ) ) ) )
43 40 42 breq12d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( N - 1 ) ) ) <-> ( ( ( if ( N e. NN , N , 1 ) - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( N e. NN , N , 1 ) - 1 ) ) ) <_ ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( if ( N e. NN , N , 1 ) - 1 ) ) ) ) )
44 oveq1 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) = ( if ( N e. NN , N , 1 ) ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) )
45 oveq2 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( if ( M e. NN0 , M , 1 ) ^ N ) = ( if ( M e. NN0 , M , 1 ) ^ if ( N e. NN , N , 1 ) ) )
46 44 45 oveq12d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) = ( ( if ( N e. NN , N , 1 ) ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ if ( N e. NN , N , 1 ) ) ) )
47 fveq2 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ! ` N ) = ( ! ` if ( N e. NN , N , 1 ) ) )
48 47 oveq2d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` N ) ) = ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` if ( N e. NN , N , 1 ) ) ) )
49 46 48 breq12d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` N ) ) <-> ( ( if ( N e. NN , N , 1 ) ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ if ( N e. NN , N , 1 ) ) ) <_ ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` if ( N e. NN , N , 1 ) ) ) ) )
50 43 49 imbi12d 
 |-  ( N = if ( N e. NN , N , 1 ) -> ( ( ( ( ( N - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( N - 1 ) ) ) <_ ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( N - 1 ) ) ) -> ( ( N ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ N ) ) <_ ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` N ) ) ) <-> ( ( ( ( if ( N e. NN , N , 1 ) - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( N e. NN , N , 1 ) - 1 ) ) ) <_ ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( if ( N e. NN , N , 1 ) - 1 ) ) ) -> ( ( if ( N e. NN , N , 1 ) ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ if ( N e. NN , N , 1 ) ) ) <_ ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` if ( N e. NN , N , 1 ) ) ) ) ) )
51 1nn 
 |-  1 e. NN
52 51 elimel 
 |-  if ( N e. NN , N , 1 ) e. NN
53 1nn0 
 |-  1 e. NN0
54 53 elimel 
 |-  if ( K e. NN0 , K , 1 ) e. NN0
55 53 elimel 
 |-  if ( M e. NN0 , M , 1 ) e. NN0
56 52 54 55 faclbnd4lem1 
 |-  ( ( ( ( if ( N e. NN , N , 1 ) - 1 ) ^ if ( K e. NN0 , K , 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( N e. NN , N , 1 ) - 1 ) ) ) <_ ( ( ( 2 ^ ( if ( K e. NN0 , K , 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + if ( K e. NN0 , K , 1 ) ) ) ) x. ( ! ` ( if ( N e. NN , N , 1 ) - 1 ) ) ) -> ( ( if ( N e. NN , N , 1 ) ^ ( if ( K e. NN0 , K , 1 ) + 1 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ if ( N e. NN , N , 1 ) ) ) <_ ( ( ( 2 ^ ( ( if ( K e. NN0 , K , 1 ) + 1 ) ^ 2 ) ) x. ( if ( M e. NN0 , M , 1 ) ^ ( if ( M e. NN0 , M , 1 ) + ( if ( K e. NN0 , K , 1 ) + 1 ) ) ) ) x. ( ! ` if ( N e. NN , N , 1 ) ) ) )
57 16 36 50 56 dedth3h 
 |-  ( ( M e. NN0 /\ K e. NN0 /\ N e. NN ) -> ( ( ( ( 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 ) ) ) )