Theorem efhalfpi

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

	Ref	Expression
Assertion	efhalfpi	⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = i

Proof

Step	Hyp	Ref	Expression
1		picn	⊢ π ∈ ℂ
2		halfcl	⊢ ( π ∈ ℂ → ( π / 2 ) ∈ ℂ )
3		efival	⊢ ( ( π / 2 ) ∈ ℂ → ( exp ‘ ( i · ( π / 2 ) ) ) = ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) ) )
4	1 2 3	mp2b	⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) )
5		coshalfpi	⊢ ( cos ‘ ( π / 2 ) ) = 0
6		sinhalfpi	⊢ ( sin ‘ ( π / 2 ) ) = 1
7	6	oveq2i	⊢ ( i · ( sin ‘ ( π / 2 ) ) ) = ( i · 1 )
8		ax-icn	⊢ i ∈ ℂ
9	8	mulridi	⊢ ( i · 1 ) = i
10	7 9	eqtri	⊢ ( i · ( sin ‘ ( π / 2 ) ) ) = i
11	5 10	oveq12i	⊢ ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) ) = ( 0 + i )
12	8	addlidi	⊢ ( 0 + i ) = i
13	11 12	eqtri	⊢ ( ( cos ‘ ( π / 2 ) ) + ( i · ( sin ‘ ( π / 2 ) ) ) ) = i
14	4 13	eqtri	⊢ ( exp ‘ ( i · ( π / 2 ) ) ) = i