Step | Hyp | Ref
| Expression |
1 | | atancl 26247 |
. . 3
β’ (π΄ β dom arctan β
(arctanβπ΄) β
β) |
2 | | cosval 16012 |
. . 3
β’
((arctanβπ΄)
β β β (cosβ(arctanβπ΄)) = (((expβ(i Β·
(arctanβπ΄))) +
(expβ(-i Β· (arctanβπ΄)))) / 2)) |
3 | 1, 2 | syl 17 |
. 2
β’ (π΄ β dom arctan β
(cosβ(arctanβπ΄)) = (((expβ(i Β·
(arctanβπ΄))) +
(expβ(-i Β· (arctanβπ΄)))) / 2)) |
4 | | efiatan2 26283 |
. . . . 5
β’ (π΄ β dom arctan β
(expβ(i Β· (arctanβπ΄))) = ((1 + (i Β· π΄)) / (ββ(1 + (π΄β2))))) |
5 | | ax-icn 11117 |
. . . . . . . . 9
β’ i β
β |
6 | | mulneg12 11600 |
. . . . . . . . 9
β’ ((i
β β β§ (arctanβπ΄) β β) β (-i Β·
(arctanβπ΄)) = (i
Β· -(arctanβπ΄))) |
7 | 5, 1, 6 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β dom arctan β (-i
Β· (arctanβπ΄))
= (i Β· -(arctanβπ΄))) |
8 | | atanneg 26273 |
. . . . . . . . 9
β’ (π΄ β dom arctan β
(arctanβ-π΄) =
-(arctanβπ΄)) |
9 | 8 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β dom arctan β (i
Β· (arctanβ-π΄))
= (i Β· -(arctanβπ΄))) |
10 | 7, 9 | eqtr4d 2780 |
. . . . . . 7
β’ (π΄ β dom arctan β (-i
Β· (arctanβπ΄))
= (i Β· (arctanβ-π΄))) |
11 | 10 | fveq2d 6851 |
. . . . . 6
β’ (π΄ β dom arctan β
(expβ(-i Β· (arctanβπ΄))) = (expβ(i Β·
(arctanβ-π΄)))) |
12 | | atandmneg 26272 |
. . . . . . 7
β’ (π΄ β dom arctan β -π΄ β dom
arctan) |
13 | | efiatan2 26283 |
. . . . . . 7
β’ (-π΄ β dom arctan β
(expβ(i Β· (arctanβ-π΄))) = ((1 + (i Β· -π΄)) / (ββ(1 + (-π΄β2))))) |
14 | 12, 13 | syl 17 |
. . . . . 6
β’ (π΄ β dom arctan β
(expβ(i Β· (arctanβ-π΄))) = ((1 + (i Β· -π΄)) / (ββ(1 + (-π΄β2))))) |
15 | | atandm4 26245 |
. . . . . . . . . . 11
β’ (π΄ β dom arctan β (π΄ β β β§ (1 +
(π΄β2)) β
0)) |
16 | 15 | simplbi 499 |
. . . . . . . . . 10
β’ (π΄ β dom arctan β π΄ β
β) |
17 | | mulneg2 11599 |
. . . . . . . . . 10
β’ ((i
β β β§ π΄
β β) β (i Β· -π΄) = -(i Β· π΄)) |
18 | 5, 16, 17 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (i
Β· -π΄) = -(i Β·
π΄)) |
19 | 18 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β dom arctan β (1 +
(i Β· -π΄)) = (1 + -(i
Β· π΄))) |
20 | | ax-1cn 11116 |
. . . . . . . . 9
β’ 1 β
β |
21 | | mulcl 11142 |
. . . . . . . . . 10
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
22 | 5, 16, 21 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β dom arctan β (i
Β· π΄) β
β) |
23 | | negsub 11456 |
. . . . . . . . 9
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + -(i Β·
π΄)) = (1 β (i
Β· π΄))) |
24 | 20, 22, 23 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β dom arctan β (1 +
-(i Β· π΄)) = (1
β (i Β· π΄))) |
25 | 19, 24 | eqtrd 2777 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 +
(i Β· -π΄)) = (1
β (i Β· π΄))) |
26 | | sqneg 14028 |
. . . . . . . . . 10
β’ (π΄ β β β (-π΄β2) = (π΄β2)) |
27 | 16, 26 | syl 17 |
. . . . . . . . 9
β’ (π΄ β dom arctan β
(-π΄β2) = (π΄β2)) |
28 | 27 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β dom arctan β (1 +
(-π΄β2)) = (1 + (π΄β2))) |
29 | 28 | fveq2d 6851 |
. . . . . . 7
β’ (π΄ β dom arctan β
(ββ(1 + (-π΄β2))) = (ββ(1 + (π΄β2)))) |
30 | 25, 29 | oveq12d 7380 |
. . . . . 6
β’ (π΄ β dom arctan β ((1 +
(i Β· -π΄)) /
(ββ(1 + (-π΄β2)))) = ((1 β (i Β· π΄)) / (ββ(1 + (π΄β2))))) |
31 | 11, 14, 30 | 3eqtrd 2781 |
. . . . 5
β’ (π΄ β dom arctan β
(expβ(-i Β· (arctanβπ΄))) = ((1 β (i Β· π΄)) / (ββ(1 + (π΄β2))))) |
32 | 4, 31 | oveq12d 7380 |
. . . 4
β’ (π΄ β dom arctan β
((expβ(i Β· (arctanβπ΄))) + (expβ(-i Β·
(arctanβπ΄)))) = (((1
+ (i Β· π΄)) /
(ββ(1 + (π΄β2)))) + ((1 β (i Β· π΄)) / (ββ(1 + (π΄β2)))))) |
33 | | addcl 11140 |
. . . . . 6
β’ ((1
β β β§ (i Β· π΄) β β) β (1 + (i Β·
π΄)) β
β) |
34 | 20, 22, 33 | sylancr 588 |
. . . . 5
β’ (π΄ β dom arctan β (1 +
(i Β· π΄)) β
β) |
35 | | subcl 11407 |
. . . . . 6
β’ ((1
β β β§ (i Β· π΄) β β) β (1 β (i
Β· π΄)) β
β) |
36 | 20, 22, 35 | sylancr 588 |
. . . . 5
β’ (π΄ β dom arctan β (1
β (i Β· π΄))
β β) |
37 | 16 | sqcld 14056 |
. . . . . . 7
β’ (π΄ β dom arctan β (π΄β2) β
β) |
38 | | addcl 11140 |
. . . . . . 7
β’ ((1
β β β§ (π΄β2) β β) β (1 + (π΄β2)) β
β) |
39 | 20, 37, 38 | sylancr 588 |
. . . . . 6
β’ (π΄ β dom arctan β (1 +
(π΄β2)) β
β) |
40 | 39 | sqrtcld 15329 |
. . . . 5
β’ (π΄ β dom arctan β
(ββ(1 + (π΄β2))) β β) |
41 | 39 | sqsqrtd 15331 |
. . . . . . 7
β’ (π΄ β dom arctan β
((ββ(1 + (π΄β2)))β2) = (1 + (π΄β2))) |
42 | 15 | simprbi 498 |
. . . . . . 7
β’ (π΄ β dom arctan β (1 +
(π΄β2)) β
0) |
43 | 41, 42 | eqnetrd 3012 |
. . . . . 6
β’ (π΄ β dom arctan β
((ββ(1 + (π΄β2)))β2) β 0) |
44 | | sqne0 14035 |
. . . . . . 7
β’
((ββ(1 + (π΄β2))) β β β
(((ββ(1 + (π΄β2)))β2) β 0 β
(ββ(1 + (π΄β2))) β 0)) |
45 | 40, 44 | syl 17 |
. . . . . 6
β’ (π΄ β dom arctan β
(((ββ(1 + (π΄β2)))β2) β 0 β
(ββ(1 + (π΄β2))) β 0)) |
46 | 43, 45 | mpbid 231 |
. . . . 5
β’ (π΄ β dom arctan β
(ββ(1 + (π΄β2))) β 0) |
47 | 34, 36, 40, 46 | divdird 11976 |
. . . 4
β’ (π΄ β dom arctan β (((1 +
(i Β· π΄)) + (1
β (i Β· π΄))) /
(ββ(1 + (π΄β2)))) = (((1 + (i Β· π΄)) / (ββ(1 + (π΄β2)))) + ((1 β (i
Β· π΄)) /
(ββ(1 + (π΄β2)))))) |
48 | 20 | a1i 11 |
. . . . . . 7
β’ (π΄ β dom arctan β 1
β β) |
49 | 48, 22, 48 | ppncand 11559 |
. . . . . 6
β’ (π΄ β dom arctan β ((1 +
(i Β· π΄)) + (1
β (i Β· π΄))) =
(1 + 1)) |
50 | | df-2 12223 |
. . . . . 6
β’ 2 = (1 +
1) |
51 | 49, 50 | eqtr4di 2795 |
. . . . 5
β’ (π΄ β dom arctan β ((1 +
(i Β· π΄)) + (1
β (i Β· π΄))) =
2) |
52 | 51 | oveq1d 7377 |
. . . 4
β’ (π΄ β dom arctan β (((1 +
(i Β· π΄)) + (1
β (i Β· π΄))) /
(ββ(1 + (π΄β2)))) = (2 / (ββ(1 +
(π΄β2))))) |
53 | 32, 47, 52 | 3eqtr2d 2783 |
. . 3
β’ (π΄ β dom arctan β
((expβ(i Β· (arctanβπ΄))) + (expβ(-i Β·
(arctanβπ΄)))) = (2 /
(ββ(1 + (π΄β2))))) |
54 | 53 | oveq1d 7377 |
. 2
β’ (π΄ β dom arctan β
(((expβ(i Β· (arctanβπ΄))) + (expβ(-i Β·
(arctanβπ΄)))) / 2) =
((2 / (ββ(1 + (π΄β2)))) / 2)) |
55 | | 2cnd 12238 |
. . . 4
β’ (π΄ β dom arctan β 2
β β) |
56 | | 2ne0 12264 |
. . . . 5
β’ 2 β
0 |
57 | 56 | a1i 11 |
. . . 4
β’ (π΄ β dom arctan β 2 β
0) |
58 | 55, 40, 55, 46, 57 | divdiv32d 11963 |
. . 3
β’ (π΄ β dom arctan β ((2 /
(ββ(1 + (π΄β2)))) / 2) = ((2 / 2) /
(ββ(1 + (π΄β2))))) |
59 | | 2div2e1 12301 |
. . . 4
β’ (2 / 2) =
1 |
60 | 59 | oveq1i 7372 |
. . 3
β’ ((2 / 2)
/ (ββ(1 + (π΄β2)))) = (1 / (ββ(1 +
(π΄β2)))) |
61 | 58, 60 | eqtrdi 2793 |
. 2
β’ (π΄ β dom arctan β ((2 /
(ββ(1 + (π΄β2)))) / 2) = (1 / (ββ(1 +
(π΄β2))))) |
62 | 3, 54, 61 | 3eqtrd 2781 |
1
β’ (π΄ β dom arctan β
(cosβ(arctanβπ΄)) = (1 / (ββ(1 + (π΄β2))))) |