Step | Hyp | Ref
| Expression |
1 | | ax-icn 11117 |
. . . . . . . . . 10
β’ i β
β |
2 | | atandm2 26243 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
3 | 2 | simp1bi 1146 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β π΄ β
β) |
4 | | mulneg2 11599 |
. . . . . . . . . 10
β’ ((i
β β β§ π΄
β β) β (i Β· -π΄) = -(i Β· π΄)) |
5 | 1, 3, 4 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (i
Β· -π΄) = -(i Β·
π΄)) |
6 | 5 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β dom arctan β (1
β (i Β· -π΄)) =
(1 β -(i Β· π΄))) |
7 | | ax-1cn 11116 |
. . . . . . . . 9
β’ 1 β
β |
8 | | mulcl 11142 |
. . . . . . . . . 10
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
9 | 1, 3, 8 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (i
Β· π΄) β
β) |
10 | | subneg 11457 |
. . . . . . . . 9
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β -(i
Β· π΄)) = (1 + (i
Β· π΄))) |
11 | 7, 9, 10 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β dom arctan β (1
β -(i Β· π΄)) =
(1 + (i Β· π΄))) |
12 | 6, 11 | eqtrd 2777 |
. . . . . . 7
β’ (π΄ β dom arctan β (1
β (i Β· -π΄)) =
(1 + (i Β· π΄))) |
13 | 12 | fveq2d 6851 |
. . . . . 6
β’ (π΄ β dom arctan β
(logβ(1 β (i Β· -π΄))) = (logβ(1 + (i Β· π΄)))) |
14 | 5 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β dom arctan β (1 +
(i Β· -π΄)) = (1 + -(i
Β· π΄))) |
15 | | negsub 11456 |
. . . . . . . . 9
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + -(i Β·
π΄)) = (1 β (i
Β· π΄))) |
16 | 7, 9, 15 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β dom arctan β (1 +
-(i Β· π΄)) = (1
β (i Β· π΄))) |
17 | 14, 16 | eqtrd 2777 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 +
(i Β· -π΄)) = (1
β (i Β· π΄))) |
18 | 17 | fveq2d 6851 |
. . . . . 6
β’ (π΄ β dom arctan β
(logβ(1 + (i Β· -π΄))) = (logβ(1 β (i Β·
π΄)))) |
19 | 13, 18 | oveq12d 7380 |
. . . . 5
β’ (π΄ β dom arctan β
((logβ(1 β (i Β· -π΄))) β (logβ(1 + (i Β·
-π΄)))) = ((logβ(1 +
(i Β· π΄))) β
(logβ(1 β (i Β· π΄))))) |
20 | | subcl 11407 |
. . . . . . . 8
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
21 | 7, 9, 20 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β β) |
22 | 2 | simp2bi 1147 |
. . . . . . 7
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β 0) |
23 | 21, 22 | logcld 25942 |
. . . . . 6
β’ (π΄ β dom arctan β
(logβ(1 β (i Β· π΄))) β β) |
24 | | addcl 11140 |
. . . . . . . 8
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
25 | 7, 9, 24 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
β) |
26 | 2 | simp3bi 1148 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
0) |
27 | 25, 26 | logcld 25942 |
. . . . . 6
β’ (π΄ β dom arctan β
(logβ(1 + (i Β· π΄))) β β) |
28 | 23, 27 | negsubdi2d 11535 |
. . . . 5
β’ (π΄ β dom arctan β
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) = ((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄))))) |
29 | 19, 28 | eqtr4d 2780 |
. . . 4
β’ (π΄ β dom arctan β
((logβ(1 β (i Β· -π΄))) β (logβ(1 + (i Β·
-π΄)))) = -((logβ(1
β (i Β· π΄)))
β (logβ(1 + (i Β· π΄))))) |
30 | 29 | oveq2d 7378 |
. . 3
β’ (π΄ β dom arctan β ((i /
2) Β· ((logβ(1 β (i Β· -π΄))) β (logβ(1 + (i Β·
-π΄))))) = ((i / 2) Β·
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
31 | | halfcl 12385 |
. . . . 5
β’ (i β
β β (i / 2) β β) |
32 | 1, 31 | ax-mp 5 |
. . . 4
β’ (i / 2)
β β |
33 | 23, 27 | subcld 11519 |
. . . 4
β’ (π΄ β dom arctan β
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β
β) |
34 | | mulneg2 11599 |
. . . 4
β’ (((i / 2)
β β β§ ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β β)
β ((i / 2) Β· -((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = -((i / 2) Β·
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
35 | 32, 33, 34 | sylancr 588 |
. . 3
β’ (π΄ β dom arctan β ((i /
2) Β· -((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = -((i / 2) Β·
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
36 | 30, 35 | eqtrd 2777 |
. 2
β’ (π΄ β dom arctan β ((i /
2) Β· ((logβ(1 β (i Β· -π΄))) β (logβ(1 + (i Β·
-π΄))))) = -((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
37 | | atandmneg 26272 |
. . 3
β’ (π΄ β dom arctan β -π΄ β dom
arctan) |
38 | | atanval 26250 |
. . 3
β’ (-π΄ β dom arctan β
(arctanβ-π΄) = ((i /
2) Β· ((logβ(1 β (i Β· -π΄))) β (logβ(1 + (i Β·
-π΄)))))) |
39 | 37, 38 | syl 17 |
. 2
β’ (π΄ β dom arctan β
(arctanβ-π΄) = ((i /
2) Β· ((logβ(1 β (i Β· -π΄))) β (logβ(1 + (i Β·
-π΄)))))) |
40 | | atanval 26250 |
. . 3
β’ (π΄ β dom arctan β
(arctanβπ΄) = ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
41 | 40 | negeqd 11402 |
. 2
β’ (π΄ β dom arctan β
-(arctanβπ΄) = -((i /
2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
42 | 36, 39, 41 | 3eqtr4d 2787 |
1
β’ (π΄ β dom arctan β
(arctanβ-π΄) =
-(arctanβπ΄)) |