Metamath Proof Explorer

Theorem atantan

Description: The arctangent function is an inverse to tan . (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atantan 
|- ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arctan ` ( tan ` A ) ) = A )

Proof

Step Hyp Ref Expression
1 cosne0 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` A ) =/= 0 )
2 atandmtan 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) e. dom arctan )
3 1 2 syldan 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( tan ` A ) e. dom arctan )
4 atanval 
 |-  ( ( tan ` A ) e. dom arctan -> ( arctan ` ( tan ` A ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) ) )
5 3 4 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arctan ` ( tan ` A ) ) = ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) ) )
6 ax-1cn 
 |-  1 e. CC
7 ax-icn 
 |-  _i e. CC
8 tancl 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) e. CC )
9 1 8 syldan 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( tan ` A ) e. CC )
10 mulcl 
 |-  ( ( _i e. CC /\ ( tan ` A ) e. CC ) -> ( _i x. ( tan ` A ) ) e. CC )
11 7 9 10 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( tan ` A ) ) e. CC )
12 addcl 
 |-  ( ( 1 e. CC /\ ( _i x. ( tan ` A ) ) e. CC ) -> ( 1 + ( _i x. ( tan ` A ) ) ) e. CC )
13 6 11 12 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 + ( _i x. ( tan ` A ) ) ) e. CC )
14 atandm2 
 |-  ( ( tan ` A ) e. dom arctan <-> ( ( tan ` A ) e. CC /\ ( 1 - ( _i x. ( tan ` A ) ) ) =/= 0 /\ ( 1 + ( _i x. ( tan ` A ) ) ) =/= 0 ) )
15 3 14 sylib 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( tan ` A ) e. CC /\ ( 1 - ( _i x. ( tan ` A ) ) ) =/= 0 /\ ( 1 + ( _i x. ( tan ` A ) ) ) =/= 0 ) )
16 15 simp3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 + ( _i x. ( tan ` A ) ) ) =/= 0 )
17 13 16 logcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) e. CC )
18 subcl 
 |-  ( ( 1 e. CC /\ ( _i x. ( tan ` A ) ) e. CC ) -> ( 1 - ( _i x. ( tan ` A ) ) ) e. CC )
19 6 11 18 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 - ( _i x. ( tan ` A ) ) ) e. CC )
20 15 simp2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 - ( _i x. ( tan ` A ) ) ) =/= 0 )
21 19 20 logcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) e. CC )
22 17 21 negsubdi2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) = ( ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) )
23 efsub 
 |-  ( ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) e. CC /\ ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) e. CC ) -> ( exp ` ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) = ( ( exp ` ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) / ( exp ` ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) )
24 17 21 23 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) = ( ( exp ` ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) / ( exp ` ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) )
25 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
26 25 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` A ) e. CC )
27 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
28 27 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( sin ` A ) e. CC )
29 mulcl 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. ( sin ` A ) ) e. CC )
30 7 28 29 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( sin ` A ) ) e. CC )
31 26 30 26 1 divdird 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) / ( cos ` A ) ) = ( ( ( cos ` A ) / ( cos ` A ) ) + ( ( _i x. ( sin ` A ) ) / ( cos ` A ) ) ) )
32 26 1 dividd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( cos ` A ) / ( cos ` A ) ) = 1 )
33 7 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> _i e. CC )
34 33 28 26 1 divassd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` A ) ) / ( cos ` A ) ) = ( _i x. ( ( sin ` A ) / ( cos ` A ) ) ) )
35 tanval 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
36 1 35 syldan 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( tan ` A ) = ( ( sin ` A ) / ( cos ` A ) ) )
37 36 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( tan ` A ) ) = ( _i x. ( ( sin ` A ) / ( cos ` A ) ) ) )
38 34 37 eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. ( sin ` A ) ) / ( cos ` A ) ) = ( _i x. ( tan ` A ) ) )
39 32 38 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) / ( cos ` A ) ) + ( ( _i x. ( sin ` A ) ) / ( cos ` A ) ) ) = ( 1 + ( _i x. ( tan ` A ) ) ) )
40 31 39 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) / ( cos ` A ) ) = ( 1 + ( _i x. ( tan ` A ) ) ) )
41 efival 
 |-  ( A e. CC -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
42 41 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. A ) ) = ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) )
43 42 oveq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) / ( cos ` A ) ) = ( ( ( cos ` A ) + ( _i x. ( sin ` A ) ) ) / ( cos ` A ) ) )
44 eflog 
 |-  ( ( ( 1 + ( _i x. ( tan ` A ) ) ) e. CC /\ ( 1 + ( _i x. ( tan ` A ) ) ) =/= 0 ) -> ( exp ` ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) = ( 1 + ( _i x. ( tan ` A ) ) ) )
45 13 16 44 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) = ( 1 + ( _i x. ( tan ` A ) ) ) )
46 40 43 45 3eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` ( _i x. A ) ) / ( cos ` A ) ) = ( exp ` ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) )
47 26 30 26 1 divsubdird 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) / ( cos ` A ) ) = ( ( ( cos ` A ) / ( cos ` A ) ) - ( ( _i x. ( sin ` A ) ) / ( cos ` A ) ) ) )
48 32 38 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) / ( cos ` A ) ) - ( ( _i x. ( sin ` A ) ) / ( cos ` A ) ) ) = ( 1 - ( _i x. ( tan ` A ) ) ) )
49 47 48 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) / ( cos ` A ) ) = ( 1 - ( _i x. ( tan ` A ) ) ) )
50 negcl 
 |-  ( A e. CC -> -u A e. CC )
