Metamath Proof Explorer

Theorem tanval3

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

Ref Expression
Assertion tanval3 
|- ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 simpl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> A e. CC )
3 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
4 1 2 3 sylancr 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. A ) e. CC )
5 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
6 4 5 syl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( _i x. A ) ) e. CC )
7 negicn 
 |-  -u _i e. CC
8 mulcl 
 |-  ( ( -u _i e. CC /\ A e. CC ) -> ( -u _i x. A ) e. CC )
9 7 2 8 sylancr 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( -u _i x. A ) e. CC )
10 efcl 
 |-  ( ( -u _i x. A ) e. CC -> ( exp ` ( -u _i x. A ) ) e. CC )
11 9 10 syl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( -u _i x. A ) ) e. CC )
12 6 11 subcld 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) e. CC )
13 6 11 addcld 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) e. CC )
14 mulcl 
 |-  ( ( _i e. CC /\ ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) e. CC ) -> ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) e. CC )
15 1 13 14 sylancr 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) e. CC )
16 2z 
 |-  2 e. ZZ
17 efexp 
 |-  ( ( ( _i x. A ) e. CC /\ 2 e. ZZ ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) ^ 2 ) )
18 4 16 17 sylancl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) ^ 2 ) )
19 6 sqvald 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) ^ 2 ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
20 18 19 eqtrd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) )
21 mulneg1 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( -u _i x. A ) = -u ( _i x. A ) )
22 1 2 21 sylancr 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( -u _i x. A ) = -u ( _i x. A ) )
23 22 fveq2d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( -u _i x. A ) ) = ( exp ` -u ( _i x. A ) ) )
24 23 oveq2d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( exp ` -u ( _i x. A ) ) ) )
25 efcan 
 |-  ( ( _i x. A ) e. CC -> ( ( exp ` ( _i x. A ) ) x. ( exp ` -u ( _i x. A ) ) ) = 1 )
26 4 25 syl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( exp ` -u ( _i x. A ) ) ) = 1 )
27 24 26 eqtr2d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> 1 = ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) )
28 20 27 oveq12d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) + ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
29 6 6 11 adddid 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) + ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
30 28 29 eqtr4d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) = ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) )
31 30 oveq2d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) = ( _i x. ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
32 1 a1i 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> _i e. CC )
33 32 6 13 mul12d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) = ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
34 31 33 eqtrd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) = ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
35 2cn 
 |-  2 e. CC
36 mulcl 
 |-  ( ( 2 e. CC /\ ( _i x. A ) e. CC ) -> ( 2 x. ( _i x. A ) ) e. CC )
37 35 4 36 sylancr 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( 2 x. ( _i x. A ) ) e. CC )
38 efcl 
 |-  ( ( 2 x. ( _i x. A ) ) e. CC -> ( exp ` ( 2 x. ( _i x. A ) ) ) e. CC )
39 37 38 syl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( 2 x. ( _i x. A ) ) ) e. CC )
40 ax-1cn 
 |-  1 e. CC
41 addcl 
 |-  ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) e. CC /\ 1 e. CC ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) e. CC )
42 39 40 41 sylancl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) e. CC )
43 ine0 
 |-  _i =/= 0
44 43 a1i 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> _i =/= 0 )
45 simpr 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 )
46 32 42 44 45 mulne0d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) =/= 0 )
47 34 46 eqnetrrd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) =/= 0 )
48 6 15 47 mulne0bbd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) =/= 0 )
49 efne0 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) =/= 0 )
50 4 49 syl 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( exp ` ( _i x. A ) ) =/= 0 )
51 12 15 6 48 50 divcan5d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) / ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( 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 ) ) ) ) ) )
52 20 27 oveq12d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
53 6 6 11 subdid 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( exp ` ( _i x. A ) ) ) - ( ( exp ` ( _i x. A ) ) x. ( exp ` ( -u _i x. A ) ) ) ) )
54 52 53 eqtr4d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) = ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) )
55 54 34 oveq12d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) ) = ( ( ( exp ` ( _i x. A ) ) x. ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) ) / ( ( exp ` ( _i x. A ) ) x. ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) ) )
56 cosval 
 |-  ( A e. CC -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
57 56 adantr 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( cos ` A ) = ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) )
58 2cnd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> 2 e. CC )
59 32 13 48 mulne0bbd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) =/= 0 )
60 2ne0 
 |-  2 =/= 0
61 60 a1i 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> 2 =/= 0 )
62 13 58 59 61 divne0d 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) / 2 ) =/= 0 )
63 57 62 eqnetrd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( cos ` A ) =/= 0 )
64 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 ) ) ) ) ) )
65 63 64 syldan 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( _i x. A ) ) - ( exp ` ( -u _i x. A ) ) ) / ( _i x. ( ( exp ` ( _i x. A ) ) + ( exp ` ( -u _i x. A ) ) ) ) ) )
66 51 55 65 3eqtr4rd 
 |-  ( ( A e. CC /\ ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) =/= 0 ) -> ( tan ` A ) = ( ( ( exp ` ( 2 x. ( _i x. A ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. A ) ) ) + 1 ) ) ) )