Metamath Proof Explorer

Theorem tanarg

Description: The basic relation between the "arg" function Im o. log and the arctangent. (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Assertion tanarg 
|- ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( tan ` ( Im ` ( log ` A ) ) ) = ( ( Im ` A ) / ( Re ` A ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = 0 -> ( Re ` A ) = ( Re ` 0 ) )
2 re0 
 |-  ( Re ` 0 ) = 0
3 1 2 eqtrdi 
 |-  ( A = 0 -> ( Re ` A ) = 0 )
4 3 necon3i 
 |-  ( ( Re ` A ) =/= 0 -> A =/= 0 )
5 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
6 4 5 sylan2 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( log ` A ) e. CC )
7 6 imcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( log ` A ) ) e. RR )
8 7 recnd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` ( log ` A ) ) e. CC )
9 sqcl 
 |-  ( A e. CC -> ( A ^ 2 ) e. CC )
10 9 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A ^ 2 ) e. CC )
11 abscl 
 |-  ( A e. CC -> ( abs ` A ) e. RR )
12 11 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( abs ` A ) e. RR )
13 12 recnd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( abs ` A ) e. CC )
14 13 sqcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( abs ` A ) ^ 2 ) e. CC )
15 absrpcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( abs ` A ) e. RR+ )
16 4 15 sylan2 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( abs ` A ) e. RR+ )
17 16 rpne0d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( abs ` A ) =/= 0 )
18 sqne0 
 |-  ( ( abs ` A ) e. CC -> ( ( ( abs ` A ) ^ 2 ) =/= 0 <-> ( abs ` A ) =/= 0 ) )
19 13 18 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( abs ` A ) ^ 2 ) =/= 0 <-> ( abs ` A ) =/= 0 ) )
20 17 19 mpbird 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( abs ` A ) ^ 2 ) =/= 0 )
21 10 14 14 20 divdird 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) + ( ( ( abs ` A ) ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) ) )
22 ax-icn 
 |-  _i e. CC
23 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` ( log ` A ) ) e. CC ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
24 22 8 23 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( Im ` ( log ` A ) ) ) e. CC )
25 2z 
 |-  2 e. ZZ
26 efexp 
 |-  ( ( ( _i x. ( Im ` ( log ` A ) ) ) e. CC /\ 2 e. ZZ ) -> ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) = ( ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ^ 2 ) )
27 24 25 26 sylancl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) = ( ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ^ 2 ) )
28 efiarg 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
29 4 28 sylan2 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) = ( A / ( abs ` A ) ) )
30 29 oveq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( exp ` ( _i x. ( Im ` ( log ` A ) ) ) ) ^ 2 ) = ( ( A / ( abs ` A ) ) ^ 2 ) )
31 simpl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> A e. CC )
32 31 13 17 sqdivd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A / ( abs ` A ) ) ^ 2 ) = ( ( A ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) )
33 27 30 32 3eqtrrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) = ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) )
34 14 20 dividd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( abs ` A ) ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) = 1 )
35 33 34 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( A ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) + ( ( ( abs ` A ) ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) ) = ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) )
36 21 35 eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) = ( ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) )
37 10 14 addcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) e. CC )
38 22 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> _i e. CC )
39 2cn 
 |-  2 e. CC
40 recl 
 |-  ( A e. CC -> ( Re ` A ) e. RR )
41 40 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) e. RR )
42 41 recnd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) e. CC )
43 42 sqcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) ^ 2 ) e. CC )
44 mulcl 
 |-  ( ( 2 e. CC /\ ( ( Re ` A ) ^ 2 ) e. CC ) -> ( 2 x. ( ( Re ` A ) ^ 2 ) ) e. CC )
45 39 43 44 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Re ` A ) ^ 2 ) ) e. CC )
46 39 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> 2 e. CC )
47 imcl 
 |-  ( A e. CC -> ( Im ` A ) e. RR )
48 47 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` A ) e. RR )
49 48 recnd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Im ` A ) e. CC )
50 42 49 mulcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) x. ( Im ` A ) ) e. CC )
51 38 46 50 mul12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) = ( 2 x. ( _i x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) )
52 38 42 49 mul12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( Re ` A ) x. ( Im ` A ) ) ) = ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) )
53 52 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( _i x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) = ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) )
54 51 53 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) = ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) )
55 mulcl 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( _i x. ( Im ` A ) ) e. CC )
56 22 49 55 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( Im ` A ) ) e. CC )
57 42 56 mulcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) e. CC )
58 mulcl 
 |-  ( ( 2 e. CC /\ ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) e. CC ) -> ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) e. CC )
