Theorem eulerid

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

	Ref	Expression
Assertion	eulerid	$$⊢{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}+1=0$$

Proof

Step	Hyp	Ref	Expression
1		efipi	$$⊢{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}=-1$$
2	1	oveq1i	$$⊢{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}+1=-1+1$$
3		ax-1cn	$$⊢1\in ℂ$$
4		neg1cn	$$⊢-1\in ℂ$$
5		1pneg1e0	$$⊢1+-1=0$$
6	3 4 5	addcomli	$$⊢-1+1=0$$
7	2 6	eqtri	$$⊢{\mathrm{e}}^{\mathrm{i}\mathrm{\pi }}+1=0$$