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