Metamath Proof Explorer

Theorem rlimcxp

Description: Any power to a positive exponent of a converging sequence also converges. (Contributed by Mario Carneiro, 18-Sep-2014)

Ref Expression
Hypotheses rlimcxp.1 
|- ( ( ph /\ n e. A ) -> B e. V )
rlimcxp.2 
|- ( ph -> ( n e. A |-> B ) ~~>r 0 )
rlimcxp.3 
|- ( ph -> C e. RR+ )
Assertion rlimcxp 
|- ( ph -> ( n e. A |-> ( B ^c C ) ) ~~>r 0 )

Proof

Step Hyp Ref Expression
1 rlimcxp.1 
 |-  ( ( ph /\ n e. A ) -> B e. V )
2 rlimcxp.2 
 |-  ( ph -> ( n e. A |-> B ) ~~>r 0 )
3 rlimcxp.3 
 |-  ( ph -> C e. RR+ )
4 rlimf 
 |-  ( ( n e. A |-> B ) ~~>r 0 -> ( n e. A |-> B ) : dom ( n e. A |-> B ) --> CC )
5 2 4 syl 
 |-  ( ph -> ( n e. A |-> B ) : dom ( n e. A |-> B ) --> CC )
6 1 ralrimiva 
 |-  ( ph -> A. n e. A B e. V )
7 dmmptg 
 |-  ( A. n e. A B e. V -> dom ( n e. A |-> B ) = A )
8 6 7 syl 
 |-  ( ph -> dom ( n e. A |-> B ) = A )
9 8 feq2d 
 |-  ( ph -> ( ( n e. A |-> B ) : dom ( n e. A |-> B ) --> CC <-> ( n e. A |-> B ) : A --> CC ) )
10 5 9 mpbid 
 |-  ( ph -> ( n e. A |-> B ) : A --> CC )
11 eqid 
 |-  ( n e. A |-> B ) = ( n e. A |-> B )
12 11 fmpt 
 |-  ( A. n e. A B e. CC <-> ( n e. A |-> B ) : A --> CC )
13 10 12 sylibr 
 |-  ( ph -> A. n e. A B e. CC )
14 13 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> A. n e. A B e. CC )
15 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
16 3 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> C e. RR+ )
17 16 rprecred 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / C ) e. RR )
18 15 17 rpcxpcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^c ( 1 / C ) ) e. RR+ )
19 2 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( n e. A |-> B ) ~~>r 0 )
20 14 18 19 rlimi 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR A. n e. A ( y <_ n -> ( abs ` ( B - 0 ) ) < ( x ^c ( 1 / C ) ) ) )
21 1 2 rlimmptrcl 
 |-  ( ( ph /\ n e. A ) -> B e. CC )
22 21 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> B e. CC )
23 22 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( abs ` B ) e. RR )
24 22 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> 0 <_ ( abs ` B ) )
25 18 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( x ^c ( 1 / C ) ) e. RR+ )
26 25 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( x ^c ( 1 / C ) ) e. RR )
27 25 rpge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> 0 <_ ( x ^c ( 1 / C ) ) )
28 3 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> C e. RR+ )
29 23 24 26 27 28 cxplt2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( ( abs ` B ) < ( x ^c ( 1 / C ) ) <-> ( ( abs ` B ) ^c C ) < ( ( x ^c ( 1 / C ) ) ^c C ) ) )
30 22 subid1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( B - 0 ) = B )
31 30 fveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( abs ` ( B - 0 ) ) = ( abs ` B ) )
32 31 breq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( ( abs ` ( B - 0 ) ) < ( x ^c ( 1 / C ) ) <-> ( abs ` B ) < ( x ^c ( 1 / C ) ) ) )
33 28 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> C e. RR )
34 abscxp2 
 |-  ( ( B e. CC /\ C e. RR ) -> ( abs ` ( B ^c C ) ) = ( ( abs ` B ) ^c C ) )
35 22 33 34 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( abs ` ( B ^c C ) ) = ( ( abs ` B ) ^c C ) )
36 28 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> C e. CC )
37 28 rpne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> C =/= 0 )
38 36 37 recid2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( ( 1 / C ) x. C ) = 1 )
39 38 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( x ^c ( ( 1 / C ) x. C ) ) = ( x ^c 1 ) )
40 simplr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> x e. RR+ )
41 17 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( 1 / C ) e. RR )
42 40 41 36 cxpmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( x ^c ( ( 1 / C ) x. C ) ) = ( ( x ^c ( 1 / C ) ) ^c C ) )
43 40 rpcnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> x e. CC )
44 43 cxp1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( x ^c 1 ) = x )
45 39 42 44 3eqtr3rd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> x = ( ( x ^c ( 1 / C ) ) ^c C ) )
46 35 45 breq12d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( ( abs ` ( B ^c C ) ) < x <-> ( ( abs ` B ) ^c C ) < ( ( x ^c ( 1 / C ) ) ^c C ) ) )
47 29 32 46 3bitr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( ( abs ` ( B - 0 ) ) < ( x ^c ( 1 / C ) ) <-> ( abs ` ( B ^c C ) ) < x ) )
48 47 biimpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( ( abs ` ( B - 0 ) ) < ( x ^c ( 1 / C ) ) -> ( abs ` ( B ^c C ) ) < x ) )
49 48 imim2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. A ) -> ( ( y <_ n -> ( abs ` ( B - 0 ) ) < ( x ^c ( 1 / C ) ) ) -> ( y <_ n -> ( abs ` ( B ^c C ) ) < x ) ) )
50 49 ralimdva 
 |-  ( ( ph /\ x e. RR+ ) -> ( A. n e. A ( y <_ n -> ( abs ` ( B - 0 ) ) < ( x ^c ( 1 / C ) ) ) -> A. n e. A ( y <_ n -> ( abs ` ( B ^c C ) ) < x ) ) )
51 50 reximdv 
 |-  ( ( ph /\ x e. RR+ ) -> ( E. y e. RR A. n e. A ( y <_ n -> ( abs ` ( B - 0 ) ) < ( x ^c ( 1 / C ) ) ) -> E. y e. RR A. n e. A ( y <_ n -> ( abs ` ( B ^c C ) ) < x ) ) )
52 20 51 mpd 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR A. n e. A ( y <_ n -> ( abs ` ( B ^c C ) ) < x ) )
53 52 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. y e. RR A. n e. A ( y <_ n -> ( abs ` ( B ^c C ) ) < x ) )
54 3 rpcnd 
 |-  ( ph -> C e. CC )
55 54 adantr 
 |-  ( ( ph /\ n e. A ) -> C e. CC )
56 21 55 cxpcld 
 |-  ( ( ph /\ n e. A ) -> ( B ^c C ) e. CC )
57 56 ralrimiva 
 |-  ( ph -> A. n e. A ( B ^c C ) e. CC )
58 rlimss 
 |-  ( ( n e. A |-> B ) ~~>r 0 -> dom ( n e. A |-> B ) C_ RR )
59 2 58 syl 
 |-  ( ph -> dom ( n e. A |-> B ) C_ RR )
60 8 59 eqsstrrd 
 |-  ( ph -> A C_ RR )
61 57 60 rlim0 
 |-  ( ph -> ( ( n e. A |-> ( B ^c C ) ) ~~>r 0 <-> A. x e. RR+ E. y e. RR A. n e. A ( y <_ n -> ( abs ` ( B ^c C ) ) < x ) ) )
62 53 61 mpbird 
 |-  ( ph -> ( n e. A |-> ( B ^c C ) ) ~~>r 0 )