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 A + n + 1 n A 0

Proof

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