Step | Hyp | Ref
| Expression |
1 | | ax-icn 11117 |
. . . . 5
β’ i β
β |
2 | | atancl 26247 |
. . . . 5
β’ (π΄ β dom arctan β
(arctanβπ΄) β
β) |
3 | | mulcl 11142 |
. . . . 5
β’ ((i
β β β§ (arctanβπ΄) β β) β (i Β·
(arctanβπ΄)) β
β) |
4 | 1, 2, 3 | sylancr 588 |
. . . 4
β’ (π΄ β dom arctan β (i
Β· (arctanβπ΄))
β β) |
5 | | efcl 15972 |
. . . 4
β’ ((i
Β· (arctanβπ΄))
β β β (expβ(i Β· (arctanβπ΄))) β β) |
6 | 4, 5 | syl 17 |
. . 3
β’ (π΄ β dom arctan β
(expβ(i Β· (arctanβπ΄))) β β) |
7 | | ax-1cn 11116 |
. . . . 5
β’ 1 β
β |
8 | | atandm2 26243 |
. . . . . . 7
β’ (π΄ β dom arctan β (π΄ β β β§ (1 β
(i Β· π΄)) β 0
β§ (1 + (i Β· π΄))
β 0)) |
9 | 8 | simp1bi 1146 |
. . . . . 6
β’ (π΄ β dom arctan β π΄ β
β) |
10 | 9 | sqcld 14056 |
. . . . 5
β’ (π΄ β dom arctan β (π΄β2) β
β) |
11 | | addcl 11140 |
. . . . 5
β’ ((1
β β β§ (π΄β2) β β) β (1 + (π΄β2)) β
β) |
12 | 7, 10, 11 | sylancr 588 |
. . . 4
β’ (π΄ β dom arctan β (1 +
(π΄β2)) β
β) |
13 | 12 | sqrtcld 15329 |
. . 3
β’ (π΄ β dom arctan β
(ββ(1 + (π΄β2))) β β) |
14 | 12 | sqsqrtd 15331 |
. . . . 5
β’ (π΄ β dom arctan β
((ββ(1 + (π΄β2)))β2) = (1 + (π΄β2))) |
15 | | atandm4 26245 |
. . . . . 6
β’ (π΄ β dom arctan β (π΄ β β β§ (1 +
(π΄β2)) β
0)) |
16 | 15 | simprbi 498 |
. . . . 5
β’ (π΄ β dom arctan β (1 +
(π΄β2)) β
0) |
17 | 14, 16 | eqnetrd 3012 |
. . . 4
β’ (π΄ β dom arctan β
((ββ(1 + (π΄β2)))β2) β 0) |
18 | | sqne0 14035 |
. . . . 5
β’
((ββ(1 + (π΄β2))) β β β
(((ββ(1 + (π΄β2)))β2) β 0 β
(ββ(1 + (π΄β2))) β 0)) |
19 | 13, 18 | syl 17 |
. . . 4
β’ (π΄ β dom arctan β
(((ββ(1 + (π΄β2)))β2) β 0 β
(ββ(1 + (π΄β2))) β 0)) |
20 | 17, 19 | mpbid 231 |
. . 3
β’ (π΄ β dom arctan β
(ββ(1 + (π΄β2))) β 0) |
21 | 6, 13, 20 | divcan4d 11944 |
. 2
β’ (π΄ β dom arctan β
(((expβ(i Β· (arctanβπ΄))) Β· (ββ(1 + (π΄β2)))) / (ββ(1
+ (π΄β2)))) =
(expβ(i Β· (arctanβπ΄)))) |
22 | | halfcn 12375 |
. . . . . . 7
β’ (1 / 2)
β β |
23 | 12, 16 | logcld 25942 |
. . . . . . 7
β’ (π΄ β dom arctan β
(logβ(1 + (π΄β2))) β β) |
24 | | mulcl 11142 |
. . . . . . 7
β’ (((1 / 2)
β β β§ (logβ(1 + (π΄β2))) β β) β ((1 / 2)
Β· (logβ(1 + (π΄β2)))) β β) |
25 | 22, 23, 24 | sylancr 588 |
. . . . . 6
β’ (π΄ β dom arctan β ((1 /
2) Β· (logβ(1 + (π΄β2)))) β β) |
26 | | efadd 15983 |
. . . . . 6
β’ (((i
Β· (arctanβπ΄))
β β β§ ((1 / 2) Β· (logβ(1 + (π΄β2)))) β β) β
(expβ((i Β· (arctanβπ΄)) + ((1 / 2) Β· (logβ(1 +
(π΄β2)))))) =
((expβ(i Β· (arctanβπ΄))) Β· (expβ((1 / 2) Β·
(logβ(1 + (π΄β2))))))) |
27 | 4, 25, 26 | syl2anc 585 |
. . . . 5
β’ (π΄ β dom arctan β
(expβ((i Β· (arctanβπ΄)) + ((1 / 2) Β· (logβ(1 +
(π΄β2)))))) =
((expβ(i Β· (arctanβπ΄))) Β· (expβ((1 / 2) Β·
(logβ(1 + (π΄β2))))))) |
28 | | 2cn 12235 |
. . . . . . . . . . . 12
β’ 2 β
β |
29 | 28 | a1i 11 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β 2
β β) |
30 | | mulcl 11142 |
. . . . . . . . . . . . . 14
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
31 | 1, 9, 30 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β (i
Β· π΄) β
β) |
32 | | addcl 11140 |
. . . . . . . . . . . . 13
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
33 | 7, 31, 32 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
β) |
34 | 8 | simp3bi 1148 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
0) |
35 | 33, 34 | logcld 25942 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β
(logβ(1 + (i Β· π΄))) β β) |
36 | 29, 35, 4 | subdid 11618 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β (2
Β· ((logβ(1 + (i Β· π΄))) β (i Β· (arctanβπ΄)))) = ((2 Β·
(logβ(1 + (i Β· π΄)))) β (2 Β· (i Β·
(arctanβπ΄))))) |
37 | | atanval 26250 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β
(arctanβπ΄) = ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))))) |
38 | 37 | oveq2d 7378 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β ((2
Β· i) Β· (arctanβπ΄)) = ((2 Β· i) Β· ((i / 2)
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))))) |
39 | 1 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β i
β β) |
40 | 29, 39, 2 | mulassd 11185 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β ((2
Β· i) Β· (arctanβπ΄)) = (2 Β· (i Β·
(arctanβπ΄)))) |
41 | | halfcl 12385 |
. . . . . . . . . . . . . . . . . 18
β’ (i β
β β (i / 2) β β) |
42 | 1, 41 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
β’ (i / 2)
β β |
43 | 28, 1, 42 | mulassi 11173 |
. . . . . . . . . . . . . . . 16
β’ ((2
Β· i) Β· (i / 2)) = (2 Β· (i Β· (i /
2))) |
44 | 28, 1, 42 | mul12i 11357 |
. . . . . . . . . . . . . . . 16
β’ (2
Β· (i Β· (i / 2))) = (i Β· (2 Β· (i /
2))) |
45 | | 2ne0 12264 |
. . . . . . . . . . . . . . . . . . 19
β’ 2 β
0 |
46 | 1, 28, 45 | divcan2i 11905 |
. . . . . . . . . . . . . . . . . 18
β’ (2
Β· (i / 2)) = i |
47 | 46 | oveq2i 7373 |
. . . . . . . . . . . . . . . . 17
β’ (i
Β· (2 Β· (i / 2))) = (i Β· i) |
48 | | ixi 11791 |
. . . . . . . . . . . . . . . . 17
β’ (i
Β· i) = -1 |
49 | 47, 48 | eqtri 2765 |
. . . . . . . . . . . . . . . 16
β’ (i
Β· (2 Β· (i / 2))) = -1 |
50 | 43, 44, 49 | 3eqtri 2769 |
. . . . . . . . . . . . . . 15
β’ ((2
Β· i) Β· (i / 2)) = -1 |
51 | 50 | oveq1i 7372 |
. . . . . . . . . . . . . 14
β’ (((2
Β· i) Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) = (-1
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
52 | | subcl 11407 |
. . . . . . . . . . . . . . . . . 18
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
53 | 7, 31, 52 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β β) |
54 | 8 | simp2bi 1147 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β 0) |
55 | 53, 54 | logcld 25942 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β dom arctan β
(logβ(1 β (i Β· π΄))) β β) |
56 | 55, 35 | subcld 11519 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom arctan β
((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) β
β) |
57 | 56 | mulm1d 11614 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom arctan β (-1
Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) = -((logβ(1
β (i Β· π΄)))
β (logβ(1 + (i Β· π΄))))) |
58 | 51, 57 | eqtrid 2789 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β (((2
Β· i) Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) =
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄))))) |
59 | | 2mulicn 12383 |
. . . . . . . . . . . . . . 15
β’ (2
Β· i) β β |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom arctan β (2
Β· i) β β) |
61 | 42 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom arctan β (i /
2) β β) |
62 | 60, 61, 56 | mulassd 11185 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β (((2
Β· i) Β· (i / 2)) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))) = ((2
Β· i) Β· ((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄))))))) |
63 | 55, 35 | negsubdi2d 11535 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β
-((logβ(1 β (i Β· π΄))) β (logβ(1 + (i Β·
π΄)))) = ((logβ(1 + (i
Β· π΄))) β
(logβ(1 β (i Β· π΄))))) |
64 | 58, 62, 63 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β ((2
Β· i) Β· ((i / 2) Β· ((logβ(1 β (i Β· π΄))) β (logβ(1 + (i
Β· π΄)))))) =
((logβ(1 + (i Β· π΄))) β (logβ(1 β (i
Β· π΄))))) |
65 | 38, 40, 64 | 3eqtr3d 2785 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β (2
Β· (i Β· (arctanβπ΄))) = ((logβ(1 + (i Β· π΄))) β (logβ(1
β (i Β· π΄))))) |
66 | 65 | oveq2d 7378 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β ((2
Β· (logβ(1 + (i Β· π΄)))) β (2 Β· (i Β·
(arctanβπ΄)))) = ((2
Β· (logβ(1 + (i Β· π΄)))) β ((logβ(1 + (i Β·
π΄))) β (logβ(1
β (i Β· π΄)))))) |
67 | | mulcl 11142 |
. . . . . . . . . . . . 13
β’ ((2
β β β§ (logβ(1 + (i Β· π΄))) β β) β (2 Β·
(logβ(1 + (i Β· π΄)))) β β) |
68 | 28, 35, 67 | sylancr 588 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β (2
Β· (logβ(1 + (i Β· π΄)))) β β) |
69 | 68, 35, 55 | subsubd 11547 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β ((2
Β· (logβ(1 + (i Β· π΄)))) β ((logβ(1 + (i Β·
π΄))) β (logβ(1
β (i Β· π΄)))))
= (((2 Β· (logβ(1 + (i Β· π΄)))) β (logβ(1 + (i Β·
π΄)))) + (logβ(1
β (i Β· π΄))))) |
70 | 35 | 2timesd 12403 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β (2
Β· (logβ(1 + (i Β· π΄)))) = ((logβ(1 + (i Β· π΄))) + (logβ(1 + (i
Β· π΄))))) |
71 | 35, 35, 70 | mvrladdd 11575 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β ((2
Β· (logβ(1 + (i Β· π΄)))) β (logβ(1 + (i Β·
π΄)))) = (logβ(1 + (i
Β· π΄)))) |
72 | 71 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β (((2
Β· (logβ(1 + (i Β· π΄)))) β (logβ(1 + (i Β·
π΄)))) + (logβ(1
β (i Β· π΄)))) =
((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄))))) |
73 | | atanlogadd 26280 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β
((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄)))) β ran
log) |
74 | | logef 25953 |
. . . . . . . . . . . . 13
β’
(((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄)))) β ran log β
(logβ(expβ((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄)))))) = ((logβ(1 +
(i Β· π΄))) +
(logβ(1 β (i Β· π΄))))) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β
(logβ(expβ((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄)))))) = ((logβ(1 +
(i Β· π΄))) +
(logβ(1 β (i Β· π΄))))) |
76 | | efadd 15983 |
. . . . . . . . . . . . . . 15
β’
(((logβ(1 + (i Β· π΄))) β β β§ (logβ(1
β (i Β· π΄)))
β β) β (expβ((logβ(1 + (i Β· π΄))) + (logβ(1 β (i
Β· π΄))))) =
((expβ(logβ(1 + (i Β· π΄)))) Β· (expβ(logβ(1
β (i Β· π΄)))))) |
77 | 35, 55, 76 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom arctan β
(expβ((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄))))) =
((expβ(logβ(1 + (i Β· π΄)))) Β· (expβ(logβ(1
β (i Β· π΄)))))) |
78 | | eflog 25948 |
. . . . . . . . . . . . . . . 16
β’ (((1 + (i
Β· π΄)) β β
β§ (1 + (i Β· π΄))
β 0) β (expβ(logβ(1 + (i Β· π΄)))) = (1 + (i Β· π΄))) |
79 | 33, 34, 78 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom arctan β
(expβ(logβ(1 + (i Β· π΄)))) = (1 + (i Β· π΄))) |
80 | | eflog 25948 |
. . . . . . . . . . . . . . . 16
β’ (((1
β (i Β· π΄))
β β β§ (1 β (i Β· π΄)) β 0) β (expβ(logβ(1
β (i Β· π΄)))) =
(1 β (i Β· π΄))) |
81 | 53, 54, 80 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom arctan β
(expβ(logβ(1 β (i Β· π΄)))) = (1 β (i Β· π΄))) |
82 | 79, 81 | oveq12d 7380 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom arctan β
((expβ(logβ(1 + (i Β· π΄)))) Β· (expβ(logβ(1
β (i Β· π΄)))))
= ((1 + (i Β· π΄))
Β· (1 β (i Β· π΄)))) |
83 | | sq1 14106 |
. . . . . . . . . . . . . . . . 17
β’
(1β2) = 1 |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β dom arctan β
(1β2) = 1) |
85 | | sqmul 14031 |
. . . . . . . . . . . . . . . . . 18
β’ ((i
β β β§ π΄
β β) β ((i Β· π΄)β2) = ((iβ2) Β· (π΄β2))) |
86 | 1, 9, 85 | sylancr 588 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β dom arctan β ((i
Β· π΄)β2) =
((iβ2) Β· (π΄β2))) |
87 | | i2 14113 |
. . . . . . . . . . . . . . . . . . 19
β’
(iβ2) = -1 |
88 | 87 | oveq1i 7372 |
. . . . . . . . . . . . . . . . . 18
β’
((iβ2) Β· (π΄β2)) = (-1 Β· (π΄β2)) |
89 | 10 | mulm1d 11614 |
. . . . . . . . . . . . . . . . . 18
β’ (π΄ β dom arctan β (-1
Β· (π΄β2)) =
-(π΄β2)) |
90 | 88, 89 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
β’ (π΄ β dom arctan β
((iβ2) Β· (π΄β2)) = -(π΄β2)) |
91 | 86, 90 | eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ (π΄ β dom arctan β ((i
Β· π΄)β2) =
-(π΄β2)) |
92 | 84, 91 | oveq12d 7380 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom arctan β
((1β2) β ((i Β· π΄)β2)) = (1 β -(π΄β2))) |
93 | | subsq 14121 |
. . . . . . . . . . . . . . . 16
β’ ((1
β β β§ (i Β· π΄) β β) β ((1β2) β
((i Β· π΄)β2)) =
((1 + (i Β· π΄))
Β· (1 β (i Β· π΄)))) |
94 | 7, 31, 93 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom arctan β
((1β2) β ((i Β· π΄)β2)) = ((1 + (i Β· π΄)) Β· (1 β (i
Β· π΄)))) |
95 | | subneg 11457 |
. . . . . . . . . . . . . . . 16
β’ ((1
β β β§ (π΄β2) β β) β (1 β
-(π΄β2)) = (1 + (π΄β2))) |
96 | 7, 10, 95 | sylancr 588 |
. . . . . . . . . . . . . . 15
β’ (π΄ β dom arctan β (1
β -(π΄β2)) = (1 +
(π΄β2))) |
97 | 92, 94, 96 | 3eqtr3d 2785 |
. . . . . . . . . . . . . 14
β’ (π΄ β dom arctan β ((1 +
(i Β· π΄)) Β· (1
β (i Β· π΄))) =
(1 + (π΄β2))) |
98 | 77, 82, 97 | 3eqtrd 2781 |
. . . . . . . . . . . . 13
β’ (π΄ β dom arctan β
(expβ((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄))))) = (1 + (π΄β2))) |
99 | 98 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π΄ β dom arctan β
(logβ(expβ((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄)))))) = (logβ(1 +
(π΄β2)))) |
100 | 75, 99 | eqtr3d 2779 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β
((logβ(1 + (i Β· π΄))) + (logβ(1 β (i Β·
π΄)))) = (logβ(1 +
(π΄β2)))) |
101 | 69, 72, 100 | 3eqtrd 2781 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β ((2
Β· (logβ(1 + (i Β· π΄)))) β ((logβ(1 + (i Β·
π΄))) β (logβ(1
β (i Β· π΄)))))
= (logβ(1 + (π΄β2)))) |
102 | 36, 66, 101 | 3eqtrd 2781 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (2
Β· ((logβ(1 + (i Β· π΄))) β (i Β· (arctanβπ΄)))) = (logβ(1 + (π΄β2)))) |
103 | 102 | oveq1d 7377 |
. . . . . . . 8
β’ (π΄ β dom arctan β ((2
Β· ((logβ(1 + (i Β· π΄))) β (i Β· (arctanβπ΄)))) / 2) = ((logβ(1 +
(π΄β2))) /
2)) |
104 | 35, 4 | subcld 11519 |
. . . . . . . . 9
β’ (π΄ β dom arctan β
((logβ(1 + (i Β· π΄))) β (i Β· (arctanβπ΄))) β
β) |
105 | 45 | a1i 11 |
. . . . . . . . 9
β’ (π΄ β dom arctan β 2 β
0) |
106 | 104, 29, 105 | divcan3d 11943 |
. . . . . . . 8
β’ (π΄ β dom arctan β ((2
Β· ((logβ(1 + (i Β· π΄))) β (i Β· (arctanβπ΄)))) / 2) = ((logβ(1 + (i
Β· π΄))) β (i
Β· (arctanβπ΄)))) |
107 | 23, 29, 105 | divrec2d 11942 |
. . . . . . . 8
β’ (π΄ β dom arctan β
((logβ(1 + (π΄β2))) / 2) = ((1 / 2) Β·
(logβ(1 + (π΄β2))))) |
108 | 103, 106,
107 | 3eqtr3d 2785 |
. . . . . . 7
β’ (π΄ β dom arctan β
((logβ(1 + (i Β· π΄))) β (i Β· (arctanβπ΄))) = ((1 / 2) Β·
(logβ(1 + (π΄β2))))) |
109 | 35, 4, 25 | subaddd 11537 |
. . . . . . 7
β’ (π΄ β dom arctan β
(((logβ(1 + (i Β· π΄))) β (i Β· (arctanβπ΄))) = ((1 / 2) Β·
(logβ(1 + (π΄β2)))) β ((i Β·
(arctanβπ΄)) + ((1 /
2) Β· (logβ(1 + (π΄β2))))) = (logβ(1 + (i Β·
π΄))))) |
110 | 108, 109 | mpbid 231 |
. . . . . 6
β’ (π΄ β dom arctan β ((i
Β· (arctanβπ΄))
+ ((1 / 2) Β· (logβ(1 + (π΄β2))))) = (logβ(1 + (i Β·
π΄)))) |
111 | 110 | fveq2d 6851 |
. . . . 5
β’ (π΄ β dom arctan β
(expβ((i Β· (arctanβπ΄)) + ((1 / 2) Β· (logβ(1 +
(π΄β2)))))) =
(expβ(logβ(1 + (i Β· π΄))))) |
112 | 27, 111 | eqtr3d 2779 |
. . . 4
β’ (π΄ β dom arctan β
((expβ(i Β· (arctanβπ΄))) Β· (expβ((1 / 2) Β·
(logβ(1 + (π΄β2)))))) = (expβ(logβ(1 +
(i Β· π΄))))) |
113 | 22 | a1i 11 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 /
2) β β) |
114 | 12, 16, 113 | cxpefd 26083 |
. . . . . 6
β’ (π΄ β dom arctan β ((1 +
(π΄β2))βπ(1 / 2))
= (expβ((1 / 2) Β· (logβ(1 + (π΄β2)))))) |
115 | | cxpsqrt 26074 |
. . . . . . 7
β’ ((1 +
(π΄β2)) β β
β ((1 + (π΄β2))βπ(1 / 2))
= (ββ(1 + (π΄β2)))) |
116 | 12, 115 | syl 17 |
. . . . . 6
β’ (π΄ β dom arctan β ((1 +
(π΄β2))βπ(1 / 2))
= (ββ(1 + (π΄β2)))) |
117 | 114, 116 | eqtr3d 2779 |
. . . . 5
β’ (π΄ β dom arctan β
(expβ((1 / 2) Β· (logβ(1 + (π΄β2))))) = (ββ(1 + (π΄β2)))) |
118 | 117 | oveq2d 7378 |
. . . 4
β’ (π΄ β dom arctan β
((expβ(i Β· (arctanβπ΄))) Β· (expβ((1 / 2) Β·
(logβ(1 + (π΄β2)))))) = ((expβ(i Β·
(arctanβπ΄))) Β·
(ββ(1 + (π΄β2))))) |
119 | 112, 118,
79 | 3eqtr3d 2785 |
. . 3
β’ (π΄ β dom arctan β
((expβ(i Β· (arctanβπ΄))) Β· (ββ(1 + (π΄β2)))) = (1 + (i Β·
π΄))) |
120 | 119 | oveq1d 7377 |
. 2
β’ (π΄ β dom arctan β
(((expβ(i Β· (arctanβπ΄))) Β· (ββ(1 + (π΄β2)))) / (ββ(1
+ (π΄β2)))) = ((1 + (i
Β· π΄)) /
(ββ(1 + (π΄β2))))) |
121 | 21, 120 | eqtr3d 2779 |
1
β’ (π΄ β dom arctan β
(expβ(i Β· (arctanβπ΄))) = ((1 + (i Β· π΄)) / (ββ(1 + (π΄β2))))) |