Theorem cxplim

Description: A power to a negative exponent goes to zero as the base becomes large. (Contributed by Mario Carneiro, 15-Sep-2014) (Revised by Mario Carneiro, 18-May-2016)

	Ref	Expression
Assertion	cxplim	$$⊢A\in {ℝ}^{+}\to \left(n\in {ℝ}^{+}⟼\frac{1}{n^A}\right)\underset{ℝ}{⇝}0$$

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢x\in {ℝ}^{+}\to x\in ℝ$$
2	1	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to x\in ℝ$$
3		rpge0	$$⊢x\in {ℝ}^{+}\to 0\le x$$
4	3	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to 0\le x$$
5		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
6	5	renegcld	$$⊢A\in {ℝ}^{+}\to -A\in ℝ$$
7	6	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to -A\in ℝ$$
8		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
9		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
10	8 9	negne0d	$$⊢A\in {ℝ}^{+}\to -A\ne 0$$
11	10	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to -A\ne 0$$
12	7 11	rereccld	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to \frac{1}{-A}\in ℝ$$
13	2 4 12	recxpcld	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to x^{\frac{1}{-A}}\in ℝ$$
14		simprl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to n\in {ℝ}^{+}$$
15	5	ad2antrr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to A\in ℝ$$
16	14 15	rpcxpcld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to n^A\in {ℝ}^{+}$$
17	16	rpreccld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \frac{1}{n^A}\in {ℝ}^{+}$$
18	17	rprege0d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \left(\frac{1}{n^A}\in ℝ\wedge 0\le \frac{1}{n^A}\right)$$
19		absid	$$⊢\left(\frac{1}{n^A}\in ℝ\wedge 0\le \frac{1}{n^A}\right)\to \left|\frac{1}{n^A}\right|=\frac{1}{n^A}$$
20	18 19	syl	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \left|\frac{1}{n^A}\right|=\frac{1}{n^A}$$
21		simplr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to x\in {ℝ}^{+}$$
22		simprr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to x^{\frac{1}{-A}}<n$$
23		rpreccl	$$⊢A\in {ℝ}^{+}\to \frac{1}{A}\in {ℝ}^{+}$$
24	23	ad2antrr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \frac{1}{A}\in {ℝ}^{+}$$
25	24	rpcnd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \frac{1}{A}\in ℂ$$
26	21 25	cxprecd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to {\left(\frac{1}{x}\right)}^{\frac{1}{A}}=\frac{1}{x^{\frac{1}{A}}}$$
27		rpcn	$$⊢x\in {ℝ}^{+}\to x\in ℂ$$
28	27	ad2antlr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to x\in ℂ$$
29		rpne0	$$⊢x\in {ℝ}^{+}\to x\ne 0$$
30	29	ad2antlr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to x\ne 0$$
31	28 30 25	cxpnegd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to x^{-\frac{1}{A}}=\frac{1}{x^{\frac{1}{A}}}$$
32		1cnd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to 1\in ℂ$$
33	8	ad2antrr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to A\in ℂ$$
34	9	ad2antrr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to A\ne 0$$
35	32 33 34	divneg2d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to -\frac{1}{A}=\frac{1}{-A}$$
36	35	oveq2d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to x^{-\frac{1}{A}}=x^{\frac{1}{-A}}$$
37	26 31 36	3eqtr2d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to {\left(\frac{1}{x}\right)}^{\frac{1}{A}}=x^{\frac{1}{-A}}$$
38	33 34	recidd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to A\left(\frac{1}{A}\right)=1$$
39	38	oveq2d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to n^{A\left(\frac{1}{A}\right)}=n^1$$
40	14 15 25	cxpmuld	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to n^{A\left(\frac{1}{A}\right)}={\left(n^A\right)}^{\frac{1}{A}}$$
41	14	rpcnd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to n\in ℂ$$
42	41	cxp1d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to n^1=n$$
43	39 40 42	3eqtr3d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to {\left(n^A\right)}^{\frac{1}{A}}=n$$
44	22 37 43	3brtr4d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to {\left(\frac{1}{x}\right)}^{\frac{1}{A}}<{\left(n^A\right)}^{\frac{1}{A}}$$
45		rpreccl	$$⊢x\in {ℝ}^{+}\to \frac{1}{x}\in {ℝ}^{+}$$
46	45	ad2antlr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \frac{1}{x}\in {ℝ}^{+}$$
47	46	rpred	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \frac{1}{x}\in ℝ$$
48	46	rpge0d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to 0\le \frac{1}{x}$$
49	16	rpred	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to n^A\in ℝ$$
50	16	rpge0d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to 0\le n^A$$
51	47 48 49 50 24	cxplt2d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \left(\frac{1}{x}<n^A\leftrightarrow {\left(\frac{1}{x}\right)}^{\frac{1}{A}}<{\left(n^A\right)}^{\frac{1}{A}}\right)$$
52	44 51	mpbird	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \frac{1}{x}<n^A$$
53	21 16 52	ltrec1d	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \frac{1}{n^A}<x$$
54	20 53	eqbrtrd	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge \left(n\in {ℝ}^{+}\wedge x^{\frac{1}{-A}}<n\right)\right)\to \left|\frac{1}{n^A}\right|<x$$
55	54	expr	$$⊢\left(\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\wedge n\in {ℝ}^{+}\right)\to \left(x^{\frac{1}{-A}}<n\to \left|\frac{1}{n^A}\right|<x\right)$$
56	55	ralrimiva	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to \forall n\in {ℝ}^{+}\left(x^{\frac{1}{-A}}<n\to \left|\frac{1}{n^A}\right|<x\right)$$
57		breq1	$$⊢y=x^{\frac{1}{-A}}\to \left(y<n\leftrightarrow x^{\frac{1}{-A}}<n\right)$$
58	57	rspceaimv	$$⊢\left(x^{\frac{1}{-A}}\in ℝ\wedge \forall n\in {ℝ}^{+}\left(x^{\frac{1}{-A}}<n\to \left|\frac{1}{n^A}\right|<x\right)\right)\to \exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{1}{n^A}\right|<x\right)$$
59	13 56 58	syl2anc	$$⊢\left(A\in {ℝ}^{+}\wedge x\in {ℝ}^{+}\right)\to \exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{1}{n^A}\right|<x\right)$$
60	59	ralrimiva	$$⊢A\in {ℝ}^{+}\to \forall x\in {ℝ}^{+}\exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{1}{n^A}\right|<x\right)$$
61		id	$$⊢n\in {ℝ}^{+}\to n\in {ℝ}^{+}$$
62		rpcxpcl	$$⊢\left(n\in {ℝ}^{+}\wedge A\in ℝ\right)\to n^A\in {ℝ}^{+}$$
63	61 5 62	syl2anr	$$⊢\left(A\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\to n^A\in {ℝ}^{+}$$
64	63	rpreccld	$$⊢\left(A\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\to \frac{1}{n^A}\in {ℝ}^{+}$$
65	64	rpcnd	$$⊢\left(A\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\to \frac{1}{n^A}\in ℂ$$
66	65	ralrimiva	$$⊢A\in {ℝ}^{+}\to \forall n\in {ℝ}^{+}\frac{1}{n^A}\in ℂ$$
67		rpssre	$$⊢{ℝ}^{+}\subseteq ℝ$$
68	67	a1i	$$⊢A\in {ℝ}^{+}\to {ℝ}^{+}\subseteq ℝ$$
69	66 68	rlim0lt	$$⊢A\in {ℝ}^{+}\to \left(\left(n\in {ℝ}^{+}⟼\frac{1}{n^A}\right)\underset{ℝ}{⇝}0\leftrightarrow \forall x\in {ℝ}^{+}\exists y\in ℝ\forall n\in {ℝ}^{+}\left(y<n\to \left|\frac{1}{n^A}\right|<x\right)\right)$$
70	60 69	mpbird	$$⊢A\in {ℝ}^{+}\to \left(n\in {ℝ}^{+}⟼\frac{1}{n^A}\right)\underset{ℝ}{⇝}0$$