Theorem tan0

Description: The value of the tangent function at zero is zero. (Contributed by David A. Wheeler, 16-Mar-2014)

	Ref	Expression
Assertion	tan0	$$⊢\tan 0=0$$

Proof

Step	Hyp	Ref	Expression
1		0cn	$$⊢0\in ℂ$$
2		cos0	$$⊢\cos 0=1$$
3		ax-1ne0	$$⊢1\ne 0$$
4	2 3	eqnetri	$$⊢\cos 0\ne 0$$
5		tanval	$$⊢\left(0\in ℂ\wedge \cos 0\ne 0\right)\to \tan 0=\frac{\sin 0}{\cos 0}$$
6	1 4 5	mp2an	$$⊢\tan 0=\frac{\sin 0}{\cos 0}$$
7		sin0	$$⊢\sin 0=0$$
8	7	oveq1i	$$⊢\frac{\sin 0}{\cos 0}=\frac{0}{\cos 0}$$
9		ax-1cn	$$⊢1\in ℂ$$
10	2 9	eqeltri	$$⊢\cos 0\in ℂ$$
11	10 4	div0i	$$⊢\frac{0}{\cos 0}=0$$
12	6 8 11	3eqtri	$$⊢\tan 0=0$$