This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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