| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
| 2 |
|
ax-icn |
⊢ i ∈ ℂ |
| 3 |
|
atandm2 |
⊢ ( 𝐴 ∈ dom arctan ↔ ( 𝐴 ∈ ℂ ∧ ( 1 − ( i · 𝐴 ) ) ≠ 0 ∧ ( 1 + ( i · 𝐴 ) ) ≠ 0 ) ) |
| 4 |
3
|
simp1bi |
⊢ ( 𝐴 ∈ dom arctan → 𝐴 ∈ ℂ ) |
| 5 |
|
mulcl |
⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · 𝐴 ) ∈ ℂ ) |
| 6 |
2 4 5
|
sylancr |
⊢ ( 𝐴 ∈ dom arctan → ( i · 𝐴 ) ∈ ℂ ) |
| 7 |
|
addcl |
⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + ( i · 𝐴 ) ) ∈ ℂ ) |
| 8 |
1 6 7
|
sylancr |
⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ∈ ℂ ) |
| 9 |
3
|
simp3bi |
⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · 𝐴 ) ) ≠ 0 ) |
| 10 |
8 9
|
logcld |
⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ∈ ℂ ) |
| 11 |
|
subcl |
⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − ( i · 𝐴 ) ) ∈ ℂ ) |
| 12 |
1 6 11
|
sylancr |
⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ∈ ℂ ) |
| 13 |
3
|
simp2bi |
⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · 𝐴 ) ) ≠ 0 ) |
| 14 |
12 13
|
logcld |
⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ∈ ℂ ) |
| 15 |
10 14
|
subcld |
⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ ) |
| 16 |
15
|
adantr |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ ) |
| 17 |
4
|
recld |
⊢ ( 𝐴 ∈ dom arctan → ( ℜ ‘ 𝐴 ) ∈ ℝ ) |
| 18 |
|
0re |
⊢ 0 ∈ ℝ |
| 19 |
|
lttri2 |
⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℝ ∧ 0 ∈ ℝ ) → ( ( ℜ ‘ 𝐴 ) ≠ 0 ↔ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) ) |
| 20 |
17 18 19
|
sylancl |
⊢ ( 𝐴 ∈ dom arctan → ( ( ℜ ‘ 𝐴 ) ≠ 0 ↔ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) ) |
| 21 |
20
|
biimpa |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) |
| 22 |
15
|
imnegd |
⊢ ( 𝐴 ∈ dom arctan → ( ℑ ‘ - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) |
| 23 |
10 14
|
negsubdi2d |
⊢ ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) |
| 24 |
|
mulneg2 |
⊢ ( ( i ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( i · - 𝐴 ) = - ( i · 𝐴 ) ) |
| 25 |
2 4 24
|
sylancr |
⊢ ( 𝐴 ∈ dom arctan → ( i · - 𝐴 ) = - ( i · 𝐴 ) ) |
| 26 |
25
|
oveq2d |
⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 + - ( i · 𝐴 ) ) ) |
| 27 |
|
negsub |
⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) ) |
| 28 |
1 6 27
|
sylancr |
⊢ ( 𝐴 ∈ dom arctan → ( 1 + - ( i · 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) ) |
| 29 |
26 28
|
eqtrd |
⊢ ( 𝐴 ∈ dom arctan → ( 1 + ( i · - 𝐴 ) ) = ( 1 − ( i · 𝐴 ) ) ) |
| 30 |
29
|
fveq2d |
⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) |
| 31 |
25
|
oveq2d |
⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 − - ( i · 𝐴 ) ) ) |
| 32 |
|
subneg |
⊢ ( ( 1 ∈ ℂ ∧ ( i · 𝐴 ) ∈ ℂ ) → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) ) |
| 33 |
1 6 32
|
sylancr |
⊢ ( 𝐴 ∈ dom arctan → ( 1 − - ( i · 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) ) |
| 34 |
31 33
|
eqtrd |
⊢ ( 𝐴 ∈ dom arctan → ( 1 − ( i · - 𝐴 ) ) = ( 1 + ( i · 𝐴 ) ) ) |
| 35 |
34
|
fveq2d |
⊢ ( 𝐴 ∈ dom arctan → ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) = ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) |
| 36 |
30 35
|
oveq12d |
⊢ ( 𝐴 ∈ dom arctan → ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) = ( ( log ‘ ( 1 − ( i · 𝐴 ) ) ) − ( log ‘ ( 1 + ( i · 𝐴 ) ) ) ) ) |
| 37 |
23 36
|
eqtr4d |
⊢ ( 𝐴 ∈ dom arctan → - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) = ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) |
| 38 |
37
|
fveq2d |
⊢ ( 𝐴 ∈ dom arctan → ( ℑ ‘ - ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ) |
| 39 |
22 38
|
eqtr3d |
⊢ ( 𝐴 ∈ dom arctan → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ) |
| 40 |
39
|
adantr |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) = ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ) |
| 41 |
|
atandmneg |
⊢ ( 𝐴 ∈ dom arctan → - 𝐴 ∈ dom arctan ) |
| 42 |
17
|
lt0neg1d |
⊢ ( 𝐴 ∈ dom arctan → ( ( ℜ ‘ 𝐴 ) < 0 ↔ 0 < - ( ℜ ‘ 𝐴 ) ) ) |
| 43 |
42
|
biimpa |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < - ( ℜ ‘ 𝐴 ) ) |
| 44 |
4
|
adantr |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 𝐴 ∈ ℂ ) |
| 45 |
44
|
renegd |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℜ ‘ - 𝐴 ) = - ( ℜ ‘ 𝐴 ) ) |
| 46 |
43 45
|
breqtrrd |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → 0 < ( ℜ ‘ - 𝐴 ) ) |
| 47 |
|
atanlogsublem |
⊢ ( ( - 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ - 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ) |
| 48 |
41 46 47
|
syl2an2r |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ) |
| 49 |
|
picn |
⊢ π ∈ ℂ |
| 50 |
49
|
negnegi |
⊢ - - π = π |
| 51 |
50
|
oveq2i |
⊢ ( - π (,) - - π ) = ( - π (,) π ) |
| 52 |
48 51
|
eleqtrrdi |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · - 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · - 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) |
| 53 |
40 52
|
eqeltrd |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) |
| 54 |
|
pire |
⊢ π ∈ ℝ |
| 55 |
54
|
renegcli |
⊢ - π ∈ ℝ |
| 56 |
15
|
adantr |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ ) |
| 57 |
56
|
imcld |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ) |
| 58 |
|
iooneg |
⊢ ( ( - π ∈ ℝ ∧ π ∈ ℝ ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ↔ - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) ) |
| 59 |
55 54 57 58
|
mp3an12i |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ↔ - ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) - - π ) ) ) |
| 60 |
53 59
|
mpbird |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) < 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ) |
| 61 |
|
atanlogsublem |
⊢ ( ( 𝐴 ∈ dom arctan ∧ 0 < ( ℜ ‘ 𝐴 ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ) |
| 62 |
60 61
|
jaodan |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ( ℜ ‘ 𝐴 ) < 0 ∨ 0 < ( ℜ ‘ 𝐴 ) ) ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ) |
| 63 |
21 62
|
syldan |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) ) |
| 64 |
|
eliooord |
⊢ ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ( - π (,) π ) → ( - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π ) ) |
| 65 |
63 64
|
syl |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π ) ) |
| 66 |
65
|
simpld |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ) |
| 67 |
65
|
simprd |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π ) |
| 68 |
16
|
imcld |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ) |
| 69 |
|
ltle |
⊢ ( ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) ) |
| 70 |
68 54 69
|
sylancl |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) < π → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) ) |
| 71 |
67 70
|
mpd |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) |
| 72 |
|
ellogrn |
⊢ ( ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log ↔ ( ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ℂ ∧ - π < ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ∧ ( ℑ ‘ ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ) ≤ π ) ) |
| 73 |
16 66 71 72
|
syl3anbrc |
⊢ ( ( 𝐴 ∈ dom arctan ∧ ( ℜ ‘ 𝐴 ) ≠ 0 ) → ( ( log ‘ ( 1 + ( i · 𝐴 ) ) ) − ( log ‘ ( 1 − ( i · 𝐴 ) ) ) ) ∈ ran log ) |