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$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		cos0	$⊢ \cos 0 = 1$
3		ax-1ne0	$⊢ 1 \neq 0$
4	2 3	eqnetri	$⊢ \cos 0 \neq 0$
5		tanval	$⊢ (0 \in ℂ \land \cos 0 \neq 0) \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$

Metamath Proof Explorer