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

Metamath Proof Explorer

Theorem atanlogsublem

Description: Lemma for atanlogsub . (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion atanlogsublem ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )

Proof

Step Hyp Ref Expression
1 ax-1cn ⊢ 1 ∈ ℂ
2 ax-icn ⊢ i ∈ ℂ
3 simpl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 𝐴 ∈ dom arctan )
4 atandm2 ⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
5 3 4 sylib ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) )
6 5 simp1d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 𝐴 ∈ ℂ )
7 mulcl ⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ )
8 2 6 7 sylancr ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · 𝐴 ) ∈ ℂ )
9 addcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
10 1 8 9 sylancr ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ )
11 5 simp3d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 1 + ( i · 𝐴 ) ) ≠ 0 )
12 10 11 logcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ )
13 subcl ⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
14 1 8 13 sylancr ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ )
15 5 simp2d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 1 − ( i · 𝐴 ) ) ≠ 0 )
16 14 15 logcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ )
17 12 16 imsubd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ℑ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) )
18 2 a1i ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → i ∈ ℂ )
19 18 6 18 subdid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · ( 𝐴 − i ) ) = ( ( i · 𝐴 ) − ( i · i ) ) )
20 ixi ⊢ ( i · i ) = - 1
21 20 oveq2i ⊢ ( ( i · 𝐴 ) − ( i · i ) ) = ( ( i · 𝐴 ) − - 1 )
22 subneg ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · 𝐴 ) − - 1 ) = ( ( i · 𝐴 ) + 1 ) )
23 8 1 22 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( i · 𝐴 ) − - 1 ) = ( ( i · 𝐴 ) + 1 ) )
24 21 23 eqtrid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( i · 𝐴 ) − ( i · i ) ) = ( ( i · 𝐴 ) + 1 ) )
25 addcom ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · 𝐴 ) + 1 ) = ( 1 + ( i · 𝐴 ) ) )
26 8 1 25 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( i · 𝐴 ) + 1 ) = ( 1 + ( i · 𝐴 ) ) )
27 19 24 26 3eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · ( 𝐴 − i ) ) = ( 1 + ( i · 𝐴 ) ) )
28 27 fveq2d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( i · ( 𝐴 − i ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) )
29 subcl ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ) → ( 𝐴 − i ) ∈ ℂ )
30 6 2 29 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 𝐴 − i ) ∈ ℂ )
31 resub ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ) → ( ℜ ‘ ( 𝐴 − i ) ) = ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ i ) ) )
32 6 2 31 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 − i ) ) = ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ i ) ) )
33 rei ⊢ ( ℜ ‘ i ) = 0
34 33 oveq2i ⊢ ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ i ) ) = ( ( ℜ ‘ 𝐴 ) − 0 )
35 6 recld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ∈ ℝ )
36 35 recnd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ∈ ℂ )
37 36 subid1d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℜ ‘ 𝐴 ) − 0 ) = ( ℜ ‘ 𝐴 ) )
38 34 37 eqtrid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℜ ‘ 𝐴 ) − ( ℜ ‘ i ) ) = ( ℜ ‘ 𝐴 ) )
39 32 38 eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 − i ) ) = ( ℜ ‘ 𝐴 ) )
40 gt0ne0 ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ≠ 0 )
41 35 40 sylancom ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ 𝐴 ) ≠ 0 )
42 39 41 eqnetrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 − i ) ) ≠ 0 )
43 fveq2 ⊢ ( ( 𝐴 − i ) = 0 → ( ℜ ‘ ( 𝐴 − i ) ) = ( ℜ ‘ 0 ) )
44 re0 ⊢ ( ℜ ‘ 0 ) = 0
45 43 44 eqtrdi ⊢ ( ( 𝐴 − i ) = 0 → ( ℜ ‘ ( 𝐴 − i ) ) = 0 )
46 45 necon3i ⊢ ( ( ℜ ‘ ( 𝐴 − i ) ) ≠ 0 → ( 𝐴 − i ) ≠ 0 )
47 42 46 syl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 𝐴 − i ) ≠ 0 )
48 simpr ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ 𝐴 ) )
49 0re ⊢ 0 ∈ ℝ
50 ltle ⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ 𝐴 ) ∈ ℝ ) → ( 0 < ( ℜ ‘ 𝐴 ) → 0 ≤ ( ℜ ‘ 𝐴 ) ) )
51 49 35 50 sylancr ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 0 < ( ℜ ‘ 𝐴 ) → 0 ≤ ( ℜ ‘ 𝐴 ) ) )
52 48 51 mpd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ 𝐴 ) )
53 52 39 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( 𝐴 − i ) ) )
54 logimul ⊢ ( ( ( 𝐴 − i ) ∈ ℂ ∧ ( 𝐴 − i ) ≠ 0 ∧ 0 ≤ ( ℜ ‘ ( 𝐴 − i ) ) ) → ( log ‘ ( i · ( 𝐴 − i ) ) ) = ( ( log ‘ ( 𝐴 − i ) ) + ( i · ( π / 2 ) ) ) )
55 30 47 53 54 syl3anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( i · ( 𝐴 − i ) ) ) = ( ( log ‘ ( 𝐴 − i ) ) + ( i · ( π / 2 ) ) ) )
56 28 55 eqtr3d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) = ( ( log ‘ ( 𝐴 − i ) ) + ( i · ( π / 2 ) ) ) )
57 56 fveq2d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 𝐴 − i ) ) + ( i · ( π / 2 ) ) ) ) )
58 30 47 logcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( 𝐴 − i ) ) ∈ ℂ )
59 halfpire ⊢ ( π / 2 ) ∈ ℝ
60 59 recni ⊢ ( π / 2 ) ∈ ℂ
61 2 60 mulcli ⊢ ( i · ( π / 2 ) ) ∈ ℂ
62 imadd ⊢ ( ( ( log ‘ ( 𝐴 − i ) ) ∈ ℂ ∧ ( i · ( π / 2 ) ) ∈ ℂ ) → ( ℑ ‘ ( ( log ‘ ( 𝐴 − i ) ) + ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( ℑ ‘ ( i · ( π / 2 ) ) ) ) )
63 58 61 62 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 𝐴 − i ) ) + ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( ℑ ‘ ( i · ( π / 2 ) ) ) ) )
64 reim ⊢ ( ( π / 2 ) ∈ ℂ → ( ℜ ‘ ( π / 2 ) ) = ( ℑ ‘ ( i · ( π / 2 ) ) ) )
65 60 64 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( ℑ ‘ ( i · ( π / 2 ) ) )
66 rere ⊢ ( ( π / 2 ) ∈ ℝ → ( ℜ ‘ ( π / 2 ) ) = ( π / 2 ) )
67 59 66 ax-mp ⊢ ( ℜ ‘ ( π / 2 ) ) = ( π / 2 )
68 65 67 eqtr3i ⊢ ( ℑ ‘ ( i · ( π / 2 ) ) ) = ( π / 2 )
69 68 oveq2i ⊢ ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( ℑ ‘ ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( π / 2 ) )
70 63 69 eqtrdi ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 𝐴 − i ) ) + ( i · ( π / 2 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( π / 2 ) ) )
71 57 70 eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( π / 2 ) ) )
72 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ) → ( 𝐴 + i ) ∈ ℂ )
73 6 2 72 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 𝐴 + i ) ∈ ℂ )
74 mulcl ⊢ ( ( i ∈ ℂ ∧ ( 𝐴 + i ) ∈ ℂ ) → ( i · ( 𝐴 + i ) ) ∈ ℂ )
75 2 73 74 sylancr ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · ( 𝐴 + i ) ) ∈ ℂ )
76 reim ⊢ ( ( 𝐴 + i ) ∈ ℂ → ( ℜ ‘ ( 𝐴 + i ) ) = ( ℑ ‘ ( i · ( 𝐴 + i ) ) ) )
77 73 76 syl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 + i ) ) = ( ℑ ‘ ( i · ( 𝐴 + i ) ) ) )
78 readd ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ) → ( ℜ ‘ ( 𝐴 + i ) ) = ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ i ) ) )
79 6 2 78 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 + i ) ) = ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ i ) ) )
80 33 oveq2i ⊢ ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ i ) ) = ( ( ℜ ‘ 𝐴 ) + 0 )
81 36 addridd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℜ ‘ 𝐴 ) + 0 ) = ( ℜ ‘ 𝐴 ) )
82 80 81 eqtrid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℜ ‘ 𝐴 ) + ( ℜ ‘ i ) ) = ( ℜ ‘ 𝐴 ) )
83 79 82 eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 + i ) ) = ( ℜ ‘ 𝐴 ) )
84 77 83 eqtr3d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( i · ( 𝐴 + i ) ) ) = ( ℜ ‘ 𝐴 ) )
85 48 84 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℑ ‘ ( i · ( 𝐴 + i ) ) ) )
86 logneg2 ⊢ ( ( ( i · ( 𝐴 + i ) ) ∈ ℂ ∧ 0 < ( ℑ ‘ ( i · ( 𝐴 + i ) ) ) ) → ( log ‘ - ( i · ( 𝐴 + i ) ) ) = ( ( log ‘ ( i · ( 𝐴 + i ) ) ) − ( i · π ) ) )
87 75 85 86 syl2anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ - ( i · ( 𝐴 + i ) ) ) = ( ( log ‘ ( i · ( 𝐴 + i ) ) ) − ( i · π ) ) )
88 18 6 18 adddid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · ( 𝐴 + i ) ) = ( ( i · 𝐴 ) + ( i · i ) ) )
89 20 oveq2i ⊢ ( ( i · 𝐴 ) + ( i · i ) ) = ( ( i · 𝐴 ) + - 1 )
90 negsub ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · 𝐴 ) + - 1 ) = ( ( i · 𝐴 ) − 1 ) )
91 8 1 90 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( i · 𝐴 ) + - 1 ) = ( ( i · 𝐴 ) − 1 ) )
92 89 91 eqtrid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( i · 𝐴 ) + ( i · i ) ) = ( ( i · 𝐴 ) − 1 ) )
93 88 92 eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · ( 𝐴 + i ) ) = ( ( i · 𝐴 ) − 1 ) )
94 93 negeqd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - ( i · ( 𝐴 + i ) ) = - ( ( i · 𝐴 ) − 1 ) )
95 negsubdi2 ⊢ ( ( ( i · 𝐴 ) ∈ ℂ ∧ 1 ∈ ℂ ) → - ( ( i · 𝐴 ) − 1 ) = ( 1 − ( i · 𝐴 ) ) )
96 8 1 95 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - ( ( i · 𝐴 ) − 1 ) = ( 1 − ( i · 𝐴 ) ) )
97 94 96 eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - ( i · ( 𝐴 + i ) ) = ( 1 − ( i · 𝐴 ) ) )
98 97 fveq2d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ - ( i · ( 𝐴 + i ) ) ) = ( log ‘ ( 1 − ( i · 𝐴 ) ) ) )
99 83 41 eqnetrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℜ ‘ ( 𝐴 + i ) ) ≠ 0 )
100 fveq2 ⊢ ( ( 𝐴 + i ) = 0 → ( ℜ ‘ ( 𝐴 + i ) ) = ( ℜ ‘ 0 ) )
101 100 44 eqtrdi ⊢ ( ( 𝐴 + i ) = 0 → ( ℜ ‘ ( 𝐴 + i ) ) = 0 )
102 101 necon3i ⊢ ( ( ℜ ‘ ( 𝐴 + i ) ) ≠ 0 → ( 𝐴 + i ) ≠ 0 )
103 99 102 syl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 𝐴 + i ) ≠ 0 )
104 73 103 logcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( 𝐴 + i ) ) ∈ ℂ )
105 61 a1i ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · ( π / 2 ) ) ∈ ℂ )
106 picn ⊢ π ∈ ℂ
107 2 106 mulcli ⊢ ( i · π ) ∈ ℂ
108 107 a1i ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( i · π ) ∈ ℂ )
109 52 83 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 ≤ ( ℜ ‘ ( 𝐴 + i ) ) )
110 logimul ⊢ ( ( ( 𝐴 + i ) ∈ ℂ ∧ ( 𝐴 + i ) ≠ 0 ∧ 0 ≤ ( ℜ ‘ ( 𝐴 + i ) ) ) → ( log ‘ ( i · ( 𝐴 + i ) ) ) = ( ( log ‘ ( 𝐴 + i ) ) + ( i · ( π / 2 ) ) ) )
111 73 103 109 110 syl3anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( i · ( 𝐴 + i ) ) ) = ( ( log ‘ ( 𝐴 + i ) ) + ( i · ( π / 2 ) ) ) )
112 111 oveq1d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( log ‘ ( i · ( 𝐴 + i ) ) ) − ( i · π ) ) = ( ( ( log ‘ ( 𝐴 + i ) ) + ( i · ( π / 2 ) ) ) − ( i · π ) ) )
113 104 105 108 112 assraddsubd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( log ‘ ( i · ( 𝐴 + i ) ) ) − ( i · π ) ) = ( ( log ‘ ( 𝐴 + i ) ) + ( ( i · ( π / 2 ) ) − ( i · π ) ) ) )
114 87 98 113 3eqtr3d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) = ( ( log ‘ ( 𝐴 + i ) ) + ( ( i · ( π / 2 ) ) − ( i · π ) ) ) )
115 114 fveq2d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 𝐴 + i ) ) + ( ( i · ( π / 2 ) ) − ( i · π ) ) ) ) )
116 61 107 subcli ⊢ ( ( i · ( π / 2 ) ) − ( i · π ) ) ∈ ℂ
117 imadd ⊢ ( ( ( log ‘ ( 𝐴 + i ) ) ∈ ℂ ∧ ( ( i · ( π / 2 ) ) − ( i · π ) ) ∈ ℂ ) → ( ℑ ‘ ( ( log ‘ ( 𝐴 + i ) ) + ( ( i · ( π / 2 ) ) − ( i · π ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + ( ℑ ‘ ( ( i · ( π / 2 ) ) − ( i · π ) ) ) ) )
118 104 116 117 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 𝐴 + i ) ) + ( ( i · ( π / 2 ) ) − ( i · π ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + ( ℑ ‘ ( ( i · ( π / 2 ) ) − ( i · π ) ) ) ) )
119 imsub ⊢ ( ( ( i · ( π / 2 ) ) ∈ ℂ ∧ ( i · π ) ∈ ℂ ) → ( ℑ ‘ ( ( i · ( π / 2 ) ) − ( i · π ) ) ) = ( ( ℑ ‘ ( i · ( π / 2 ) ) ) − ( ℑ ‘ ( i · π ) ) ) )
120 61 107 119 mp2an ⊢ ( ℑ ‘ ( ( i · ( π / 2 ) ) − ( i · π ) ) ) = ( ( ℑ ‘ ( i · ( π / 2 ) ) ) − ( ℑ ‘ ( i · π ) ) )
121 reim ⊢ ( π ∈ ℂ → ( ℜ ‘ π ) = ( ℑ ‘ ( i · π ) ) )
122 106 121 ax-mp ⊢ ( ℜ ‘ π ) = ( ℑ ‘ ( i · π ) )
123 pire ⊢ π ∈ ℝ
124 rere ⊢ ( π ∈ ℝ → ( ℜ ‘ π ) = π )
125 123 124 ax-mp ⊢ ( ℜ ‘ π ) = π
126 122 125 eqtr3i ⊢ ( ℑ ‘ ( i · π ) ) = π
127 68 126 oveq12i ⊢ ( ( ℑ ‘ ( i · ( π / 2 ) ) ) − ( ℑ ‘ ( i · π ) ) ) = ( ( π / 2 ) − π )
128 60 negcli ⊢ - ( π / 2 ) ∈ ℂ
129 106 60 negsubi ⊢ ( π + - ( π / 2 ) ) = ( π − ( π / 2 ) )
130 pidiv2halves ⊢ ( ( π / 2 ) + ( π / 2 ) ) = π
131 106 60 60 130 subaddrii ⊢ ( π − ( π / 2 ) ) = ( π / 2 )
132 129 131 eqtri ⊢ ( π + - ( π / 2 ) ) = ( π / 2 )
133 60 106 128 132 subaddrii ⊢ ( ( π / 2 ) − π ) = - ( π / 2 )
134 120 127 133 3eqtri ⊢ ( ℑ ‘ ( ( i · ( π / 2 ) ) − ( i · π ) ) ) = - ( π / 2 )
135 134 oveq2i ⊢ ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + ( ℑ ‘ ( ( i · ( π / 2 ) ) − ( i · π ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + - ( π / 2 ) )
136 118 135 eqtrdi ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 𝐴 + i ) ) + ( ( i · ( π / 2 ) ) − ( i · π ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + - ( π / 2 ) ) )
137 115 136 eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + - ( π / 2 ) ) )
138 71 137 oveq12d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) − ( ℑ ‘ ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( π / 2 ) ) − ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + - ( π / 2 ) ) ) )
139 58 imcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ∈ ℝ )
140 139 recnd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ∈ ℂ )
141 60 a1i ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( π / 2 ) ∈ ℂ )
142 104 imcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∈ ℝ )
143 142 recnd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∈ ℂ )
144 128 a1i ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - ( π / 2 ) ∈ ℂ )
145 140 141 143 144 addsub4d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( π / 2 ) ) − ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + - ( π / 2 ) ) ) = ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + ( ( π / 2 ) − - ( π / 2 ) ) ) )
146 60 60 subnegi ⊢ ( ( π / 2 ) − - ( π / 2 ) ) = ( ( π / 2 ) + ( π / 2 ) )
147 146 130 eqtri ⊢ ( ( π / 2 ) − - ( π / 2 ) ) = π
148 147 oveq2i ⊢ ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + ( ( π / 2 ) − - ( π / 2 ) ) ) = ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π )
149 145 148 eqtrdi ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + ( π / 2 ) ) − ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) + - ( π / 2 ) ) ) = ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) )
150 17 138 149 3eqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) )
151 139 142 resubcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) ∈ ℝ )
152 readdcl ⊢ ( ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∈ ℝ )
153 151 123 152 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∈ ℝ )
154 123 renegcli ⊢ - π ∈ ℝ
155 154 recni ⊢ - π ∈ ℂ
156 155 106 negsubi ⊢ ( - π + - π ) = ( - π − π )
157 154 a1i ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - π ∈ ℝ )
158 142 renegcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∈ ℝ )
159 30 47 logimcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ∧ ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ≤ π ) )
160 159 simpld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - π < ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) )
161 73 103 logimcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - π < ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∧ ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ≤ π ) )
162 161 simprd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ≤ π )
163 leneg ⊢ ( ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ≤ π ↔ - π ≤ - ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
164 142 123 163 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ≤ π ↔ - π ≤ - ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
165 162 164 mpbid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - π ≤ - ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) )
166 157 157 139 158 160 165 ltleaddd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - π + - π ) < ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + - ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
167 140 143 negsubd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) + - ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) = ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
168 166 167 breqtrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - π + - π ) < ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
169 156 168 eqbrtrrid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( - π − π ) < ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
170 123 a1i ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → π ∈ ℝ )
171 157 170 151 ltsubaddd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( - π − π ) < ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) ↔ - π < ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ) )
172 169 171 mpbid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → - π < ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) )
173 0red ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 ∈ ℝ )
174 6 imcld ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
175 peano2rem ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℝ → ( ( ℑ ‘ 𝐴 ) − 1 ) ∈ ℝ )
176 174 175 syl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ 𝐴 ) − 1 ) ∈ ℝ )
177 peano2re ⊢ ( ( ℑ ‘ 𝐴 ) ∈ ℝ → ( ( ℑ ‘ 𝐴 ) + 1 ) ∈ ℝ )
178 174 177 syl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ 𝐴 ) + 1 ) ∈ ℝ )
179 174 ltm1d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ 𝐴 ) − 1 ) < ( ℑ ‘ 𝐴 ) )
180 174 ltp1d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ 𝐴 ) < ( ( ℑ ‘ 𝐴 ) + 1 ) )
181 176 174 178 179 180 lttrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ 𝐴 ) − 1 ) < ( ( ℑ ‘ 𝐴 ) + 1 ) )
182 ltdiv1 ⊢ ( ( ( ( ℑ ‘ 𝐴 ) − 1 ) ∈ ℝ ∧ ( ( ℑ ‘ 𝐴 ) + 1 ) ∈ ℝ ∧ ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 < ( ℜ ‘ 𝐴 ) ) ) → ( ( ( ℑ ‘ 𝐴 ) − 1 ) < ( ( ℑ ‘ 𝐴 ) + 1 ) ↔ ( ( ( ℑ ‘ 𝐴 ) − 1 ) / ( ℜ ‘ 𝐴 ) ) < ( ( ( ℑ ‘ 𝐴 ) + 1 ) / ( ℜ ‘ 𝐴 ) ) ) )
183 176 178 35 48 182 syl112anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ 𝐴 ) − 1 ) < ( ( ℑ ‘ 𝐴 ) + 1 ) ↔ ( ( ( ℑ ‘ 𝐴 ) − 1 ) / ( ℜ ‘ 𝐴 ) ) < ( ( ( ℑ ‘ 𝐴 ) + 1 ) / ( ℜ ‘ 𝐴 ) ) ) )
184 181 183 mpbid ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ 𝐴 ) − 1 ) / ( ℜ ‘ 𝐴 ) ) < ( ( ( ℑ ‘ 𝐴 ) + 1 ) / ( ℜ ‘ 𝐴 ) ) )
185 imsub ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ) → ( ℑ ‘ ( 𝐴 − i ) ) = ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ i ) ) )
186 6 2 185 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( 𝐴 − i ) ) = ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ i ) ) )
187 imi ⊢ ( ℑ ‘ i ) = 1
188 187 oveq2i ⊢ ( ( ℑ ‘ 𝐴 ) − ( ℑ ‘ i ) ) = ( ( ℑ ‘ 𝐴 ) − 1 )
189 186 188 eqtrdi ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( 𝐴 − i ) ) = ( ( ℑ ‘ 𝐴 ) − 1 ) )
190 189 39 oveq12d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( 𝐴 − i ) ) / ( ℜ ‘ ( 𝐴 − i ) ) ) = ( ( ( ℑ ‘ 𝐴 ) − 1 ) / ( ℜ ‘ 𝐴 ) ) )
191 imadd ⊢ ( ( 𝐴 ∈ ℂ ∧ i ∈ ℂ ) → ( ℑ ‘ ( 𝐴 + i ) ) = ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ i ) ) )
192 6 2 191 sylancl ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( 𝐴 + i ) ) = ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ i ) ) )
193 187 oveq2i ⊢ ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ i ) ) = ( ( ℑ ‘ 𝐴 ) + 1 )
194 192 193 eqtrdi ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( 𝐴 + i ) ) = ( ( ℑ ‘ 𝐴 ) + 1 ) )
195 194 83 oveq12d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( 𝐴 + i ) ) / ( ℜ ‘ ( 𝐴 + i ) ) ) = ( ( ( ℑ ‘ 𝐴 ) + 1 ) / ( ℜ ‘ 𝐴 ) ) )
196 184 190 195 3brtr4d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( 𝐴 − i ) ) / ( ℜ ‘ ( 𝐴 − i ) ) ) < ( ( ℑ ‘ ( 𝐴 + i ) ) / ( ℜ ‘ ( 𝐴 + i ) ) ) )
197 tanarg ⊢ ( ( ( 𝐴 − i ) ∈ ℂ ∧ ( ℜ ‘ ( 𝐴 − i ) ) ≠ 0 ) → ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ) = ( ( ℑ ‘ ( 𝐴 − i ) ) / ( ℜ ‘ ( 𝐴 − i ) ) ) )
198 30 42 197 syl2anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ) = ( ( ℑ ‘ ( 𝐴 − i ) ) / ( ℜ ‘ ( 𝐴 − i ) ) ) )
199 tanarg ⊢ ( ( ( 𝐴 + i ) ∈ ℂ ∧ ( ℜ ‘ ( 𝐴 + i ) ) ≠ 0 ) → ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) = ( ( ℑ ‘ ( 𝐴 + i ) ) / ( ℜ ‘ ( 𝐴 + i ) ) ) )
200 73 99 199 syl2anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) = ( ( ℑ ‘ ( 𝐴 + i ) ) / ( ℜ ‘ ( 𝐴 + i ) ) ) )
201 196 198 200 3brtr4d ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ) < ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
202 48 39 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ ( 𝐴 − i ) ) )
203 argregt0 ⊢ ( ( ( 𝐴 − i ) ∈ ℂ ∧ 0 < ( ℜ ‘ ( 𝐴 − i ) ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
204 30 202 203 syl2anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
205 48 83 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → 0 < ( ℜ ‘ ( 𝐴 + i ) ) )
206 argregt0 ⊢ ( ( ( 𝐴 + i ) ∈ ℂ ∧ 0 < ( ℜ ‘ ( 𝐴 + i ) ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
207 73 205 206 syl2anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) )
208 tanord ⊢ ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ∧ ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ∈ ( - ( π / 2 ) (,) ( π / 2 ) ) ) → ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) < ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ↔ ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ) < ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) ) )
209 204 207 208 syl2anc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) < ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ↔ ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) ) < ( tan ‘ ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) ) )
210 201 209 mpbird ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) < ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) )
211 143 addlidd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( 0 + ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) = ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) )
212 210 211 breqtrrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) < ( 0 + ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) )
213 139 142 173 ltsubaddd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) < 0 ↔ ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) < ( 0 + ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) ) )
214 212 213 mpbird ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) < 0 )
215 151 173 170 214 ltadd1dd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) < ( 0 + π ) )
216 106 addlidi ⊢ ( 0 + π ) = π
217 215 216 breqtrdi ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) < π )
218 154 rexri ⊢ - π ∈ ℝ*
219 123 rexri ⊢ π ∈ ℝ*
220 elioo2 ⊢ ( ( - π ∈ ℝ* ∧ π ∈ ℝ* ) → ( ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∈ ( - π (,) π ) ↔ ( ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∈ ℝ ∧ - π < ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∧ ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) < π ) ) )
221 218 219 220 mp2an ⊢ ( ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∈ ( - π (,) π ) ↔ ( ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∈ ℝ ∧ - π < ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∧ ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) < π ) )
222 153 172 217 221 syl3anbrc ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ( ( ℑ ‘ ( log ‘ ( 𝐴 − i ) ) ) − ( ℑ ‘ ( log ‘ ( 𝐴 + i ) ) ) ) + π ) ∈ ( - π (,) π ) )
223 150 222 eqeltrd ⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) )