Metamath Proof Explorer


Theorem efhalfpi

Description: The exponential of _ipi / 2 is i . (Contributed by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion efhalfpi
|- ( exp ` ( _i x. ( _pi / 2 ) ) ) = _i

Proof

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