Metamath Proof Explorer


Theorem tanval

Description: Value of the tangent function. (Contributed by Mario Carneiro, 14-Mar-2014)

Ref Expression
Assertion tanval
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )

Proof

Step Hyp Ref Expression
1 simpl
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> A e. CC )
2 coscl
 |-  ( A e. CC -> ( cos ` A ) e. CC )
3 2 anim1i
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) )
4 eldifsn
 |-  ( ( cos ` A ) e. ( CC \ { 0 } ) <-> ( ( cos ` A ) e. CC /\ ( cos ` A ) =/= 0 ) )
5 3 4 sylibr
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) e. ( CC \ { 0 } ) )
6 cosf
 |-  cos : CC --> CC
7 ffn
 |-  ( cos : CC --> CC -> cos Fn CC )
8 elpreima
 |-  ( cos Fn CC -> ( A e. ( `' cos " ( CC \ { 0 } ) ) <-> ( A e. CC /\ ( cos ` A ) e. ( CC \ { 0 } ) ) ) )
9 6 7 8 mp2b
 |-  ( A e. ( `' cos " ( CC \ { 0 } ) ) <-> ( A e. CC /\ ( cos ` A ) e. ( CC \ { 0 } ) ) )
10 1 5 9 sylanbrc
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> A e. ( `' cos " ( CC \ { 0 } ) ) )
11 fveq2
 |-  ( x = A -> ( sin ` x ) = ( sin ` A ) )
12 fveq2
 |-  ( x = A -> ( cos ` x ) = ( cos ` A ) )
13 11 12 oveq12d
 |-  ( x = A -> ( ( sin ` x ) / ( cos ` x ) ) = ( ( sin ` A ) / ( cos ` A ) ) )
14 df-tan
 |-  tan = ( x e. ( `' cos " ( CC \ { 0 } ) ) |-> ( ( sin ` x ) / ( cos ` x ) ) )
15 ovex
 |-  ( ( sin ` A ) / ( cos ` A ) ) e. _V
16 13 14 15 fvmpt
 |-  ( A e. ( `' cos " ( CC \ { 0 } ) ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
17 10 16 syl
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )