Metamath Proof Explorer

Theorem cxplim

Description: A power to a negative exponent goes to zero as the base becomes large. (Contributed by Mario Carneiro, 15-Sep-2014) (Revised by Mario Carneiro, 18-May-2016)

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

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( x e. RR+ -> x e. RR )
2 1 adantl 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> x e. RR )
3 rpge0 
 |-  ( x e. RR+ -> 0 <_ x )
4 3 adantl 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> 0 <_ x )
5 rpre 
 |-  ( A e. RR+ -> A e. RR )
6 5 renegcld 
 |-  ( A e. RR+ -> -u A e. RR )
7 6 adantr 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> -u A e. RR )
8 rpcn 
 |-  ( A e. RR+ -> A e. CC )
9 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
10 8 9 negne0d 
 |-  ( A e. RR+ -> -u A =/= 0 )
11 10 adantr 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> -u A =/= 0 )
12 7 11 rereccld 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> ( 1 / -u A ) e. RR )
13 2 4 12 recxpcld 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> ( x ^c ( 1 / -u A ) ) e. RR )
14 simprl 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> n e. RR+ )
15 5 ad2antrr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> A e. RR )
16 14 15 rpcxpcld 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( n ^c A ) e. RR+ )
17 16 rpreccld 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( 1 / ( n ^c A ) ) e. RR+ )
18 17 rprege0d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( ( 1 / ( n ^c A ) ) e. RR /\ 0 <_ ( 1 / ( n ^c A ) ) ) )
19 absid 
 |-  ( ( ( 1 / ( n ^c A ) ) e. RR /\ 0 <_ ( 1 / ( n ^c A ) ) ) -> ( abs ` ( 1 / ( n ^c A ) ) ) = ( 1 / ( n ^c A ) ) )
20 18 19 syl 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( abs ` ( 1 / ( n ^c A ) ) ) = ( 1 / ( n ^c A ) ) )
21 simplr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> x e. RR+ )
22 simprr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( x ^c ( 1 / -u A ) ) < n )
23 rpreccl 
 |-  ( A e. RR+ -> ( 1 / A ) e. RR+ )
24 23 ad2antrr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( 1 / A ) e. RR+ )
25 24 rpcnd 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( 1 / A ) e. CC )
26 21 25 cxprecd 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( ( 1 / x ) ^c ( 1 / A ) ) = ( 1 / ( x ^c ( 1 / A ) ) ) )
27 rpcn 
 |-  ( x e. RR+ -> x e. CC )
28 27 ad2antlr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> x e. CC )
29 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
30 29 ad2antlr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> x =/= 0 )
31 28 30 25 cxpnegd 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( x ^c -u ( 1 / A ) ) = ( 1 / ( x ^c ( 1 / A ) ) ) )
32 1cnd 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> 1 e. CC )
33 8 ad2antrr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> A e. CC )
34 9 ad2antrr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> A =/= 0 )
35 32 33 34 divneg2d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> -u ( 1 / A ) = ( 1 / -u A ) )
36 35 oveq2d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( x ^c -u ( 1 / A ) ) = ( x ^c ( 1 / -u A ) ) )
37 26 31 36 3eqtr2d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( ( 1 / x ) ^c ( 1 / A ) ) = ( x ^c ( 1 / -u A ) ) )
38 33 34 recidd 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( A x. ( 1 / A ) ) = 1 )
39 38 oveq2d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( n ^c ( A x. ( 1 / A ) ) ) = ( n ^c 1 ) )
40 14 15 25 cxpmuld 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( n ^c ( A x. ( 1 / A ) ) ) = ( ( n ^c A ) ^c ( 1 / A ) ) )
41 14 rpcnd 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> n e. CC )
42 41 cxp1d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( n ^c 1 ) = n )
43 39 40 42 3eqtr3d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( ( n ^c A ) ^c ( 1 / A ) ) = n )
44 22 37 43 3brtr4d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( ( 1 / x ) ^c ( 1 / A ) ) < ( ( n ^c A ) ^c ( 1 / A ) ) )
45 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
46 45 ad2antlr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( 1 / x ) e. RR+ )
47 46 rpred 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( 1 / x ) e. RR )
48 46 rpge0d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> 0 <_ ( 1 / x ) )
49 16 rpred 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( n ^c A ) e. RR )
50 16 rpge0d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> 0 <_ ( n ^c A ) )
51 47 48 49 50 24 cxplt2d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( ( 1 / x ) < ( n ^c A ) <-> ( ( 1 / x ) ^c ( 1 / A ) ) < ( ( n ^c A ) ^c ( 1 / A ) ) ) )
52 44 51 mpbird 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( 1 / x ) < ( n ^c A ) )
53 21 16 52 ltrec1d 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( 1 / ( n ^c A ) ) < x )
54 20 53 eqbrtrd 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ ( n e. RR+ /\ ( x ^c ( 1 / -u A ) ) < n ) ) -> ( abs ` ( 1 / ( n ^c A ) ) ) < x )
55 54 expr 
 |-  ( ( ( A e. RR+ /\ x e. RR+ ) /\ n e. RR+ ) -> ( ( x ^c ( 1 / -u A ) ) < n -> ( abs ` ( 1 / ( n ^c A ) ) ) < x ) )
56 55 ralrimiva 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> A. n e. RR+ ( ( x ^c ( 1 / -u A ) ) < n -> ( abs ` ( 1 / ( n ^c A ) ) ) < x ) )
57 breq1 
 |-  ( y = ( x ^c ( 1 / -u A ) ) -> ( y < n <-> ( x ^c ( 1 / -u A ) ) < n ) )
58 57 rspceaimv 
 |-  ( ( ( x ^c ( 1 / -u A ) ) e. RR /\ A. n e. RR+ ( ( x ^c ( 1 / -u A ) ) < n -> ( abs ` ( 1 / ( n ^c A ) ) ) < x ) ) -> E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( 1 / ( n ^c A ) ) ) < x ) )
59 13 56 58 syl2anc 
 |-  ( ( A e. RR+ /\ x e. RR+ ) -> E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( 1 / ( n ^c A ) ) ) < x ) )
60 59 ralrimiva 
 |-  ( A e. RR+ -> A. x e. RR+ E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( 1 / ( n ^c A ) ) ) < x ) )
61 id 
 |-  ( n e. RR+ -> n e. RR+ )
62 rpcxpcl 
 |-  ( ( n e. RR+ /\ A e. RR ) -> ( n ^c A ) e. RR+ )
63 61 5 62 syl2anr 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( n ^c A ) e. RR+ )
64 63 rpreccld 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( 1 / ( n ^c A ) ) e. RR+ )
65 64 rpcnd 
 |-  ( ( A e. RR+ /\ n e. RR+ ) -> ( 1 / ( n ^c A ) ) e. CC )
66 65 ralrimiva 
 |-  ( A e. RR+ -> A. n e. RR+ ( 1 / ( n ^c A ) ) e. CC )
67 rpssre 
 |-  RR+ C_ RR
68 67 a1i 
 |-  ( A e. RR+ -> RR+ C_ RR )
69 66 68 rlim0lt 
 |-  ( A e. RR+ -> ( ( n e. RR+ |-> ( 1 / ( n ^c A ) ) ) ~~>r 0 <-> A. x e. RR+ E. y e. RR A. n e. RR+ ( y < n -> ( abs ` ( 1 / ( n ^c A ) ) ) < x ) ) )
70 60 69 mpbird 
 |-  ( A e. RR+ -> ( n e. RR+ |-> ( 1 / ( n ^c A ) ) ) ~~>r 0 )