59 39 57 58 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) e. CC )
60 54 59 eqeltrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) e. CC )
61 38 45 60 adddid 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( 2 x. ( ( Re ` A ) ^ 2 ) ) + ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) ) = ( ( _i x. ( 2 x. ( ( Re ` A ) ^ 2 ) ) ) + ( _i x. ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) ) )
62 mulcl 
 |-  ( ( ( Re ` A ) e. CC /\ _i e. CC ) -> ( ( Re ` A ) x. _i ) e. CC )
63 42 22 62 sylancl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) x. _i ) e. CC )
64 46 63 42 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) = ( 2 x. ( ( ( Re ` A ) x. _i ) x. ( Re ` A ) ) ) )
65 42 sqvald 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) ^ 2 ) = ( ( Re ` A ) x. ( Re ` A ) ) )
66 65 oveq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( Re ` A ) ^ 2 ) x. _i ) = ( ( ( Re ` A ) x. ( Re ` A ) ) x. _i ) )
67 mulcom 
 |-  ( ( ( ( Re ` A ) ^ 2 ) e. CC /\ _i e. CC ) -> ( ( ( Re ` A ) ^ 2 ) x. _i ) = ( _i x. ( ( Re ` A ) ^ 2 ) ) )
68 43 22 67 sylancl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( Re ` A ) ^ 2 ) x. _i ) = ( _i x. ( ( Re ` A ) ^ 2 ) ) )
69 42 42 38 mul32d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( Re ` A ) x. ( Re ` A ) ) x. _i ) = ( ( ( Re ` A ) x. _i ) x. ( Re ` A ) ) )
70 66 68 69 3eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( Re ` A ) ^ 2 ) ) = ( ( ( Re ` A ) x. _i ) x. ( Re ` A ) ) )
71 70 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( _i x. ( ( Re ` A ) ^ 2 ) ) ) = ( 2 x. ( ( ( Re ` A ) x. _i ) x. ( Re ` A ) ) ) )
72 46 38 43 mul12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( _i x. ( ( Re ` A ) ^ 2 ) ) ) = ( _i x. ( 2 x. ( ( Re ` A ) ^ 2 ) ) ) )
73 64 71 72 3eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) = ( _i x. ( 2 x. ( ( Re ` A ) ^ 2 ) ) ) )
74 ixi 
 |-  ( _i x. _i ) = -u 1
75 74 oveq1i 
 |-  ( ( _i x. _i ) x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) = ( -u 1 x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) )
76 mulcl 
 |-  ( ( 2 e. CC /\ ( Im ` A ) e. CC ) -> ( 2 x. ( Im ` A ) ) e. CC )
77 39 49 76 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( Im ` A ) ) e. CC )
78 77 42 mulcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) e. CC )
79 38 38 78 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i x. _i ) x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) = ( _i x. ( _i x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) ) )
80 75 79 eqtr3id 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( -u 1 x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) = ( _i x. ( _i x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) ) )
81 78 mulm1d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( -u 1 x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) = -u ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) )
82 46 49 42 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) = ( 2 x. ( ( Im ` A ) x. ( Re ` A ) ) ) )
83 49 42 mulcomd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Im ` A ) x. ( Re ` A ) ) = ( ( Re ` A ) x. ( Im ` A ) ) )
84 83 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Im ` A ) x. ( Re ` A ) ) ) = ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) )
85 82 84 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) = ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) )
86 85 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) = ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) )
87 86 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( _i x. ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) ) = ( _i x. ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) )
88 80 81 87 3eqtr3d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> -u ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) = ( _i x. ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) )
89 73 88 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) + -u ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) = ( ( _i x. ( 2 x. ( ( Re ` A ) ^ 2 ) ) ) + ( _i x. ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) ) )
90 mulcl 
 |-  ( ( 2 e. CC /\ ( ( Re ` A ) x. _i ) e. CC ) -> ( 2 x. ( ( Re ` A ) x. _i ) ) e. CC )
91 39 63 90 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Re ` A ) x. _i ) ) e. CC )
92 91 42 mulcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) e. CC )
93 92 78 negsubd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) + -u ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) - ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) )
94 61 89 93 3eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( 2 x. ( ( Re ` A ) ^ 2 ) ) + ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) - ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) )
95 49 sqcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Im ` A ) ^ 2 ) e. CC )
96 59 95 subcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) e. CC )
97 43 96 43 95 add4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) ) + ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( ( Re ` A ) ^ 2 ) ) + ( ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) + ( ( Im ` A ) ^ 2 ) ) ) )
98 replim 
 |-  ( A e. CC -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
99 98 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> A = ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) )
100 99 oveq1d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A ^ 2 ) = ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ^ 2 ) )
101 binom2 
 |-  ( ( ( Re ` A ) e. CC /\ ( _i x. ( Im ` A ) ) e. CC ) -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ^ 2 ) = ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) + ( ( _i x. ( Im ` A ) ) ^ 2 ) ) )
102 42 56 101 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ^ 2 ) = ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) + ( ( _i x. ( Im ` A ) ) ^ 2 ) ) )
103 sqmul 
 |-  ( ( _i e. CC /\ ( Im ` A ) e. CC ) -> ( ( _i x. ( Im ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( Im ` A ) ^ 2 ) ) )
