Metamath Proof Explorer

Theorem eulerid

Description: Euler's identity. (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 9-May-2014)

Ref Expression
Assertion eulerid 
|- ( ( exp ` ( _i x. _pi ) ) + 1 ) = 0

Proof

Step Hyp Ref Expression
1 efipi 
 |-  ( exp ` ( _i x. _pi ) ) = -u 1
2 1 oveq1i 
 |-  ( ( exp ` ( _i x. _pi ) ) + 1 ) = ( -u 1 + 1 )
3 ax-1cn 
 |-  1 e. CC
4 neg1cn 
 |-  -u 1 e. CC
5 1pneg1e0 
 |-  ( 1 + -u 1 ) = 0
6 3 4 5 addcomli 
 |-  ( -u 1 + 1 ) = 0
7 2 6 eqtri 
 |-  ( ( exp ` ( _i x. _pi ) ) + 1 ) = 0