This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )