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 · π ) ) + 1 ) = 0

Proof

Step	Hyp	Ref	Expression
1		efipi	⊢ ( exp ‘ ( i · π ) ) = - 1
2	1	oveq1i	⊢ ( ( exp ‘ ( i · π ) ) + 1 ) = ( - 1 + 1 )
3		ax-1cn	⊢ 1 ∈ ℂ
4		neg1cn	⊢ - 1 ∈ ℂ
5		1pneg1e0	⊢ ( 1 + - 1 ) = 0
6	3 4 5	addcomli	⊢ ( - 1 + 1 ) = 0
7	2 6	eqtri	⊢ ( ( exp ‘ ( i · π ) ) + 1 ) = 0