Step | Hyp | Ref
| Expression |
1 | | negcl 11406 |
. . 3
β’ (π΄ β β β -π΄ β
β) |
2 | | sinval 16009 |
. . 3
β’ (-π΄ β β β
(sinβ-π΄) =
(((expβ(i Β· -π΄)) β (expβ(-i Β· -π΄))) / (2 Β·
i))) |
3 | 1, 2 | syl 17 |
. 2
β’ (π΄ β β β
(sinβ-π΄) =
(((expβ(i Β· -π΄)) β (expβ(-i Β· -π΄))) / (2 Β·
i))) |
4 | | sinval 16009 |
. . . . 5
β’ (π΄ β β β
(sinβπ΄) =
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
5 | 4 | negeqd 11400 |
. . . 4
β’ (π΄ β β β
-(sinβπ΄) =
-(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
6 | | ax-icn 11115 |
. . . . . . . 8
β’ i β
β |
7 | | mulcl 11140 |
. . . . . . . 8
β’ ((i
β β β§ π΄
β β) β (i Β· π΄) β β) |
8 | 6, 7 | mpan 689 |
. . . . . . 7
β’ (π΄ β β β (i
Β· π΄) β
β) |
9 | | efcl 15970 |
. . . . . . 7
β’ ((i
Β· π΄) β β
β (expβ(i Β· π΄)) β β) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π΄ β β β
(expβ(i Β· π΄))
β β) |
11 | | negicn 11407 |
. . . . . . . 8
β’ -i β
β |
12 | | mulcl 11140 |
. . . . . . . 8
β’ ((-i
β β β§ π΄
β β) β (-i Β· π΄) β β) |
13 | 11, 12 | mpan 689 |
. . . . . . 7
β’ (π΄ β β β (-i
Β· π΄) β
β) |
14 | | efcl 15970 |
. . . . . . 7
β’ ((-i
Β· π΄) β β
β (expβ(-i Β· π΄)) β β) |
15 | 13, 14 | syl 17 |
. . . . . 6
β’ (π΄ β β β
(expβ(-i Β· π΄))
β β) |
16 | 10, 15 | subcld 11517 |
. . . . 5
β’ (π΄ β β β
((expβ(i Β· π΄))
β (expβ(-i Β· π΄))) β β) |
17 | | 2mulicn 12381 |
. . . . . 6
β’ (2
Β· i) β β |
18 | | 2muline0 12382 |
. . . . . 6
β’ (2
Β· i) β 0 |
19 | | divneg 11852 |
. . . . . 6
β’
((((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) β β β§ (2
Β· i) β β β§ (2 Β· i) β 0) β -(((expβ(i
Β· π΄)) β
(expβ(-i Β· π΄))) / (2 Β· i)) = (-((expβ(i
Β· π΄)) β
(expβ(-i Β· π΄))) / (2 Β· i))) |
20 | 17, 18, 19 | mp3an23 1454 |
. . . . 5
β’
(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) β β β
-(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) =
(-((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
21 | 16, 20 | syl 17 |
. . . 4
β’ (π΄ β β β
-(((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β· i)) =
(-((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
22 | 5, 21 | eqtrd 2773 |
. . 3
β’ (π΄ β β β
-(sinβπ΄) =
(-((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
23 | | mulneg12 11598 |
. . . . . . . . 9
β’ ((i
β β β§ π΄
β β) β (-i Β· π΄) = (i Β· -π΄)) |
24 | 6, 23 | mpan 689 |
. . . . . . . 8
β’ (π΄ β β β (-i
Β· π΄) = (i Β·
-π΄)) |
25 | 24 | eqcomd 2739 |
. . . . . . 7
β’ (π΄ β β β (i
Β· -π΄) = (-i Β·
π΄)) |
26 | 25 | fveq2d 6847 |
. . . . . 6
β’ (π΄ β β β
(expβ(i Β· -π΄))
= (expβ(-i Β· π΄))) |
27 | | mul2neg 11599 |
. . . . . . . 8
β’ ((i
β β β§ π΄
β β) β (-i Β· -π΄) = (i Β· π΄)) |
28 | 6, 27 | mpan 689 |
. . . . . . 7
β’ (π΄ β β β (-i
Β· -π΄) = (i Β·
π΄)) |
29 | 28 | fveq2d 6847 |
. . . . . 6
β’ (π΄ β β β
(expβ(-i Β· -π΄)) = (expβ(i Β· π΄))) |
30 | 26, 29 | oveq12d 7376 |
. . . . 5
β’ (π΄ β β β
((expβ(i Β· -π΄)) β (expβ(-i Β· -π΄))) = ((expβ(-i Β·
π΄)) β (expβ(i
Β· π΄)))) |
31 | 10, 15 | negsubdi2d 11533 |
. . . . 5
β’ (π΄ β β β
-((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) = ((expβ(-i Β·
π΄)) β (expβ(i
Β· π΄)))) |
32 | 30, 31 | eqtr4d 2776 |
. . . 4
β’ (π΄ β β β
((expβ(i Β· -π΄)) β (expβ(-i Β· -π΄))) = -((expβ(i Β·
π΄)) β (expβ(-i
Β· π΄)))) |
33 | 32 | oveq1d 7373 |
. . 3
β’ (π΄ β β β
(((expβ(i Β· -π΄)) β (expβ(-i Β· -π΄))) / (2 Β· i)) =
(-((expβ(i Β· π΄)) β (expβ(-i Β· π΄))) / (2 Β·
i))) |
34 | 22, 33 | eqtr4d 2776 |
. 2
β’ (π΄ β β β
-(sinβπ΄) =
(((expβ(i Β· -π΄)) β (expβ(-i Β· -π΄))) / (2 Β·
i))) |
35 | 3, 34 | eqtr4d 2776 |
1
β’ (π΄ β β β
(sinβ-π΄) =
-(sinβπ΄)) |