Metamath Proof Explorer

Theorem efmul2picn

Description: Multiplying by (i x. ( 2 x. pi ) ) and taking the exponential preserves continuity. (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Hypothesis efmul2picn.1 
|- ( ph -> ( x e. A |-> B ) e. ( A -cn-> CC ) )
Assertion efmul2picn 
|- ( ph -> ( x e. A |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. B ) ) ) e. ( A -cn-> CC ) )

Proof

Step Hyp Ref Expression
1 efmul2picn.1 
 |-  ( ph -> ( x e. A |-> B ) e. ( A -cn-> CC ) )
2 efcn 
 |-  exp e. ( CC -cn-> CC )
3 2 a1i 
 |-  ( ph -> exp e. ( CC -cn-> CC ) )
4 ax-icn 
 |-  _i e. CC
5 2cn 
 |-  2 e. CC
6 picn 
 |-  _pi e. CC
7 5 6 mulcli 
 |-  ( 2 x. _pi ) e. CC
8 4 7 mulcli 
 |-  ( _i x. ( 2 x. _pi ) ) e. CC
9 8 a1i 
 |-  ( ph -> ( _i x. ( 2 x. _pi ) ) e. CC )
10 cncfrss 
 |-  ( ( x e. A |-> B ) e. ( A -cn-> CC ) -> A C_ CC )
11 1 10 syl 
 |-  ( ph -> A C_ CC )
12 ssidd 
 |-  ( ph -> CC C_ CC )
13 cncfmptc 
 |-  ( ( ( _i x. ( 2 x. _pi ) ) e. CC /\ A C_ CC /\ CC C_ CC ) -> ( x e. A |-> ( _i x. ( 2 x. _pi ) ) ) e. ( A -cn-> CC ) )
14 9 11 12 13 syl3anc 
 |-  ( ph -> ( x e. A |-> ( _i x. ( 2 x. _pi ) ) ) e. ( A -cn-> CC ) )
15 14 1 mulcncf 
 |-  ( ph -> ( x e. A |-> ( ( _i x. ( 2 x. _pi ) ) x. B ) ) e. ( A -cn-> CC ) )
16 3 15 cncfmpt1f 
 |-  ( ph -> ( x e. A |-> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. B ) ) ) e. ( A -cn-> CC ) )