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