efhalfpi

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

		Ref	Expression
	Assertion	efhalfpi	$⊢ e^{i (\frac{π}{2})} = i$

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

Metamath Proof Explorer