# 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)

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 24 25 26 syl2anr
` |-  ( ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) /\ n e. CC ) -> ( n ^ ( k + 1 ) ) = ( ( n ^ k ) x. n ) )`
28 27 mpteq2dva
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> ( n e. CC |-> ( n ^ ( k + 1 ) ) ) = ( n e. CC |-> ( ( n ^ k ) x. n ) ) )`
29 23 28 syl5eq
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> ( x e. CC |-> ( x ^ ( k + 1 ) ) ) = ( n e. CC |-> ( ( n ^ k ) x. n ) ) )`
30 16 a1i
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> J e. ( TopOn ` CC ) )`
31 oveq1
` |-  ( x = n -> ( x ^ k ) = ( n ^ k ) )`
32 31 cbvmptv
` |-  ( x e. CC |-> ( x ^ k ) ) = ( n e. CC |-> ( n ^ k ) )`
33 simpr
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) )`
34 32 33 eqeltrrid
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> ( n e. CC |-> ( n ^ k ) ) e. ( J Cn J ) )`
35 30 cnmptid
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> ( n e. CC |-> n ) e. ( J Cn J ) )`
36 1 mulcn
` |-  x. e. ( ( J tX J ) Cn J )`
37 36 a1i
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> x. e. ( ( J tX J ) Cn J ) )`
38 30 34 35 37 cnmpt12f
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> ( n e. CC |-> ( ( n ^ k ) x. n ) ) e. ( J Cn J ) )`
39 29 38 eqeltrd
` |-  ( ( k e. NN0 /\ ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) ) -> ( x e. CC |-> ( x ^ ( k + 1 ) ) ) e. ( J Cn J ) )`
40 39 ex
` |-  ( k e. NN0 -> ( ( x e. CC |-> ( x ^ k ) ) e. ( J Cn J ) -> ( x e. CC |-> ( x ^ ( k + 1 ) ) ) e. ( J Cn J ) ) )`
41 4 7 10 13 21 40 nn0ind
` |-  ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( J Cn J ) )`