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