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 ` CCfld )
Assertion expcn
|- ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( J Cn J ) )

Proof

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