Proof of Theorem atanlogsub
Step | Hyp | Ref
| Expression |
1 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
2 | | ax-icn 9874 |
. . . . . . 7
⊢ i ∈
ℂ |
3 | | atandm2 24404 |
. . . . . . . 8
⊢ (𝐴 ∈ dom arctan ↔ (𝐴 ∈ ℂ ∧ (1 −
(i · 𝐴)) ≠ 0
∧ (1 + (i · 𝐴))
≠ 0)) |
4 | 3 | simp1bi 1069 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan → 𝐴 ∈
ℂ) |
5 | | mulcl 9899 |
. . . . . . 7
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · 𝐴) ∈ ℂ) |
6 | 2, 4, 5 | sylancr 694 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan → (i
· 𝐴) ∈
ℂ) |
7 | | addcl 9897 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + (i ·
𝐴)) ∈
ℂ) |
8 | 1, 6, 7 | sylancr 694 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ∈
ℂ) |
9 | 3 | simp3bi 1071 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1 +
(i · 𝐴)) ≠
0) |
10 | 8, 9 | logcld 24121 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · 𝐴))) ∈ ℂ) |
11 | | subcl 10159 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − (i
· 𝐴)) ∈
ℂ) |
12 | 1, 6, 11 | sylancr 694 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
∈ ℂ) |
13 | 3 | simp2bi 1070 |
. . . . 5
⊢ (𝐴 ∈ dom arctan → (1
− (i · 𝐴))
≠ 0) |
14 | 12, 13 | logcld 24121 |
. . . 4
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · 𝐴))) ∈ ℂ) |
15 | 10, 14 | subcld 10271 |
. . 3
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) |
16 | 15 | adantr 480 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) |
17 | 4 | recld 13782 |
. . . . . . 7
⊢ (𝐴 ∈ dom arctan →
(ℜ‘𝐴) ∈
ℝ) |
18 | | 0re 9919 |
. . . . . . 7
⊢ 0 ∈
ℝ |
19 | | lttri2 9999 |
. . . . . . 7
⊢
(((ℜ‘𝐴)
∈ ℝ ∧ 0 ∈ ℝ) → ((ℜ‘𝐴) ≠ 0 ↔ ((ℜ‘𝐴) < 0 ∨ 0 <
(ℜ‘𝐴)))) |
20 | 17, 18, 19 | sylancl 693 |
. . . . . 6
⊢ (𝐴 ∈ dom arctan →
((ℜ‘𝐴) ≠ 0
↔ ((ℜ‘𝐴)
< 0 ∨ 0 < (ℜ‘𝐴)))) |
21 | 20 | biimpa 500 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℜ‘𝐴)
< 0 ∨ 0 < (ℜ‘𝐴))) |
22 | 15 | imnegd 13798 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan →
(ℑ‘-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
-(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) |
23 | 10, 14 | negsubdi2d 10287 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) =
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
24 | | mulneg2 10346 |
. . . . . . . . . . . . . . . . 17
⊢ ((i
∈ ℂ ∧ 𝐴
∈ ℂ) → (i · -𝐴) = -(i · 𝐴)) |
25 | 2, 4, 24 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ dom arctan → (i
· -𝐴) = -(i ·
𝐴)) |
26 | 25 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1 +
(i · -𝐴)) = (1 + -(i
· 𝐴))) |
27 | | negsub 10208 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 + -(i ·
𝐴)) = (1 − (i
· 𝐴))) |
28 | 1, 6, 27 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1 +
-(i · 𝐴)) = (1
− (i · 𝐴))) |
29 | 26, 28 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (1 +
(i · -𝐴)) = (1
− (i · 𝐴))) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(log‘(1 + (i · -𝐴))) = (log‘(1 − (i ·
𝐴)))) |
31 | 25 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1
− (i · -𝐴)) =
(1 − -(i · 𝐴))) |
32 | | subneg 10209 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (i · 𝐴) ∈ ℂ) → (1 − -(i
· 𝐴)) = (1 + (i
· 𝐴))) |
33 | 1, 6, 32 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ dom arctan → (1
− -(i · 𝐴)) =
(1 + (i · 𝐴))) |
34 | 31, 33 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ dom arctan → (1
− (i · -𝐴)) =
(1 + (i · 𝐴))) |
35 | 34 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ dom arctan →
(log‘(1 − (i · -𝐴))) = (log‘(1 + (i · 𝐴)))) |
36 | 30, 35 | oveq12d 6567 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))) =
((log‘(1 − (i · 𝐴))) − (log‘(1 + (i ·
𝐴))))) |
37 | 23, 36 | eqtr4d 2647 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan →
-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) =
((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) |
38 | 37 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝐴 ∈ dom arctan →
(ℑ‘-((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))))) |
39 | 22, 38 | eqtr3d 2646 |
. . . . . . . . 9
⊢ (𝐴 ∈ dom arctan →
-(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))))) |
40 | 39 | adantr 480 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) =
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴)))))) |
41 | | atandmneg 24433 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ dom arctan → -𝐴 ∈ dom
arctan) |
42 | 41 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ -𝐴 ∈ dom
arctan) |
43 | 17 | lt0neg1d 10476 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ dom arctan →
((ℜ‘𝐴) < 0
↔ 0 < -(ℜ‘𝐴))) |
44 | 43 | biimpa 500 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ 0 < -(ℜ‘𝐴)) |
45 | 4 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ 𝐴 ∈
ℂ) |
46 | 45 | renegd 13797 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℜ‘-𝐴) =
-(ℜ‘𝐴)) |
47 | 44, 46 | breqtrrd 4611 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ 0 < (ℜ‘-𝐴)) |
48 | | atanlogsublem 24442 |
. . . . . . . . . 10
⊢ ((-𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘-𝐴)) →
(ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) ∈
(-π(,)π)) |
49 | 42, 47, 48 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) ∈
(-π(,)π)) |
50 | | picn 24015 |
. . . . . . . . . . 11
⊢ π
∈ ℂ |
51 | 50 | negnegi 10230 |
. . . . . . . . . 10
⊢ --π =
π |
52 | 51 | oveq2i 6560 |
. . . . . . . . 9
⊢
(-π(,)--π) = (-π(,)π) |
53 | 49, 52 | syl6eleqr 2699 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · -𝐴))) − (log‘(1 − (i
· -𝐴))))) ∈
(-π(,)--π)) |
54 | 40, 53 | eqeltrd 2688 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)--π)) |
55 | | pire 24014 |
. . . . . . . . . 10
⊢ π
∈ ℝ |
56 | 55 | renegcli 10221 |
. . . . . . . . 9
⊢ -π
∈ ℝ |
57 | 56 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ -π ∈ ℝ) |
58 | 55 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ π ∈ ℝ) |
59 | 15 | adantr 480 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈
ℂ) |
60 | 59 | imcld 13783 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
ℝ) |
61 | | iooneg 12163 |
. . . . . . . 8
⊢ ((-π
∈ ℝ ∧ π ∈ ℝ ∧ (ℑ‘((log‘(1 +
(i · 𝐴))) −
(log‘(1 − (i · 𝐴))))) ∈ ℝ) →
((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π) ↔ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴)))))
∈ (-π(,)--π))) |
62 | 57, 58, 60, 61 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ ((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π) ↔ -(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴)))))
∈ (-π(,)--π))) |
63 | 54, 62 | mpbird 246 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) < 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
64 | | atanlogsublem 24442 |
. . . . . 6
⊢ ((𝐴 ∈ dom arctan ∧ 0 <
(ℜ‘𝐴)) →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
65 | 63, 64 | jaodan 822 |
. . . . 5
⊢ ((𝐴 ∈ dom arctan ∧
((ℜ‘𝐴) < 0
∨ 0 < (ℜ‘𝐴))) → (ℑ‘((log‘(1 +
(i · 𝐴))) −
(log‘(1 − (i · 𝐴))))) ∈
(-π(,)π)) |
66 | 21, 65 | syldan 486 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π)) |
67 | | eliooord 12104 |
. . . 4
⊢
((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
(-π(,)π) → (-π < (ℑ‘((log‘(1 + (i ·
𝐴))) − (log‘(1
− (i · 𝐴)))))
∧ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) <
π)) |
68 | 66, 67 | syl 17 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (-π < (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1
− (i · 𝐴)))))
∧ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) <
π)) |
69 | 68 | simpld 474 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ -π < (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))))) |
70 | 68 | simprd 478 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) <
π) |
71 | 16 | imcld 13783 |
. . . 4
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
ℝ) |
72 | | ltle 10005 |
. . . 4
⊢
(((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ∈
ℝ ∧ π ∈ ℝ) → ((ℑ‘((log‘(1 + (i
· 𝐴))) −
(log‘(1 − (i · 𝐴))))) < π →
(ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ≤
π)) |
73 | 71, 55, 72 | sylancl 693 |
. . 3
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) < π
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ≤
π)) |
74 | 70, 73 | mpd 15 |
. 2
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ (ℑ‘((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴))))) ≤
π) |
75 | | ellogrn 24110 |
. 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
· 𝐴))))) ≤
π)) |
76 | 16, 69, 74, 75 | syl3anbrc 1239 |
1
⊢ ((𝐴 ∈ dom arctan ∧
(ℜ‘𝐴) ≠ 0)
→ ((log‘(1 + (i · 𝐴))) − (log‘(1 − (i
· 𝐴)))) ∈ ran
log) |