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 ∈ ℂ
2		cos0	⊢ ( cos ‘ 0 ) = 1
3		ax-1ne0	⊢ 1 ≠ 0
4	2 3	eqnetri	⊢ ( cos ‘ 0 ) ≠ 0
5		tanval	⊢ ( ( 0 ∈ ℂ ∧ ( cos ‘ 0 ) ≠ 0 ) → ( tan ‘ 0 ) = ( ( sin ‘ 0 ) / ( cos ‘ 0 ) ) )
6	1 4 5	mp2an	⊢ ( tan ‘ 0 ) = ( ( sin ‘ 0 ) / ( cos ‘ 0 ) )
7		sin0	⊢ ( sin ‘ 0 ) = 0
8	7	oveq1i	⊢ ( ( sin ‘ 0 ) / ( cos ‘ 0 ) ) = ( 0 / ( cos ‘ 0 ) )
9		ax-1cn	⊢ 1 ∈ ℂ
10	2 9	eqeltri	⊢ ( cos ‘ 0 ) ∈ ℂ
11	10 4	div0i	⊢ ( 0 / ( cos ‘ 0 ) ) = 0
12	6 8 11	3eqtri	⊢ ( tan ‘ 0 ) = 0