51 50 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u A e. CC )
52 efival 
 |-  ( -u A e. CC -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) )
53 51 52 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) )
54 cosneg 
 |-  ( A e. CC -> ( cos ` -u A ) = ( cos ` A ) )
55 54 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` -u A ) = ( cos ` A ) )
56 sinneg 
 |-  ( A e. CC -> ( sin ` -u A ) = -u ( sin ` A ) )
57 56 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( sin ` -u A ) = -u ( sin ` A ) )
58 57 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( sin ` -u A ) ) = ( _i x. -u ( sin ` A ) ) )
59 mulneg2 
 |-  ( ( _i e. CC /\ ( sin ` A ) e. CC ) -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
60 7 28 59 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. -u ( sin ` A ) ) = -u ( _i x. ( sin ` A ) ) )
61 58 60 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( sin ` -u A ) ) = -u ( _i x. ( sin ` A ) ) )
62 55 61 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( cos ` -u A ) + ( _i x. ( sin ` -u A ) ) ) = ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) )
63 53 62 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. -u A ) ) = ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) )
64 simpl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> A e. CC )
65 mulneg2 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. -u A ) = -u ( _i x. A ) )
66 7 64 65 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. -u A ) = -u ( _i x. A ) )
67 66 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. -u A ) ) = ( exp ` -u ( _i x. A ) ) )
68 26 30 negsubd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( cos ` A ) + -u ( _i x. ( sin ` A ) ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
69 63 67 68 3eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` -u ( _i x. A ) ) = ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) )
70 69 oveq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` -u ( _i x. A ) ) / ( cos ` A ) ) = ( ( ( cos ` A ) - ( _i x. ( sin ` A ) ) ) / ( cos ` A ) ) )
71 eflog 
 |-  ( ( ( 1 - ( _i x. ( tan ` A ) ) ) e. CC /\ ( 1 - ( _i x. ( tan ` A ) ) ) =/= 0 ) -> ( exp ` ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) = ( 1 - ( _i x. ( tan ` A ) ) ) )
72 19 20 71 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) = ( 1 - ( _i x. ( tan ` A ) ) ) )
73 49 70 72 3eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( exp ` -u ( _i x. A ) ) / ( cos ` A ) ) = ( exp ` ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) )
74 46 73 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) / ( cos ` A ) ) / ( ( exp ` -u ( _i x. A ) ) / ( cos ` A ) ) ) = ( ( exp ` ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) / ( exp ` ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) )
75 mulcl 
 |-  ( ( _i e. CC /\ A e. CC ) -> ( _i x. A ) e. CC )
76 7 64 75 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. A ) e. CC )
77 efcl 
 |-  ( ( _i x. A ) e. CC -> ( exp ` ( _i x. A ) ) e. CC )
