Metamath Proof Explorer


Theorem expcn

Description: The power function on complex numbers, for fixed exponent N , is continuous. (Contributed by Mario Carneiro, 5-May-2014) (Revised by Mario Carneiro, 23-Aug-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

Ref Expression
Hypothesis expcn.j J = TopOpen fld
Assertion expcn N 0 x x N J Cn J

Proof

Step Hyp Ref Expression
1 expcn.j J = TopOpen fld
2 oveq2 n = 0 x n = x 0
3 2 mpteq2dv n = 0 x x n = x x 0
4 3 eleq1d n = 0 x x n J Cn J x x 0 J Cn J
5 oveq2 n = k x n = x k
6 5 mpteq2dv n = k x x n = x x k
7 6 eleq1d n = k x x n J Cn J x x k J Cn J
8 oveq2 n = k + 1 x n = x k + 1
9 8 mpteq2dv n = k + 1 x x n = x x k + 1
10 9 eleq1d n = k + 1 x x n J Cn J x x k + 1 J Cn J
11 oveq2 n = N x n = x N
12 11 mpteq2dv n = N x x n = x x N
13 12 eleq1d n = N x x n J Cn J x x N J Cn J
14 exp0 x x 0 = 1
15 14 mpteq2ia x x 0 = x 1
16 1 cnfldtopon J TopOn
17 16 a1i J TopOn
18 1cnd 1
19 17 17 18 cnmptc x 1 J Cn J
20 19 mptru x 1 J Cn J
21 15 20 eqeltri x x 0 J Cn J
22 oveq1 x = n x k + 1 = n k + 1
23 22 cbvmptv x x k + 1 = n n k + 1
24 id n n
25 simpl k 0 x x k J Cn J k 0
26 expp1 n k 0 n k + 1 = n k n
27 expcl n k 0 n k
28 simpl n k 0 n
29 ovmpot n k n n k u , v u v n = n k n
30 27 28 29 syl2anc n k 0 n k u , v u v n = n k n
31 26 30 eqtr4d n k 0 n k + 1 = n k u , v u v n
32 24 25 31 syl2anr k 0 x x k J Cn J n n k + 1 = n k u , v u v n
33 32 mpteq2dva k 0 x x k J Cn J n n k + 1 = n n k u , v u v n
34 23 33 eqtrid k 0 x x k J Cn J x x k + 1 = n n k u , v u v n
35 16 a1i k 0 x x k J Cn J J TopOn
36 oveq1 x = n x k = n k
37 36 cbvmptv x x k = n n k
38 simpr k 0 x x k J Cn J x x k J Cn J
39 37 38 eqeltrrid k 0 x x k J Cn J n n k J Cn J
40 35 cnmptid k 0 x x k J Cn J n n J Cn J
41 1 mpomulcn u , v u v J × t J Cn J
42 41 a1i k 0 x x k J Cn J u , v u v J × t J Cn J
43 35 39 40 42 cnmpt12f k 0 x x k J Cn J n n k u , v u v n J Cn J
44 34 43 eqeltrd k 0 x x k J Cn J x x k + 1 J Cn J
45 44 ex k 0 x x k J Cn J x x k + 1 J Cn J
46 4 7 10 13 21 45 nn0ind N 0 x x N J Cn J