Description: Euler's identity. (Contributed by Paul Chapman, 23Jan2008) (Revised by Mario Carneiro, 9May2014)
Ref  Expression  

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

1  efipi   ( exp ` ( _i x. _pi ) ) = u 1 

2  1  oveq1i   ( ( exp ` ( _i x. _pi ) ) + 1 ) = ( u 1 + 1 ) 
3  ax1cn   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 