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

Metamath Proof Explorer

Theorem cxp2lim

Description: Any power grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Assertion cxp2lim 
|- ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) ~~>r 0 )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 elicopnf 
 |-  ( 1 e. RR -> ( n e. ( 1 [,) +oo ) <-> ( n e. RR /\ 1 <_ n ) ) )
3 1 2 ax-mp 
 |-  ( n e. ( 1 [,) +oo ) <-> ( n e. RR /\ 1 <_ n ) )
4 3 simplbi 
 |-  ( n e. ( 1 [,) +oo ) -> n e. RR )
5 0red 
 |-  ( n e. ( 1 [,) +oo ) -> 0 e. RR )
6 1red 
 |-  ( n e. ( 1 [,) +oo ) -> 1 e. RR )
7 0lt1 
 |-  0 < 1
8 7 a1i 
 |-  ( n e. ( 1 [,) +oo ) -> 0 < 1 )
9 3 simprbi 
 |-  ( n e. ( 1 [,) +oo ) -> 1 <_ n )
10 5 6 4 8 9 ltletrd 
 |-  ( n e. ( 1 [,) +oo ) -> 0 < n )
11 4 10 elrpd 
 |-  ( n e. ( 1 [,) +oo ) -> n e. RR+ )
12 11 ssriv 
 |-  ( 1 [,) +oo ) C_ RR+
13 resmpt 
 |-  ( ( 1 [,) +oo ) C_ RR+ -> ( ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) |` ( 1 [,) +oo ) ) = ( n e. ( 1 [,) +oo ) |-> ( ( n ^c A ) / ( B ^c n ) ) ) )
14 12 13 ax-mp 
 |-  ( ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) |` ( 1 [,) +oo ) ) = ( n e. ( 1 [,) +oo ) |-> ( ( n ^c A ) / ( B ^c n ) ) )
15 0red 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 0 e. RR )
16 12 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 [,) +oo ) C_ RR+ )
17 rpre 
 |-  ( n e. RR+ -> n e. RR )
18 17 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> n e. RR )
19 rpge0 
 |-  ( n e. RR+ -> 0 <_ n )
20 19 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> 0 <_ n )
21 simpl2 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> B e. RR )
22 0red 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> 0 e. RR )
23 1red 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> 1 e. RR )
24 7 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> 0 < 1 )
25 simpl3 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> 1 < B )
26 22 23 21 24 25 lttrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> 0 < B )
27 21 26 elrpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> B e. RR+ )
28 27 18 rpcxpcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( B ^c n ) e. RR+ )
29 simp1 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> A e. RR )
30 ifcl 
 |-  ( ( A e. RR /\ 1 e. RR ) -> if ( 1 <_ A , A , 1 ) e. RR )
31 29 1 30 sylancl 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> if ( 1 <_ A , A , 1 ) e. RR )
32 1red 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 1 e. RR )
33 7 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 0 < 1 )
34 max1 
 |-  ( ( 1 e. RR /\ A e. RR ) -> 1 <_ if ( 1 <_ A , A , 1 ) )
