Theorem ef2pi

Description: The exponential of 2pi i is 1 . (Contributed by Mario Carneiro, 9-May-2014)

	Ref	Expression
Assertion	ef2pi	⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = 1

Proof

Step	Hyp	Ref	Expression
1		2cn	⊢ 2 ∈ ℂ
2		picn	⊢ π ∈ ℂ
3	1 2	mulcli	⊢ ( 2 · π ) ∈ ℂ
4		efival	⊢ ( ( 2 · π ) ∈ ℂ → ( exp ‘ ( i · ( 2 · π ) ) ) = ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) ) )
5	3 4	ax-mp	⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) )
6		cos2pi	⊢ ( cos ‘ ( 2 · π ) ) = 1
7		sin2pi	⊢ ( sin ‘ ( 2 · π ) ) = 0
8	7	oveq2i	⊢ ( i · ( sin ‘ ( 2 · π ) ) ) = ( i · 0 )
9		it0e0	⊢ ( i · 0 ) = 0
10	8 9	eqtri	⊢ ( i · ( sin ‘ ( 2 · π ) ) ) = 0
11	6 10	oveq12i	⊢ ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) ) = ( 1 + 0 )
12		1p0e1	⊢ ( 1 + 0 ) = 1
13	11 12	eqtri	⊢ ( ( cos ‘ ( 2 · π ) ) + ( i · ( sin ‘ ( 2 · π ) ) ) ) = 1
14	5 13	eqtri	⊢ ( exp ‘ ( i · ( 2 · π ) ) ) = 1