Proof of Theorem atanlogsublem
| Step | Hyp | Ref
| Expression |
| 1 | | ax-1cn 11213 |
. . . . . 6
⊢ 1 ∈
ℂ |
| 2 | | ax-icn 11214 |
. . . . . . 7
⊢ i ∈
ℂ |
| 3 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
𝐴 ∈ dom
arctan) |
| 4 | | atandm2 26920 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
| 5 | 3, 4 | sylib 218 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(𝐴 ∈ ℂ ∧ (1
− (i · 𝐴))
≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0)) |
| 6 | 5 | simp1d 1143 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
𝐴 ∈
ℂ) |
| 7 | | mulcl 11239 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
| 8 | 2, 6, 7 | sylancr 587 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· 𝐴) ∈
ℂ) |
| 9 | | addcl 11237 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
| 10 | 1, 8, 9 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (1
+ (i · 𝐴)) ∈
ℂ) |
| 11 | 5 | simp3d 1145 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (1
+ (i · 𝐴)) ≠
0) |
| 12 | 10, 11 | logcld 26612 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(1 + (i · 𝐴))) ∈ ℂ) |
| 13 | | subcl 11507 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
| 14 | 1, 8, 13 | sylancr 587 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (1
− (i · 𝐴))
∈ ℂ) |
| 15 | 5 | simp2d 1144 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (1
− (i · 𝐴))
≠ 0) |
| 16 | 14, 15 | logcld 26612 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(1 − (i · 𝐴))) ∈ ℂ) |
| 17 | 12, 16 | imsubd 15256 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
((ℑ‘(log‘(1 + (i · 𝐴)))) − (ℑ‘(log‘(1
− (i · 𝐴)))))) |
| 18 | 2 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → i
∈ ℂ) |
| 19 | 18, 6, 18 | subdid 11719 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· (𝐴 − i)) =
((i · 𝐴) − (i
· i))) |
| 20 | | ixi 11892 |
. . . . . . . . . . 11
⊢ (i
· i) = -1 |
| 21 | 20 | oveq2i 7442 |
. . . . . . . . . 10
⊢ ((i
· 𝐴) − (i
· i)) = ((i · 𝐴) − -1) |
| 22 | | subneg 11558 |
. . . . . . . . . . 11
⊢ (((i
· 𝐴) ∈ ℂ
∧ 1 ∈ ℂ) → ((i · 𝐴) − -1) = ((i · 𝐴) + 1)) |
| 23 | 8, 1, 22 | sylancl 586 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((i · 𝐴) − -1)
= ((i · 𝐴) +
1)) |
| 24 | 21, 23 | eqtrid 2789 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((i · 𝐴) − (i
· i)) = ((i · 𝐴) + 1)) |
| 25 | | addcom 11447 |
. . . . . . . . . 10
⊢ (((i
· 𝐴) ∈ ℂ
∧ 1 ∈ ℂ) → ((i · 𝐴) + 1) = (1 + (i · 𝐴))) |
| 26 | 8, 1, 25 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((i · 𝐴) + 1) = (1 +
(i · 𝐴))) |
| 27 | 19, 24, 26 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· (𝐴 − i)) =
(1 + (i · 𝐴))) |
| 28 | 27 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(i · (𝐴
− i))) = (log‘(1 + (i · 𝐴)))) |
| 29 | | subcl 11507 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (𝐴 −
i) ∈ ℂ) |
| 30 | 6, 2, 29 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(𝐴 − i) ∈
ℂ) |
| 31 | | resub 15166 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (ℜ‘(𝐴 − i)) = ((ℜ‘𝐴) −
(ℜ‘i))) |
| 32 | 6, 2, 31 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 −
i)) = ((ℜ‘𝐴)
− (ℜ‘i))) |
| 33 | | rei 15195 |
. . . . . . . . . . . . 13
⊢
(ℜ‘i) = 0 |
| 34 | 33 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢
((ℜ‘𝐴)
− (ℜ‘i)) = ((ℜ‘𝐴) − 0) |
| 35 | 6 | recld 15233 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘𝐴) ∈
ℝ) |
| 36 | 35 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘𝐴) ∈
ℂ) |
| 37 | 36 | subid1d 11609 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℜ‘𝐴) −
0) = (ℜ‘𝐴)) |
| 38 | 34, 37 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℜ‘𝐴) −
(ℜ‘i)) = (ℜ‘𝐴)) |
| 39 | 32, 38 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 −
i)) = (ℜ‘𝐴)) |
| 40 | | gt0ne0 11728 |
. . . . . . . . . . 11
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ≠ 0) |
| 41 | 35, 40 | sylancom 588 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘𝐴) ≠
0) |
| 42 | 39, 41 | eqnetrd 3008 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 −
i)) ≠ 0) |
| 43 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ ((𝐴 − i) = 0 →
(ℜ‘(𝐴 −
i)) = (ℜ‘0)) |
| 44 | | re0 15191 |
. . . . . . . . . . 11
⊢
(ℜ‘0) = 0 |
| 45 | 43, 44 | eqtrdi 2793 |
. . . . . . . . . 10
⊢ ((𝐴 − i) = 0 →
(ℜ‘(𝐴 −
i)) = 0) |
| 46 | 45 | necon3i 2973 |
. . . . . . . . 9
⊢
((ℜ‘(𝐴
− i)) ≠ 0 → (𝐴 − i) ≠ 0) |
| 47 | 42, 46 | syl 17 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(𝐴 − i) ≠
0) |
| 48 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
< (ℜ‘𝐴)) |
| 49 | | 0re 11263 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
| 50 | | ltle 11349 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (0 <
(ℜ‘𝐴) → 0
≤ (ℜ‘𝐴))) |
| 51 | 49, 35, 50 | sylancr 587 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (0
< (ℜ‘𝐴)
→ 0 ≤ (ℜ‘𝐴))) |
| 52 | 48, 51 | mpd 15 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
≤ (ℜ‘𝐴)) |
| 53 | 52, 39 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
≤ (ℜ‘(𝐴
− i))) |
| 54 | | logimul 26656 |
. . . . . . . 8
⊢ (((𝐴 − i) ∈ ℂ ∧
(𝐴 − i) ≠ 0 ∧
0 ≤ (ℜ‘(𝐴
− i))) → (log‘(i · (𝐴 − i))) = ((log‘(𝐴 − i)) + (i · (π
/ 2)))) |
| 55 | 30, 47, 53, 54 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(i · (𝐴
− i))) = ((log‘(𝐴 − i)) + (i · (π /
2)))) |
| 56 | 28, 55 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(1 + (i · 𝐴))) = ((log‘(𝐴 − i)) + (i · (π /
2)))) |
| 57 | 56 | fveq2d 6910 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(1 + (i · 𝐴)))) = (ℑ‘((log‘(𝐴 − i)) + (i · (π
/ 2))))) |
| 58 | 30, 47 | logcld 26612 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(𝐴 − i))
∈ ℂ) |
| 59 | | halfpire 26506 |
. . . . . . . . 9
⊢ (π /
2) ∈ ℝ |
| 60 | 59 | recni 11275 |
. . . . . . . 8
⊢ (π /
2) ∈ ℂ |
| 61 | 2, 60 | mulcli 11268 |
. . . . . . 7
⊢ (i
· (π / 2)) ∈ ℂ |
| 62 | | imadd 15173 |
. . . . . . 7
⊢
(((log‘(𝐴
− i)) ∈ ℂ ∧ (i · (π / 2)) ∈ ℂ) →
(ℑ‘((log‘(𝐴 − i)) + (i · (π / 2)))) =
((ℑ‘(log‘(𝐴 − i))) + (ℑ‘(i ·
(π / 2))))) |
| 63 | 58, 61, 62 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(𝐴 − i)) + (i · (π / 2)))) =
((ℑ‘(log‘(𝐴 − i))) + (ℑ‘(i ·
(π / 2))))) |
| 64 | | reim 15148 |
. . . . . . . . 9
⊢ ((π /
2) ∈ ℂ → (ℜ‘(π / 2)) = (ℑ‘(i ·
(π / 2)))) |
| 65 | 60, 64 | ax-mp 5 |
. . . . . . . 8
⊢
(ℜ‘(π / 2)) = (ℑ‘(i · (π /
2))) |
| 66 | | rere 15161 |
. . . . . . . . 9
⊢ ((π /
2) ∈ ℝ → (ℜ‘(π / 2)) = (π /
2)) |
| 67 | 59, 66 | ax-mp 5 |
. . . . . . . 8
⊢
(ℜ‘(π / 2)) = (π / 2) |
| 68 | 65, 67 | eqtr3i 2767 |
. . . . . . 7
⊢
(ℑ‘(i · (π / 2))) = (π / 2) |
| 69 | 68 | oveq2i 7442 |
. . . . . 6
⊢
((ℑ‘(log‘(𝐴 − i))) + (ℑ‘(i ·
(π / 2)))) = ((ℑ‘(log‘(𝐴 − i))) + (π / 2)) |
| 70 | 63, 69 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(𝐴 − i)) + (i · (π / 2)))) =
((ℑ‘(log‘(𝐴 − i))) + (π /
2))) |
| 71 | 57, 70 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(1 + (i · 𝐴)))) = ((ℑ‘(log‘(𝐴 − i))) + (π /
2))) |
| 72 | | addcl 11237 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (𝐴 + i)
∈ ℂ) |
| 73 | 6, 2, 72 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(𝐴 + i) ∈
ℂ) |
| 74 | | mulcl 11239 |
. . . . . . . . 9
⊢ ((i
∈ ℂ ∧ (𝐴 +
i) ∈ ℂ) → (i · (𝐴 + i)) ∈ ℂ) |
| 75 | 2, 73, 74 | sylancr 587 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· (𝐴 + i)) ∈
ℂ) |
| 76 | | reim 15148 |
. . . . . . . . . . 11
⊢ ((𝐴 + i) ∈ ℂ →
(ℜ‘(𝐴 + i)) =
(ℑ‘(i · (𝐴 + i)))) |
| 77 | 73, 76 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 + i)) =
(ℑ‘(i · (𝐴 + i)))) |
| 78 | | readd 15165 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (ℜ‘(𝐴 + i)) = ((ℜ‘𝐴) + (ℜ‘i))) |
| 79 | 6, 2, 78 | sylancl 586 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 + i)) =
((ℜ‘𝐴) +
(ℜ‘i))) |
| 80 | 33 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢
((ℜ‘𝐴) +
(ℜ‘i)) = ((ℜ‘𝐴) + 0) |
| 81 | 36 | addridd 11461 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℜ‘𝐴) + 0) =
(ℜ‘𝐴)) |
| 82 | 80, 81 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℜ‘𝐴) +
(ℜ‘i)) = (ℜ‘𝐴)) |
| 83 | 79, 82 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 + i)) =
(ℜ‘𝐴)) |
| 84 | 77, 83 | eqtr3d 2779 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(i · (𝐴 + i))) = (ℜ‘𝐴)) |
| 85 | 48, 84 | breqtrrd 5171 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
< (ℑ‘(i · (𝐴 + i)))) |
| 86 | | logneg2 26657 |
. . . . . . . 8
⊢ (((i
· (𝐴 + i)) ∈
ℂ ∧ 0 < (ℑ‘(i · (𝐴 + i)))) → (log‘-(i ·
(𝐴 + i))) = ((log‘(i
· (𝐴 + i))) −
(i · π))) |
| 87 | 75, 85, 86 | syl2anc 584 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘-(i · (𝐴
+ i))) = ((log‘(i · (𝐴 + i))) − (i ·
π))) |
| 88 | 18, 6, 18 | adddid 11285 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· (𝐴 + i)) = ((i
· 𝐴) + (i ·
i))) |
| 89 | 20 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ ((i
· 𝐴) + (i ·
i)) = ((i · 𝐴) +
-1) |
| 90 | | negsub 11557 |
. . . . . . . . . . . . 13
⊢ (((i
· 𝐴) ∈ ℂ
∧ 1 ∈ ℂ) → ((i · 𝐴) + -1) = ((i · 𝐴) − 1)) |
| 91 | 8, 1, 90 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((i · 𝐴) + -1) = ((i
· 𝐴) −
1)) |
| 92 | 89, 91 | eqtrid 2789 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((i · 𝐴) + (i
· i)) = ((i · 𝐴) − 1)) |
| 93 | 88, 92 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· (𝐴 + i)) = ((i
· 𝐴) −
1)) |
| 94 | 93 | negeqd 11502 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-(i · (𝐴 + i)) =
-((i · 𝐴) −
1)) |
| 95 | | negsubdi2 11568 |
. . . . . . . . . 10
⊢ (((i
· 𝐴) ∈ ℂ
∧ 1 ∈ ℂ) → -((i · 𝐴) − 1) = (1 − (i · 𝐴))) |
| 96 | 8, 1, 95 | sylancl 586 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-((i · 𝐴) − 1)
= (1 − (i · 𝐴))) |
| 97 | 94, 96 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-(i · (𝐴 + i)) = (1
− (i · 𝐴))) |
| 98 | 97 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘-(i · (𝐴
+ i))) = (log‘(1 − (i · 𝐴)))) |
| 99 | 83, 41 | eqnetrd 3008 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℜ‘(𝐴 + i)) ≠
0) |
| 100 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ ((𝐴 + i) = 0 →
(ℜ‘(𝐴 + i)) =
(ℜ‘0)) |
| 101 | 100, 44 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝐴 + i) = 0 →
(ℜ‘(𝐴 + i)) =
0) |
| 102 | 101 | necon3i 2973 |
. . . . . . . . . 10
⊢
((ℜ‘(𝐴 +
i)) ≠ 0 → (𝐴 + i)
≠ 0) |
| 103 | 99, 102 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(𝐴 + i) ≠
0) |
| 104 | 73, 103 | logcld 26612 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(𝐴 + i)) ∈
ℂ) |
| 105 | 61 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· (π / 2)) ∈ ℂ) |
| 106 | | picn 26501 |
. . . . . . . . . 10
⊢ π
∈ ℂ |
| 107 | 2, 106 | mulcli 11268 |
. . . . . . . . 9
⊢ (i
· π) ∈ ℂ |
| 108 | 107 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (i
· π) ∈ ℂ) |
| 109 | 52, 83 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
≤ (ℜ‘(𝐴 +
i))) |
| 110 | | logimul 26656 |
. . . . . . . . . 10
⊢ (((𝐴 + i) ∈ ℂ ∧
(𝐴 + i) ≠ 0 ∧ 0 ≤
(ℜ‘(𝐴 + i)))
→ (log‘(i · (𝐴 + i))) = ((log‘(𝐴 + i)) + (i · (π /
2)))) |
| 111 | 73, 103, 109, 110 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(i · (𝐴 +
i))) = ((log‘(𝐴 + i))
+ (i · (π / 2)))) |
| 112 | 111 | oveq1d 7446 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((log‘(i · (𝐴
+ i))) − (i · π)) = (((log‘(𝐴 + i)) + (i · (π / 2))) − (i
· π))) |
| 113 | 104, 105,
108, 112 | assraddsubd 11677 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((log‘(i · (𝐴
+ i))) − (i · π)) = ((log‘(𝐴 + i)) + ((i · (π / 2)) − (i
· π)))) |
| 114 | 87, 98, 113 | 3eqtr3d 2785 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(log‘(1 − (i · 𝐴))) = ((log‘(𝐴 + i)) + ((i · (π / 2)) − (i
· π)))) |
| 115 | 114 | fveq2d 6910 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(1 − (i · 𝐴)))) = (ℑ‘((log‘(𝐴 + i)) + ((i · (π /
2)) − (i · π))))) |
| 116 | 61, 107 | subcli 11585 |
. . . . . . 7
⊢ ((i
· (π / 2)) − (i · π)) ∈ ℂ |
| 117 | | imadd 15173 |
. . . . . . 7
⊢
(((log‘(𝐴 +
i)) ∈ ℂ ∧ ((i · (π / 2)) − (i · π))
∈ ℂ) → (ℑ‘((log‘(𝐴 + i)) + ((i · (π / 2)) − (i
· π)))) = ((ℑ‘(log‘(𝐴 + i))) + (ℑ‘((i · (π
/ 2)) − (i · π))))) |
| 118 | 104, 116,
117 | sylancl 586 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(𝐴 + i)) + ((i · (π / 2)) − (i
· π)))) = ((ℑ‘(log‘(𝐴 + i))) + (ℑ‘((i · (π
/ 2)) − (i · π))))) |
| 119 | | imsub 15174 |
. . . . . . . . 9
⊢ (((i
· (π / 2)) ∈ ℂ ∧ (i · π) ∈ ℂ)
→ (ℑ‘((i · (π / 2)) − (i · π))) =
((ℑ‘(i · (π / 2))) − (ℑ‘(i ·
π)))) |
| 120 | 61, 107, 119 | mp2an 692 |
. . . . . . . 8
⊢
(ℑ‘((i · (π / 2)) − (i · π))) =
((ℑ‘(i · (π / 2))) − (ℑ‘(i ·
π))) |
| 121 | | reim 15148 |
. . . . . . . . . . 11
⊢ (π
∈ ℂ → (ℜ‘π) = (ℑ‘(i ·
π))) |
| 122 | 106, 121 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℜ‘π) = (ℑ‘(i · π)) |
| 123 | | pire 26500 |
. . . . . . . . . . 11
⊢ π
∈ ℝ |
| 124 | | rere 15161 |
. . . . . . . . . . 11
⊢ (π
∈ ℝ → (ℜ‘π) = π) |
| 125 | 123, 124 | ax-mp 5 |
. . . . . . . . . 10
⊢
(ℜ‘π) = π |
| 126 | 122, 125 | eqtr3i 2767 |
. . . . . . . . 9
⊢
(ℑ‘(i · π)) = π |
| 127 | 68, 126 | oveq12i 7443 |
. . . . . . . 8
⊢
((ℑ‘(i · (π / 2))) − (ℑ‘(i
· π))) = ((π / 2) − π) |
| 128 | 60 | negcli 11577 |
. . . . . . . . 9
⊢ -(π /
2) ∈ ℂ |
| 129 | 106, 60 | negsubi 11587 |
. . . . . . . . . 10
⊢ (π +
-(π / 2)) = (π − (π / 2)) |
| 130 | | pidiv2halves 26509 |
. . . . . . . . . . 11
⊢ ((π /
2) + (π / 2)) = π |
| 131 | 106, 60, 60, 130 | subaddrii 11598 |
. . . . . . . . . 10
⊢ (π
− (π / 2)) = (π / 2) |
| 132 | 129, 131 | eqtri 2765 |
. . . . . . . . 9
⊢ (π +
-(π / 2)) = (π / 2) |
| 133 | 60, 106, 128, 132 | subaddrii 11598 |
. . . . . . . 8
⊢ ((π /
2) − π) = -(π / 2) |
| 134 | 120, 127,
133 | 3eqtri 2769 |
. . . . . . 7
⊢
(ℑ‘((i · (π / 2)) − (i · π))) =
-(π / 2) |
| 135 | 134 | oveq2i 7442 |
. . . . . 6
⊢
((ℑ‘(log‘(𝐴 + i))) + (ℑ‘((i · (π
/ 2)) − (i · π)))) = ((ℑ‘(log‘(𝐴 + i))) + -(π /
2)) |
| 136 | 118, 135 | eqtrdi 2793 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(𝐴 + i)) + ((i · (π / 2)) − (i
· π)))) = ((ℑ‘(log‘(𝐴 + i))) + -(π / 2))) |
| 137 | 115, 136 | eqtrd 2777 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(1 − (i · 𝐴)))) = ((ℑ‘(log‘(𝐴 + i))) + -(π /
2))) |
| 138 | 71, 137 | oveq12d 7449 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(log‘(1 + (i · 𝐴)))) − (ℑ‘(log‘(1
− (i · 𝐴)))))
= (((ℑ‘(log‘(𝐴 − i))) + (π / 2)) −
((ℑ‘(log‘(𝐴 + i))) + -(π / 2)))) |
| 139 | 58 | imcld 15234 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 − i))) ∈
ℝ) |
| 140 | 139 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 − i))) ∈
ℂ) |
| 141 | 60 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(π / 2) ∈ ℂ) |
| 142 | 104 | imcld 15234 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 + i))) ∈ ℝ) |
| 143 | 142 | recnd 11289 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 + i))) ∈ ℂ) |
| 144 | 128 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-(π / 2) ∈ ℂ) |
| 145 | 140, 141,
143, 144 | addsub4d 11667 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘(log‘(𝐴 − i))) + (π / 2)) −
((ℑ‘(log‘(𝐴 + i))) + -(π / 2))) =
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + ((π / 2) − -(π /
2)))) |
| 146 | 60, 60 | subnegi 11588 |
. . . . . 6
⊢ ((π /
2) − -(π / 2)) = ((π / 2) + (π / 2)) |
| 147 | 146, 130 | eqtri 2765 |
. . . . 5
⊢ ((π /
2) − -(π / 2)) = π |
| 148 | 147 | oveq2i 7442 |
. . . 4
⊢
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + ((π / 2) − -(π / 2)))
= (((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) |
| 149 | 145, 148 | eqtrdi 2793 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘(log‘(𝐴 − i))) + (π / 2)) −
((ℑ‘(log‘(𝐴 + i))) + -(π / 2))) =
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π)) |
| 150 | 17, 138, 149 | 3eqtrd 2781 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π)) |
| 151 | 139, 142 | resubcld 11691 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) ∈ ℝ) |
| 152 | | readdcl 11238 |
. . . 4
⊢
((((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) ∈ ℝ ∧ π ∈
ℝ) → (((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∈
ℝ) |
| 153 | 151, 123,
152 | sylancl 586 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∈
ℝ) |
| 154 | 123 | renegcli 11570 |
. . . . . . 7
⊢ -π
∈ ℝ |
| 155 | 154 | recni 11275 |
. . . . . 6
⊢ -π
∈ ℂ |
| 156 | 155, 106 | negsubi 11587 |
. . . . 5
⊢ (-π +
-π) = (-π − π) |
| 157 | 154 | a1i 11 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-π ∈ ℝ) |
| 158 | 142 | renegcld 11690 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-(ℑ‘(log‘(𝐴 + i))) ∈ ℝ) |
| 159 | 30, 47 | logimcld 26613 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(-π < (ℑ‘(log‘(𝐴 − i))) ∧
(ℑ‘(log‘(𝐴 − i))) ≤ π)) |
| 160 | 159 | simpld 494 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-π < (ℑ‘(log‘(𝐴 − i)))) |
| 161 | 73, 103 | logimcld 26613 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(-π < (ℑ‘(log‘(𝐴 + i))) ∧
(ℑ‘(log‘(𝐴 + i))) ≤ π)) |
| 162 | 161 | simprd 495 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 + i))) ≤ π) |
| 163 | | leneg 11766 |
. . . . . . . . 9
⊢
(((ℑ‘(log‘(𝐴 + i))) ∈ ℝ ∧ π ∈
ℝ) → ((ℑ‘(log‘(𝐴 + i))) ≤ π ↔ -π ≤
-(ℑ‘(log‘(𝐴 + i))))) |
| 164 | 142, 123,
163 | sylancl 586 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(log‘(𝐴 + i))) ≤ π ↔ -π ≤
-(ℑ‘(log‘(𝐴 + i))))) |
| 165 | 162, 164 | mpbid 232 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-π ≤ -(ℑ‘(log‘(𝐴 + i)))) |
| 166 | 157, 157,
139, 158, 160, 165 | ltleaddd 11884 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(-π + -π) < ((ℑ‘(log‘(𝐴 − i))) +
-(ℑ‘(log‘(𝐴 + i))))) |
| 167 | 140, 143 | negsubd 11626 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(log‘(𝐴 − i))) +
-(ℑ‘(log‘(𝐴 + i)))) = ((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i))))) |
| 168 | 166, 167 | breqtrd 5169 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(-π + -π) < ((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i))))) |
| 169 | 156, 168 | eqbrtrrid 5179 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(-π − π) < ((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i))))) |
| 170 | 123 | a1i 11 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
π ∈ ℝ) |
| 171 | 157, 170,
151 | ltsubaddd 11859 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((-π − π) < ((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) ↔ -π <
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π))) |
| 172 | 169, 171 | mpbid 232 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
-π < (((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π)) |
| 173 | | 0red 11264 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
∈ ℝ) |
| 174 | 6 | imcld 15234 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘𝐴) ∈
ℝ) |
| 175 | | peano2rem 11576 |
. . . . . . . . . . . . 13
⊢
((ℑ‘𝐴)
∈ ℝ → ((ℑ‘𝐴) − 1) ∈
ℝ) |
| 176 | 174, 175 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘𝐴) −
1) ∈ ℝ) |
| 177 | | peano2re 11434 |
. . . . . . . . . . . . 13
⊢
((ℑ‘𝐴)
∈ ℝ → ((ℑ‘𝐴) + 1) ∈ ℝ) |
| 178 | 174, 177 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘𝐴) + 1)
∈ ℝ) |
| 179 | 174 | ltm1d 12200 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘𝐴) −
1) < (ℑ‘𝐴)) |
| 180 | 174 | ltp1d 12198 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘𝐴) <
((ℑ‘𝐴) +
1)) |
| 181 | 176, 174,
178, 179, 180 | lttrd 11422 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘𝐴) −
1) < ((ℑ‘𝐴)
+ 1)) |
| 182 | | ltdiv1 12132 |
. . . . . . . . . . . 12
⊢
((((ℑ‘𝐴)
− 1) ∈ ℝ ∧ ((ℑ‘𝐴) + 1) ∈ ℝ ∧
((ℜ‘𝐴) ∈
ℝ ∧ 0 < (ℜ‘𝐴))) → (((ℑ‘𝐴) − 1) <
((ℑ‘𝐴) + 1)
↔ (((ℑ‘𝐴)
− 1) / (ℜ‘𝐴)) < (((ℑ‘𝐴) + 1) / (ℜ‘𝐴)))) |
| 183 | 176, 178,
35, 48, 182 | syl112anc 1376 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘𝐴) −
1) < ((ℑ‘𝐴)
+ 1) ↔ (((ℑ‘𝐴) − 1) / (ℜ‘𝐴)) < (((ℑ‘𝐴) + 1) / (ℜ‘𝐴)))) |
| 184 | 181, 183 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘𝐴) −
1) / (ℜ‘𝐴)) <
(((ℑ‘𝐴) + 1) /
(ℜ‘𝐴))) |
| 185 | | imsub 15174 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (ℑ‘(𝐴 − i)) = ((ℑ‘𝐴) −
(ℑ‘i))) |
| 186 | 6, 2, 185 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(𝐴 −
i)) = ((ℑ‘𝐴)
− (ℑ‘i))) |
| 187 | | imi 15196 |
. . . . . . . . . . . . 13
⊢
(ℑ‘i) = 1 |
| 188 | 187 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝐴)
− (ℑ‘i)) = ((ℑ‘𝐴) − 1) |
| 189 | 186, 188 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(𝐴 −
i)) = ((ℑ‘𝐴)
− 1)) |
| 190 | 189, 39 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(𝐴 −
i)) / (ℜ‘(𝐴
− i))) = (((ℑ‘𝐴) − 1) / (ℜ‘𝐴))) |
| 191 | | imadd 15173 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℂ ∧ i ∈
ℂ) → (ℑ‘(𝐴 + i)) = ((ℑ‘𝐴) + (ℑ‘i))) |
| 192 | 6, 2, 191 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(𝐴 + i)) =
((ℑ‘𝐴) +
(ℑ‘i))) |
| 193 | 187 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢
((ℑ‘𝐴) +
(ℑ‘i)) = ((ℑ‘𝐴) + 1) |
| 194 | 192, 193 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(𝐴 + i)) =
((ℑ‘𝐴) +
1)) |
| 195 | 194, 83 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(𝐴 + i)) /
(ℜ‘(𝐴 + i))) =
(((ℑ‘𝐴) + 1) /
(ℜ‘𝐴))) |
| 196 | 184, 190,
195 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(𝐴 −
i)) / (ℜ‘(𝐴
− i))) < ((ℑ‘(𝐴 + i)) / (ℜ‘(𝐴 + i)))) |
| 197 | | tanarg 26661 |
. . . . . . . . . 10
⊢ (((𝐴 − i) ∈ ℂ ∧
(ℜ‘(𝐴 −
i)) ≠ 0) → (tan‘(ℑ‘(log‘(𝐴 − i)))) = ((ℑ‘(𝐴 − i)) /
(ℜ‘(𝐴 −
i)))) |
| 198 | 30, 42, 197 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(tan‘(ℑ‘(log‘(𝐴 − i)))) = ((ℑ‘(𝐴 − i)) /
(ℜ‘(𝐴 −
i)))) |
| 199 | | tanarg 26661 |
. . . . . . . . . 10
⊢ (((𝐴 + i) ∈ ℂ ∧
(ℜ‘(𝐴 + i)) ≠
0) → (tan‘(ℑ‘(log‘(𝐴 + i)))) = ((ℑ‘(𝐴 + i)) / (ℜ‘(𝐴 + i)))) |
| 200 | 73, 99, 199 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(tan‘(ℑ‘(log‘(𝐴 + i)))) = ((ℑ‘(𝐴 + i)) / (ℜ‘(𝐴 + i)))) |
| 201 | 196, 198,
200 | 3brtr4d 5175 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(tan‘(ℑ‘(log‘(𝐴 − i)))) <
(tan‘(ℑ‘(log‘(𝐴 + i))))) |
| 202 | 48, 39 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
< (ℜ‘(𝐴
− i))) |
| 203 | | argregt0 26652 |
. . . . . . . . . 10
⊢ (((𝐴 − i) ∈ ℂ ∧
0 < (ℜ‘(𝐴
− i))) → (ℑ‘(log‘(𝐴 − i))) ∈ (-(π / 2)(,)(π /
2))) |
| 204 | 30, 202, 203 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 − i))) ∈ (-(π / 2)(,)(π /
2))) |
| 205 | 48, 83 | breqtrrd 5171 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → 0
< (ℜ‘(𝐴 +
i))) |
| 206 | | argregt0 26652 |
. . . . . . . . . 10
⊢ (((𝐴 + i) ∈ ℂ ∧ 0
< (ℜ‘(𝐴 +
i))) → (ℑ‘(log‘(𝐴 + i))) ∈ (-(π / 2)(,)(π /
2))) |
| 207 | 73, 205, 206 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 + i))) ∈ (-(π / 2)(,)(π /
2))) |
| 208 | | tanord 26580 |
. . . . . . . . 9
⊢
(((ℑ‘(log‘(𝐴 − i))) ∈ (-(π / 2)(,)(π /
2)) ∧ (ℑ‘(log‘(𝐴 + i))) ∈ (-(π / 2)(,)(π / 2)))
→ ((ℑ‘(log‘(𝐴 − i))) <
(ℑ‘(log‘(𝐴 + i))) ↔
(tan‘(ℑ‘(log‘(𝐴 − i)))) <
(tan‘(ℑ‘(log‘(𝐴 + i)))))) |
| 209 | 204, 207,
208 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(log‘(𝐴 − i))) <
(ℑ‘(log‘(𝐴 + i))) ↔
(tan‘(ℑ‘(log‘(𝐴 − i)))) <
(tan‘(ℑ‘(log‘(𝐴 + i)))))) |
| 210 | 201, 209 | mpbird 257 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 − i))) <
(ℑ‘(log‘(𝐴 + i)))) |
| 211 | 143 | addlidd 11462 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) → (0
+ (ℑ‘(log‘(𝐴 + i)))) = (ℑ‘(log‘(𝐴 + i)))) |
| 212 | 210, 211 | breqtrrd 5171 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘(log‘(𝐴 − i))) < (0 +
(ℑ‘(log‘(𝐴 + i))))) |
| 213 | 139, 142,
173 | ltsubaddd 11859 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) < 0 ↔
(ℑ‘(log‘(𝐴 − i))) < (0 +
(ℑ‘(log‘(𝐴 + i)))))) |
| 214 | 212, 213 | mpbird 257 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) < 0) |
| 215 | 151, 173,
170, 214 | ltadd1dd 11874 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) < (0 +
π)) |
| 216 | 106 | addlidi 11449 |
. . . 4
⊢ (0 +
π) = π |
| 217 | 215, 216 | breqtrdi 5184 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) < π) |
| 218 | 154 | rexri 11319 |
. . . 4
⊢ -π
∈ ℝ* |
| 219 | 123 | rexri 11319 |
. . . 4
⊢ π
∈ ℝ* |
| 220 | | elioo2 13428 |
. . . 4
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ*) →
((((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∈ (-π(,)π)
↔ ((((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∈ ℝ ∧ -π
< (((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∧
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) <
π))) |
| 221 | 218, 219,
220 | mp2an 692 |
. . 3
⊢
((((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∈ (-π(,)π)
↔ ((((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∈ ℝ ∧ -π
< (((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∧
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) <
π)) |
| 222 | 153, 172,
217, 221 | syl3anbrc 1344 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(((ℑ‘(log‘(𝐴 − i))) −
(ℑ‘(log‘(𝐴 + i)))) + π) ∈
(-π(,)π)) |
| 223 | 150, 222 | eqeltrd 2841 |
1
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |