Step |
Hyp |
Ref |
Expression |
1 |
|
picn |
|- _pi e. CC |
2 |
|
halfcl |
|- ( _pi e. CC -> ( _pi / 2 ) e. CC ) |
3 |
|
efival |
|- ( ( _pi / 2 ) e. CC -> ( exp ` ( _i x. ( _pi / 2 ) ) ) = ( ( cos ` ( _pi / 2 ) ) + ( _i x. ( sin ` ( _pi / 2 ) ) ) ) ) |
4 |
1 2 3
|
mp2b |
|- ( exp ` ( _i x. ( _pi / 2 ) ) ) = ( ( cos ` ( _pi / 2 ) ) + ( _i x. ( sin ` ( _pi / 2 ) ) ) ) |
5 |
|
coshalfpi |
|- ( cos ` ( _pi / 2 ) ) = 0 |
6 |
|
sinhalfpi |
|- ( sin ` ( _pi / 2 ) ) = 1 |
7 |
6
|
oveq2i |
|- ( _i x. ( sin ` ( _pi / 2 ) ) ) = ( _i x. 1 ) |
8 |
|
ax-icn |
|- _i e. CC |
9 |
8
|
mulid1i |
|- ( _i x. 1 ) = _i |
10 |
7 9
|
eqtri |
|- ( _i x. ( sin ` ( _pi / 2 ) ) ) = _i |
11 |
5 10
|
oveq12i |
|- ( ( cos ` ( _pi / 2 ) ) + ( _i x. ( sin ` ( _pi / 2 ) ) ) ) = ( 0 + _i ) |
12 |
8
|
addid2i |
|- ( 0 + _i ) = _i |
13 |
11 12
|
eqtri |
|- ( ( cos ` ( _pi / 2 ) ) + ( _i x. ( sin ` ( _pi / 2 ) ) ) ) = _i |
14 |
4 13
|
eqtri |
|- ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i |