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 mulridi 
 |-  ( _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 addlidi 
 |-  ( 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