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	⊢ ( 𝐴 ∈ ℝ+ → ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) ⇝𝑟 0 )

Proof

Step	Hyp	Ref	Expression
1		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
3		rpge0	⊢ ( 𝑥 ∈ ℝ+ → 0 ≤ 𝑥 )
4	3	adantl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ 𝑥 )
5		rpre	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ )
6	5	renegcld	⊢ ( 𝐴 ∈ ℝ+ → - 𝐴 ∈ ℝ )
7	6	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → - 𝐴 ∈ ℝ )
8		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
9		rpne0	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
10	8 9	negne0d	⊢ ( 𝐴 ∈ ℝ+ → - 𝐴 ≠ 0 )
11	10	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → - 𝐴 ≠ 0 )
12	7 11	rereccld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / - 𝐴 ) ∈ ℝ )
13	2 4 12	recxpcld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) ∈ ℝ )
14		simprl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝑛 ∈ ℝ+ )
15	5	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝐴 ∈ ℝ )
16	14 15	rpcxpcld	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑛 ↑𝑐 𝐴 ) ∈ ℝ+ )
17	16	rpreccld	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℝ+ )
18	17	rprege0d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) )
19		absid	⊢ ( ( ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) = ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) )
20	18 19	syl	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) = ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) )
21		simplr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝑥 ∈ ℝ+ )
22		simprr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 )
23		rpreccl	⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℝ+ )
24	23	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 1 / 𝐴 ) ∈ ℝ+ )
25	24	rpcnd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 1 / 𝐴 ) ∈ ℂ )
26	21 25	cxprecd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( ( 1 / 𝑥 ) ↑𝑐 ( 1 / 𝐴 ) ) = ( 1 / ( 𝑥 ↑𝑐 ( 1 / 𝐴 ) ) ) )
27		rpcn	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℂ )
28	27	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝑥 ∈ ℂ )
29		rpne0	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ≠ 0 )
30	29	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝑥 ≠ 0 )
31	28 30 25	cxpnegd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑥 ↑𝑐 - ( 1 / 𝐴 ) ) = ( 1 / ( 𝑥 ↑𝑐 ( 1 / 𝐴 ) ) ) )
32		1cnd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 1 ∈ ℂ )
33	8	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝐴 ∈ ℂ )
34	9	ad2antrr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝐴 ≠ 0 )
35	32 33 34	divneg2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → - ( 1 / 𝐴 ) = ( 1 / - 𝐴 ) )
36	35	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑥 ↑𝑐 - ( 1 / 𝐴 ) ) = ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) )
37	26 31 36	3eqtr2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( ( 1 / 𝑥 ) ↑𝑐 ( 1 / 𝐴 ) ) = ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) )
38	33 34	recidd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝐴 · ( 1 / 𝐴 ) ) = 1 )
39	38	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑛 ↑𝑐 ( 𝐴 · ( 1 / 𝐴 ) ) ) = ( 𝑛 ↑𝑐 1 ) )
40	14 15 25	cxpmuld	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑛 ↑𝑐 ( 𝐴 · ( 1 / 𝐴 ) ) ) = ( ( 𝑛 ↑𝑐 𝐴 ) ↑𝑐 ( 1 / 𝐴 ) ) )
41	14	rpcnd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 𝑛 ∈ ℂ )
42	41	cxp1d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑛 ↑𝑐 1 ) = 𝑛 )
43	39 40 42	3eqtr3d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( ( 𝑛 ↑𝑐 𝐴 ) ↑𝑐 ( 1 / 𝐴 ) ) = 𝑛 )
44	22 37 43	3brtr4d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( ( 1 / 𝑥 ) ↑𝑐 ( 1 / 𝐴 ) ) < ( ( 𝑛 ↑𝑐 𝐴 ) ↑𝑐 ( 1 / 𝐴 ) ) )
45		rpreccl	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
46	45	ad2antlr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 1 / 𝑥 ) ∈ ℝ+ )
47	46	rpred	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 1 / 𝑥 ) ∈ ℝ )
48	46	rpge0d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 0 ≤ ( 1 / 𝑥 ) )
49	16	rpred	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 𝑛 ↑𝑐 𝐴 ) ∈ ℝ )
50	16	rpge0d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → 0 ≤ ( 𝑛 ↑𝑐 𝐴 ) )
51	47 48 49 50 24	cxplt2d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( ( 1 / 𝑥 ) < ( 𝑛 ↑𝑐 𝐴 ) ↔ ( ( 1 / 𝑥 ) ↑𝑐 ( 1 / 𝐴 ) ) < ( ( 𝑛 ↑𝑐 𝐴 ) ↑𝑐 ( 1 / 𝐴 ) ) ) )
52	44 51	mpbird	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 1 / 𝑥 ) < ( 𝑛 ↑𝑐 𝐴 ) )
53	21 16 52	ltrec1d	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) < 𝑥 )
54	20 53	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ℝ+ ∧ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) ) → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 )
55	54	expr	⊢ ( ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) )
56	55	ralrimiva	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑛 ∈ ℝ+ ( ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) )
57		breq1	⊢ ( 𝑦 = ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) → ( 𝑦 < 𝑛 ↔ ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 ) )
58	57	rspceaimv	⊢ ( ( ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) ∈ ℝ ∧ ∀ 𝑛 ∈ ℝ+ ( ( 𝑥 ↑𝑐 ( 1 / - 𝐴 ) ) < 𝑛 → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) )
59	13 56 58	syl2anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) )
60	59	ralrimiva	⊢ ( 𝐴 ∈ ℝ+ → ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) )
61		id	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ+ )
62		rpcxpcl	⊢ ( ( 𝑛 ∈ ℝ+ ∧ 𝐴 ∈ ℝ ) → ( 𝑛 ↑𝑐 𝐴 ) ∈ ℝ+ )
63	61 5 62	syl2anr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑𝑐 𝐴 ) ∈ ℝ+ )
64	63	rpreccld	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℝ+ )
65	64	rpcnd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℂ )
66	65	ralrimiva	⊢ ( 𝐴 ∈ ℝ+ → ∀ 𝑛 ∈ ℝ+ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ∈ ℂ )
67		rpssre	⊢ ℝ+ ⊆ ℝ
68	67	a1i	⊢ ( 𝐴 ∈ ℝ+ → ℝ+ ⊆ ℝ )
69	66 68	rlim0lt	⊢ ( 𝐴 ∈ ℝ+ → ( ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) ⇝𝑟 0 ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ ℝ+ ( 𝑦 < 𝑛 → ( abs ‘ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) < 𝑥 ) ) )
70	60 69	mpbird	⊢ ( 𝐴 ∈ ℝ+ → ( 𝑛 ∈ ℝ+ ↦ ( 1 / ( 𝑛 ↑𝑐 𝐴 ) ) ) ⇝𝑟 0 )