cos0

Description: Value of the cosine function at 0. (Contributed by NM, 30-Apr-2005)

		Ref	Expression
	Assertion	cos0	$⊢ \cos 0 = 1$

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		recosval	$⊢ 0 \in ℝ \to \cos 0 = ℜ (e^{i \cdot 0})$
3	1 2	ax-mp	$⊢ \cos 0 = ℜ (e^{i \cdot 0})$
4		it0e0	$⊢ i \cdot 0 = 0$
5	4	fveq2i	$⊢ e^{i \cdot 0} = e^{0}$
6		ef0	$⊢ e^{0} = 1$
7	5 6	eqtri	$⊢ e^{i \cdot 0} = 1$
8	7	fveq2i	$⊢ ℜ (e^{i \cdot 0}) = ℜ (1)$
9		re1	$⊢ ℜ (1) = 1$
10	8 9	eqtri	$⊢ ℜ (e^{i \cdot 0}) = 1$
11	3 10	eqtri	$⊢ \cos 0 = 1$

Metamath Proof Explorer