104 22 49 103 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i x. ( Im ` A ) ) ^ 2 ) = ( ( _i ^ 2 ) x. ( ( Im ` A ) ^ 2 ) ) )
105 i2 
 |-  ( _i ^ 2 ) = -u 1
106 105 oveq1i 
 |-  ( ( _i ^ 2 ) x. ( ( Im ` A ) ^ 2 ) ) = ( -u 1 x. ( ( Im ` A ) ^ 2 ) )
107 104 106 eqtrdi 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i x. ( Im ` A ) ) ^ 2 ) = ( -u 1 x. ( ( Im ` A ) ^ 2 ) ) )
108 95 mulm1d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( -u 1 x. ( ( Im ` A ) ^ 2 ) ) = -u ( ( Im ` A ) ^ 2 ) )
109 107 108 eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i x. ( Im ` A ) ) ^ 2 ) = -u ( ( Im ` A ) ^ 2 ) )
110 109 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) + ( ( _i x. ( Im ` A ) ) ^ 2 ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) + -u ( ( Im ` A ) ^ 2 ) ) )
111 43 59 addcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) e. CC )
112 111 95 negsubd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) + -u ( ( Im ` A ) ^ 2 ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) )
113 102 110 112 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( Re ` A ) + ( _i x. ( Im ` A ) ) ) ^ 2 ) = ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) )
114 43 59 95 addsubassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) ) )
115 100 113 114 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( A ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) ) )
116 absvalsq2 
 |-  ( A e. CC -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
117 116 adantr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( abs ` A ) ^ 2 ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
118 115 117 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) ) + ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
119 43 2timesd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Re ` A ) ^ 2 ) ) = ( ( ( Re ` A ) ^ 2 ) + ( ( Re ` A ) ^ 2 ) ) )
120 59 95 npcand 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) + ( ( Im ` A ) ^ 2 ) ) = ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) )
121 53 51 120 3eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) = ( ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) + ( ( Im ` A ) ^ 2 ) ) )
122 119 121 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) ^ 2 ) ) + ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( ( Re ` A ) ^ 2 ) ) + ( ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) + ( ( Im ` A ) ^ 2 ) ) ) )
123 97 118 122 3eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) = ( ( 2 x. ( ( Re ` A ) ^ 2 ) ) + ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) )
124 123 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) = ( _i x. ( ( 2 x. ( ( Re ` A ) ^ 2 ) ) + ( _i x. ( 2 x. ( ( Re ` A ) x. ( Im ` A ) ) ) ) ) ) )
125 91 77 42 subdird 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Re ` A ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Re ` A ) ) - ( ( 2 x. ( Im ` A ) ) x. ( Re ` A ) ) ) )
126 94 124 125 3eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Re ` A ) ) )
127 91 77 subcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) e. CC )
128 mulcom 
 |-  ( ( ( Re ` A ) e. CC /\ _i e. CC ) -> ( ( Re ` A ) x. _i ) = ( _i x. ( Re ` A ) ) )
129 42 22 128 sylancl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) x. _i ) = ( _i x. ( Re ` A ) ) )
130 simpr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( Re ` A ) =/= 0 )
131 eleq1 
 |-  ( ( _i x. ( Re ` A ) ) = ( Im ` A ) -> ( ( _i x. ( Re ` A ) ) e. RR <-> ( Im ` A ) e. RR ) )
132 48 131 syl5ibrcom 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i x. ( Re ` A ) ) = ( Im ` A ) -> ( _i x. ( Re ` A ) ) e. RR ) )
133 rimul 
 |-  ( ( ( Re ` A ) e. RR /\ ( _i x. ( Re ` A ) ) e. RR ) -> ( Re ` A ) = 0 )
134 41 132 133 syl6an 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i x. ( Re ` A ) ) = ( Im ` A ) -> ( Re ` A ) = 0 ) )
135 134 necon3d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) =/= 0 -> ( _i x. ( Re ` A ) ) =/= ( Im ` A ) ) )
136 130 135 mpd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( Re ` A ) ) =/= ( Im ` A ) )
137 129 136 eqnetrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Re ` A ) x. _i ) =/= ( Im ` A ) )
138 91 77 subeq0ad 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) = 0 <-> ( 2 x. ( ( Re ` A ) x. _i ) ) = ( 2 x. ( Im ` A ) ) ) )
139 2ne0 
 |-  2 =/= 0