78 76 77 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( _i x. A ) ) e. CC )
79 76 negcld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( _i x. A ) e. CC )
80 efcl 
 |-  ( -u ( _i x. A ) e. CC -> ( exp ` -u ( _i x. A ) ) e. CC )
81 79 80 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` -u ( _i x. A ) ) e. CC )
82 efne0 
 |-  ( -u ( _i x. A ) e. CC -> ( exp ` -u ( _i x. A ) ) =/= 0 )
83 79 82 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` -u ( _i x. A ) ) =/= 0 )
84 78 81 26 83 1 divcan7d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) / ( cos ` A ) ) / ( ( exp ` -u ( _i x. A ) ) / ( cos ` A ) ) ) = ( ( exp ` ( _i x. A ) ) / ( exp ` -u ( _i x. A ) ) ) )
85 efsub 
 |-  ( ( ( _i x. A ) e. CC /\ -u ( _i x. A ) e. CC ) -> ( exp ` ( ( _i x. A ) - -u ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) / ( exp ` -u ( _i x. A ) ) ) )
86 76 79 85 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( ( _i x. A ) - -u ( _i x. A ) ) ) = ( ( exp ` ( _i x. A ) ) / ( exp ` -u ( _i x. A ) ) ) )
87 76 76 subnegd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. A ) - -u ( _i x. A ) ) = ( ( _i x. A ) + ( _i x. A ) ) )
88 76 2timesd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( _i x. A ) ) = ( ( _i x. A ) + ( _i x. A ) ) )
89 87 88 eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. A ) - -u ( _i x. A ) ) = ( 2 x. ( _i x. A ) ) )
90 89 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( ( _i x. A ) - -u ( _i x. A ) ) ) = ( exp ` ( 2 x. ( _i x. A ) ) ) )
91 84 86 90 3eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( exp ` ( _i x. A ) ) / ( cos ` A ) ) / ( ( exp ` -u ( _i x. A ) ) / ( cos ` A ) ) ) = ( exp ` ( 2 x. ( _i x. A ) ) ) )
92 24 74 91 3eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( exp ` ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) = ( exp ` ( 2 x. ( _i x. A ) ) ) )
93 92 fveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( exp ` ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) ) = ( log ` ( exp ` ( 2 x. ( _i x. A ) ) ) ) )
94 64 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> A e. CC )
95 94 renegd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` -u A ) = -u ( Re ` A ) )
96 94 recld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` A ) e. RR )
97 96 renegcld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> -u ( Re ` A ) e. RR )
98 simpr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` A ) < 0 )
99 96 lt0neg1d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( ( Re ` A ) < 0 <-> 0 < -u ( Re ` A ) ) )
100 98 99 mpbid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> 0 < -u ( Re ` A ) )
101 eliooord 
 |-  ( ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( -u ( _pi / 2 ) < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) )
102 101 adantl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u ( _pi / 2 ) < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) )
103 102 simpld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( _pi / 2 ) < ( Re ` A ) )
104 103 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> -u ( _pi / 2 ) < ( Re ` A ) )
105 halfpire 
 |-  ( _pi / 2 ) e. RR
