Metamath Proof Explorer

Theorem efipi

Description: The exponential of _i x. _pi is -u 1 . (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

Ref Expression
Assertion efipi 
|- ( exp ` ( _i x. _pi ) ) = -u 1

Proof

Step Hyp Ref Expression
1 picn 
 |-  _pi e. CC
2 efival 
 |-  ( _pi e. CC -> ( exp ` ( _i x. _pi ) ) = ( ( cos ` _pi ) + ( _i x. ( sin ` _pi ) ) ) )
3 1 2 ax-mp 
 |-  ( exp ` ( _i x. _pi ) ) = ( ( cos ` _pi ) + ( _i x. ( sin ` _pi ) ) )
4 cospi 
 |-  ( cos ` _pi ) = -u 1
5 sinpi 
 |-  ( sin ` _pi ) = 0
6 5 oveq2i 
 |-  ( _i x. ( sin ` _pi ) ) = ( _i x. 0 )
7 it0e0 
 |-  ( _i x. 0 ) = 0
8 6 7 eqtri 
 |-  ( _i x. ( sin ` _pi ) ) = 0
9 4 8 oveq12i 
 |-  ( ( cos ` _pi ) + ( _i x. ( sin ` _pi ) ) ) = ( -u 1 + 0 )
10 neg1cn 
 |-  -u 1 e. CC
11 10 addid1i 
 |-  ( -u 1 + 0 ) = -u 1
12 9 11 eqtri 
 |-  ( ( cos ` _pi ) + ( _i x. ( sin ` _pi ) ) ) = -u 1
13 3 12 eqtri 
 |-  ( exp ` ( _i x. _pi ) ) = -u 1