Theorem sin0

Description: Value of the sine function at 0. (Contributed by Steve Rodriguez, 14-Mar-2005)

	Ref	Expression
Assertion	sin0	⊢ ( sin ‘ 0 ) = 0

Proof

Step	Hyp	Ref	Expression
1		neg0	⊢ - 0 = 0
2	1	fveq2i	⊢ ( sin ‘ - 0 ) = ( sin ‘ 0 )
3		0cn	⊢ 0 ∈ ℂ
4		sinneg	⊢ ( 0 ∈ ℂ → ( sin ‘ - 0 ) = - ( sin ‘ 0 ) )
5	3 4	ax-mp	⊢ ( sin ‘ - 0 ) = - ( sin ‘ 0 )
6	2 5	eqtr3i	⊢ ( sin ‘ 0 ) = - ( sin ‘ 0 )
7		sincl	⊢ ( 0 ∈ ℂ → ( sin ‘ 0 ) ∈ ℂ )
8	3 7	ax-mp	⊢ ( sin ‘ 0 ) ∈ ℂ
9	8	eqnegi	⊢ ( ( sin ‘ 0 ) = - ( sin ‘ 0 ) ↔ ( sin ‘ 0 ) = 0 )
10	6 9	mpbi	⊢ ( sin ‘ 0 ) = 0