Step | Hyp | Ref
| Expression |
1 | | asincl 26239 |
. . 3
β’ (π΄ β β β
(arcsinβπ΄) β
β) |
2 | | sinval 16011 |
. . 3
β’
((arcsinβπ΄)
β β β (sinβ(arcsinβπ΄)) = (((expβ(i Β·
(arcsinβπ΄))) β
(expβ(-i Β· (arcsinβπ΄)))) / (2 Β· i))) |
3 | 1, 2 | syl 17 |
. 2
β’ (π΄ β β β
(sinβ(arcsinβπ΄)) = (((expβ(i Β·
(arcsinβπ΄))) β
(expβ(-i Β· (arcsinβπ΄)))) / (2 Β· i))) |
4 | | ax-icn 11117 |
. . . . . 6
β’ i β
β |
5 | | mulcl 11142 |
. . . . . 6
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
6 | 4, 5 | mpan 689 |
. . . . 5
β’ (π΄ β β β (i
Β· π΄) β
β) |
7 | 6 | negcld 11506 |
. . . . 5
β’ (π΄ β β β -(i
Β· π΄) β
β) |
8 | | ax-1cn 11116 |
. . . . . . 7
β’ 1 β
β |
9 | | sqcl 14030 |
. . . . . . 7
β’ (π΄ β β β (π΄β2) β
β) |
10 | | subcl 11407 |
. . . . . . 7
β’ ((1
β β β§ (π΄β2) β β) β (1 β
(π΄β2)) β
β) |
11 | 8, 9, 10 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (1
β (π΄β2)) β
β) |
12 | 11 | sqrtcld 15329 |
. . . . 5
β’ (π΄ β β β
(ββ(1 β (π΄β2))) β β) |
13 | 6, 7, 12 | pnpcan2d 11557 |
. . . 4
β’ (π΄ β β β (((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β (-(i Β· π΄) + (ββ(1 β
(π΄β2))))) = ((i
Β· π΄) β -(i
Β· π΄))) |
14 | | efiasin 26254 |
. . . . 5
β’ (π΄ β β β
(expβ(i Β· (arcsinβπ΄))) = ((i Β· π΄) + (ββ(1 β (π΄β2))))) |
15 | | mulneg12 11600 |
. . . . . . . . 9
β’ ((i
β β β§ (arcsinβπ΄) β β) β (-i Β·
(arcsinβπ΄)) = (i
Β· -(arcsinβπ΄))) |
16 | 4, 1, 15 | sylancr 588 |
. . . . . . . 8
β’ (π΄ β β β (-i
Β· (arcsinβπ΄))
= (i Β· -(arcsinβπ΄))) |
17 | | asinneg 26252 |
. . . . . . . . 9
β’ (π΄ β β β
(arcsinβ-π΄) =
-(arcsinβπ΄)) |
18 | 17 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β β β (i
Β· (arcsinβ-π΄))
= (i Β· -(arcsinβπ΄))) |
19 | 16, 18 | eqtr4d 2780 |
. . . . . . 7
β’ (π΄ β β β (-i
Β· (arcsinβπ΄))
= (i Β· (arcsinβ-π΄))) |
20 | 19 | fveq2d 6851 |
. . . . . 6
β’ (π΄ β β β
(expβ(-i Β· (arcsinβπ΄))) = (expβ(i Β·
(arcsinβ-π΄)))) |
21 | | negcl 11408 |
. . . . . . 7
β’ (π΄ β β β -π΄ β
β) |
22 | | efiasin 26254 |
. . . . . . 7
β’ (-π΄ β β β
(expβ(i Β· (arcsinβ-π΄))) = ((i Β· -π΄) + (ββ(1 β (-π΄β2))))) |
23 | 21, 22 | syl 17 |
. . . . . 6
β’ (π΄ β β β
(expβ(i Β· (arcsinβ-π΄))) = ((i Β· -π΄) + (ββ(1 β (-π΄β2))))) |
24 | | mulneg2 11599 |
. . . . . . . 8
β’ ((i
β β β§ π΄
β β) β (i Β· -π΄) = -(i Β· π΄)) |
25 | 4, 24 | mpan 689 |
. . . . . . 7
β’ (π΄ β β β (i
Β· -π΄) = -(i Β·
π΄)) |
26 | | sqneg 14028 |
. . . . . . . . 9
β’ (π΄ β β β (-π΄β2) = (π΄β2)) |
27 | 26 | oveq2d 7378 |
. . . . . . . 8
β’ (π΄ β β β (1
β (-π΄β2)) = (1
β (π΄β2))) |
28 | 27 | fveq2d 6851 |
. . . . . . 7
β’ (π΄ β β β
(ββ(1 β (-π΄β2))) = (ββ(1 β
(π΄β2)))) |
29 | 25, 28 | oveq12d 7380 |
. . . . . 6
β’ (π΄ β β β ((i
Β· -π΄) +
(ββ(1 β (-π΄β2)))) = (-(i Β· π΄) + (ββ(1 β
(π΄β2))))) |
30 | 20, 23, 29 | 3eqtrd 2781 |
. . . . 5
β’ (π΄ β β β
(expβ(-i Β· (arcsinβπ΄))) = (-(i Β· π΄) + (ββ(1 β (π΄β2))))) |
31 | 14, 30 | oveq12d 7380 |
. . . 4
β’ (π΄ β β β
((expβ(i Β· (arcsinβπ΄))) β (expβ(-i Β·
(arcsinβπ΄)))) = (((i
Β· π΄) +
(ββ(1 β (π΄β2)))) β (-(i Β· π΄) + (ββ(1 β
(π΄β2)))))) |
32 | 6 | 2timesd 12403 |
. . . . 5
β’ (π΄ β β β (2
Β· (i Β· π΄)) =
((i Β· π΄) + (i
Β· π΄))) |
33 | | 2cn 12235 |
. . . . . 6
β’ 2 β
β |
34 | | mulass 11146 |
. . . . . 6
β’ ((2
β β β§ i β β β§ π΄ β β) β ((2 Β· i)
Β· π΄) = (2 Β·
(i Β· π΄))) |
35 | 33, 4, 34 | mp3an12 1452 |
. . . . 5
β’ (π΄ β β β ((2
Β· i) Β· π΄) =
(2 Β· (i Β· π΄))) |
36 | 6, 6 | subnegd 11526 |
. . . . 5
β’ (π΄ β β β ((i
Β· π΄) β -(i
Β· π΄)) = ((i Β·
π΄) + (i Β· π΄))) |
37 | 32, 35, 36 | 3eqtr4d 2787 |
. . . 4
β’ (π΄ β β β ((2
Β· i) Β· π΄) =
((i Β· π΄) β -(i
Β· π΄))) |
38 | 13, 31, 37 | 3eqtr4d 2787 |
. . 3
β’ (π΄ β β β
((expβ(i Β· (arcsinβπ΄))) β (expβ(-i Β·
(arcsinβπ΄)))) = ((2
Β· i) Β· π΄)) |
39 | | mulcl 11142 |
. . . . . . 7
β’ ((i
β β β§ (arcsinβπ΄) β β) β (i Β·
(arcsinβπ΄)) β
β) |
40 | 4, 1, 39 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (i
Β· (arcsinβπ΄))
β β) |
41 | | efcl 15972 |
. . . . . 6
β’ ((i
Β· (arcsinβπ΄))
β β β (expβ(i Β· (arcsinβπ΄))) β β) |
42 | 40, 41 | syl 17 |
. . . . 5
β’ (π΄ β β β
(expβ(i Β· (arcsinβπ΄))) β β) |
43 | | negicn 11409 |
. . . . . . 7
β’ -i β
β |
44 | | mulcl 11142 |
. . . . . . 7
β’ ((-i
β β β§ (arcsinβπ΄) β β) β (-i Β·
(arcsinβπ΄)) β
β) |
45 | 43, 1, 44 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (-i
Β· (arcsinβπ΄))
β β) |
46 | | efcl 15972 |
. . . . . 6
β’ ((-i
Β· (arcsinβπ΄))
β β β (expβ(-i Β· (arcsinβπ΄))) β β) |
47 | 45, 46 | syl 17 |
. . . . 5
β’ (π΄ β β β
(expβ(-i Β· (arcsinβπ΄))) β β) |
48 | 42, 47 | subcld 11519 |
. . . 4
β’ (π΄ β β β
((expβ(i Β· (arcsinβπ΄))) β (expβ(-i Β·
(arcsinβπ΄)))) β
β) |
49 | | id 22 |
. . . 4
β’ (π΄ β β β π΄ β
β) |
50 | | 2mulicn 12383 |
. . . . 5
β’ (2
Β· i) β β |
51 | 50 | a1i 11 |
. . . 4
β’ (π΄ β β β (2
Β· i) β β) |
52 | | 2muline0 12384 |
. . . . 5
β’ (2
Β· i) β 0 |
53 | 52 | a1i 11 |
. . . 4
β’ (π΄ β β β (2
Β· i) β 0) |
54 | 48, 49, 51, 53 | divmul2d 11971 |
. . 3
β’ (π΄ β β β
((((expβ(i Β· (arcsinβπ΄))) β (expβ(-i Β·
(arcsinβπ΄)))) / (2
Β· i)) = π΄ β
((expβ(i Β· (arcsinβπ΄))) β (expβ(-i Β·
(arcsinβπ΄)))) = ((2
Β· i) Β· π΄))) |
55 | 38, 54 | mpbird 257 |
. 2
β’ (π΄ β β β
(((expβ(i Β· (arcsinβπ΄))) β (expβ(-i Β·
(arcsinβπ΄)))) / (2
Β· i)) = π΄) |
56 | 3, 55 | eqtrd 2777 |
1
β’ (π΄ β β β
(sinβ(arcsinβπ΄)) = π΄) |