Metamath Proof Explorer

Theorem expmulnbnd

Description: Exponentiation with a base greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion expmulnbnd 
|- ( ( A e. RR /\ B e. RR /\ 1 < B ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( A x. k ) < ( B ^ k ) )

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> A e. RR )
3 remulcl 
 |-  ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
4 1 2 3 sylancr 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 2 x. A ) e. RR )
5 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 1 < B )
6 1re 
 |-  1 e. RR
7 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> B e. RR )
8 difrp 
 |-  ( ( 1 e. RR /\ B e. RR ) -> ( 1 < B <-> ( B - 1 ) e. RR+ ) )
9 6 7 8 sylancr 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 < B <-> ( B - 1 ) e. RR+ ) )
10 5 9 mpbid 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( B - 1 ) e. RR+ )
11 4 10 rerpdivcld 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( ( 2 x. A ) / ( B - 1 ) ) e. RR )
12 expnbnd 
 |-  ( ( ( ( 2 x. A ) / ( B - 1 ) ) e. RR /\ B e. RR /\ 1 < B ) -> E. n e. NN ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) )
13 11 7 5 12 syl3anc 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> E. n e. NN ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) )
14 2nn0 
 |-  2 e. NN0
15 nnnn0 
 |-  ( n e. NN -> n e. NN0 )
16 15 ad2antrl 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) -> n e. NN0 )
17 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ n e. NN0 ) -> ( 2 x. n ) e. NN0 )
18 14 16 17 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) -> ( 2 x. n ) e. NN0 )
19 2 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> A e. RR )
20 2nn 
 |-  2 e. NN
21 simprl 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) -> n e. NN )
22 nnmulcl 
 |-  ( ( 2 e. NN /\ n e. NN ) -> ( 2 x. n ) e. NN )
23 20 21 22 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) -> ( 2 x. n ) e. NN )
24 eluznn 
 |-  ( ( ( 2 x. n ) e. NN /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. NN )
25 23 24 sylan 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. NN )
26 25 nnred 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. RR )
27 19 26 remulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( A x. k ) e. RR )
28 0re 
 |-  0 e. RR
29 ifcl 
 |-  ( ( A e. RR /\ 0 e. RR ) -> if ( 0 <_ A , A , 0 ) e. RR )
30 19 28 29 sylancl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> if ( 0 <_ A , A , 0 ) e. RR )
31 remulcl 
 |-  ( ( 2 e. RR /\ if ( 0 <_ A , A , 0 ) e. RR ) -> ( 2 x. if ( 0 <_ A , A , 0 ) ) e. RR )
32 1 30 31 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. if ( 0 <_ A , A , 0 ) ) e. RR )
33 simplrl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> n e. NN )
34 33 nnred 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> n e. RR )
35 26 34 resubcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k - n ) e. RR )
36 32 35 remulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) e. RR )
37 7 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> B e. RR )
38 25 nnnn0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. NN0 )
39 reexpcl 
 |-  ( ( B e. RR /\ k e. NN0 ) -> ( B ^ k ) e. RR )
40 37 38 39 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B ^ k ) e. RR )
41 remulcl 
 |-  ( ( 2 e. RR /\ ( k - n ) e. RR ) -> ( 2 x. ( k - n ) ) e. RR )
42 1 35 41 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. ( k - n ) ) e. RR )
43 38 nn0ge0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 <_ k )
44 max1 
 |-  ( ( 0 e. RR /\ A e. RR ) -> 0 <_ if ( 0 <_ A , A , 0 ) )
45 28 19 44 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 <_ if ( 0 <_ A , A , 0 ) )
46 remulcl 
 |-  ( ( 2 e. RR /\ n e. RR ) -> ( 2 x. n ) e. RR )