106 ltnegcon1 
 |-  ( ( ( _pi / 2 ) e. RR /\ ( Re ` A ) e. RR ) -> ( -u ( _pi / 2 ) < ( Re ` A ) <-> -u ( Re ` A ) < ( _pi / 2 ) ) )
107 105 96 106 sylancr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( -u ( _pi / 2 ) < ( Re ` A ) <-> -u ( Re ` A ) < ( _pi / 2 ) ) )
108 104 107 mpbid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> -u ( Re ` A ) < ( _pi / 2 ) )
109 0xr 
 |-  0 e. RR*
110 105 rexri 
 |-  ( _pi / 2 ) e. RR*
111 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( -u ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( -u ( Re ` A ) e. RR /\ 0 < -u ( Re ` A ) /\ -u ( Re ` A ) < ( _pi / 2 ) ) ) )
112 109 110 111 mp2an 
 |-  ( -u ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( -u ( Re ` A ) e. RR /\ 0 < -u ( Re ` A ) /\ -u ( Re ` A ) < ( _pi / 2 ) ) )
113 97 100 108 112 syl3anbrc 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> -u ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) )
114 95 113 eqeltrd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` -u A ) e. ( 0 (,) ( _pi / 2 ) ) )
115 tanregt0 
 |-  ( ( -u A e. CC /\ ( Re ` -u A ) e. ( 0 (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( tan ` -u A ) ) )
116 51 114 115 syl2an2r 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> 0 < ( Re ` ( tan ` -u A ) ) )
117 tanneg 
 |-  ( ( A e. CC /\ ( cos ` A ) =/= 0 ) -> ( tan ` -u A ) = -u ( tan ` A ) )
118 1 117 syldan 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( tan ` -u A ) = -u ( tan ` A ) )
119 118 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( tan ` -u A ) = -u ( tan ` A ) )
120 119 fveq2d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` ( tan ` -u A ) ) = ( Re ` -u ( tan ` A ) ) )
121 9 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( tan ` A ) e. CC )
122 121 renegd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` -u ( tan ` A ) ) = -u ( Re ` ( tan ` A ) ) )
123 120 122 eqtrd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` ( tan ` -u A ) ) = -u ( Re ` ( tan ` A ) ) )
124 116 123 breqtrd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> 0 < -u ( Re ` ( tan ` A ) ) )
125 9 recld 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` ( tan ` A ) ) e. RR )
126 125 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` ( tan ` A ) ) e. RR )
127 126 lt0neg1d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( ( Re ` ( tan ` A ) ) < 0 <-> 0 < -u ( Re ` ( tan ` A ) ) ) )
128 124 127 mpbird 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` ( tan ` A ) ) < 0 )
129 128 lt0ne0d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( Re ` ( tan ` A ) ) =/= 0 )
130 atanlogsub 
 |-  ( ( ( tan ` A ) e. dom arctan /\ ( Re ` ( tan ` A ) ) =/= 0 ) -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. ran log )
131 3 129 130 syl2an2r 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) < 0 ) -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. ran log )
132 1re 
 |-  1 e. RR
133 ioossre 
 |-  ( -u 1 (,) 1 ) C_ RR
134 7 a1i 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> _i e. CC )
135 11 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. ( tan ` A ) ) e. CC )
136 ine0 
 |-  _i =/= 0
137 136 a1i 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> _i =/= 0 )
138 ixi 
 |-  ( _i x. _i ) = -u 1
139 138 oveq1i 
 |-  ( ( _i x. _i ) x. ( tan ` A ) ) = ( -u 1 x. ( tan ` A ) )
140 9 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( tan ` A ) e. CC )
141 140 mulm1d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( -u 1 x. ( tan ` A ) ) = -u ( tan ` A ) )
142 118 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( tan ` -u A ) = -u ( tan ` A ) )
143 141 142 eqtr4d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( -u 1 x. ( tan ` A ) ) = ( tan ` -u A ) )
144 139 143 eqtrid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( _i x. _i ) x. ( tan ` A ) ) = ( tan ` -u A ) )
145 134 134 140 mulassd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( _i x. _i ) x. ( tan ` A ) ) = ( _i x. ( _i x. ( tan ` A ) ) ) )
146 138 oveq1i 
 |-  ( ( _i x. _i ) x. A ) = ( -u 1 x. A )
