Metamath Proof Explorer

Theorem atancj

Description: The arctangent function distributes under conjugation. (The condition that Re ( A ) =/= 0 is necessary because the branch cuts are chosen so that the negative imaginary line "agrees with" neighboring values with negative real part, while the positive imaginary line agrees with values with positive real part. This makes atanneg true unconditionally but messes up conjugation symmetry, and it is impossible to have both in a single-valued function. The claim is true on the imaginary line between -u 1 and 1 , though.) (Contributed by Mario Carneiro, 31-Mar-2015)

Ref Expression
Assertion atancj ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 𝐴 ∈ dom arctan ∧ ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ ℂ )
2 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) ≠ 0 )
3 fveq2 ⊢ ( 𝐴 = - i → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ - i ) )
4 ax-icn ⊢ i ∈ ℂ
5 4 renegi ⊢ ( ℜ ‘ - i ) = - ( ℜ ‘ i )
6 rei ⊢ ( ℜ ‘ i ) = 0
7 6 negeqi ⊢ - ( ℜ ‘ i ) = - 0
8 neg0 ⊢ - 0 = 0
9 5 7 8 3eqtri ⊢ ( ℜ ‘ - i ) = 0
10 3 9 eqtrdi ⊢ ( 𝐴 = - i → ( ℜ ‘ 𝐴 ) = 0 )
11 10 necon3i ⊢ ( ( ℜ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ - i )
12 2 11 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ≠ - i )
13 fveq2 ⊢ ( 𝐴 = i → ( ℜ ‘ 𝐴 ) = ( ℜ ‘ i ) )
14 13 6 eqtrdi ⊢ ( 𝐴 = i → ( ℜ ‘ 𝐴 ) = 0 )
15 14 necon3i ⊢ ( ( ℜ ‘ 𝐴 ) ≠ 0 → 𝐴 ≠ i )
16 2 15 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ≠ i )
17 atandm ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ - i ∧ 𝐴 ≠ i ) )
18 1 12 16 17 syl3anbrc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ dom arctan )
19 halfcl ⊢ ( i ∈ ℂ → ( i / 2 ) ∈ ℂ )
20 4 19 ax-mp ⊢ ( i / 2 ) ∈ ℂ
21 ax-1cn ⊢ 1 ∈ ℂ
22 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
23 4 1 22 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( i · 𝐴 ) ∈ ℂ )
24 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
25 21 23 24 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
26 atandm2 ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
27 18 26 sylib ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
28 27 simp2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
29 25 28 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
30 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
31 21 23 30 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
32 27 simp3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
33 31 32 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
34 29 33 subcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ )
35 cjmul ⊢ ( ( ( i / 2 ) ∈ ℂ ∧ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ∈ ℂ ) → ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
36 20 34 35 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
37 2ne0 ⊢ 2 ≠ 0
38 2cn ⊢ 2 ∈ ℂ
39 4 38 cjdivi ⊢ ( 2 ≠ 0 → ( ∗ ‘ ( i / 2 ) ) = ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) ) )
40 37 39 ax-mp ⊢ ( ∗ ‘ ( i / 2 ) ) = ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) )
41 divneg ⊢ ( ( i ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → - ( i / 2 ) = ( - i / 2 ) )
42 4 38 37 41 mp3an ⊢ - ( i / 2 ) = ( - i / 2 )
43 cji ⊢ ( ∗ ‘ i ) = - i
44 2re ⊢ 2 ∈ ℝ
45 cjre ⊢ ( 2 ∈ ℝ → ( ∗ ‘ 2 ) = 2 )
46 44 45 ax-mp ⊢ ( ∗ ‘ 2 ) = 2
47 43 46 oveq12i ⊢ ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) ) = ( - i / 2 )
48 42 47 eqtr4i ⊢ - ( i / 2 ) = ( ( ∗ ‘ i ) / ( ∗ ‘ 2 ) )
49 40 48 eqtr4i ⊢ ( ∗ ‘ ( i / 2 ) ) = - ( i / 2 )
50 49 oveq1i ⊢ ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( - ( i / 2 ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
51 34 cjcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ∈ ℂ )
52 mulneg12 ⊢ ( ( ( i / 2 ) ∈ ℂ ∧ ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ∈ ℂ ) → ( - ( i / 2 ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
53 20 51 52 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - ( i / 2 ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
54 50 53 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ ( i / 2 ) ) · ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
55 cjsub ⊢ ( ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ ∧ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) − ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
56 29 33 55 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) − ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
57 imsub ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( i · 𝐴 ) ) ) )
58 21 23 57 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( i · 𝐴 ) ) ) )
59 reim ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
60 59 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) = ( ℑ ‘ ( i · 𝐴 ) ) )
61 60 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( ( ℑ ‘ 1 ) − ( ℑ ‘ ( i · 𝐴 ) ) ) )
62 58 61 eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) )
63 df-neg ⊢ - ( ℜ ‘ 𝐴 ) = ( 0 − ( ℜ ‘ 𝐴 ) )
64 im1 ⊢ ( ℑ ‘ 1 ) = 0
65 64 oveq1i ⊢ ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) ) = ( 0 − ( ℜ ‘ 𝐴 ) )
66 63 65 eqtr4i ⊢ - ( ℜ ‘ 𝐴 ) = ( ( ℑ ‘ 1 ) − ( ℜ ‘ 𝐴 ) )
67 62 66 eqtr4di ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) = - ( ℜ ‘ 𝐴 ) )
68 recl ⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) ∈ ℝ )
69 68 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
70 69 recnd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
71 70 2 negne0d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ℜ ‘ 𝐴 ) ≠ 0 )
72 67 71 eqnetrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) ≠ 0 )
73 logcj ⊢ ( ( ( 1 − ( i · 𝐴 ) ) ∈ ℂ ∧ ( ℑ ‘ ( 1 − ( i · 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
74 25 72 73 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) )
75 cjsub ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝐴 ) ) ) )
76 21 23 75 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝐴 ) ) ) )
77 1re ⊢ 1 ∈ ℝ
78 cjre ⊢ ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 )
79 77 78 mp1i ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ 1 ) = 1 )
80 cjmul ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ∗ ‘ ( i · 𝐴 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) )
81 4 1 80 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( i · 𝐴 ) ) = ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) )
82 43 oveq1i ⊢ ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) = ( - i · ( ∗ ‘ 𝐴 ) )
83 cjcl ⊢ ( 𝐴 ∈ ℂ → ( ∗ ‘ 𝐴 ) ∈ ℂ )
84 83 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
85 mulneg1 ⊢ ( ( i ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( - i · ( ∗ ‘ 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
86 4 84 85 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - i · ( ∗ ‘ 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
87 82 86 syl5eq ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ i ) · ( ∗ ‘ 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
88 81 87 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( i · 𝐴 ) ) = - ( i · ( ∗ ‘ 𝐴 ) ) )
89 79 88 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ 1 ) − ( ∗ ‘ ( i · 𝐴 ) ) ) = ( 1 − - ( i · ( ∗ ‘ 𝐴 ) ) ) )
90 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ∗ ‘ 𝐴 ) ∈ ℂ ) → ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
91 4 84 90 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
92 subneg ⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 − - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) )
93 21 91 92 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) )
94 76 89 93 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) = ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) )
95 94 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
96 74 95 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
97 imadd ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) )
98 21 23 97 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) )
99 60 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 + ( ℜ ‘ 𝐴 ) ) = ( 0 + ( ℑ ‘ ( i · 𝐴 ) ) ) )
100 64 oveq1i ⊢ ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) = ( 0 + ( ℑ ‘ ( i · 𝐴 ) ) )
101 99 100 eqtr4di ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 + ( ℜ ‘ 𝐴 ) ) = ( ( ℑ ‘ 1 ) + ( ℑ ‘ ( i · 𝐴 ) ) ) )
102 70 addid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 0 + ( ℜ ‘ 𝐴 ) ) = ( ℜ ‘ 𝐴 ) )
103 98 101 102 3eqtr2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ℜ ‘ 𝐴 ) )
104 103 2 eqnetrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) ≠ 0 )
105 logcj ⊢ ( ( ( 1 + ( i · 𝐴 ) ) ∈ ℂ ∧ ( ℑ ‘ ( 1 + ( i · 𝐴 ) ) ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
106 31 104 105 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) )
107 cjadd ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) + ( ∗ ‘ ( i · 𝐴 ) ) ) )
108 21 23 107 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( ∗ ‘ 1 ) + ( ∗ ‘ ( i · 𝐴 ) ) ) )
109 79 88 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ 1 ) + ( ∗ ‘ ( i · 𝐴 ) ) ) = ( 1 + - ( i · ( ∗ ‘ 𝐴 ) ) ) )
110 negsub ⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 + - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) )
111 21 91 110 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + - ( i · ( ∗ ‘ 𝐴 ) ) ) = ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) )
112 108 109 111 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) = ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) )
113 112 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( ∗ ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
114 106 113 eqtr3d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) )
115 96 114 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ∗ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) − ( ∗ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
116 56 115 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
117 116 negeqd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = - ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
118 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
119 21 91 118 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
120 atandmcj ⊢ ( 𝐴 ∈ dom arctan → ( ∗ ‘ 𝐴 ) ∈ dom arctan )
121 18 120 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ 𝐴 ) ∈ dom arctan )
122 atandm2 ⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan ↔ ( ( ∗ ‘ 𝐴 ) ∈ ℂ ∧ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 ∧ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 ) )
123 122 simp3bi ⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
124 121 123 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
125 119 124 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ∈ ℂ )
126 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · ( ∗ ‘ 𝐴 ) ) ∈ ℂ ) → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
127 21 91 126 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ∈ ℂ )
128 122 simp2bi ⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
129 121 128 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ≠ 0 )
130 127 129 logcld ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ∈ ℂ )
131 125 130 negsubdi2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
132 117 131 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) = ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) )
133 132 oveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( i / 2 ) · - ( ∗ ‘ ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
134 36 54 133 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
135 atanval ⊢ ( 𝐴 ∈ dom arctan → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
136 18 135 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( arctan ‘ 𝐴 ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) )
137 136 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( ∗ ‘ ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) ) )
138 atanval ⊢ ( ( ∗ ‘ 𝐴 ) ∈ dom arctan → ( arctan ‘ ( ∗ ‘ 𝐴 ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
139 121 138 syl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( arctan ‘ ( ∗ ‘ 𝐴 ) ) = ( ( i / 2 ) · ( ( log ‘ ( 1 − ( i · ( ∗ ‘ 𝐴 ) ) ) ) − ( log ‘ ( 1 + ( i · ( ∗ ‘ 𝐴 ) ) ) ) ) ) )
140 134 137 139 3eqtr4d ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) )
141 18 140 jca ⊢ ( ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( 𝐴 ∈ dom arctan ∧ ( ∗ ‘ ( arctan ‘ 𝐴 ) ) = ( arctan ‘ ( ∗ ‘ 𝐴 ) ) ) )