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 ) )