47 1 34 46 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. n ) e. RR )
48 eluzle 
 |-  ( k e. ( ZZ>= ` ( 2 x. n ) ) -> ( 2 x. n ) <_ k )
49 48 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. n ) <_ k )
50 47 26 26 49 leadd2dd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k + ( 2 x. n ) ) <_ ( k + k ) )
51 26 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. CC )
52 51 2timesd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. k ) = ( k + k ) )
53 50 52 breqtrrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k + ( 2 x. n ) ) <_ ( 2 x. k ) )
54 remulcl 
 |-  ( ( 2 e. RR /\ k e. RR ) -> ( 2 x. k ) e. RR )
55 1 26 54 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. k ) e. RR )
56 leaddsub 
 |-  ( ( k e. RR /\ ( 2 x. n ) e. RR /\ ( 2 x. k ) e. RR ) -> ( ( k + ( 2 x. n ) ) <_ ( 2 x. k ) <-> k <_ ( ( 2 x. k ) - ( 2 x. n ) ) ) )
57 26 47 55 56 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( k + ( 2 x. n ) ) <_ ( 2 x. k ) <-> k <_ ( ( 2 x. k ) - ( 2 x. n ) ) ) )
58 53 57 mpbid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k <_ ( ( 2 x. k ) - ( 2 x. n ) ) )
59 2cnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 2 e. CC )
60 34 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> n e. CC )
61 59 51 60 subdid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. ( k - n ) ) = ( ( 2 x. k ) - ( 2 x. n ) ) )
62 58 61 breqtrrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k <_ ( 2 x. ( k - n ) ) )
63 max2 
 |-  ( ( 0 e. RR /\ A e. RR ) -> A <_ if ( 0 <_ A , A , 0 ) )
64 28 19 63 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> A <_ if ( 0 <_ A , A , 0 ) )
65 26 42 19 30 43 45 62 64 lemul12bd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k x. A ) <_ ( ( 2 x. ( k - n ) ) x. if ( 0 <_ A , A , 0 ) ) )
66 19 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> A e. CC )
67 66 51 mulcomd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( A x. k ) = ( k x. A ) )
68 30 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> if ( 0 <_ A , A , 0 ) e. CC )
69 35 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k - n ) e. CC )
70 59 68 69 mul32d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) = ( ( 2 x. ( k - n ) ) x. if ( 0 <_ A , A , 0 ) ) )
71 65 67 70 3brtr4d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( A x. k ) <_ ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) )
72 10 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B - 1 ) e. RR+ )
73 72 rpred 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B - 1 ) e. RR )
74 73 35 remulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( B - 1 ) x. ( k - n ) ) e. RR )
75 33 nnnn0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> n e. NN0 )
76 reexpcl 
 |-  ( ( B e. RR /\ n e. NN0 ) -> ( B ^ n ) e. RR )
77 37 75 76 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B ^ n ) e. RR )
78 74 77 remulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( ( B - 1 ) x. ( k - n ) ) x. ( B ^ n ) ) e. RR )
79 simplrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) )
80 1 19 3 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. A ) e. RR )
81 80 77 72 ltdivmuld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) <-> ( 2 x. A ) < ( ( B - 1 ) x. ( B ^ n ) ) ) )
82 79 81 mpbid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. A ) < ( ( B - 1 ) x. ( B ^ n ) ) )
83 5 ad2antrr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 1 < B )
84 posdif 
 |-  ( ( 1 e. RR /\ B e. RR ) -> ( 1 < B <-> 0 < ( B - 1 ) ) )
85 6 37 84 sylancr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 1 < B <-> 0 < ( B - 1 ) ) )
86 83 85 mpbid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 < ( B - 1 ) )
87 33 nnzd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> n e. ZZ )
88 28 a1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 e. RR )
89 6 a1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 1 e. RR )
90 0lt1 
 |-  0 < 1
91 90 a1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 < 1 )
92 88 89 37 91 83 lttrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 < B )
93 expgt0 
 |-  ( ( B e. RR /\ n e. ZZ /\ 0 < B ) -> 0 < ( B ^ n ) )
94 37 87 92 93 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 < ( B ^ n ) )
95 73 77 86 94 mulgt0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 < ( ( B - 1 ) x. ( B ^ n ) ) )
96 oveq2 
 |-  ( A = if ( 0 <_ A , A , 0 ) -> ( 2 x. A ) = ( 2 x. if ( 0 <_ A , A , 0 ) ) )
97 96 breq1d 
 |-  ( A = if ( 0 <_ A , A , 0 ) -> ( ( 2 x. A ) < ( ( B - 1 ) x. ( B ^ n ) ) <-> ( 2 x. if ( 0 <_ A , A , 0 ) ) < ( ( B - 1 ) x. ( B ^ n ) ) ) )
98 2t0e0 
 |-  ( 2 x. 0 ) = 0
99 oveq2 
 |-  ( 0 = if ( 0 <_ A , A , 0 ) -> ( 2 x. 0 ) = ( 2 x. if ( 0 <_ A , A , 0 ) ) )
100 98 99 eqtr3id 
 |-  ( 0 = if ( 0 <_ A , A , 0 ) -> 0 = ( 2 x. if ( 0 <_ A , A , 0 ) ) )
101 100 breq1d 
 |-  ( 0 = if ( 0 <_ A , A , 0 ) -> ( 0 < ( ( B - 1 ) x. ( B ^ n ) ) <-> ( 2 x. if ( 0 <_ A , A , 0 ) ) < ( ( B - 1 ) x. ( B ^ n ) ) ) )
102 97 101 ifboth 
 |-  ( ( ( 2 x. A ) < ( ( B - 1 ) x. ( B ^ n ) ) /\ 0 < ( ( B - 1 ) x. ( B ^ n ) ) ) -> ( 2 x. if ( 0 <_ A , A , 0 ) ) < ( ( B - 1 ) x. ( B ^ n ) ) )
103 82 95 102 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. if ( 0 <_ A , A , 0 ) ) < ( ( B - 1 ) x. ( B ^ n ) ) )
104 73 77 remulcld 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( B - 1 ) x. ( B ^ n ) ) e. RR )
105 simpr 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. ( ZZ>= ` ( 2 x. n ) ) )
106 60 2timesd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( 2 x. n ) = ( n + n ) )
107 106 fveq2d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ZZ>= ` ( 2 x. n ) ) = ( ZZ>= ` ( n + n ) ) )
108 105 107 eleqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. ( ZZ>= ` ( n + n ) ) )
109 eluzsub 
 |-  ( ( n e. ZZ /\ n e. ZZ /\ k e. ( ZZ>= ` ( n + n ) ) ) -> ( k - n ) e. ( ZZ>= ` n ) )
110 87 87 108 109 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k - n ) e. ( ZZ>= ` n ) )
111 eluznn 
 |-  ( ( n e. NN /\ ( k - n ) e. ( ZZ>= ` n ) ) -> ( k - n ) e. NN )
112 33 110 111 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k - n ) e. NN )
113 112 nngt0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 < ( k - n ) )
114 ltmul1 
 |-  ( ( ( 2 x. if ( 0 <_ A , A , 0 ) ) e. RR /\ ( ( B - 1 ) x. ( B ^ n ) ) e. RR /\ ( ( k - n ) e. RR /\ 0 < ( k - n ) ) ) -> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) < ( ( B - 1 ) x. ( B ^ n ) ) <-> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) < ( ( ( B - 1 ) x. ( B ^ n ) ) x. ( k - n ) ) ) )
115 32 104 35 113 114 syl112anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) < ( ( B - 1 ) x. ( B ^ n ) ) <-> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) < ( ( ( B - 1 ) x. ( B ^ n ) ) x. ( k - n ) ) ) )
116 103 115 mpbid 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) < ( ( ( B - 1 ) x. ( B ^ n ) ) x. ( k - n ) ) )
117 73 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B - 1 ) e. CC )
118 77 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B ^ n ) e. CC )
119 117 118 69 mul32d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( ( B - 1 ) x. ( B ^ n ) ) x. ( k - n ) ) = ( ( ( B - 1 ) x. ( k - n ) ) x. ( B ^ n ) ) )
120 116 119 breqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) < ( ( ( B - 1 ) x. ( k - n ) ) x. ( B ^ n ) ) )
121 peano2re 
 |-  ( ( ( B - 1 ) x. ( k - n ) ) e. RR -> ( ( ( B - 1 ) x. ( k - n ) ) + 1 ) e. RR )
122 74 121 syl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( ( B - 1 ) x. ( k - n ) ) + 1 ) e. RR )
123 112 nnnn0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( k - n ) e. NN0 )
124 reexpcl 
 |-  ( ( B e. RR /\ ( k - n ) e. NN0 ) -> ( B ^ ( k - n ) ) e. RR )
125 37 123 124 syl2anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B ^ ( k - n ) ) e. RR )
126 74 ltp1d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( B - 1 ) x. ( k - n ) ) < ( ( ( B - 1 ) x. ( k - n ) ) + 1 ) )
127 88 37 92 ltled 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> 0 <_ B )
128 bernneq2 
 |-  ( ( B e. RR /\ ( k - n ) e. NN0 /\ 0 <_ B ) -> ( ( ( B - 1 ) x. ( k - n ) ) + 1 ) <_ ( B ^ ( k - n ) ) )
129 37 123 127 128 syl3anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( ( B - 1 ) x. ( k - n ) ) + 1 ) <_ ( B ^ ( k - n ) ) )
130 74 122 125 126 129 ltletrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( B - 1 ) x. ( k - n ) ) < ( B ^ ( k - n ) ) )
131 37 recnd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> B e. CC )
132 92 gt0ne0d 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> B =/= 0 )
133 eluzelz 
 |-  ( k e. ( ZZ>= ` ( 2 x. n ) ) -> k e. ZZ )
134 133 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> k e. ZZ )
135 expsub 
 |-  ( ( ( B e. CC /\ B =/= 0 ) /\ ( k e. ZZ /\ n e. ZZ ) ) -> ( B ^ ( k - n ) ) = ( ( B ^ k ) / ( B ^ n ) ) )
