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 )