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 )