Step | Hyp | Ref
| Expression |
1 | | atanval 26250 |
. . . . 5
β’ (π΄ β dom arctan β
(arctanβπ΄) = ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
2 | 1 | oveq2d 7378 |
. . . 4
β’ (π΄ β dom arctan β (i
Β· (arctanβπ΄))
= (i Β· ((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))))) |
3 | | ax-icn 11117 |
. . . . . 6
β’ i β
β |
4 | 3 | a1i 11 |
. . . . 5
β’ (π΄ β dom arctan β i
β β) |
5 | | halfcl 12385 |
. . . . . 6
β’ (i β
β β (i / 2) β β) |
6 | 3, 5 | mp1i 13 |
. . . . 5
β’ (π΄ β dom arctan β (i /
2) β β) |
7 | | ax-1cn 11116 |
. . . . . . . 8
β’ 1 β
β |
8 | | atandm2 26243 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
9 | 8 | simp1bi 1146 |
. . . . . . . . 9
β’ (π΄ β dom arctan β π΄ β
β) |
10 | | mulcl 11142 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
11 | 3, 9, 10 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β dom arctan β (i
Β· π΄) β
β) |
12 | | subcl 11407 |
. . . . . . . 8
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
13 | 7, 11, 12 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β β) |
14 | 8 | simp2bi 1147 |
. . . . . . 7
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β 0) |
15 | 13, 14 | logcld 25942 |
. . . . . 6
β’ (π΄ β dom arctan β
(logβ(1 β (i Β· π΄))) β β) |
16 | | addcl 11140 |
. . . . . . . 8
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
17 | 7, 11, 16 | sylancr 588 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
β) |
18 | 8 | simp3bi 1148 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
0) |
19 | 17, 18 | logcld 25942 |
. . . . . 6
β’ (π΄ β dom arctan β
(logβ(1 + (i Β· π΄))) β β) |
20 | 15, 19 | subcld 11519 |
. . . . 5
β’ (π΄ β dom arctan β
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β
β) |
21 | 4, 6, 20 | mulassd 11185 |
. . . 4
β’ (π΄ β dom arctan β ((i
Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = (i Β· ((i /
2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
22 | | 2cn 12235 |
. . . . . . . 8
β’ 2 β
β |
23 | | 2ne0 12264 |
. . . . . . . 8
β’ 2 β
0 |
24 | | divneg 11854 |
. . . . . . . 8
β’ ((1
β β β§ 2 β β β§ 2 β 0) β -(1 / 2) = (-1 /
2)) |
25 | 7, 22, 23, 24 | mp3an 1462 |
. . . . . . 7
β’ -(1 / 2)
= (-1 / 2) |
26 | | ixi 11791 |
. . . . . . . 8
β’ (i
Β· i) = -1 |
27 | 26 | oveq1i 7372 |
. . . . . . 7
β’ ((i
Β· i) / 2) = (-1 / 2) |
28 | 3, 3, 22, 23 | divassi 11918 |
. . . . . . 7
β’ ((i
Β· i) / 2) = (i Β· (i / 2)) |
29 | 25, 27, 28 | 3eqtr2i 2771 |
. . . . . 6
β’ -(1 / 2)
= (i Β· (i / 2)) |
30 | 29 | oveq1i 7372 |
. . . . 5
β’ (-(1 / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = ((i Β· (i /
2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
31 | | halfcn 12375 |
. . . . . . 7
β’ (1 / 2)
β β |
32 | | mulneg12 11600 |
. . . . . . 7
β’ (((1 / 2)
β β β§ ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β β)
β (-(1 / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = ((1 / 2) Β·
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
33 | 31, 20, 32 | sylancr 588 |
. . . . . 6
β’ (π΄ β dom arctan β (-(1 /
2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = ((1 / 2) Β·
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
34 | 15, 19 | negsubdi2d 11535 |
. . . . . . 7
β’ (π΄ β dom arctan β
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) = ((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄))))) |
35 | 34 | oveq2d 7378 |
. . . . . 6
β’ (π΄ β dom arctan β ((1 /
2) Β· -((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = ((1 / 2) Β·
((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄)))))) |
36 | 31 | a1i 11 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 /
2) β β) |
37 | 36, 19, 15 | subdid 11618 |
. . . . . 6
β’ (π΄ β dom arctan β ((1 /
2) Β· ((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) = (((1 / 2)
Β· (logβ(1 + (i Β· π΄)))) β ((1 / 2) Β· (logβ(1
β (i Β· π΄)))))) |
38 | 33, 35, 37 | 3eqtrd 2781 |
. . . . 5
β’ (π΄ β dom arctan β (-(1 /
2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = (((1 / 2) Β·
(logβ(1 + (i Β· π΄)))) β ((1 / 2) Β· (logβ(1
β (i Β· π΄)))))) |
39 | 30, 38 | eqtr3id 2791 |
. . . 4
β’ (π΄ β dom arctan β ((i
Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = (((1 / 2) Β·
(logβ(1 + (i Β· π΄)))) β ((1 / 2) Β· (logβ(1
β (i Β· π΄)))))) |
40 | 2, 21, 39 | 3eqtr2d 2783 |
. . 3
β’ (π΄ β dom arctan β (i
Β· (arctanβπ΄))
= (((1 / 2) Β· (logβ(1 + (i Β· π΄)))) β ((1 / 2) Β· (logβ(1
β (i Β· π΄)))))) |
41 | 40 | fveq2d 6851 |
. 2
β’ (π΄ β dom arctan β
(expβ(i Β· (arctanβπ΄))) = (expβ(((1 / 2) Β·
(logβ(1 + (i Β· π΄)))) β ((1 / 2) Β· (logβ(1
β (i Β· π΄))))))) |
42 | | mulcl 11142 |
. . . 4
β’ (((1 / 2)
β β β§ (logβ(1 + (i Β· π΄))) β β) β ((1 / 2) Β·
(logβ(1 + (i Β· π΄)))) β β) |
43 | 31, 19, 42 | sylancr 588 |
. . 3
β’ (π΄ β dom arctan β ((1 /
2) Β· (logβ(1 + (i Β· π΄)))) β β) |
44 | | mulcl 11142 |
. . . 4
β’ (((1 / 2)
β β β§ (logβ(1 β (i Β· π΄))) β β) β ((1 / 2) Β·
(logβ(1 β (i Β· π΄)))) β β) |
45 | 31, 15, 44 | sylancr 588 |
. . 3
β’ (π΄ β dom arctan β ((1 /
2) Β· (logβ(1 β (i Β· π΄)))) β β) |
46 | | efsub 15989 |
. . 3
β’ ((((1 /
2) Β· (logβ(1 + (i Β· π΄)))) β β β§ ((1 / 2) Β·
(logβ(1 β (i Β· π΄)))) β β) β (expβ(((1
/ 2) Β· (logβ(1 + (i Β· π΄)))) β ((1 / 2) Β· (logβ(1
β (i Β· π΄))))))
= ((expβ((1 / 2) Β· (logβ(1 + (i Β· π΄))))) / (expβ((1 / 2) Β·
(logβ(1 β (i Β· π΄))))))) |
47 | 43, 45, 46 | syl2anc 585 |
. 2
β’ (π΄ β dom arctan β
(expβ(((1 / 2) Β· (logβ(1 + (i Β· π΄)))) β ((1 / 2) Β· (logβ(1
β (i Β· π΄))))))
= ((expβ((1 / 2) Β· (logβ(1 + (i Β· π΄))))) / (expβ((1 / 2) Β·
(logβ(1 β (i Β· π΄))))))) |
48 | 17, 18, 36 | cxpefd 26083 |
. . . 4
β’ (π΄ β dom arctan β ((1 +
(i Β· π΄))βπ(1 / 2)) =
(expβ((1 / 2) Β· (logβ(1 + (i Β· π΄)))))) |
49 | | cxpsqrt 26074 |
. . . . 5
β’ ((1 + (i
Β· π΄)) β β
β ((1 + (i Β· π΄))βπ(1 / 2)) =
(ββ(1 + (i Β· π΄)))) |
50 | 17, 49 | syl 17 |
. . . 4
β’ (π΄ β dom arctan β ((1 +
(i Β· π΄))βπ(1 / 2)) =
(ββ(1 + (i Β· π΄)))) |
51 | 48, 50 | eqtr3d 2779 |
. . 3
β’ (π΄ β dom arctan β
(expβ((1 / 2) Β· (logβ(1 + (i Β· π΄))))) = (ββ(1 + (i Β·
π΄)))) |
52 | 13, 14, 36 | cxpefd 26083 |
. . . 4
β’ (π΄ β dom arctan β ((1
β (i Β· π΄))βπ(1 / 2)) =
(expβ((1 / 2) Β· (logβ(1 β (i Β· π΄)))))) |
53 | | cxpsqrt 26074 |
. . . . 5
β’ ((1
β (i Β· π΄))
β β β ((1 β (i Β· π΄))βπ(1 / 2)) =
(ββ(1 β (i Β· π΄)))) |
54 | 13, 53 | syl 17 |
. . . 4
β’ (π΄ β dom arctan β ((1
β (i Β· π΄))βπ(1 / 2)) =
(ββ(1 β (i Β· π΄)))) |
55 | 52, 54 | eqtr3d 2779 |
. . 3
β’ (π΄ β dom arctan β
(expβ((1 / 2) Β· (logβ(1 β (i Β· π΄))))) = (ββ(1
β (i Β· π΄)))) |
56 | 51, 55 | oveq12d 7380 |
. 2
β’ (π΄ β dom arctan β
((expβ((1 / 2) Β· (logβ(1 + (i Β· π΄))))) / (expβ((1 / 2) Β·
(logβ(1 β (i Β· π΄)))))) = ((ββ(1 + (i Β·
π΄))) / (ββ(1
β (i Β· π΄))))) |
57 | 41, 47, 56 | 3eqtrd 2781 |
1
β’ (π΄ β dom arctan β
(expβ(i Β· (arctanβπ΄))) = ((ββ(1 + (i Β· π΄))) / (ββ(1 β
(i Β· π΄))))) |