This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐴 ) ) ) = ( ( ℑ ‘ 𝐴 ) / ( ℜ ‘ 𝐴 ) ) )