Step | Hyp | Ref
| Expression |
1 | | asincl 26239 |
. . 3
β’ (π΄ β β β
(arcsinβπ΄) β
β) |
2 | | cosval 16012 |
. . 3
β’
((arcsinβπ΄)
β β β (cosβ(arcsinβπ΄)) = (((expβ(i Β·
(arcsinβπ΄))) +
(expβ(-i Β· (arcsinβπ΄)))) / 2)) |
3 | 1, 2 | syl 17 |
. 2
β’ (π΄ β β β
(cosβ(arcsinβπ΄)) = (((expβ(i Β·
(arcsinβπ΄))) +
(expβ(-i Β· (arcsinβπ΄)))) / 2)) |
4 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
5 | | sqcl 14030 |
. . . . . . 7
β’ (π΄ β β β (π΄β2) β
β) |
6 | | subcl 11407 |
. . . . . . 7
β’ ((1
β β β§ (π΄β2) β β) β (1 β
(π΄β2)) β
β) |
7 | 4, 5, 6 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (1
β (π΄β2)) β
β) |
8 | 7 | sqrtcld 15329 |
. . . . 5
β’ (π΄ β β β
(ββ(1 β (π΄β2))) β β) |
9 | | ax-icn 11117 |
. . . . . 6
β’ i β
β |
10 | | mulcl 11142 |
. . . . . 6
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
11 | 9, 10 | mpan 689 |
. . . . 5
β’ (π΄ β β β (i
Β· π΄) β
β) |
12 | 8, 11, 8 | ppncand 11559 |
. . . 4
β’ (π΄ β β β
(((ββ(1 β (π΄β2))) + (i Β· π΄)) + ((ββ(1 β (π΄β2))) β (i Β·
π΄))) = ((ββ(1
β (π΄β2))) +
(ββ(1 β (π΄β2))))) |
13 | | efiasin 26254 |
. . . . . 6
β’ (π΄ β β β
(expβ(i Β· (arcsinβπ΄))) = ((i Β· π΄) + (ββ(1 β (π΄β2))))) |
14 | 11, 8, 13 | comraddd 11376 |
. . . . 5
β’ (π΄ β β β
(expβ(i Β· (arcsinβπ΄))) = ((ββ(1 β (π΄β2))) + (i Β· π΄))) |
15 | | mulneg12 11600 |
. . . . . . . . . 10
β’ ((i
β β β§ (arcsinβπ΄) β β) β (-i Β·
(arcsinβπ΄)) = (i
Β· -(arcsinβπ΄))) |
16 | 9, 1, 15 | sylancr 588 |
. . . . . . . . 9
β’ (π΄ β β β (-i
Β· (arcsinβπ΄))
= (i Β· -(arcsinβπ΄))) |
17 | | asinneg 26252 |
. . . . . . . . . 10
β’ (π΄ β β β
(arcsinβ-π΄) =
-(arcsinβπ΄)) |
18 | 17 | oveq2d 7378 |
. . . . . . . . 9
β’ (π΄ β β β (i
Β· (arcsinβ-π΄))
= (i Β· -(arcsinβπ΄))) |
19 | 16, 18 | eqtr4d 2780 |
. . . . . . . 8
β’ (π΄ β β β (-i
Β· (arcsinβπ΄))
= (i Β· (arcsinβ-π΄))) |
20 | 19 | fveq2d 6851 |
. . . . . . 7
β’ (π΄ β β β
(expβ(-i Β· (arcsinβπ΄))) = (expβ(i Β·
(arcsinβ-π΄)))) |
21 | | negcl 11408 |
. . . . . . . 8
β’ (π΄ β β β -π΄ β
β) |
22 | | efiasin 26254 |
. . . . . . . 8
β’ (-π΄ β β β
(expβ(i Β· (arcsinβ-π΄))) = ((i Β· -π΄) + (ββ(1 β (-π΄β2))))) |
23 | 21, 22 | syl 17 |
. . . . . . 7
β’ (π΄ β β β
(expβ(i Β· (arcsinβ-π΄))) = ((i Β· -π΄) + (ββ(1 β (-π΄β2))))) |
24 | | mulneg2 11599 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (i Β· -π΄) = -(i Β· π΄)) |
25 | 9, 24 | mpan 689 |
. . . . . . . 8
β’ (π΄ β β β (i
Β· -π΄) = -(i Β·
π΄)) |
26 | | sqneg 14028 |
. . . . . . . . . 10
β’ (π΄ β β β (-π΄β2) = (π΄β2)) |
27 | 26 | oveq2d 7378 |
. . . . . . . . 9
β’ (π΄ β β β (1
β (-π΄β2)) = (1
β (π΄β2))) |
28 | 27 | fveq2d 6851 |
. . . . . . . 8
β’ (π΄ β β β
(ββ(1 β (-π΄β2))) = (ββ(1 β
(π΄β2)))) |
29 | 25, 28 | oveq12d 7380 |
. . . . . . 7
β’ (π΄ β β β ((i
Β· -π΄) +
(ββ(1 β (-π΄β2)))) = (-(i Β· π΄) + (ββ(1 β
(π΄β2))))) |
30 | 20, 23, 29 | 3eqtrd 2781 |
. . . . . 6
β’ (π΄ β β β
(expβ(-i Β· (arcsinβπ΄))) = (-(i Β· π΄) + (ββ(1 β (π΄β2))))) |
31 | 11 | negcld 11506 |
. . . . . . 7
β’ (π΄ β β β -(i
Β· π΄) β
β) |
32 | 31, 8 | addcomd 11364 |
. . . . . 6
β’ (π΄ β β β (-(i
Β· π΄) +
(ββ(1 β (π΄β2)))) = ((ββ(1 β
(π΄β2))) + -(i Β·
π΄))) |
33 | 8, 11 | negsubd 11525 |
. . . . . 6
β’ (π΄ β β β
((ββ(1 β (π΄β2))) + -(i Β· π΄)) = ((ββ(1 β (π΄β2))) β (i Β·
π΄))) |
34 | 30, 32, 33 | 3eqtrd 2781 |
. . . . 5
β’ (π΄ β β β
(expβ(-i Β· (arcsinβπ΄))) = ((ββ(1 β (π΄β2))) β (i Β·
π΄))) |
35 | 14, 34 | oveq12d 7380 |
. . . 4
β’ (π΄ β β β
((expβ(i Β· (arcsinβπ΄))) + (expβ(-i Β·
(arcsinβπ΄)))) =
(((ββ(1 β (π΄β2))) + (i Β· π΄)) + ((ββ(1 β (π΄β2))) β (i Β·
π΄)))) |
36 | 8 | 2timesd 12403 |
. . . 4
β’ (π΄ β β β (2
Β· (ββ(1 β (π΄β2)))) = ((ββ(1 β
(π΄β2))) +
(ββ(1 β (π΄β2))))) |
37 | 12, 35, 36 | 3eqtr4d 2787 |
. . 3
β’ (π΄ β β β
((expβ(i Β· (arcsinβπ΄))) + (expβ(-i Β·
(arcsinβπ΄)))) = (2
Β· (ββ(1 β (π΄β2))))) |
38 | 37 | oveq1d 7377 |
. 2
β’ (π΄ β β β
(((expβ(i Β· (arcsinβπ΄))) + (expβ(-i Β·
(arcsinβπ΄)))) / 2) =
((2 Β· (ββ(1 β (π΄β2)))) / 2)) |
39 | | 2cnd 12238 |
. . 3
β’ (π΄ β β β 2 β
β) |
40 | | 2ne0 12264 |
. . . 4
β’ 2 β
0 |
41 | 40 | a1i 11 |
. . 3
β’ (π΄ β β β 2 β
0) |
42 | 8, 39, 41 | divcan3d 11943 |
. 2
β’ (π΄ β β β ((2
Β· (ββ(1 β (π΄β2)))) / 2) = (ββ(1 β
(π΄β2)))) |
43 | 3, 38, 42 | 3eqtrd 2781 |
1
β’ (π΄ β β β
(cosβ(arcsinβπ΄)) = (ββ(1 β (π΄β2)))) |