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

Metamath Proof Explorer

Theorem expcnfg

Description: If F is a complex continuous function and N is a fixed number, then F^N is continuous too. A generalization of expcncf . (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses expcnfg.1 
|- F/_ x F
expcnfg.2 
|- ( ph -> F e. ( A -cn-> CC ) )
expcnfg.3 
|- ( ph -> N e. NN0 )
Assertion expcnfg 
|- ( ph -> ( x e. A |-> ( ( F ` x ) ^ N ) ) e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 expcnfg.1 
 |-  F/_ x F
2 expcnfg.2 
 |-  ( ph -> F e. ( A -cn-> CC ) )
3 expcnfg.3 
 |-  ( ph -> N e. NN0 )
4 nfcv 
 |-  F/_ t ( ( F ` x ) ^ N )
5 nfcv 
 |-  F/_ x t
6 1 5 nffv 
 |-  F/_ x ( F ` t )
7 nfcv 
 |-  F/_ x ^
8 nfcv 
 |-  F/_ x N
9 6 7 8 nfov 
 |-  F/_ x ( ( F ` t ) ^ N )
10 fveq2 
 |-  ( x = t -> ( F ` x ) = ( F ` t ) )
11 10 oveq1d 
 |-  ( x = t -> ( ( F ` x ) ^ N ) = ( ( F ` t ) ^ N ) )
12 4 9 11 cbvmpt 
 |-  ( x e. A |-> ( ( F ` x ) ^ N ) ) = ( t e. A |-> ( ( F ` t ) ^ N ) )
13 cncff 
 |-  ( F e. ( A -cn-> CC ) -> F : A --> CC )
14 2 13 syl 
 |-  ( ph -> F : A --> CC )
15 14 ffvelcdmda 
 |-  ( ( ph /\ t e. A ) -> ( F ` t ) e. CC )
16 3 adantr 
 |-  ( ( ph /\ t e. A ) -> N e. NN0 )
17 15 16 expcld 
 |-  ( ( ph /\ t e. A ) -> ( ( F ` t ) ^ N ) e. CC )
18 oveq1 
 |-  ( x = ( F ` t ) -> ( x ^ N ) = ( ( F ` t ) ^ N ) )
19 eqid 
 |-  ( x e. CC |-> ( x ^ N ) ) = ( x e. CC |-> ( x ^ N ) )
20 6 9 18 19 fvmptf 
 |-  ( ( ( F ` t ) e. CC /\ ( ( F ` t ) ^ N ) e. CC ) -> ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` t ) ) = ( ( F ` t ) ^ N ) )
21 15 17 20 syl2anc 
 |-  ( ( ph /\ t e. A ) -> ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` t ) ) = ( ( F ` t ) ^ N ) )
22 21 eqcomd 
 |-  ( ( ph /\ t e. A ) -> ( ( F ` t ) ^ N ) = ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` t ) ) )
23 22 mpteq2dva 
 |-  ( ph -> ( t e. A |-> ( ( F ` t ) ^ N ) ) = ( t e. A |-> ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` t ) ) ) )
24 12 23 eqtrid 
 |-  ( ph -> ( x e. A |-> ( ( F ` x ) ^ N ) ) = ( t e. A |-> ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` t ) ) ) )
25 simpr 
 |-  ( ( ph /\ x e. CC ) -> x e. CC )
26 3 adantr 
 |-  ( ( ph /\ x e. CC ) -> N e. NN0 )
27 25 26 expcld 
 |-  ( ( ph /\ x e. CC ) -> ( x ^ N ) e. CC )
28 27 fmpttd 
 |-  ( ph -> ( x e. CC |-> ( x ^ N ) ) : CC --> CC )
29 fcompt 
 |-  ( ( ( x e. CC |-> ( x ^ N ) ) : CC --> CC /\ F : A --> CC ) -> ( ( x e. CC |-> ( x ^ N ) ) o. F ) = ( t e. A |-> ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` t ) ) ) )
30 28 14 29 syl2anc 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) o. F ) = ( t e. A |-> ( ( x e. CC |-> ( x ^ N ) ) ` ( F ` t ) ) ) )
31 24 30 eqtr4d 
 |-  ( ph -> ( x e. A |-> ( ( F ` x ) ^ N ) ) = ( ( x e. CC |-> ( x ^ N ) ) o. F ) )
32 expcncf 
 |-  ( N e. NN0 -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
33 3 32 syl 
 |-  ( ph -> ( x e. CC |-> ( x ^ N ) ) e. ( CC -cn-> CC ) )
34 2 33 cncfco 
 |-  ( ph -> ( ( x e. CC |-> ( x ^ N ) ) o. F ) e. ( A -cn-> CC ) )
35 31 34 eqeltrd 
 |-  ( ph -> ( x e. A |-> ( ( F ` x ) ^ N ) ) e. ( A -cn-> CC ) )