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 โŠข ( ( ๐œ‘ โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ต โˆˆ ๐‘‰ )
rlimcxp.2 โŠข ( ๐œ‘ โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โ‡๐‘Ÿ 0 )
rlimcxp.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
Assertion rlimcxp ( ๐œ‘ โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ( ๐ต โ†‘๐‘ ๐ถ ) ) โ‡๐‘Ÿ 0 )

Proof

Step Hyp Ref Expression
1 rlimcxp.1 โŠข ( ( ๐œ‘ โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ต โˆˆ ๐‘‰ )
2 rlimcxp.2 โŠข ( ๐œ‘ โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โ‡๐‘Ÿ 0 )
3 rlimcxp.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„+ )
4 rlimf โŠข ( ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โ‡๐‘Ÿ 0 โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) : dom ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โŸถ โ„‚ )
5 2 4 syl โŠข ( ๐œ‘ โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) : dom ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โŸถ โ„‚ )
6 1 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘› โˆˆ ๐ด ๐ต โˆˆ ๐‘‰ )
7 dmmptg โŠข ( โˆ€ ๐‘› โˆˆ ๐ด ๐ต โˆˆ ๐‘‰ โ†’ dom ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) = ๐ด )
8 6 7 syl โŠข ( ๐œ‘ โ†’ dom ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) = ๐ด )
9 8 feq2d โŠข ( ๐œ‘ โ†’ ( ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) : dom ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โŸถ โ„‚ โ†” ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) : ๐ด โŸถ โ„‚ ) )
10 5 9 mpbid โŠข ( ๐œ‘ โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) : ๐ด โŸถ โ„‚ )
11 eqid โŠข ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) = ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต )
12 11 fmpt โŠข ( โˆ€ ๐‘› โˆˆ ๐ด ๐ต โˆˆ โ„‚ โ†” ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) : ๐ด โŸถ โ„‚ )
13 10 12 sylibr โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘› โˆˆ ๐ด ๐ต โˆˆ โ„‚ )
14 13 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ โˆ€ ๐‘› โˆˆ ๐ด ๐ต โˆˆ โ„‚ )
15 simpr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ ๐‘ฅ โˆˆ โ„+ )
16 3 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ ๐ถ โˆˆ โ„+ )
17 16 rprecred โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ ( 1 / ๐ถ ) โˆˆ โ„ )
18 15 17 rpcxpcld โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โˆˆ โ„+ )
19 2 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โ‡๐‘Ÿ 0 )
20 14 18 19 rlimi โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ โˆƒ ๐‘ฆ โˆˆ โ„ โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) ) )
21 1 2 rlimmptrcl โŠข ( ( ๐œ‘ โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ต โˆˆ โ„‚ )
22 21 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ต โˆˆ โ„‚ )
23 22 abscld โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( abs โ€˜ ๐ต ) โˆˆ โ„ )
24 22 absge0d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ 0 โ‰ค ( abs โ€˜ ๐ต ) )
25 18 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โˆˆ โ„+ )
26 25 rpred โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โˆˆ โ„ )
27 25 rpge0d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ 0 โ‰ค ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) )
28 3 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ถ โˆˆ โ„+ )
29 23 24 26 27 28 cxplt2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ( abs โ€˜ ๐ต ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†” ( ( abs โ€˜ ๐ต ) โ†‘๐‘ ๐ถ ) < ( ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†‘๐‘ ๐ถ ) ) )
30 22 subid1d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ๐ต โˆ’ 0 ) = ๐ต )
31 30 fveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) = ( abs โ€˜ ๐ต ) )
32 31 breq1d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†” ( abs โ€˜ ๐ต ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) ) )
33 28 rpred โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ถ โˆˆ โ„ )
34 abscxp2 โŠข ( ( ๐ต โˆˆ โ„‚ โˆง ๐ถ โˆˆ โ„ ) โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) = ( ( abs โ€˜ ๐ต ) โ†‘๐‘ ๐ถ ) )
35 22 33 34 syl2anc โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) = ( ( abs โ€˜ ๐ต ) โ†‘๐‘ ๐ถ ) )
36 28 rpcnd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ถ โˆˆ โ„‚ )
37 28 rpne0d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ถ โ‰  0 )
38 36 37 recid2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ( 1 / ๐ถ ) ยท ๐ถ ) = 1 )
39 38 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ๐‘ฅ โ†‘๐‘ ( ( 1 / ๐ถ ) ยท ๐ถ ) ) = ( ๐‘ฅ โ†‘๐‘ 1 ) )
40 simplr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐‘ฅ โˆˆ โ„+ )
41 17 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( 1 / ๐ถ ) โˆˆ โ„ )
42 40 41 36 cxpmuld โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ๐‘ฅ โ†‘๐‘ ( ( 1 / ๐ถ ) ยท ๐ถ ) ) = ( ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†‘๐‘ ๐ถ ) )
43 40 rpcnd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐‘ฅ โˆˆ โ„‚ )
44 43 cxp1d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ๐‘ฅ โ†‘๐‘ 1 ) = ๐‘ฅ )
45 39 42 44 3eqtr3rd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐‘ฅ = ( ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†‘๐‘ ๐ถ ) )
46 35 45 breq12d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ โ†” ( ( abs โ€˜ ๐ต ) โ†‘๐‘ ๐ถ ) < ( ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†‘๐‘ ๐ถ ) ) )
47 29 32 46 3bitr4d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†” ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) )
48 47 biimpd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) )
49 48 imim2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) ) โ†’ ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) ) )
50 49 ralimdva โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ ( โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) ) โ†’ โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) ) )
51 50 reximdv โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ ( โˆƒ ๐‘ฆ โˆˆ โ„ โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โˆ’ 0 ) ) < ( ๐‘ฅ โ†‘๐‘ ( 1 / ๐ถ ) ) ) โ†’ โˆƒ ๐‘ฆ โˆˆ โ„ โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) ) )
52 20 51 mpd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ โ„+ ) โ†’ โˆƒ ๐‘ฆ โˆˆ โ„ โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) )
53 52 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ โ„+ โˆƒ ๐‘ฆ โˆˆ โ„ โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) )
54 3 rpcnd โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
55 54 adantr โŠข ( ( ๐œ‘ โˆง ๐‘› โˆˆ ๐ด ) โ†’ ๐ถ โˆˆ โ„‚ )
56 21 55 cxpcld โŠข ( ( ๐œ‘ โˆง ๐‘› โˆˆ ๐ด ) โ†’ ( ๐ต โ†‘๐‘ ๐ถ ) โˆˆ โ„‚ )
57 56 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘› โˆˆ ๐ด ( ๐ต โ†‘๐‘ ๐ถ ) โˆˆ โ„‚ )
58 rlimss โŠข ( ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โ‡๐‘Ÿ 0 โ†’ dom ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โІ โ„ )
59 2 58 syl โŠข ( ๐œ‘ โ†’ dom ( ๐‘› โˆˆ ๐ด โ†ฆ ๐ต ) โІ โ„ )
60 8 59 eqsstrrd โŠข ( ๐œ‘ โ†’ ๐ด โІ โ„ )
61 57 60 rlim0 โŠข ( ๐œ‘ โ†’ ( ( ๐‘› โˆˆ ๐ด โ†ฆ ( ๐ต โ†‘๐‘ ๐ถ ) ) โ‡๐‘Ÿ 0 โ†” โˆ€ ๐‘ฅ โˆˆ โ„+ โˆƒ ๐‘ฆ โˆˆ โ„ โˆ€ ๐‘› โˆˆ ๐ด ( ๐‘ฆ โ‰ค ๐‘› โ†’ ( abs โ€˜ ( ๐ต โ†‘๐‘ ๐ถ ) ) < ๐‘ฅ ) ) )
62 53 61 mpbird โŠข ( ๐œ‘ โ†’ ( ๐‘› โˆˆ ๐ด โ†ฆ ( ๐ต โ†‘๐‘ ๐ถ ) ) โ‡๐‘Ÿ 0 )