147 64 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> A e. CC )
148 147 mulm1d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( -u 1 x. A ) = -u A )
149 146 148 eqtrid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( _i x. _i ) x. A ) = -u A )
150 134 134 147 mulassd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( _i x. _i ) x. A ) = ( _i x. ( _i x. A ) ) )
151 149 150 eqtr3d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> -u A = ( _i x. ( _i x. A ) ) )
152 151 fveq2d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( tan ` -u A ) = ( tan ` ( _i x. ( _i x. A ) ) ) )
153 144 145 152 3eqtr3d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. ( _i x. ( tan ` A ) ) ) = ( tan ` ( _i x. ( _i x. A ) ) ) )
154 134 135 137 153 mvllmuld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. ( tan ` A ) ) = ( ( tan ` ( _i x. ( _i x. A ) ) ) / _i ) )
155 76 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. A ) e. CC )
156 reim 
 |-  ( A e. CC -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
157 156 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) = ( Im ` ( _i x. A ) ) )
158 157 eqeq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( Re ` A ) = 0 <-> ( Im ` ( _i x. A ) ) = 0 ) )
159 158 biimpa 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( Im ` ( _i x. A ) ) = 0 )
160 155 159 reim0bd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. A ) e. RR )
161 tanhbnd 
 |-  ( ( _i x. A ) e. RR -> ( ( tan ` ( _i x. ( _i x. A ) ) ) / _i ) e. ( -u 1 (,) 1 ) )
162 160 161 syl 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( tan ` ( _i x. ( _i x. A ) ) ) / _i ) e. ( -u 1 (,) 1 ) )
163 154 162 eqeltrd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. ( tan ` A ) ) e. ( -u 1 (,) 1 ) )
164 133 163 sselid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. ( tan ` A ) ) e. RR )
165 readdcl 
 |-  ( ( 1 e. RR /\ ( _i x. ( tan ` A ) ) e. RR ) -> ( 1 + ( _i x. ( tan ` A ) ) ) e. RR )
166 132 164 165 sylancr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( 1 + ( _i x. ( tan ` A ) ) ) e. RR )
167 df-neg 
 |-  -u 1 = ( 0 - 1 )
168 eliooord 
 |-  ( ( _i x. ( tan ` A ) ) e. ( -u 1 (,) 1 ) -> ( -u 1 < ( _i x. ( tan ` A ) ) /\ ( _i x. ( tan ` A ) ) < 1 ) )
169 163 168 syl 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( -u 1 < ( _i x. ( tan ` A ) ) /\ ( _i x. ( tan ` A ) ) < 1 ) )
170 169 simpld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> -u 1 < ( _i x. ( tan ` A ) ) )
171 167 170 eqbrtrrid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( 0 - 1 ) < ( _i x. ( tan ` A ) ) )
172 0red 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> 0 e. RR )
173 132 a1i 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> 1 e. RR )
174 172 173 164 ltsubadd2d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( 0 - 1 ) < ( _i x. ( tan ` A ) ) <-> 0 < ( 1 + ( _i x. ( tan ` A ) ) ) ) )
175 171 174 mpbid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> 0 < ( 1 + ( _i x. ( tan ` A ) ) ) )
176 166 175 elrpd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( 1 + ( _i x. ( tan ` A ) ) ) e. RR+ )
177 176 relogcld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) e. RR )
178 169 simprd 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( _i x. ( tan ` A ) ) < 1 )
179 difrp 
 |-  ( ( ( _i x. ( tan ` A ) ) e. RR /\ 1 e. RR ) -> ( ( _i x. ( tan ` A ) ) < 1 <-> ( 1 - ( _i x. ( tan ` A ) ) ) e. RR+ ) )
