Theorem cos0

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

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

Proof

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