MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  atanlogsublem Structured version   Visualization version   GIF version

Theorem atanlogsublem 24356
Description: Lemma for atanlogsub 24357. (Contributed by Mario Carneiro, 4-Apr-2015.)
Assertion
Ref Expression
atanlogsublem ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π))

Proof of Theorem atanlogsublem
StepHypRef Expression
1 ax-1cn 9847 . . . . . 6 1 ∈ ℂ
2 ax-icn 9848 . . . . . . 7 i ∈ ℂ
3 simpl 471 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ dom arctan)
4 atandm2 24318 . . . . . . . . 9 (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0))
53, 4sylib 206 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (𝐴 ∈ ℂ ∧ (1 − (i · 𝐴)) ≠ 0 ∧ (1 + (i · 𝐴)) ≠ 0))
65simp1d 1065 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 𝐴 ∈ ℂ)
7 mulcl 9873 . . . . . . 7 ((i ∈ ℂ ∧ 𝐴 ∈ ℂ) → (i · 𝐴) ∈ ℂ)
82, 6, 7sylancr 693 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · 𝐴) ∈ ℂ)
9 addcl 9871 . . . . . 6 ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i · 𝐴)) ∈ ℂ)
101, 8, 9sylancr 693 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (1 + (i · 𝐴)) ∈ ℂ)
115simp3d 1067 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (1 + (i · 𝐴)) ≠ 0)
1210, 11logcld 24035 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(1 + (i · 𝐴))) ∈ ℂ)
13 subcl 10128 . . . . . 6 ((1 ∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i · 𝐴)) ∈ ℂ)
141, 8, 13sylancr 693 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (1 − (i · 𝐴)) ∈ ℂ)
155simp2d 1066 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (1 − (i · 𝐴)) ≠ 0)
1614, 15logcld 24035 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(1 − (i · 𝐴))) ∈ ℂ)
1712, 16imsubd 13748 . . 3 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) = ((ℑ‘(log‘(1 + (i · 𝐴)))) − (ℑ‘(log‘(1 − (i · 𝐴))))))
182a1i 11 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → i ∈ ℂ)
1918, 6, 18subdid 10333 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · (𝐴 − i)) = ((i · 𝐴) − (i · i)))
20 ixi 10502 . . . . . . . . . . 11 (i · i) = -1
2120oveq2i 6535 . . . . . . . . . 10 ((i · 𝐴) − (i · i)) = ((i · 𝐴) − -1)
22 subneg 10178 . . . . . . . . . . 11 (((i · 𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝐴) − -1) = ((i · 𝐴) + 1))
238, 1, 22sylancl 692 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((i · 𝐴) − -1) = ((i · 𝐴) + 1))
2421, 23syl5eq 2652 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((i · 𝐴) − (i · i)) = ((i · 𝐴) + 1))
25 addcom 10070 . . . . . . . . . 10 (((i · 𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝐴) + 1) = (1 + (i · 𝐴)))
268, 1, 25sylancl 692 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((i · 𝐴) + 1) = (1 + (i · 𝐴)))
2719, 24, 263eqtrd 2644 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · (𝐴 − i)) = (1 + (i · 𝐴)))
2827fveq2d 6089 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(i · (𝐴 − i))) = (log‘(1 + (i · 𝐴))))
29 subcl 10128 . . . . . . . . 9 ((𝐴 ∈ ℂ ∧ i ∈ ℂ) → (𝐴 − i) ∈ ℂ)
306, 2, 29sylancl 692 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (𝐴 − i) ∈ ℂ)
31 resub 13658 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ i ∈ ℂ) → (ℜ‘(𝐴 − i)) = ((ℜ‘𝐴) − (ℜ‘i)))
326, 2, 31sylancl 692 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(𝐴 − i)) = ((ℜ‘𝐴) − (ℜ‘i)))
33 rei 13687 . . . . . . . . . . . . 13 (ℜ‘i) = 0
3433oveq2i 6535 . . . . . . . . . . . 12 ((ℜ‘𝐴) − (ℜ‘i)) = ((ℜ‘𝐴) − 0)
356recld 13725 . . . . . . . . . . . . . 14 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℝ)
3635recnd 9921 . . . . . . . . . . . . 13 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ∈ ℂ)
3736subid1d 10229 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℜ‘𝐴) − 0) = (ℜ‘𝐴))
3834, 37syl5eq 2652 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℜ‘𝐴) − (ℜ‘i)) = (ℜ‘𝐴))
3932, 38eqtrd 2640 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(𝐴 − i)) = (ℜ‘𝐴))
40 gt0ne0 10339 . . . . . . . . . . 11 (((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ≠ 0)
4135, 40sylancom 697 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘𝐴) ≠ 0)
4239, 41eqnetrd 2845 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(𝐴 − i)) ≠ 0)
43 fveq2 6085 . . . . . . . . . . 11 ((𝐴 − i) = 0 → (ℜ‘(𝐴 − i)) = (ℜ‘0))
44 re0 13683 . . . . . . . . . . 11 (ℜ‘0) = 0
4543, 44syl6eq 2656 . . . . . . . . . 10 ((𝐴 − i) = 0 → (ℜ‘(𝐴 − i)) = 0)
4645necon3i 2810 . . . . . . . . 9 ((ℜ‘(𝐴 − i)) ≠ 0 → (𝐴 − i) ≠ 0)
4742, 46syl 17 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (𝐴 − i) ≠ 0)
48 simpr 475 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘𝐴))
49 0re 9893 . . . . . . . . . . 11 0 ∈ ℝ
50 ltle 9974 . . . . . . . . . . 11 ((0 ∈ ℝ ∧ (ℜ‘𝐴) ∈ ℝ) → (0 < (ℜ‘𝐴) → 0 ≤ (ℜ‘𝐴)))
5149, 35, 50sylancr 693 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (0 < (ℜ‘𝐴) → 0 ≤ (ℜ‘𝐴)))
5248, 51mpd 15 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 ≤ (ℜ‘𝐴))
5352, 39breqtrrd 4602 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 ≤ (ℜ‘(𝐴 − i)))
54 logimul 24078 . . . . . . . 8 (((𝐴 − i) ∈ ℂ ∧ (𝐴 − i) ≠ 0 ∧ 0 ≤ (ℜ‘(𝐴 − i))) → (log‘(i · (𝐴 − i))) = ((log‘(𝐴 − i)) + (i · (π / 2))))
5530, 47, 53, 54syl3anc 1317 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(i · (𝐴 − i))) = ((log‘(𝐴 − i)) + (i · (π / 2))))
5628, 55eqtr3d 2642 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(1 + (i · 𝐴))) = ((log‘(𝐴 − i)) + (i · (π / 2))))
5756fveq2d 6089 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 + (i · 𝐴)))) = (ℑ‘((log‘(𝐴 − i)) + (i · (π / 2)))))
5830, 47logcld 24035 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(𝐴 − i)) ∈ ℂ)
59 halfpire 23934 . . . . . . . . 9 (π / 2) ∈ ℝ
6059recni 9905 . . . . . . . 8 (π / 2) ∈ ℂ
612, 60mulcli 9898 . . . . . . 7 (i · (π / 2)) ∈ ℂ
62 imadd 13665 . . . . . . 7 (((log‘(𝐴 − i)) ∈ ℂ ∧ (i · (π / 2)) ∈ ℂ) → (ℑ‘((log‘(𝐴 − i)) + (i · (π / 2)))) = ((ℑ‘(log‘(𝐴 − i))) + (ℑ‘(i · (π / 2)))))
6358, 61, 62sylancl 692 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(𝐴 − i)) + (i · (π / 2)))) = ((ℑ‘(log‘(𝐴 − i))) + (ℑ‘(i · (π / 2)))))
64 reim 13640 . . . . . . . . 9 ((π / 2) ∈ ℂ → (ℜ‘(π / 2)) = (ℑ‘(i · (π / 2))))
6560, 64ax-mp 5 . . . . . . . 8 (ℜ‘(π / 2)) = (ℑ‘(i · (π / 2)))
66 rere 13653 . . . . . . . . 9 ((π / 2) ∈ ℝ → (ℜ‘(π / 2)) = (π / 2))
6759, 66ax-mp 5 . . . . . . . 8 (ℜ‘(π / 2)) = (π / 2)
6865, 67eqtr3i 2630 . . . . . . 7 (ℑ‘(i · (π / 2))) = (π / 2)
6968oveq2i 6535 . . . . . 6 ((ℑ‘(log‘(𝐴 − i))) + (ℑ‘(i · (π / 2)))) = ((ℑ‘(log‘(𝐴 − i))) + (π / 2))
7063, 69syl6eq 2656 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(𝐴 − i)) + (i · (π / 2)))) = ((ℑ‘(log‘(𝐴 − i))) + (π / 2)))
7157, 70eqtrd 2640 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 + (i · 𝐴)))) = ((ℑ‘(log‘(𝐴 − i))) + (π / 2)))
72 addcl 9871 . . . . . . . . . 10 ((𝐴 ∈ ℂ ∧ i ∈ ℂ) → (𝐴 + i) ∈ ℂ)
736, 2, 72sylancl 692 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (𝐴 + i) ∈ ℂ)
74 mulcl 9873 . . . . . . . . 9 ((i ∈ ℂ ∧ (𝐴 + i) ∈ ℂ) → (i · (𝐴 + i)) ∈ ℂ)
752, 73, 74sylancr 693 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · (𝐴 + i)) ∈ ℂ)
76 reim 13640 . . . . . . . . . . 11 ((𝐴 + i) ∈ ℂ → (ℜ‘(𝐴 + i)) = (ℑ‘(i · (𝐴 + i))))
7773, 76syl 17 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(𝐴 + i)) = (ℑ‘(i · (𝐴 + i))))
78 readd 13657 . . . . . . . . . . . 12 ((𝐴 ∈ ℂ ∧ i ∈ ℂ) → (ℜ‘(𝐴 + i)) = ((ℜ‘𝐴) + (ℜ‘i)))
796, 2, 78sylancl 692 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(𝐴 + i)) = ((ℜ‘𝐴) + (ℜ‘i)))
8033oveq2i 6535 . . . . . . . . . . . 12 ((ℜ‘𝐴) + (ℜ‘i)) = ((ℜ‘𝐴) + 0)
8136addid1d 10084 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℜ‘𝐴) + 0) = (ℜ‘𝐴))
8280, 81syl5eq 2652 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℜ‘𝐴) + (ℜ‘i)) = (ℜ‘𝐴))
8379, 82eqtrd 2640 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(𝐴 + i)) = (ℜ‘𝐴))
8477, 83eqtr3d 2642 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(i · (𝐴 + i))) = (ℜ‘𝐴))
8548, 84breqtrrd 4602 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 < (ℑ‘(i · (𝐴 + i))))
86 logneg2 24079 . . . . . . . 8 (((i · (𝐴 + i)) ∈ ℂ ∧ 0 < (ℑ‘(i · (𝐴 + i)))) → (log‘-(i · (𝐴 + i))) = ((log‘(i · (𝐴 + i))) − (i · π)))
8775, 85, 86syl2anc 690 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘-(i · (𝐴 + i))) = ((log‘(i · (𝐴 + i))) − (i · π)))
8818, 6, 18adddid 9917 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · (𝐴 + i)) = ((i · 𝐴) + (i · i)))
8920oveq2i 6535 . . . . . . . . . . . 12 ((i · 𝐴) + (i · i)) = ((i · 𝐴) + -1)
90 negsub 10177 . . . . . . . . . . . . 13 (((i · 𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → ((i · 𝐴) + -1) = ((i · 𝐴) − 1))
918, 1, 90sylancl 692 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((i · 𝐴) + -1) = ((i · 𝐴) − 1))
9289, 91syl5eq 2652 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((i · 𝐴) + (i · i)) = ((i · 𝐴) − 1))
9388, 92eqtrd 2640 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · (𝐴 + i)) = ((i · 𝐴) − 1))
9493negeqd 10123 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -(i · (𝐴 + i)) = -((i · 𝐴) − 1))
95 negsubdi2 10188 . . . . . . . . . 10 (((i · 𝐴) ∈ ℂ ∧ 1 ∈ ℂ) → -((i · 𝐴) − 1) = (1 − (i · 𝐴)))
968, 1, 95sylancl 692 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -((i · 𝐴) − 1) = (1 − (i · 𝐴)))
9794, 96eqtrd 2640 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -(i · (𝐴 + i)) = (1 − (i · 𝐴)))
9897fveq2d 6089 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘-(i · (𝐴 + i))) = (log‘(1 − (i · 𝐴))))
9983, 41eqnetrd 2845 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℜ‘(𝐴 + i)) ≠ 0)
100 fveq2 6085 . . . . . . . . . . . . 13 ((𝐴 + i) = 0 → (ℜ‘(𝐴 + i)) = (ℜ‘0))
101100, 44syl6eq 2656 . . . . . . . . . . . 12 ((𝐴 + i) = 0 → (ℜ‘(𝐴 + i)) = 0)
102101necon3i 2810 . . . . . . . . . . 11 ((ℜ‘(𝐴 + i)) ≠ 0 → (𝐴 + i) ≠ 0)
10399, 102syl 17 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (𝐴 + i) ≠ 0)
10452, 83breqtrrd 4602 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 ≤ (ℜ‘(𝐴 + i)))
105 logimul 24078 . . . . . . . . . 10 (((𝐴 + i) ∈ ℂ ∧ (𝐴 + i) ≠ 0 ∧ 0 ≤ (ℜ‘(𝐴 + i))) → (log‘(i · (𝐴 + i))) = ((log‘(𝐴 + i)) + (i · (π / 2))))
10673, 103, 104, 105syl3anc 1317 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(i · (𝐴 + i))) = ((log‘(𝐴 + i)) + (i · (π / 2))))
107106oveq1d 6539 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((log‘(i · (𝐴 + i))) − (i · π)) = (((log‘(𝐴 + i)) + (i · (π / 2))) − (i · π)))
10873, 103logcld 24035 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(𝐴 + i)) ∈ ℂ)
10961a1i 11 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · (π / 2)) ∈ ℂ)
110 picn 23929 . . . . . . . . . . 11 π ∈ ℂ
1112, 110mulcli 9898 . . . . . . . . . 10 (i · π) ∈ ℂ
112111a1i 11 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (i · π) ∈ ℂ)
113108, 109, 112addsubassd 10260 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((log‘(𝐴 + i)) + (i · (π / 2))) − (i · π)) = ((log‘(𝐴 + i)) + ((i · (π / 2)) − (i · π))))
114107, 113eqtrd 2640 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((log‘(i · (𝐴 + i))) − (i · π)) = ((log‘(𝐴 + i)) + ((i · (π / 2)) − (i · π))))
11587, 98, 1143eqtr3d 2648 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (log‘(1 − (i · 𝐴))) = ((log‘(𝐴 + i)) + ((i · (π / 2)) − (i · π))))
116115fveq2d 6089 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 − (i · 𝐴)))) = (ℑ‘((log‘(𝐴 + i)) + ((i · (π / 2)) − (i · π)))))
11761, 111subcli 10205 . . . . . . 7 ((i · (π / 2)) − (i · π)) ∈ ℂ
118 imadd 13665 . . . . . . 7 (((log‘(𝐴 + i)) ∈ ℂ ∧ ((i · (π / 2)) − (i · π)) ∈ ℂ) → (ℑ‘((log‘(𝐴 + i)) + ((i · (π / 2)) − (i · π)))) = ((ℑ‘(log‘(𝐴 + i))) + (ℑ‘((i · (π / 2)) − (i · π)))))
119108, 117, 118sylancl 692 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(𝐴 + i)) + ((i · (π / 2)) − (i · π)))) = ((ℑ‘(log‘(𝐴 + i))) + (ℑ‘((i · (π / 2)) − (i · π)))))
120 imsub 13666 . . . . . . . . 9 (((i · (π / 2)) ∈ ℂ ∧ (i · π) ∈ ℂ) → (ℑ‘((i · (π / 2)) − (i · π))) = ((ℑ‘(i · (π / 2))) − (ℑ‘(i · π))))
12161, 111, 120mp2an 703 . . . . . . . 8 (ℑ‘((i · (π / 2)) − (i · π))) = ((ℑ‘(i · (π / 2))) − (ℑ‘(i · π)))
122 reim 13640 . . . . . . . . . . 11 (π ∈ ℂ → (ℜ‘π) = (ℑ‘(i · π)))
123110, 122ax-mp 5 . . . . . . . . . 10 (ℜ‘π) = (ℑ‘(i · π))
124 pire 23928 . . . . . . . . . . 11 π ∈ ℝ
125 rere 13653 . . . . . . . . . . 11 (π ∈ ℝ → (ℜ‘π) = π)
126124, 125ax-mp 5 . . . . . . . . . 10 (ℜ‘π) = π
127123, 126eqtr3i 2630 . . . . . . . . 9 (ℑ‘(i · π)) = π
12868, 127oveq12i 6536 . . . . . . . 8 ((ℑ‘(i · (π / 2))) − (ℑ‘(i · π))) = ((π / 2) − π)
12960negcli 10197 . . . . . . . . 9 -(π / 2) ∈ ℂ
130110, 60negsubi 10207 . . . . . . . . . 10 (π + -(π / 2)) = (π − (π / 2))
131 pidiv2halves 23937 . . . . . . . . . . 11 ((π / 2) + (π / 2)) = π
132110, 60, 60, 131subaddrii 10218 . . . . . . . . . 10 (π − (π / 2)) = (π / 2)
133130, 132eqtri 2628 . . . . . . . . 9 (π + -(π / 2)) = (π / 2)
13460, 110, 129, 133subaddrii 10218 . . . . . . . 8 ((π / 2) − π) = -(π / 2)
135121, 128, 1343eqtri 2632 . . . . . . 7 (ℑ‘((i · (π / 2)) − (i · π))) = -(π / 2)
136135oveq2i 6535 . . . . . 6 ((ℑ‘(log‘(𝐴 + i))) + (ℑ‘((i · (π / 2)) − (i · π)))) = ((ℑ‘(log‘(𝐴 + i))) + -(π / 2))
137119, 136syl6eq 2656 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(𝐴 + i)) + ((i · (π / 2)) − (i · π)))) = ((ℑ‘(log‘(𝐴 + i))) + -(π / 2)))
138116, 137eqtrd 2640 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(1 − (i · 𝐴)))) = ((ℑ‘(log‘(𝐴 + i))) + -(π / 2)))
13971, 138oveq12d 6542 . . 3 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(1 + (i · 𝐴)))) − (ℑ‘(log‘(1 − (i · 𝐴))))) = (((ℑ‘(log‘(𝐴 − i))) + (π / 2)) − ((ℑ‘(log‘(𝐴 + i))) + -(π / 2))))
14058imcld 13726 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 − i))) ∈ ℝ)
141140recnd 9921 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 − i))) ∈ ℂ)
14260a1i 11 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (π / 2) ∈ ℂ)
143108imcld 13726 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 + i))) ∈ ℝ)
144143recnd 9921 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 + i))) ∈ ℂ)
145129a1i 11 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -(π / 2) ∈ ℂ)
146141, 142, 144, 145addsub4d 10287 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘(log‘(𝐴 − i))) + (π / 2)) − ((ℑ‘(log‘(𝐴 + i))) + -(π / 2))) = (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + ((π / 2) − -(π / 2))))
14760, 60subnegi 10208 . . . . . 6 ((π / 2) − -(π / 2)) = ((π / 2) + (π / 2))
148147, 131eqtri 2628 . . . . 5 ((π / 2) − -(π / 2)) = π
149148oveq2i 6535 . . . 4 (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + ((π / 2) − -(π / 2))) = (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π)
150146, 149syl6eq 2656 . . 3 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘(log‘(𝐴 − i))) + (π / 2)) − ((ℑ‘(log‘(𝐴 + i))) + -(π / 2))) = (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π))
15117, 139, 1503eqtrd 2644 . 2 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) = (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π))
152140, 143resubcld 10306 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) ∈ ℝ)
153 readdcl 9872 . . . 4 ((((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) ∈ ℝ ∧ π ∈ ℝ) → (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∈ ℝ)
154152, 124, 153sylancl 692 . . 3 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∈ ℝ)
155124renegcli 10190 . . . . . . 7 -π ∈ ℝ
156155recni 9905 . . . . . 6 -π ∈ ℂ
157156, 110negsubi 10207 . . . . 5 (-π + -π) = (-π − π)
158155a1i 11 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π ∈ ℝ)
159143renegcld 10305 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -(ℑ‘(log‘(𝐴 + i))) ∈ ℝ)
16030, 47logimcld 24036 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (-π < (ℑ‘(log‘(𝐴 − i))) ∧ (ℑ‘(log‘(𝐴 − i))) ≤ π))
161160simpld 473 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π < (ℑ‘(log‘(𝐴 − i))))
16273, 103logimcld 24036 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (-π < (ℑ‘(log‘(𝐴 + i))) ∧ (ℑ‘(log‘(𝐴 + i))) ≤ π))
163162simprd 477 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 + i))) ≤ π)
164 leneg 10377 . . . . . . . . 9 (((ℑ‘(log‘(𝐴 + i))) ∈ ℝ ∧ π ∈ ℝ) → ((ℑ‘(log‘(𝐴 + i))) ≤ π ↔ -π ≤ -(ℑ‘(log‘(𝐴 + i)))))
165143, 124, 164sylancl 692 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(𝐴 + i))) ≤ π ↔ -π ≤ -(ℑ‘(log‘(𝐴 + i)))))
166163, 165mpbid 220 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π ≤ -(ℑ‘(log‘(𝐴 + i))))
167158, 158, 140, 159, 161, 166ltleaddd 10494 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (-π + -π) < ((ℑ‘(log‘(𝐴 − i))) + -(ℑ‘(log‘(𝐴 + i)))))
168141, 144negsubd 10246 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(𝐴 − i))) + -(ℑ‘(log‘(𝐴 + i)))) = ((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))))
169167, 168breqtrd 4600 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (-π + -π) < ((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))))
170157, 169syl5eqbrr 4610 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (-π − π) < ((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))))
171124a1i 11 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → π ∈ ℝ)
172158, 171, 152ltsubaddd 10469 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((-π − π) < ((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) ↔ -π < (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π)))
173170, 172mpbid 220 . . 3 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → -π < (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π))
174 0red 9894 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 ∈ ℝ)
1756imcld 13726 . . . . . . . . . . . . 13 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘𝐴) ∈ ℝ)
176 peano2rem 10196 . . . . . . . . . . . . 13 ((ℑ‘𝐴) ∈ ℝ → ((ℑ‘𝐴) − 1) ∈ ℝ)
177175, 176syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘𝐴) − 1) ∈ ℝ)
178 peano2re 10057 . . . . . . . . . . . . 13 ((ℑ‘𝐴) ∈ ℝ → ((ℑ‘𝐴) + 1) ∈ ℝ)
179175, 178syl 17 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘𝐴) + 1) ∈ ℝ)
180175ltm1d 10802 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘𝐴) − 1) < (ℑ‘𝐴))
181175ltp1d 10800 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘𝐴) < ((ℑ‘𝐴) + 1))
182177, 175, 179, 180, 181lttrd 10046 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘𝐴) − 1) < ((ℑ‘𝐴) + 1))
183 ltdiv1 10733 . . . . . . . . . . . 12 ((((ℑ‘𝐴) − 1) ∈ ℝ ∧ ((ℑ‘𝐴) + 1) ∈ ℝ ∧ ((ℜ‘𝐴) ∈ ℝ ∧ 0 < (ℜ‘𝐴))) → (((ℑ‘𝐴) − 1) < ((ℑ‘𝐴) + 1) ↔ (((ℑ‘𝐴) − 1) / (ℜ‘𝐴)) < (((ℑ‘𝐴) + 1) / (ℜ‘𝐴))))
184177, 179, 35, 48, 183syl112anc 1321 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘𝐴) − 1) < ((ℑ‘𝐴) + 1) ↔ (((ℑ‘𝐴) − 1) / (ℜ‘𝐴)) < (((ℑ‘𝐴) + 1) / (ℜ‘𝐴))))
185182, 184mpbid 220 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘𝐴) − 1) / (ℜ‘𝐴)) < (((ℑ‘𝐴) + 1) / (ℜ‘𝐴)))
186 imsub 13666 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ i ∈ ℂ) → (ℑ‘(𝐴 − i)) = ((ℑ‘𝐴) − (ℑ‘i)))
1876, 2, 186sylancl 692 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(𝐴 − i)) = ((ℑ‘𝐴) − (ℑ‘i)))
188 imi 13688 . . . . . . . . . . . . 13 (ℑ‘i) = 1
189188oveq2i 6535 . . . . . . . . . . . 12 ((ℑ‘𝐴) − (ℑ‘i)) = ((ℑ‘𝐴) − 1)
190187, 189syl6eq 2656 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(𝐴 − i)) = ((ℑ‘𝐴) − 1))
191190, 39oveq12d 6542 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(𝐴 − i)) / (ℜ‘(𝐴 − i))) = (((ℑ‘𝐴) − 1) / (ℜ‘𝐴)))
192 imadd 13665 . . . . . . . . . . . . 13 ((𝐴 ∈ ℂ ∧ i ∈ ℂ) → (ℑ‘(𝐴 + i)) = ((ℑ‘𝐴) + (ℑ‘i)))
1936, 2, 192sylancl 692 . . . . . . . . . . . 12 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(𝐴 + i)) = ((ℑ‘𝐴) + (ℑ‘i)))
194188oveq2i 6535 . . . . . . . . . . . 12 ((ℑ‘𝐴) + (ℑ‘i)) = ((ℑ‘𝐴) + 1)
195193, 194syl6eq 2656 . . . . . . . . . . 11 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(𝐴 + i)) = ((ℑ‘𝐴) + 1))
196195, 83oveq12d 6542 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(𝐴 + i)) / (ℜ‘(𝐴 + i))) = (((ℑ‘𝐴) + 1) / (ℜ‘𝐴)))
197185, 191, 1963brtr4d 4606 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(𝐴 − i)) / (ℜ‘(𝐴 − i))) < ((ℑ‘(𝐴 + i)) / (ℜ‘(𝐴 + i))))
198 tanarg 24083 . . . . . . . . . 10 (((𝐴 − i) ∈ ℂ ∧ (ℜ‘(𝐴 − i)) ≠ 0) → (tan‘(ℑ‘(log‘(𝐴 − i)))) = ((ℑ‘(𝐴 − i)) / (ℜ‘(𝐴 − i))))
19930, 42, 198syl2anc 690 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (tan‘(ℑ‘(log‘(𝐴 − i)))) = ((ℑ‘(𝐴 − i)) / (ℜ‘(𝐴 − i))))
200 tanarg 24083 . . . . . . . . . 10 (((𝐴 + i) ∈ ℂ ∧ (ℜ‘(𝐴 + i)) ≠ 0) → (tan‘(ℑ‘(log‘(𝐴 + i)))) = ((ℑ‘(𝐴 + i)) / (ℜ‘(𝐴 + i))))
20173, 99, 200syl2anc 690 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (tan‘(ℑ‘(log‘(𝐴 + i)))) = ((ℑ‘(𝐴 + i)) / (ℜ‘(𝐴 + i))))
202197, 199, 2013brtr4d 4606 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (tan‘(ℑ‘(log‘(𝐴 − i)))) < (tan‘(ℑ‘(log‘(𝐴 + i)))))
20348, 39breqtrrd 4602 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘(𝐴 − i)))
204 argregt0 24074 . . . . . . . . . 10 (((𝐴 − i) ∈ ℂ ∧ 0 < (ℜ‘(𝐴 − i))) → (ℑ‘(log‘(𝐴 − i))) ∈ (-(π / 2)(,)(π / 2)))
20530, 203, 204syl2anc 690 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 − i))) ∈ (-(π / 2)(,)(π / 2)))
20648, 83breqtrrd 4602 . . . . . . . . . 10 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → 0 < (ℜ‘(𝐴 + i)))
207 argregt0 24074 . . . . . . . . . 10 (((𝐴 + i) ∈ ℂ ∧ 0 < (ℜ‘(𝐴 + i))) → (ℑ‘(log‘(𝐴 + i))) ∈ (-(π / 2)(,)(π / 2)))
20873, 206, 207syl2anc 690 . . . . . . . . 9 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 + i))) ∈ (-(π / 2)(,)(π / 2)))
209 tanord 24002 . . . . . . . . 9 (((ℑ‘(log‘(𝐴 − i))) ∈ (-(π / 2)(,)(π / 2)) ∧ (ℑ‘(log‘(𝐴 + i))) ∈ (-(π / 2)(,)(π / 2))) → ((ℑ‘(log‘(𝐴 − i))) < (ℑ‘(log‘(𝐴 + i))) ↔ (tan‘(ℑ‘(log‘(𝐴 − i)))) < (tan‘(ℑ‘(log‘(𝐴 + i))))))
210205, 208, 209syl2anc 690 . . . . . . . 8 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(𝐴 − i))) < (ℑ‘(log‘(𝐴 + i))) ↔ (tan‘(ℑ‘(log‘(𝐴 − i)))) < (tan‘(ℑ‘(log‘(𝐴 + i))))))
211202, 210mpbird 245 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 − i))) < (ℑ‘(log‘(𝐴 + i))))
212144addid2d 10085 . . . . . . 7 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (0 + (ℑ‘(log‘(𝐴 + i)))) = (ℑ‘(log‘(𝐴 + i))))
213211, 212breqtrrd 4602 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘(log‘(𝐴 − i))) < (0 + (ℑ‘(log‘(𝐴 + i)))))
214140, 143, 174ltsubaddd 10469 . . . . . 6 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) < 0 ↔ (ℑ‘(log‘(𝐴 − i))) < (0 + (ℑ‘(log‘(𝐴 + i))))))
215213, 214mpbird 245 . . . . 5 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → ((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) < 0)
216152, 174, 171, 215ltadd1dd 10484 . . . 4 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) < (0 + π))
217110addid2i 10072 . . . 4 (0 + π) = π
218216, 217syl6breq 4615 . . 3 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) < π)
219155rexri 9945 . . . 4 -π ∈ ℝ*
220124rexri 9945 . . . 4 π ∈ ℝ*
221 elioo2 12040 . . . 4 ((-π ∈ ℝ* ∧ π ∈ ℝ*) → ((((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∈ (-π(,)π) ↔ ((((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∈ ℝ ∧ -π < (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∧ (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) < π)))
222219, 220, 221mp2an 703 . . 3 ((((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∈ (-π(,)π) ↔ ((((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∈ ℝ ∧ -π < (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∧ (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) < π))
223154, 173, 218, 222syl3anbrc 1238 . 2 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (((ℑ‘(log‘(𝐴 − i))) − (ℑ‘(log‘(𝐴 + i)))) + π) ∈ (-π(,)π))
224151, 223eqeltrd 2684 1 ((𝐴 ∈ dom arctan ∧ 0 < (ℜ‘𝐴)) → (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i · 𝐴))))) ∈ (-π(,)π))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2776   class class class wbr 4574  dom cdm 5025  cfv 5787  (class class class)co 6524  cc 9787  cr 9788  0cc0 9789  1c1 9790  ici 9791   + caddc 9792   · cmul 9794  *cxr 9926   < clt 9927  cle 9928  cmin 10114  -cneg 10115   / cdiv 10530  2c2 10914  (,)cioo 11999  cre 13628  cim 13629  tanctan 14578  πcpi 14579  logclog 24019  arctancatan 24305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586  ax-rep 4690  ax-sep 4700  ax-nul 4709  ax-pow 4761  ax-pr 4825  ax-un 6821  ax-inf2 8395  ax-cnex 9845  ax-resscn 9846  ax-1cn 9847  ax-icn 9848  ax-addcl 9849  ax-addrcl 9850  ax-mulcl 9851  ax-mulrcl 9852  ax-mulcom 9853  ax-addass 9854  ax-mulass 9855  ax-distr 9856  ax-i2m1 9857  ax-1ne0 9858  ax-1rid 9859  ax-rnegex 9860  ax-rrecex 9861  ax-cnre 9862  ax-pre-lttri 9863  ax-pre-lttrn 9864  ax-pre-ltadd 9865  ax-pre-mulgt0 9866  ax-pre-sup 9867  ax-addf 9868  ax-mulf 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2458  df-mo 2459  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ne 2778  df-nel 2779  df-ral 2897  df-rex 2898  df-reu 2899  df-rmo 2900  df-rab 2901  df-v 3171  df-sbc 3399  df-csb 3496  df-dif 3539  df-un 3541  df-in 3543  df-ss 3550  df-pss 3552  df-nul 3871  df-if 4033  df-pw 4106  df-sn 4122  df-pr 4124  df-tp 4126  df-op 4128  df-uni 4364  df-int 4402  df-iun 4448  df-iin 4449  df-br 4575  df-opab 4635  df-mpt 4636  df-tr 4672  df-eprel 4936  df-id 4940  df-po 4946  df-so 4947  df-fr 4984  df-se 4985  df-we 4986  df-xp 5031  df-rel 5032  df-cnv 5033  df-co 5034  df-dm 5035  df-rn 5036  df-res 5037  df-ima 5038  df-pred 5580  df-ord 5626  df-on 5627  df-lim 5628  df-suc 5629  df-iota 5751  df-fun 5789  df-fn 5790  df-f 5791  df-f1 5792  df-fo 5793  df-f1o 5794  df-fv 5795  df-isom 5796  df-riota 6486  df-ov 6527  df-oprab 6528  df-mpt2 6529  df-of 6769  df-om 6932  df-1st 7033  df-2nd 7034  df-supp 7157  df-wrecs 7268  df-recs 7329  df-rdg 7367  df-1o 7421  df-2o 7422  df-oadd 7425  df-er 7603  df-map 7720  df-pm 7721  df-ixp 7769  df-en 7816  df-dom 7817  df-sdom 7818  df-fin 7819  df-fsupp 8133  df-fi 8174  df-sup 8205  df-inf 8206  df-oi 8272  df-card 8622  df-cda 8847  df-pnf 9929  df-mnf 9930  df-xr 9931  df-ltxr 9932  df-le 9933  df-sub 10116  df-neg 10117  df-div 10531  df-nn 10865  df-2 10923  df-3 10924  df-4 10925  df-5 10926  df-6 10927  df-7 10928  df-8 10929  df-9 10930  df-n0 11137  df-z 11208  df-dec 11323  df-uz 11517  df-q 11618  df-rp 11662  df-xneg 11775  df-xadd 11776  df-xmul 11777  df-ioo 12003  df-ioc 12004  df-ico 12005  df-icc 12006  df-fz 12150  df-fzo 12287  df-fl 12407  df-mod 12483  df-seq 12616  df-exp 12675  df-fac 12875  df-bc 12904  df-hash 12932  df-shft 13598  df-cj 13630  df-re 13631  df-im 13632  df-sqrt 13766  df-abs 13767  df-limsup 13993  df-clim 14010  df-rlim 14011  df-sum 14208  df-ef 14580  df-sin 14582  df-cos 14583  df-tan 14584  df-pi 14585  df-struct 15640  df-ndx 15641  df-slot 15642  df-base 15643  df-sets 15644  df-ress 15645  df-plusg 15724  df-mulr 15725  df-starv 15726  df-sca 15727  df-vsca 15728  df-ip 15729  df-tset 15730  df-ple 15731  df-ds 15734  df-unif 15735  df-hom 15736  df-cco 15737  df-rest 15849  df-topn 15850  df-0g 15868  df-gsum 15869  df-topgen 15870  df-pt 15871  df-prds 15874  df-xrs 15928  df-qtop 15933  df-imas 15934  df-xps 15936  df-mre 16012  df-mrc 16013  df-acs 16015  df-mgm 17008  df-sgrp 17050  df-mnd 17061  df-submnd 17102  df-mulg 17307  df-cntz 17516  df-cmn 17961  df-psmet 19502  df-xmet 19503  df-met 19504  df-bl 19505  df-mopn 19506  df-fbas 19507  df-fg 19508  df-cnfld 19511  df-top 20460  df-bases 20461  df-topon 20462  df-topsp 20463  df-cld 20572  df-ntr 20573  df-cls 20574  df-nei 20651  df-lp 20689  df-perf 20690  df-cn 20780  df-cnp 20781  df-haus 20868  df-tx 21114  df-hmeo 21307  df-fil 21399  df-fm 21491  df-flim 21492  df-flf 21493  df-xms 21873  df-ms 21874  df-tms 21875  df-cncf 22417  df-limc 23350  df-dv 23351  df-log 24021  df-atan 24308
This theorem is referenced by:  atanlogsub  24357  atanbndlem  24366
  Copyright terms: Public domain W3C validator