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 ∈ ℝ
2		recosval	⊢ ( 0 ∈ ℝ → ( cos ‘ 0 ) = ( ℜ ‘ ( exp ‘ ( i · 0 ) ) ) )
3	1 2	ax-mp	⊢ ( cos ‘ 0 ) = ( ℜ ‘ ( exp ‘ ( i · 0 ) ) )
4		it0e0	⊢ ( i · 0 ) = 0
5	4	fveq2i	⊢ ( exp ‘ ( i · 0 ) ) = ( exp ‘ 0 )
6		ef0	⊢ ( exp ‘ 0 ) = 1
7	5 6	eqtri	⊢ ( exp ‘ ( i · 0 ) ) = 1
8	7	fveq2i	⊢ ( ℜ ‘ ( exp ‘ ( i · 0 ) ) ) = ( ℜ ‘ 1 )
9		re1	⊢ ( ℜ ‘ 1 ) = 1
10	8 9	eqtri	⊢ ( ℜ ‘ ( exp ‘ ( i · 0 ) ) ) = 1
11	3 10	eqtri	⊢ ( cos ‘ 0 ) = 1