35 1 29 34 sylancr 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 1 <_ if ( 1 <_ A , A , 1 ) )
36 15 32 31 33 35 ltletrd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 0 < if ( 1 <_ A , A , 1 ) )
37 31 36 elrpd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> if ( 1 <_ A , A , 1 ) e. RR+ )
38 37 rprecred 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 / if ( 1 <_ A , A , 1 ) ) e. RR )
39 38 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( 1 / if ( 1 <_ A , A , 1 ) ) e. RR )
40 28 39 rpcxpcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) e. RR+ )
41 31 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> if ( 1 <_ A , A , 1 ) e. CC )
42 41 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> if ( 1 <_ A , A , 1 ) e. CC )
43 18 20 40 42 divcxpd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) ^c if ( 1 <_ A , A , 1 ) ) = ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c if ( 1 <_ A , A , 1 ) ) ) )
44 37 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> if ( 1 <_ A , A , 1 ) e. RR+ )
45 44 rpne0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> if ( 1 <_ A , A , 1 ) =/= 0 )
46 42 45 recid2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( 1 / if ( 1 <_ A , A , 1 ) ) x. if ( 1 <_ A , A , 1 ) ) = 1 )
47 46 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( B ^c n ) ^c ( ( 1 / if ( 1 <_ A , A , 1 ) ) x. if ( 1 <_ A , A , 1 ) ) ) = ( ( B ^c n ) ^c 1 ) )
48 28 39 42 cxpmuld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( B ^c n ) ^c ( ( 1 / if ( 1 <_ A , A , 1 ) ) x. if ( 1 <_ A , A , 1 ) ) ) = ( ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c if ( 1 <_ A , A , 1 ) ) )
49 28 rpcnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( B ^c n ) e. CC )
50 49 cxp1d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( B ^c n ) ^c 1 ) = ( B ^c n ) )
51 47 48 50 3eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c if ( 1 <_ A , A , 1 ) ) = ( B ^c n ) )
52 51 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c if ( 1 <_ A , A , 1 ) ) ) = ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) )
53 43 52 eqtrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) ^c if ( 1 <_ A , A , 1 ) ) = ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) )
54 53 mpteq2dva 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) ^c if ( 1 <_ A , A , 1 ) ) ) = ( n e. RR+ |-> ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) ) )
55 ovexd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) e. _V )
56 18 recnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> n e. CC )
57 38 recnd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 / if ( 1 <_ A , A , 1 ) ) e. CC )
58 57 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( 1 / if ( 1 <_ A , A , 1 ) ) e. CC )
59 56 58 mulcomd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( n x. ( 1 / if ( 1 <_ A , A , 1 ) ) ) = ( ( 1 / if ( 1 <_ A , A , 1 ) ) x. n ) )
60 59 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( B ^c ( n x. ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) = ( B ^c ( ( 1 / if ( 1 <_ A , A , 1 ) ) x. n ) ) )
61 27 18 58 cxpmuld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( B ^c ( n x. ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) = ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) )
62 27 39 56 cxpmuld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( B ^c ( ( 1 / if ( 1 <_ A , A , 1 ) ) x. n ) ) = ( ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c n ) )
63 60 61 62 3eqtr3d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) = ( ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c n ) )
64 63 oveq2d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) = ( n / ( ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c n ) ) )
65 64 mpteq2dva 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) ) = ( n e. RR+ |-> ( n / ( ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c n ) ) ) )
66 simp2 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> B e. RR )
67 simp3 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 1 < B )
68 15 32 66 33 67 lttrd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 0 < B )
69 66 68 elrpd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> B e. RR+ )
70 69 38 rpcxpcld 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) e. RR+ )
71 70 rpred 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) e. RR )
72 57 1cxpd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) = 1 )
73 0le1 
 |-  0 <_ 1
74 73 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 0 <_ 1 )
75 69 rpge0d 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 0 <_ B )
76 37 rpreccld 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 / if ( 1 <_ A , A , 1 ) ) e. RR+ )
77 32 74 66 75 76 cxplt2d 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 < B <-> ( 1 ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) < ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) )
78 67 77 mpbid 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( 1 ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) < ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) )
79 72 78 eqbrtrrd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> 1 < ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) )
80 cxp2limlem 
 |-  ( ( ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) e. RR /\ 1 < ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) -> ( n e. RR+ |-> ( n / ( ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c n ) ) ) ~~>r 0 )
