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