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\in ℂ$$
4		sinneg	$$⊢0\in ℂ\to \sin -0=-\sin 0$$
5	3 4	ax-mp	$$⊢\sin -0=-\sin 0$$
6	2 5	eqtr3i	$$⊢\sin 0=-\sin 0$$
7		sincl	$$⊢0\in ℂ\to \sin 0\in ℂ$$
8	3 7	ax-mp	$$⊢\sin 0\in ℂ$$
9	8	eqnegi	$$⊢\sin 0=-\sin 0\leftrightarrow \sin 0=0$$
10	6 9	mpbi	$$⊢\sin 0=0$$