140 139 a1i 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> 2 =/= 0 )
141 63 49 46 140 mulcand 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. _i ) ) = ( 2 x. ( Im ` A ) ) <-> ( ( Re ` A ) x. _i ) = ( Im ` A ) ) )
142 138 141 bitrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) = 0 <-> ( ( Re ` A ) x. _i ) = ( Im ` A ) ) )
143 142 necon3bid 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) =/= 0 <-> ( ( Re ` A ) x. _i ) =/= ( Im ` A ) ) )
144 137 143 mpbird 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) =/= 0 )
145 127 42 144 130 mulne0d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Re ` A ) ) =/= 0 )
146 126 145 eqnetrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) =/= 0 )
147 oveq2 
 |-  ( ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) = 0 -> ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) = ( _i x. 0 ) )
148 it0e0 
 |-  ( _i x. 0 ) = 0
149 147 148 eqtrdi 
 |-  ( ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) = 0 -> ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) = 0 )
150 149 necon3i 
 |-  ( ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) =/= 0 -> ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) =/= 0 )
151 146 150 syl 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) =/= 0 )
152 37 14 151 20 divne0d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) =/= 0 )
153 36 152 eqnetrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) =/= 0 )
154 tanval3 
 |-  ( ( ( Im ` ( log ` A ) ) e. CC /\ ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) =/= 0 ) -> ( tan ` ( Im ` ( log ` A ) ) ) = ( ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) ) ) )
155 8 153 154 syl2anc 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( tan ` ( Im ` ( log ` A ) ) ) = ( ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) ) ) )
156 10 14 14 20 divsubdird 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) = ( ( ( A ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) - ( ( ( abs ` A ) ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) ) )
157 33 34 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( A ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) - ( ( ( abs ` A ) ^ 2 ) / ( ( abs ` A ) ^ 2 ) ) ) = ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) - 1 ) )
158 156 157 eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) - 1 ) = ( ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) )
159 36 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) ) = ( _i x. ( ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) ) )
160 38 37 14 20 divassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) / ( ( abs ` A ) ^ 2 ) ) = ( _i x. ( ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) ) )
161 159 160 eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) ) = ( ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) / ( ( abs ` A ) ^ 2 ) ) )
162 158 161 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) - 1 ) / ( _i x. ( ( exp ` ( 2 x. ( _i x. ( Im ` ( log ` A ) ) ) ) ) + 1 ) ) ) = ( ( ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) / ( ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) / ( ( abs ` A ) ^ 2 ) ) ) )
163 10 14 subcld 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) e. CC )
164 mulcl 
 |-  ( ( _i e. CC /\ ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) e. CC ) -> ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) e. CC )
165 22 37 164 sylancr 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) e. CC )
166 163 165 14 146 20 divcan7d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) / ( ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) / ( ( abs ` A ) ^ 2 ) ) ) = ( ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) / ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) ) )
167 115 117 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) = ( ( ( ( Re ` A ) ^ 2 ) + ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) ) - ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
168 43 96 95 pnpcand 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( Re ` A ) ^ 2 ) + ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) ) - ( ( ( Re ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) = ( ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) - ( ( Im ` A ) ^ 2 ) ) )
169 59 95 95 subsub4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) - ( ( Im ` A ) ^ 2 ) ) = ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( ( Im ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
170 95 2timesd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Im ` A ) ^ 2 ) ) = ( ( ( Im ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) )
171 170 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( 2 x. ( ( Im ` A ) ^ 2 ) ) ) = ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( ( Im ` A ) ^ 2 ) + ( ( Im ` A ) ^ 2 ) ) ) )
172 46 63 49 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Im ` A ) ) = ( 2 x. ( ( ( Re ` A ) x. _i ) x. ( Im ` A ) ) ) )
173 42 38 49 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( Re ` A ) x. _i ) x. ( Im ` A ) ) = ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) )
174 173 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( ( Re ` A ) x. _i ) x. ( Im ` A ) ) ) = ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) )
175 172 174 eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) = ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Im ` A ) ) )
176 49 sqvald 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( Im ` A ) ^ 2 ) = ( ( Im ` A ) x. ( Im ` A ) ) )
177 176 oveq2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Im ` A ) ^ 2 ) ) = ( 2 x. ( ( Im ` A ) x. ( Im ` A ) ) ) )
178 46 49 49 mulassd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( Im ` A ) ) x. ( Im ` A ) ) = ( 2 x. ( ( Im ` A ) x. ( Im ` A ) ) ) )
179 177 178 eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( 2 x. ( ( Im ` A ) ^ 2 ) ) = ( ( 2 x. ( Im ` A ) ) x. ( Im ` A ) ) )
180 175 179 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( 2 x. ( ( Im ` A ) ^ 2 ) ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Im ` A ) ) - ( ( 2 x. ( Im ` A ) ) x. ( Im ` A ) ) ) )
181 91 77 49 subdird 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Im ` A ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) x. ( Im ` A ) ) - ( ( 2 x. ( Im ` A ) ) x. ( Im ` A ) ) ) )
182 180 181 eqtr4d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( 2 x. ( ( Im ` A ) ^ 2 ) ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Im ` A ) ) )
183 169 171 182 3eqtr2d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( 2 x. ( ( Re ` A ) x. ( _i x. ( Im ` A ) ) ) ) - ( ( Im ` A ) ^ 2 ) ) - ( ( Im ` A ) ^ 2 ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Im ` A ) ) )
184 167 168 183 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) = ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Im ` A ) ) )
185 184 126 oveq12d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) / ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) ) = ( ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Im ` A ) ) / ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Re ` A ) ) ) )
186 49 42 127 130 144 divcan5d 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Im ` A ) ) / ( ( ( 2 x. ( ( Re ` A ) x. _i ) ) - ( 2 x. ( Im ` A ) ) ) x. ( Re ` A ) ) ) = ( ( Im ` A ) / ( Re ` A ) ) )
187 166 185 186 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( ( ( ( A ^ 2 ) - ( ( abs ` A ) ^ 2 ) ) / ( ( abs ` A ) ^ 2 ) ) / ( ( _i x. ( ( A ^ 2 ) + ( ( abs ` A ) ^ 2 ) ) ) / ( ( abs ` A ) ^ 2 ) ) ) = ( ( Im ` A ) / ( Re ` A ) ) )
188 155 162 187 3eqtrd 
 |-  ( ( A e. CC /\ ( Re ` A ) =/= 0 ) -> ( tan ` ( Im ` ( log ` A ) ) ) = ( ( Im ` A ) / ( Re ` A ) ) )