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