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 ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( tan ‘ ( ℑ ‘ ( log ‘ 𝐴 ) ) ) = ( ( ℑ ‘ 𝐴 ) / ( ℜ ‘ 𝐴 ) ) )

Proof

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