Metamath Proof Explorer

Theorem tanval2

Description: Express the tangent function directly in terms of exp . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion tanval2 
|- ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
2 2cn 
 |-  2 e. CC
3 ax-icn 
 |-  _i e. CC
4 2 3 mulcomi 
 |-  ( 2 x. _i ) = ( _i x. 2 )
5 4 oveq2i 
 |-  ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. 2 ) )
6 sinval 
 |-  ( A e. CC -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
7 6 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sin ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( 2 x. _i ) ) )
8 simpl 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> A e. CC )
9 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
10 3 8 9 sylancr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( _i x. A ) e. CC )
11 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
12 10 11 syl 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( exp ` ( _i x. A ) ) e. CC )
13 negicn 
 |-  -u _i e. CC
14 mulcl 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
15 13 8 14 sylancr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( -u _i x. A ) e. CC )
16 efcl 
 |-  ( ( -u _i x. A ) e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
17 15 16 syl 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( exp ` ( -u _i x. A ) ) e. CC )
18 12 17 subcld 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) e. CC )
19 3 a1i 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> _i e. CC )
20 2 a1i 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> 2 e. CC )
21 ine0 
 |-  _i =/= 0
22 21 a1i 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> _i =/= 0 )
23 2ne0 
 |-  2 =/= 0
24 23 a1i 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> 2 =/= 0 )
25 18 19 20 22 24 divdiv1d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) / 2 ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. 2 ) ) )
26 5 7 25 3eqtr4a 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( sin ` A ) = ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) / 2 ) )
27 cosval 
 |-  ( A e. CC -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
28 27 adantr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
29 26 28 oveq12d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( sin ` A ) / ( cos ` A ) ) = ( ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) / 2 ) / ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) ) )
30 1 29 eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) / 2 ) / ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) ) )
31 18 19 22 divcld 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) e. CC )
32 12 17 addcld 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) e. CC )
33 simpr 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( cos ` A ) =/= 0 )
34 28 33 eqnetrrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) =/= 0 )
35 32 20 24 diveq0ad 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) = 0 <-> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) = 0 ) )
36 35 necon3bid 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) =/= 0 <-> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) =/= 0 ) )
37 34 36 mpbid 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) =/= 0 )
38 31 32 20 37 24 divcan7d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) / 2 ) / ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) ) = ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) / ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) )
39 18 19 32 22 37 divdiv1d 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / _i ) / ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
40 30 38 39 3eqtrd 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )