Theorem efhalfpi

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

	Ref	Expression
Assertion	efhalfpi	$$⊢{\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}$$

Proof

Step	Hyp	Ref	Expression
1		picn	$$⊢\mathrm{\pi }\in ℂ$$
2		halfcl	$$⊢\mathrm{\pi }\in ℂ\to \frac{\mathrm{\pi }}{2}\in ℂ$$
3		efival	$$⊢\frac{\mathrm{\pi }}{2}\in ℂ\to {\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\cos \left(\frac{\mathrm{\pi }}{2}\right)+\mathrm{i}\sin \left(\frac{\mathrm{\pi }}{2}\right)$$
4	1 2 3	mp2b	$$⊢{\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\cos \left(\frac{\mathrm{\pi }}{2}\right)+\mathrm{i}\sin \left(\frac{\mathrm{\pi }}{2}\right)$$
5		coshalfpi	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)=0$$
6		sinhalfpi	$$⊢\sin \left(\frac{\mathrm{\pi }}{2}\right)=1$$
7	6	oveq2i	$$⊢\mathrm{i}\sin \left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{i}\cdot 1$$
8		ax-icn	$$⊢\mathrm{i}\in ℂ$$
9	8	mulid1i	$$⊢\mathrm{i}\cdot 1=\mathrm{i}$$
10	7 9	eqtri	$$⊢\mathrm{i}\sin \left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{i}$$
11	5 10	oveq12i	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)+\mathrm{i}\sin \left(\frac{\mathrm{\pi }}{2}\right)=0+\mathrm{i}$$
12	8	addid2i	$$⊢0+\mathrm{i}=\mathrm{i}$$
13	11 12	eqtri	$$⊢\cos \left(\frac{\mathrm{\pi }}{2}\right)+\mathrm{i}\sin \left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{i}$$
14	4 13	eqtri	$$⊢{\mathrm{e}}^{\mathrm{i}\left(\frac{\mathrm{\pi }}{2}\right)}=\mathrm{i}$$