136 131 132 134 87 135 syl22anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( B ^ ( k - n ) ) = ( ( B ^ k ) / ( B ^ n ) ) )
137 130 136 breqtrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( B - 1 ) x. ( k - n ) ) < ( ( B ^ k ) / ( B ^ n ) ) )
138 ltmuldiv 
 |-  ( ( ( ( B - 1 ) x. ( k - n ) ) e. RR /\ ( B ^ k ) e. RR /\ ( ( B ^ n ) e. RR /\ 0 < ( B ^ n ) ) ) -> ( ( ( ( B - 1 ) x. ( k - n ) ) x. ( B ^ n ) ) < ( B ^ k ) <-> ( ( B - 1 ) x. ( k - n ) ) < ( ( B ^ k ) / ( B ^ n ) ) ) )
139 74 40 77 94 138 syl112anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( ( ( B - 1 ) x. ( k - n ) ) x. ( B ^ n ) ) < ( B ^ k ) <-> ( ( B - 1 ) x. ( k - n ) ) < ( ( B ^ k ) / ( B ^ n ) ) ) )
140 137 139 mpbird 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( ( B - 1 ) x. ( k - n ) ) x. ( B ^ n ) ) < ( B ^ k ) )
141 36 78 40 120 140 lttrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( ( 2 x. if ( 0 <_ A , A , 0 ) ) x. ( k - n ) ) < ( B ^ k ) )
142 27 36 40 71 141 lelttrd 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) /\ k e. ( ZZ>= ` ( 2 x. n ) ) ) -> ( A x. k ) < ( B ^ k ) )
143 142 ralrimiva 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) -> A. k e. ( ZZ>= ` ( 2 x. n ) ) ( A x. k ) < ( B ^ k ) )
144 fveq2 
 |-  ( j = ( 2 x. n ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( 2 x. n ) ) )
145 144 raleqdv 
 |-  ( j = ( 2 x. n ) -> ( A. k e. ( ZZ>= ` j ) ( A x. k ) < ( B ^ k ) <-> A. k e. ( ZZ>= ` ( 2 x. n ) ) ( A x. k ) < ( B ^ k ) ) )
146 145 rspcev 
 |-  ( ( ( 2 x. n ) e. NN0 /\ A. k e. ( ZZ>= ` ( 2 x. n ) ) ( A x. k ) < ( B ^ k ) ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( A x. k ) < ( B ^ k ) )
147 18 143 146 syl2anc 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. NN /\ ( ( 2 x. A ) / ( B - 1 ) ) < ( B ^ n ) ) ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( A x. k ) < ( B ^ k ) )
148 13 147 rexlimddv 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> E. j e. NN0 A. k e. ( ZZ>= ` j ) ( A x. k ) < ( B ^ k ) )