180 164 132 179 sylancl 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( _i x. ( tan ` A ) ) < 1 <-> ( 1 - ( _i x. ( tan ` A ) ) ) e. RR+ ) )
181 178 180 mpbid 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( 1 - ( _i x. ( tan ` A ) ) ) e. RR+ )
182 181 relogcld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) e. RR )
183 177 182 resubcld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. RR )
184 relogrn 
 |-  ( ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. RR -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. ran log )
185 183 184 syl 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ ( Re ` A ) = 0 ) -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. ran log )
186 64 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> A e. CC )
187 186 recld 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> ( Re ` A ) e. RR )
188 simpr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` A ) )
189 102 simprd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) < ( _pi / 2 ) )
190 189 adantr 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> ( Re ` A ) < ( _pi / 2 ) )
191 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( ( Re ` A ) e. RR /\ 0 < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) ) )
192 109 110 191 mp2an 
 |-  ( ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( ( Re ` A ) e. RR /\ 0 < ( Re ` A ) /\ ( Re ` A ) < ( _pi / 2 ) ) )
193 187 188 190 192 syl3anbrc 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) )
194 tanregt0 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( 0 (,) ( _pi / 2 ) ) ) -> 0 < ( Re ` ( tan ` A ) ) )
195 64 193 194 syl2an2r 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> 0 < ( Re ` ( tan ` A ) ) )
196 195 gt0ne0d 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> ( Re ` ( tan ` A ) ) =/= 0 )
197 3 196 130 syl2an2r 
 |-  ( ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) /\ 0 < ( Re ` A ) ) -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. ran log )
198 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
199 198 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Re ` A ) e. RR )
200 0re 
 |-  0 e. RR
201 lttri4 
 |-  ( ( ( Re ` A ) e. RR /\ 0 e. RR ) -> ( ( Re ` A ) < 0 \/ ( Re ` A ) = 0 \/ 0 < ( Re ` A ) ) )
202 199 200 201 sylancl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( Re ` A ) < 0 \/ ( Re ` A ) = 0 \/ 0 < ( Re ` A ) ) )
203 131 185 197 202 mpjao3dan 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. ran log )
204 logef 
 |-  ( ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) e. ran log -> ( log ` ( exp ` ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) ) = ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) )
205 203 204 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( exp ` ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) ) ) = ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) )
206 2cn 
 |-  2 e. CC
207 mulcl 
 |-  ( ( 2 e. CC /\ ( _i x. A ) e. CC ) -> ( 2 x. ( _i x. A ) ) e. CC )
208 206 76 207 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( _i x. A ) ) e. CC )
209 picn 
 |-  _pi e. CC
210 2ne0 
 |-  2 =/= 0
211 divneg 
 |-  ( ( _pi e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> -u ( _pi / 2 ) = ( -u _pi / 2 ) )
212 209 206 210 211 mp3an 
 |-  -u ( _pi / 2 ) = ( -u _pi / 2 )
213 212 103 eqbrtrrid 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u _pi / 2 ) < ( Re ` A ) )
214 pire 
 |-  _pi e. RR
215 214 renegcli 
 |-  -u _pi e. RR
216 215 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _pi e. RR )
217 2re 
 |-  2 e. RR
218 217 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 2 e. RR )
219 2pos 
 |-  0 < 2
220 219 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 0 < 2 )
221 ltdivmul 
 |-  ( ( -u _pi e. RR /\ ( Re ` A ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( -u _pi / 2 ) < ( Re ` A ) <-> -u _pi < ( 2 x. ( Re ` A ) ) ) )
222 216 199 218 220 221 syl112anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( -u _pi / 2 ) < ( Re ` A ) <-> -u _pi < ( 2 x. ( Re ` A ) ) ) )
223 213 222 mpbid 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _pi < ( 2 x. ( Re ` A ) ) )
224 immul2 
 |-  ( ( 2 e. RR /\ ( _i x. A ) e. CC ) -> ( Im ` ( 2 x. ( _i x. A ) ) ) = ( 2 x. ( Im ` ( _i x. A ) ) ) )
225 217 76 224 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( 2 x. ( _i x. A ) ) ) = ( 2 x. ( Im ` ( _i x. A ) ) ) )
226 157 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( Re ` A ) ) = ( 2 x. ( Im ` ( _i x. A ) ) ) )
227 225 226 eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( 2 x. ( _i x. A ) ) ) = ( 2 x. ( Re ` A ) ) )
228 223 227 breqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u _pi < ( Im ` ( 2 x. ( _i x. A ) ) ) )
229 remulcl 
 |-  ( ( 2 e. RR /\ ( Re ` A ) e. RR ) -> ( 2 x. ( Re ` A ) ) e. RR )
230 217 199 229 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( Re ` A ) ) e. RR )
231 214 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> _pi e. RR )
232 ltmuldiv2 
 |-  ( ( ( Re ` A ) e. RR /\ _pi e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. ( Re ` A ) ) < _pi <-> ( Re ` A ) < ( _pi / 2 ) ) )
233 199 231 218 220 232 syl112anc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( 2 x. ( Re ` A ) ) < _pi <-> ( Re ` A ) < ( _pi / 2 ) ) )
234 189 233 mpbird 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( Re ` A ) ) < _pi )
235 230 231 234 ltled 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( Re ` A ) ) <_ _pi )
236 227 235 eqbrtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( Im ` ( 2 x. ( _i x. A ) ) ) <_ _pi )
237 ellogrn 
 |-  ( ( 2 x. ( _i x. A ) ) e. ran log <-> ( ( 2 x. ( _i x. A ) ) e. CC /\ -u _pi < ( Im ` ( 2 x. ( _i x. A ) ) ) /\ ( Im ` ( 2 x. ( _i x. A ) ) ) <_ _pi ) )
