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	$⊢ (φ \land n \in A) \to B \in V$
	rlimcxp.2	$⊢ φ \to (n \in A ⟼ B) \underset{ℝ}{⇝} 0$
	rlimcxp.3	$⊢ φ \to C \in ℝ^{+}$
Assertion	rlimcxp	$⊢ φ \to (n \in A ⟼ B^{C}) \underset{ℝ}{⇝} 0$

Proof

Step	Hyp	Ref	Expression
1		rlimcxp.1	$⊢ (φ \land n \in A) \to B \in V$
2		rlimcxp.2	$⊢ φ \to (n \in A ⟼ B) \underset{ℝ}{⇝} 0$
3		rlimcxp.3	$⊢ φ \to C \in ℝ^{+}$
4		rlimf	$⊢ (n \in A ⟼ B) \underset{ℝ}{⇝} 0 \to (n \in A ⟼ B) : dom (n \in A ⟼ B) ⟶ ℂ$
5	2 4	syl	$⊢ φ \to (n \in A ⟼ B) : dom (n \in A ⟼ B) ⟶ ℂ$
6	1	ralrimiva	$⊢ φ \to \forall n \in A B \in V$
7		dmmptg	$⊢ \forall n \in A B \in V \to dom (n \in A ⟼ B) = A$
8	6 7	syl	$⊢ φ \to dom (n \in A ⟼ B) = A$
9	8	feq2d	$⊢ φ \to ((n \in A ⟼ B) : dom (n \in A ⟼ B) ⟶ ℂ \leftrightarrow (n \in A ⟼ B) : A ⟶ ℂ)$
10	5 9	mpbid	$⊢ φ \to (n \in A ⟼ B) : A ⟶ ℂ$
11		eqid	$⊢ (n \in A ⟼ B) = (n \in A ⟼ B)$
12	11	fmpt	$⊢ \forall n \in A B \in ℂ \leftrightarrow (n \in A ⟼ B) : A ⟶ ℂ$
13	10 12	sylibr	$⊢ φ \to \forall n \in A B \in ℂ$
14	13	adantr	$⊢ (φ \land x \in ℝ^{+}) \to \forall n \in A B \in ℂ$
15		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
16	3	adantr	$⊢ (φ \land x \in ℝ^{+}) \to C \in ℝ^{+}$
17	16	rprecred	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{C} \in ℝ$
18	15 17	rpcxpcld	$⊢ (φ \land x \in ℝ^{+}) \to x^{\frac{1}{C}} \in ℝ^{+}$
19	2	adantr	$⊢ (φ \land x \in ℝ^{+}) \to (n \in A ⟼ B) \underset{ℝ}{⇝} 0$
20	14 18 19	rlimi	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ \forall n \in A (y \leq n \to \|B - 0\| < x^{\frac{1}{C}})$
21	1 2	rlimmptrcl	$⊢ (φ \land n \in A) \to B \in ℂ$
22	21	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to B \in ℂ$
23	22	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to \|B\| \in ℝ$
24	22	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to 0 \leq \|B\|$
25	18	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x^{\frac{1}{C}} \in ℝ^{+}$
26	25	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x^{\frac{1}{C}} \in ℝ$
27	25	rpge0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to 0 \leq x^{\frac{1}{C}}$
28	3	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to C \in ℝ^{+}$
29	23 24 26 27 28	cxplt2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to (\|B\| < x^{\frac{1}{C}} \leftrightarrow {\|B\|}^{C} < {(x^{\frac{1}{C}})}^{C})$
30	22	subid1d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to B - 0 = B$
31	30	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to \|B - 0\| = \|B\|$
32	31	breq1d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to (\|B - 0\| < x^{\frac{1}{C}} \leftrightarrow \|B\| < x^{\frac{1}{C}})$
33	28	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to C \in ℝ$
34		abscxp2	$⊢ (B \in ℂ \land C \in ℝ) \to \|B^{C}\| = {\|B\|}^{C}$
35	22 33 34	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to \|B^{C}\| = {\|B\|}^{C}$
36	28	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to C \in ℂ$
37	28	rpne0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to C \neq 0$
38	36 37	recid2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to (\frac{1}{C}) C = 1$
39	38	oveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x^{(\frac{1}{C}) C} = x^{1}$
40		simplr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x \in ℝ^{+}$
41	17	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to \frac{1}{C} \in ℝ$
42	40 41 36	cxpmuld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x^{(\frac{1}{C}) C} = {(x^{\frac{1}{C}})}^{C}$
43	40	rpcnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x \in ℂ$
44	43	cxp1d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x^{1} = x$
45	39 42 44	3eqtr3rd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to x = {(x^{\frac{1}{C}})}^{C}$
46	35 45	breq12d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to (\|B^{C}\| < x \leftrightarrow {\|B\|}^{C} < {(x^{\frac{1}{C}})}^{C})$
47	29 32 46	3bitr4d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to (\|B - 0\| < x^{\frac{1}{C}} \leftrightarrow \|B^{C}\| < x)$
48	47	biimpd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to (\|B - 0\| < x^{\frac{1}{C}} \to \|B^{C}\| < x)$
49	48	imim2d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in A) \to ((y \leq n \to \|B - 0\| < x^{\frac{1}{C}}) \to (y \leq n \to \|B^{C}\| < x))$
50	49	ralimdva	$⊢ (φ \land x \in ℝ^{+}) \to (\forall n \in A (y \leq n \to \|B - 0\| < x^{\frac{1}{C}}) \to \forall n \in A (y \leq n \to \|B^{C}\| < x))$
51	50	reximdv	$⊢ (φ \land x \in ℝ^{+}) \to (\exists y \in ℝ \forall n \in A (y \leq n \to \|B - 0\| < x^{\frac{1}{C}}) \to \exists y \in ℝ \forall n \in A (y \leq n \to \|B^{C}\| < x))$
52	20 51	mpd	$⊢ (φ \land x \in ℝ^{+}) \to \exists y \in ℝ \forall n \in A (y \leq n \to \|B^{C}\| < x)$
53	52	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists y \in ℝ \forall n \in A (y \leq n \to \|B^{C}\| < x)$
54	3	rpcnd	$⊢ φ \to C \in ℂ$
55	54	adantr	$⊢ (φ \land n \in A) \to C \in ℂ$
56	21 55	cxpcld	$⊢ (φ \land n \in A) \to B^{C} \in ℂ$
57	56	ralrimiva	$⊢ φ \to \forall n \in A B^{C} \in ℂ$
58		rlimss	$⊢ (n \in A ⟼ B) \underset{ℝ}{⇝} 0 \to dom (n \in A ⟼ B) \subseteq ℝ$
59	2 58	syl	$⊢ φ \to dom (n \in A ⟼ B) \subseteq ℝ$
60	8 59	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
61	57 60	rlim0	$⊢ φ \to ((n \in A ⟼ B^{C}) \underset{ℝ}{⇝} 0 \leftrightarrow \forall x \in ℝ^{+} \exists y \in ℝ \forall n \in A (y \leq n \to \|B^{C}\| < x))$
62	53 61	mpbird	$⊢ φ \to (n \in A ⟼ B^{C}) \underset{ℝ}{⇝} 0$

Metamath Proof Explorer

Theorem rlimcxp

Proof