Metamath Proof Explorer

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 )