238 208 228 236 237 syl3anbrc 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. ( _i x. A ) ) e. ran log )
239 logef 
 |-  ( ( 2 x. ( _i x. A ) ) e. ran log -> ( log ` ( exp ` ( 2 x. ( _i x. A ) ) ) ) = ( 2 x. ( _i x. A ) ) )
240 238 239 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( log ` ( exp ` ( 2 x. ( _i x. A ) ) ) ) = ( 2 x. ( _i x. A ) ) )
241 93 205 240 3eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) = ( 2 x. ( _i x. A ) ) )
242 241 negeqd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> -u ( ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) ) = -u ( 2 x. ( _i x. A ) ) )
243 22 242 eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) = -u ( 2 x. ( _i x. A ) ) )
244 243 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i / 2 ) x. ( ( log ` ( 1 - ( _i x. ( tan ` A ) ) ) ) - ( log ` ( 1 + ( _i x. ( tan ` A ) ) ) ) ) ) = ( ( _i / 2 ) x. -u ( 2 x. ( _i x. A ) ) ) )
245 halfcl 
 |-  ( _i e. CC -> ( _i / 2 ) e. CC )
246 7 245 mp1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i / 2 ) e. CC )
247 206 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> 2 e. CC )
248 246 247 79 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( _i / 2 ) x. 2 ) x. -u ( _i x. A ) ) = ( ( _i / 2 ) x. ( 2 x. -u ( _i x. A ) ) ) )
249 7 206 210 divcan1i 
 |-  ( ( _i / 2 ) x. 2 ) = _i
250 249 oveq1i 
 |-  ( ( ( _i / 2 ) x. 2 ) x. -u ( _i x. A ) ) = ( _i x. -u ( _i x. A ) )
251 33 33 51 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. _i ) x. -u A ) = ( _i x. ( _i x. -u A ) ) )
252 138 oveq1i 
 |-  ( ( _i x. _i ) x. -u A ) = ( -u 1 x. -u A )
253 mul2neg 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( -u 1 x. -u A ) = ( 1 x. A ) )
254 6 64 253 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u 1 x. -u A ) = ( 1 x. A ) )
255 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
256 255 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 1 x. A ) = A )
257 254 256 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( -u 1 x. -u A ) = A )
258 252 257 eqtrid 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i x. _i ) x. -u A ) = A )
259 66 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. ( _i x. -u A ) ) = ( _i x. -u ( _i x. A ) ) )
260 251 258 259 3eqtr3rd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( _i x. -u ( _i x. A ) ) = A )
261 250 260 eqtrid 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( ( _i / 2 ) x. 2 ) x. -u ( _i x. A ) ) = A )
262 mulneg2 
 |-  ( ( 2 e. CC /\ ( _i x. A ) e. CC ) -> ( 2 x. -u ( _i x. A ) ) = -u ( 2 x. ( _i x. A ) ) )
263 206 76 262 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( 2 x. -u ( _i x. A ) ) = -u ( 2 x. ( _i x. A ) ) )
264 263 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i / 2 ) x. ( 2 x. -u ( _i x. A ) ) ) = ( ( _i / 2 ) x. -u ( 2 x. ( _i x. A ) ) ) )
265 248 261 264 3eqtr3rd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( _i / 2 ) x. -u ( 2 x. ( _i x. A ) ) ) = A )
266 5 244 265 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arctan ` ( tan ` A ) ) = A )