Step | Hyp | Ref
| Expression |
1 | | ixi 11789 |
. . . . . . . . 9
β’ (i
Β· i) = -1 |
2 | 1 | oveq1i 7368 |
. . . . . . . 8
β’ ((i
Β· i) Β· π΄) =
(-1 Β· π΄) |
3 | | ax-icn 11115 |
. . . . . . . . 9
β’ i β
β |
4 | | mulass 11144 |
. . . . . . . . 9
β’ ((i
β β β§ i β β β§ π΄ β β) β ((i Β· i)
Β· π΄) = (i Β·
(i Β· π΄))) |
5 | 3, 3, 4 | mp3an12 1452 |
. . . . . . . 8
β’ (π΄ β β β ((i
Β· i) Β· π΄) =
(i Β· (i Β· π΄))) |
6 | | mulm1 11601 |
. . . . . . . 8
β’ (π΄ β β β (-1
Β· π΄) = -π΄) |
7 | 2, 5, 6 | 3eqtr3a 2797 |
. . . . . . 7
β’ (π΄ β β β (i
Β· (i Β· π΄)) =
-π΄) |
8 | 7 | fveq2d 6847 |
. . . . . 6
β’ (π΄ β β β
(expβ(i Β· (i Β· π΄))) = (expβ-π΄)) |
9 | 3, 3 | mulneg1i 11606 |
. . . . . . . . . 10
β’ (-i
Β· i) = -(i Β· i) |
10 | 1 | negeqi 11399 |
. . . . . . . . . . 11
β’ -(i
Β· i) = --1 |
11 | | negneg1e1 12276 |
. . . . . . . . . . 11
β’ --1 =
1 |
12 | 10, 11 | eqtri 2761 |
. . . . . . . . . 10
β’ -(i
Β· i) = 1 |
13 | 9, 12 | eqtri 2761 |
. . . . . . . . 9
β’ (-i
Β· i) = 1 |
14 | 13 | oveq1i 7368 |
. . . . . . . 8
β’ ((-i
Β· i) Β· π΄) =
(1 Β· π΄) |
15 | | negicn 11407 |
. . . . . . . . 9
β’ -i β
β |
16 | | mulass 11144 |
. . . . . . . . 9
β’ ((-i
β β β§ i β β β§ π΄ β β) β ((-i Β· i)
Β· π΄) = (-i Β·
(i Β· π΄))) |
17 | 15, 3, 16 | mp3an12 1452 |
. . . . . . . 8
β’ (π΄ β β β ((-i
Β· i) Β· π΄) =
(-i Β· (i Β· π΄))) |
18 | | mulid2 11159 |
. . . . . . . 8
β’ (π΄ β β β (1
Β· π΄) = π΄) |
19 | 14, 17, 18 | 3eqtr3a 2797 |
. . . . . . 7
β’ (π΄ β β β (-i
Β· (i Β· π΄)) =
π΄) |
20 | 19 | fveq2d 6847 |
. . . . . 6
β’ (π΄ β β β
(expβ(-i Β· (i Β· π΄))) = (expβπ΄)) |
21 | 8, 20 | oveq12d 7376 |
. . . . 5
β’ (π΄ β β β
((expβ(i Β· (i Β· π΄))) β (expβ(-i Β· (i
Β· π΄)))) =
((expβ-π΄) β
(expβπ΄))) |
22 | 21 | oveq1d 7373 |
. . . 4
β’ (π΄ β β β
(((expβ(i Β· (i Β· π΄))) β (expβ(-i Β· (i
Β· π΄)))) / (2
Β· i)) = (((expβ-π΄) β (expβπ΄)) / (2 Β· i))) |
23 | | mulcl 11140 |
. . . . . 6
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
24 | 3, 23 | mpan 689 |
. . . . 5
β’ (π΄ β β β (i
Β· π΄) β
β) |
25 | | sinval 16009 |
. . . . 5
β’ ((i
Β· π΄) β β
β (sinβ(i Β· π΄)) = (((expβ(i Β· (i Β·
π΄))) β (expβ(-i
Β· (i Β· π΄))))
/ (2 Β· i))) |
26 | 24, 25 | syl 17 |
. . . 4
β’ (π΄ β β β
(sinβ(i Β· π΄))
= (((expβ(i Β· (i Β· π΄))) β (expβ(-i Β· (i
Β· π΄)))) / (2
Β· i))) |
27 | | irec 14111 |
. . . . . . . 8
β’ (1 / i) =
-i |
28 | 27 | negeqi 11399 |
. . . . . . 7
β’ -(1 / i)
= --i |
29 | 3 | negnegi 11476 |
. . . . . . 7
β’ --i =
i |
30 | 28, 29 | eqtri 2761 |
. . . . . 6
β’ -(1 / i)
= i |
31 | 30 | oveq1i 7368 |
. . . . 5
β’ (-(1 / i)
Β· (((expβπ΄)
β (expβ-π΄)) /
2)) = (i Β· (((expβπ΄) β (expβ-π΄)) / 2)) |
32 | | ine0 11595 |
. . . . . . . 8
β’ i β
0 |
33 | 3, 32 | reccli 11890 |
. . . . . . 7
β’ (1 / i)
β β |
34 | | efcl 15970 |
. . . . . . . . 9
β’ (π΄ β β β
(expβπ΄) β
β) |
35 | | negcl 11406 |
. . . . . . . . . 10
β’ (π΄ β β β -π΄ β
β) |
36 | | efcl 15970 |
. . . . . . . . . 10
β’ (-π΄ β β β
(expβ-π΄) β
β) |
37 | 35, 36 | syl 17 |
. . . . . . . . 9
β’ (π΄ β β β
(expβ-π΄) β
β) |
38 | 34, 37 | subcld 11517 |
. . . . . . . 8
β’ (π΄ β β β
((expβπ΄) β
(expβ-π΄)) β
β) |
39 | 38 | halfcld 12403 |
. . . . . . 7
β’ (π΄ β β β
(((expβπ΄) β
(expβ-π΄)) / 2) β
β) |
40 | | mulneg12 11598 |
. . . . . . 7
β’ (((1 / i)
β β β§ (((expβπ΄) β (expβ-π΄)) / 2) β β) β (-(1 / i)
Β· (((expβπ΄)
β (expβ-π΄)) /
2)) = ((1 / i) Β· -(((expβπ΄) β (expβ-π΄)) / 2))) |
41 | 33, 39, 40 | sylancr 588 |
. . . . . 6
β’ (π΄ β β β (-(1 / i)
Β· (((expβπ΄)
β (expβ-π΄)) /
2)) = ((1 / i) Β· -(((expβπ΄) β (expβ-π΄)) / 2))) |
42 | | 2cnd 12236 |
. . . . . . . . . 10
β’ (π΄ β β β 2 β
β) |
43 | | 2ne0 12262 |
. . . . . . . . . . 11
β’ 2 β
0 |
44 | 43 | a1i 11 |
. . . . . . . . . 10
β’ (π΄ β β β 2 β
0) |
45 | 38, 42, 44 | divnegd 11949 |
. . . . . . . . 9
β’ (π΄ β β β
-(((expβπ΄) β
(expβ-π΄)) / 2) =
(-((expβπ΄) β
(expβ-π΄)) /
2)) |
46 | 34, 37 | negsubdi2d 11533 |
. . . . . . . . . 10
β’ (π΄ β β β
-((expβπ΄) β
(expβ-π΄)) =
((expβ-π΄) β
(expβπ΄))) |
47 | 46 | oveq1d 7373 |
. . . . . . . . 9
β’ (π΄ β β β
(-((expβπ΄) β
(expβ-π΄)) / 2) =
(((expβ-π΄) β
(expβπ΄)) /
2)) |
48 | 45, 47 | eqtrd 2773 |
. . . . . . . 8
β’ (π΄ β β β
-(((expβπ΄) β
(expβ-π΄)) / 2) =
(((expβ-π΄) β
(expβπ΄)) /
2)) |
49 | 48 | oveq2d 7374 |
. . . . . . 7
β’ (π΄ β β β ((1 / i)
Β· -(((expβπ΄)
β (expβ-π΄)) /
2)) = ((1 / i) Β· (((expβ-π΄) β (expβπ΄)) / 2))) |
50 | 37, 34 | subcld 11517 |
. . . . . . . . 9
β’ (π΄ β β β
((expβ-π΄) β
(expβπ΄)) β
β) |
51 | 50 | halfcld 12403 |
. . . . . . . 8
β’ (π΄ β β β
(((expβ-π΄) β
(expβπ΄)) / 2) β
β) |
52 | 3 | a1i 11 |
. . . . . . . 8
β’ (π΄ β β β i β
β) |
53 | 32 | a1i 11 |
. . . . . . . 8
β’ (π΄ β β β i β
0) |
54 | 51, 52, 53 | divrec2d 11940 |
. . . . . . 7
β’ (π΄ β β β
((((expβ-π΄) β
(expβπ΄)) / 2) / i) =
((1 / i) Β· (((expβ-π΄) β (expβπ΄)) / 2))) |
55 | 50, 42, 52, 44, 53 | divdiv1d 11967 |
. . . . . . 7
β’ (π΄ β β β
((((expβ-π΄) β
(expβπ΄)) / 2) / i) =
(((expβ-π΄) β
(expβπ΄)) / (2
Β· i))) |
56 | 49, 54, 55 | 3eqtr2d 2779 |
. . . . . 6
β’ (π΄ β β β ((1 / i)
Β· -(((expβπ΄)
β (expβ-π΄)) /
2)) = (((expβ-π΄)
β (expβπ΄)) / (2
Β· i))) |
57 | 41, 56 | eqtrd 2773 |
. . . . 5
β’ (π΄ β β β (-(1 / i)
Β· (((expβπ΄)
β (expβ-π΄)) /
2)) = (((expβ-π΄)
β (expβπ΄)) / (2
Β· i))) |
58 | 31, 57 | eqtr3id 2787 |
. . . 4
β’ (π΄ β β β (i
Β· (((expβπ΄)
β (expβ-π΄)) /
2)) = (((expβ-π΄)
β (expβπ΄)) / (2
Β· i))) |
59 | 22, 26, 58 | 3eqtr4d 2783 |
. . 3
β’ (π΄ β β β
(sinβ(i Β· π΄))
= (i Β· (((expβπ΄) β (expβ-π΄)) / 2))) |
60 | 59 | oveq1d 7373 |
. 2
β’ (π΄ β β β
((sinβ(i Β· π΄))
/ i) = ((i Β· (((expβπ΄) β (expβ-π΄)) / 2)) / i)) |
61 | 39, 52, 53 | divcan3d 11941 |
. 2
β’ (π΄ β β β ((i
Β· (((expβπ΄)
β (expβ-π΄)) /
2)) / i) = (((expβπ΄)
β (expβ-π΄)) /
2)) |
62 | 60, 61 | eqtrd 2773 |
1
β’ (π΄ β β β
((sinβ(i Β· π΄))
/ i) = (((expβπ΄)
β (expβ-π΄)) /
2)) |