Theorem efipi

Description: The exponential of _i x. _pi is -u 1 . (Contributed by Paul Chapman, 23-Jan-2008) (Revised by Mario Carneiro, 10-May-2014)

	Ref	Expression
Assertion	efipi	⊢ ( exp ‘ ( i · π ) ) = - 1

Proof

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