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