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