81 71 79 80 syl2anc 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( n / ( ( B ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ^c n ) ) ) ~~>r 0 )
82 65 81 eqbrtrd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) ) ~~>r 0 )
83 55 82 37 rlimcxp 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( ( n / ( ( B ^c n ) ^c ( 1 / if ( 1 <_ A , A , 1 ) ) ) ) ^c if ( 1 <_ A , A , 1 ) ) ) ~~>r 0 )
84 54 83 eqbrtrrd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) ) ~~>r 0 )
85 16 84 rlimres2 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. ( 1 [,) +oo ) |-> ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) ) ~~>r 0 )
86 simpr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> n e. RR+ )
87 31 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> if ( 1 <_ A , A , 1 ) e. RR )
88 86 87 rpcxpcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( n ^c if ( 1 <_ A , A , 1 ) ) e. RR+ )
89 88 28 rpdivcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) e. RR+ )
90 89 rpred 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) e. RR )
91 11 90 sylan2 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) e. RR )
92 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> A e. RR )
93 86 92 rpcxpcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( n ^c A ) e. RR+ )
94 93 28 rpdivcld 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( n ^c A ) / ( B ^c n ) ) e. RR+ )
95 11 94 sylan2 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( ( n ^c A ) / ( B ^c n ) ) e. RR+ )
96 95 rpred 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( ( n ^c A ) / ( B ^c n ) ) e. RR )
97 11 93 sylan2 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( n ^c A ) e. RR+ )
98 97 rpred 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( n ^c A ) e. RR )
99 11 88 sylan2 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( n ^c if ( 1 <_ A , A , 1 ) ) e. RR+ )
100 99 rpred 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( n ^c if ( 1 <_ A , A , 1 ) ) e. RR )
101 11 28 sylan2 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( B ^c n ) e. RR+ )
102 4 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> n e. RR )
103 9 adantl 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> 1 <_ n )
104 simpl1 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> A e. RR )
105 31 adantr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> if ( 1 <_ A , A , 1 ) e. RR )
106 max2 
 |-  ( ( 1 e. RR /\ A e. RR ) -> A <_ if ( 1 <_ A , A , 1 ) )
107 1 104 106 sylancr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> A <_ if ( 1 <_ A , A , 1 ) )
108 102 103 104 105 107 cxplead 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( n ^c A ) <_ ( n ^c if ( 1 <_ A , A , 1 ) ) )
109 98 100 101 108 lediv1dd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> ( ( n ^c A ) / ( B ^c n ) ) <_ ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) )
110 109 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. ( 1 [,) +oo ) /\ 0 <_ n ) ) -> ( ( n ^c A ) / ( B ^c n ) ) <_ ( ( n ^c if ( 1 <_ A , A , 1 ) ) / ( B ^c n ) ) )
111 95 rpge0d 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. ( 1 [,) +oo ) ) -> 0 <_ ( ( n ^c A ) / ( B ^c n ) ) )
112 111 adantrr 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ ( n e. ( 1 [,) +oo ) /\ 0 <_ n ) ) -> 0 <_ ( ( n ^c A ) / ( B ^c n ) ) )
113 15 15 85 91 96 110 112 rlimsqz2 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. ( 1 [,) +oo ) |-> ( ( n ^c A ) / ( B ^c n ) ) ) ~~>r 0 )
114 14 113 eqbrtrid 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) |` ( 1 [,) +oo ) ) ~~>r 0 )
115 94 rpcnd 
 |-  ( ( ( A e. RR /\ B e. RR /\ 1 < B ) /\ n e. RR+ ) -> ( ( n ^c A ) / ( B ^c n ) ) e. CC )
116 115 fmpttd 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) : RR+ --> CC )
117 rpssre 
 |-  RR+ C_ RR
118 117 a1i 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> RR+ C_ RR )
119 116 118 32 rlimresb 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) ~~>r 0 <-> ( ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) |` ( 1 [,) +oo ) ) ~~>r 0 ) )
120 114 119 mpbird 
 |-  ( ( A e. RR /\ B e. RR /\ 1 < B ) -> ( n e. RR+ |-> ( ( n ^c A ) / ( B ^c n ) ) ) ~~>r 0 )