Proof of Theorem atanlogsub
Step | Hyp | Ref
| Expression |
1 | | ax-1cn 10787 |
. . . . . 6
⊢ 1 ∈
ℂ |
2 | | ax-icn 10788 |
. . . . . . 7
⊢ i ∈
ℂ |
3 | | atandm2 25760 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
4 | 3 | simp1bi 1147 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) |
5 | | mulcl 10813 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
6 | 2, 4, 5 | sylancr 590 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (i
· 𝐴) ∈
ℂ) |
7 | | addcl 10811 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
8 | 1, 6, 7 | sylancr 590 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ∈
ℂ) |
9 | 3 | simp3bi 1149 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ≠
0) |
10 | 8, 9 | logcld 25459 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · 𝐴))) ∈ ℂ) |
11 | | subcl 11077 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
12 | 1, 6, 11 | sylancr 590 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
∈ ℂ) |
13 | 3 | simp2bi 1148 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
≠ 0) |
14 | 12, 13 | logcld 25459 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · 𝐴))) ∈ ℂ) |
15 | 10, 14 | subcld 11189 |
. . 3
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) |
16 | 15 | adantr 484 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) |
17 | 4 | recld 14757 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
(ℜ‘𝐴) ∈
ℝ) |
18 | | 0re 10835 |
. . . . . . 7
⊢ 0 ∈
ℝ |
19 | | lttri2 10915 |
. . . . . . 7
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝐴) ≠ 0 ↔ ((ℜ‘𝐴) < 0 ∨ 0 <
(ℜ‘𝐴)))) |
20 | 17, 18, 19 | sylancl 589 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan →
((ℜ‘𝐴) ≠ 0
↔ ((ℜ‘𝐴)
< 0 ∨ 0 < (ℜ‘𝐴)))) |
21 | 20 | biimpa 480 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
< 0 ∨ 0 < (ℜ‘𝐴))) |
22 | 15 | imnegd 14773 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan →
(ℑ‘-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
-(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) |
23 | 10, 14 | negsubdi2d 11205 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) =
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
24 | | mulneg2 11269 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · -𝐴) = -(i · 𝐴)) |
25 | 2, 4, 24 | sylancr 590 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan → (i
· -𝐴) = -(i ·
𝐴)) |
26 | 25 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1 +
(i · -𝐴)) = (1 + -(i
· 𝐴))) |
27 | | negsub 11126 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + -(i ·
𝐴)) = (1 − (i
· 𝐴))) |
28 | 1, 6, 27 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1 +
-(i · 𝐴)) = (1
− (i · 𝐴))) |
29 | 26, 28 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (1 +
(i · -𝐴)) = (1
− (i · 𝐴))) |
30 | 29 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · -𝐴))) = (log‘(1 − (i ·
𝐴)))) |
31 | 25 | oveq2d 7229 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1
− (i · -𝐴)) =
(1 − -(i · 𝐴))) |
32 | | subneg 11127 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − -(i
· 𝐴)) = (1 + (i
· 𝐴))) |
33 | 1, 6, 32 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1
− -(i · 𝐴)) =
(1 + (i · 𝐴))) |
34 | 31, 33 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (1
− (i · -𝐴)) =
(1 + (i · 𝐴))) |
35 | 34 | fveq2d 6721 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · -𝐴))) = (log‘(1 + (i · 𝐴)))) |
36 | 30, 35 | oveq12d 7231 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))) =
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
37 | 23, 36 | eqtr4d 2780 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) =
((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) |
38 | 37 | fveq2d 6721 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan →
(ℑ‘-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))))) |
39 | 22, 38 | eqtr3d 2779 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan →
-(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))))) |
40 | 39 | adantr 484 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))))) |
41 | | atandmneg 25789 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈ dom
arctan) |
42 | 17 | lt0neg1d 11401 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
((ℜ‘𝐴) < 0
↔ 0 < -(ℜ‘𝐴))) |
43 | 42 | biimpa 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ 0 < -(ℜ‘𝐴)) |
44 | 4 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ 𝐴 ∈
ℂ) |
45 | 44 | renegd 14772 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℜ‘-𝐴) =
-(ℜ‘𝐴)) |
46 | 43, 45 | breqtrrd 5081 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ 0 < (ℜ‘-𝐴)) |
47 | | atanlogsublem 25798 |
. . . . . . . . . 10
⊢ ((-𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘-𝐴)) →
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) ∈
(-π(,)π)) |
48 | 41, 46, 47 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) ∈
(-π(,)π)) |
49 | | picn 25349 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
50 | 49 | negnegi 11148 |
. . . . . . . . . 10
⊢ --π =
π |
51 | 50 | oveq2i 7224 |
. . . . . . . . 9
⊢
(-π(,)--π) = (-π(,)π) |
52 | 48, 51 | eleqtrrdi 2849 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) ∈
(-π(,)--π)) |
53 | 40, 52 | eqeltrd 2838 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)--π)) |
54 | | pire 25348 |
. . . . . . . . 9
⊢ π
∈ ℝ |
55 | 54 | renegcli 11139 |
. . . . . . . 8
⊢ -π
∈ ℝ |
56 | 15 | adantr 484 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) |
57 | 56 | imcld 14758 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
ℝ) |
58 | | iooneg 13059 |
. . . . . . . 8
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ ∧ (ℑ‘((log‘(1 +
(i · 𝐴))) −
(log‘(1 − (i · 𝐴))))) ∈ ℝ) →
((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π) ↔ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴)))))
∈ (-π(,)--π))) |
59 | 55, 54, 57, 58 | mp3an12i 1467 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ ((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π) ↔ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴)))))
∈ (-π(,)--π))) |
60 | 53, 59 | mpbird 260 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
61 | | atanlogsublem 25798 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
62 | 60, 61 | jaodan 958 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧
((ℜ‘𝐴) < 0
∨ 0 < (ℜ‘𝐴))) → (ℑ‘((log‘(1 +
(i · 𝐴))) −
(log‘(1 − (i · 𝐴))))) ∈
(-π(,)π)) |
63 | 21, 62 | syldan 594 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
64 | | eliooord 12994 |
. . . 4
⊢
((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π) → (-π < (ℑ‘((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))
∧ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) <
π)) |
65 | 63, 64 | syl 17 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (-π < (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴)))))
∧ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) <
π)) |
66 | 65 | simpld 498 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ -π < (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) |
67 | 65 | simprd 499 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) <
π) |
68 | 16 | imcld 14758 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
ℝ) |
69 | | ltle 10921 |
. . . 4
⊢
(((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
ℝ ∧ π ∈ ℝ) → ((ℑ‘((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴))))) < π →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ≤
π)) |
70 | 68, 54, 69 | sylancl 589 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) < π
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ≤
π)) |
71 | 67, 70 | mpd 15 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ≤
π) |
72 | | ellogrn 25448 |
. 2
⊢
(((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 1345 |
1
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈ ran
log) |