Metamath Proof Explorer

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 e. CC
2 cos0 
 |-  ( cos ` 0 ) = 1
3 ax-1ne0 
 |-  1 =/= 0
4 2 3 eqnetri 
 |-  ( cos ` 0 ) =/= 0
5 tanval 
 |-  ( ( 0 e. CC /\ ( 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 e. CC
10 2 9 eqeltri 
 |-  ( cos ` 0 ) e. CC
11 10 4 div0i 
 |-  ( 0 / ( cos ` 0 ) ) = 0
12 6 8 11 3eqtri 
 |-  ( tan ` 0 ) = 0