Step | Hyp | Ref
| Expression |
1 | | cnelprrecn 11202 |
. . . . . 6
β’ β
β {β, β} |
2 | 1 | a1i 11 |
. . . . 5
β’ (β€
β β β {β, β}) |
3 | | ax-icn 11168 |
. . . . . . . . . 10
β’ i β
β |
4 | 3 | a1i 11 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β i β β) |
5 | | simpr 485 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β π₯
β β) |
6 | 4, 5 | mulcld 11233 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β (i Β· π₯) β β) |
7 | | efcl 16025 |
. . . . . . . 8
β’ ((i
Β· π₯) β β
β (expβ(i Β· π₯)) β β) |
8 | 6, 7 | syl 17 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β (expβ(i Β· π₯)) β β) |
9 | | ine0 11648 |
. . . . . . . 8
β’ i β
0 |
10 | 9 | a1i 11 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β i β 0) |
11 | 8, 4, 10 | divcld 11989 |
. . . . . 6
β’
((β€ β§ π₯
β β) β ((expβ(i Β· π₯)) / i) β β) |
12 | | negicn 11460 |
. . . . . . . . . 10
β’ -i β
β |
13 | | mulcl 11193 |
. . . . . . . . . 10
β’ ((-i
β β β§ π₯
β β) β (-i Β· π₯) β β) |
14 | 12, 5, 13 | sylancr 587 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (-i Β· π₯) β β) |
15 | | efcl 16025 |
. . . . . . . . 9
β’ ((-i
Β· π₯) β β
β (expβ(-i Β· π₯)) β β) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β (expβ(-i Β· π₯)) β β) |
17 | 16, 4, 10 | divcld 11989 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β ((expβ(-i Β· π₯)) / i) β β) |
18 | 17 | negcld 11557 |
. . . . . 6
β’
((β€ β§ π₯
β β) β -((expβ(-i Β· π₯)) / i) β β) |
19 | 11, 18 | addcld 11232 |
. . . . 5
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) / i) + -((expβ(-i Β· π₯)) / i)) β
β) |
20 | 8, 16 | addcld 11232 |
. . . . 5
β’
((β€ β§ π₯
β β) β ((expβ(i Β· π₯)) + (expβ(-i Β· π₯))) β
β) |
21 | 8, 4 | mulcld 11233 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β ((expβ(i Β· π₯)) Β· i) β
β) |
22 | | efcl 16025 |
. . . . . . . . . 10
β’ (π¦ β β β
(expβπ¦) β
β) |
23 | 22 | adantl 482 |
. . . . . . . . 9
β’
((β€ β§ π¦
β β) β (expβπ¦) β β) |
24 | | 1cnd 11208 |
. . . . . . . . . . 11
β’
((β€ β§ π₯
β β) β 1 β β) |
25 | 2 | dvmptid 25473 |
. . . . . . . . . . 11
β’ (β€
β (β D (π₯ β
β β¦ π₯)) =
(π₯ β β β¦
1)) |
26 | 3 | a1i 11 |
. . . . . . . . . . 11
β’ (β€
β i β β) |
27 | 2, 5, 24, 25, 26 | dvmptcmul 25480 |
. . . . . . . . . 10
β’ (β€
β (β D (π₯ β
β β¦ (i Β· π₯))) = (π₯ β β β¦ (i Β·
1))) |
28 | 3 | mulridi 11217 |
. . . . . . . . . . 11
β’ (i
Β· 1) = i |
29 | 28 | mpteq2i 5253 |
. . . . . . . . . 10
β’ (π₯ β β β¦ (i
Β· 1)) = (π₯ β
β β¦ i) |
30 | 27, 29 | eqtrdi 2788 |
. . . . . . . . 9
β’ (β€
β (β D (π₯ β
β β¦ (i Β· π₯))) = (π₯ β β β¦ i)) |
31 | | eff 16024 |
. . . . . . . . . . . . 13
β’
exp:ββΆβ |
32 | 31 | a1i 11 |
. . . . . . . . . . . 12
β’ (β€
β exp:ββΆβ) |
33 | 32 | feqmptd 6960 |
. . . . . . . . . . 11
β’ (β€
β exp = (π¦ β
β β¦ (expβπ¦))) |
34 | 33 | oveq2d 7424 |
. . . . . . . . . 10
β’ (β€
β (β D exp) = (β D (π¦ β β β¦ (expβπ¦)))) |
35 | | dvef 25496 |
. . . . . . . . . . 11
β’ (β
D exp) = exp |
36 | 35, 33 | eqtrid 2784 |
. . . . . . . . . 10
β’ (β€
β (β D exp) = (π¦
β β β¦ (expβπ¦))) |
37 | 34, 36 | eqtr3d 2774 |
. . . . . . . . 9
β’ (β€
β (β D (π¦ β
β β¦ (expβπ¦))) = (π¦ β β β¦ (expβπ¦))) |
38 | | fveq2 6891 |
. . . . . . . . 9
β’ (π¦ = (i Β· π₯) β (expβπ¦) = (expβ(i Β· π₯))) |
39 | 2, 2, 6, 4, 23, 23, 30, 37, 38, 38 | dvmptco 25488 |
. . . . . . . 8
β’ (β€
β (β D (π₯ β
β β¦ (expβ(i Β· π₯)))) = (π₯ β β β¦ ((expβ(i
Β· π₯)) Β·
i))) |
40 | 9 | a1i 11 |
. . . . . . . 8
β’ (β€
β i β 0) |
41 | 2, 8, 21, 39, 26, 40 | dvmptdivc 25481 |
. . . . . . 7
β’ (β€
β (β D (π₯ β
β β¦ ((expβ(i Β· π₯)) / i))) = (π₯ β β β¦ (((expβ(i
Β· π₯)) Β· i) /
i))) |
42 | 8, 4, 10 | divcan4d 11995 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) Β· i) / i) = (expβ(i Β·
π₯))) |
43 | 42 | mpteq2dva 5248 |
. . . . . . 7
β’ (β€
β (π₯ β β
β¦ (((expβ(i Β· π₯)) Β· i) / i)) = (π₯ β β β¦ (expβ(i
Β· π₯)))) |
44 | 41, 43 | eqtrd 2772 |
. . . . . 6
β’ (β€
β (β D (π₯ β
β β¦ ((expβ(i Β· π₯)) / i))) = (π₯ β β β¦ (expβ(i
Β· π₯)))) |
45 | | mulcl 11193 |
. . . . . . . . . 10
β’
(((expβ(-i Β· π₯)) β β β§ -i β β)
β ((expβ(-i Β· π₯)) Β· -i) β
β) |
46 | 16, 12, 45 | sylancl 586 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β ((expβ(-i Β· π₯)) Β· -i) β
β) |
47 | 46, 4, 10 | divcld 11989 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β (((expβ(-i Β· π₯)) Β· -i) / i) β
β) |
48 | 12 | a1i 11 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β -i β β) |
49 | 12 | a1i 11 |
. . . . . . . . . . . 12
β’ (β€
β -i β β) |
50 | 2, 5, 24, 25, 49 | dvmptcmul 25480 |
. . . . . . . . . . 11
β’ (β€
β (β D (π₯ β
β β¦ (-i Β· π₯))) = (π₯ β β β¦ (-i Β·
1))) |
51 | 12 | mulridi 11217 |
. . . . . . . . . . . 12
β’ (-i
Β· 1) = -i |
52 | 51 | mpteq2i 5253 |
. . . . . . . . . . 11
β’ (π₯ β β β¦ (-i
Β· 1)) = (π₯ β
β β¦ -i) |
53 | 50, 52 | eqtrdi 2788 |
. . . . . . . . . 10
β’ (β€
β (β D (π₯ β
β β¦ (-i Β· π₯))) = (π₯ β β β¦ -i)) |
54 | | fveq2 6891 |
. . . . . . . . . 10
β’ (π¦ = (-i Β· π₯) β (expβπ¦) = (expβ(-i Β·
π₯))) |
55 | 2, 2, 14, 48, 23, 23, 53, 37, 54, 54 | dvmptco 25488 |
. . . . . . . . 9
β’ (β€
β (β D (π₯ β
β β¦ (expβ(-i Β· π₯)))) = (π₯ β β β¦ ((expβ(-i
Β· π₯)) Β·
-i))) |
56 | 2, 16, 46, 55, 26, 40 | dvmptdivc 25481 |
. . . . . . . 8
β’ (β€
β (β D (π₯ β
β β¦ ((expβ(-i Β· π₯)) / i))) = (π₯ β β β¦ (((expβ(-i
Β· π₯)) Β· -i) /
i))) |
57 | 2, 17, 47, 56 | dvmptneg 25482 |
. . . . . . 7
β’ (β€
β (β D (π₯ β
β β¦ -((expβ(-i Β· π₯)) / i))) = (π₯ β β β¦ -(((expβ(-i
Β· π₯)) Β· -i) /
i))) |
58 | 46, 4, 10 | divneg2d 12003 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β -(((expβ(-i Β· π₯)) Β· -i) / i) = (((expβ(-i
Β· π₯)) Β· -i) /
-i)) |
59 | 3, 9 | negne0i 11534 |
. . . . . . . . . . 11
β’ -i β
0 |
60 | 59 | a1i 11 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β -i β 0) |
61 | 16, 48, 60 | divcan4d 11995 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (((expβ(-i Β· π₯)) Β· -i) / -i) = (expβ(-i
Β· π₯))) |
62 | 58, 61 | eqtrd 2772 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β -(((expβ(-i Β· π₯)) Β· -i) / i) = (expβ(-i
Β· π₯))) |
63 | 62 | mpteq2dva 5248 |
. . . . . . 7
β’ (β€
β (π₯ β β
β¦ -(((expβ(-i Β· π₯)) Β· -i) / i)) = (π₯ β β β¦ (expβ(-i
Β· π₯)))) |
64 | 57, 63 | eqtrd 2772 |
. . . . . 6
β’ (β€
β (β D (π₯ β
β β¦ -((expβ(-i Β· π₯)) / i))) = (π₯ β β β¦ (expβ(-i
Β· π₯)))) |
65 | 2, 11, 8, 44, 18, 16, 64 | dvmptadd 25476 |
. . . . 5
β’ (β€
β (β D (π₯ β
β β¦ (((expβ(i Β· π₯)) / i) + -((expβ(-i Β· π₯)) / i)))) = (π₯ β β β¦ ((expβ(i
Β· π₯)) +
(expβ(-i Β· π₯))))) |
66 | | 2cnd 12289 |
. . . . 5
β’ (β€
β 2 β β) |
67 | | 2ne0 12315 |
. . . . . 6
β’ 2 β
0 |
68 | 67 | a1i 11 |
. . . . 5
β’ (β€
β 2 β 0) |
69 | 2, 19, 20, 65, 66, 68 | dvmptdivc 25481 |
. . . 4
β’ (β€
β (β D (π₯ β
β β¦ ((((expβ(i Β· π₯)) / i) + -((expβ(-i Β· π₯)) / i)) / 2))) = (π₯ β β β¦
(((expβ(i Β· π₯)) + (expβ(-i Β· π₯))) / 2))) |
70 | | df-sin 16012 |
. . . . . 6
β’ sin =
(π₯ β β β¦
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (2 Β·
i))) |
71 | 8, 16 | subcld 11570 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β ((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) β
β) |
72 | | 2cnd 12289 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β 2 β β) |
73 | 67 | a1i 11 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β 2 β 0) |
74 | 71, 4, 72, 10, 73 | divdiv1d 12020 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β ((((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) / 2) = (((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) / (i Β· 2))) |
75 | | 2cn 12286 |
. . . . . . . . . . 11
β’ 2 β
β |
76 | 3, 75 | mulcomi 11221 |
. . . . . . . . . 10
β’ (i
Β· 2) = (2 Β· i) |
77 | 76 | oveq2i 7419 |
. . . . . . . . 9
β’
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (i Β· 2)) =
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (2 Β·
i)) |
78 | 74, 77 | eqtrdi 2788 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β ((((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) / 2) = (((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) / (2 Β· i))) |
79 | 8, 16, 4, 10 | divsubdird 12028 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) = (((expβ(i
Β· π₯)) / i) β
((expβ(-i Β· π₯)) / i))) |
80 | 11, 17 | negsubd 11576 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) / i) + -((expβ(-i Β· π₯)) / i)) = (((expβ(i
Β· π₯)) / i) β
((expβ(-i Β· π₯)) / i))) |
81 | 79, 80 | eqtr4d 2775 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) = (((expβ(i
Β· π₯)) / i) +
-((expβ(-i Β· π₯)) / i))) |
82 | 81 | oveq1d 7423 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β ((((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) / 2) = ((((expβ(i
Β· π₯)) / i) +
-((expβ(-i Β· π₯)) / i)) / 2)) |
83 | 78, 82 | eqtr3d 2774 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (2 Β· i)) =
((((expβ(i Β· π₯)) / i) + -((expβ(-i Β· π₯)) / i)) / 2)) |
84 | 83 | mpteq2dva 5248 |
. . . . . 6
β’ (β€
β (π₯ β β
β¦ (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (2 Β· i))) = (π₯ β β β¦
((((expβ(i Β· π₯)) / i) + -((expβ(-i Β· π₯)) / i)) / 2))) |
85 | 70, 84 | eqtrid 2784 |
. . . . 5
β’ (β€
β sin = (π₯ β
β β¦ ((((expβ(i Β· π₯)) / i) + -((expβ(-i Β· π₯)) / i)) / 2))) |
86 | 85 | oveq2d 7424 |
. . . 4
β’ (β€
β (β D sin) = (β D (π₯ β β β¦ ((((expβ(i
Β· π₯)) / i) +
-((expβ(-i Β· π₯)) / i)) / 2)))) |
87 | | df-cos 16013 |
. . . . 5
β’ cos =
(π₯ β β β¦
(((expβ(i Β· π₯)) + (expβ(-i Β· π₯))) / 2)) |
88 | 87 | a1i 11 |
. . . 4
β’ (β€
β cos = (π₯ β
β β¦ (((expβ(i Β· π₯)) + (expβ(-i Β· π₯))) / 2))) |
89 | 69, 86, 88 | 3eqtr4d 2782 |
. . 3
β’ (β€
β (β D sin) = cos) |
90 | 21, 46 | addcld 11232 |
. . . . 5
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) Β· i) + ((expβ(-i Β·
π₯)) Β· -i)) β
β) |
91 | 2, 8, 21, 39, 16, 46, 55 | dvmptadd 25476 |
. . . . 5
β’ (β€
β (β D (π₯ β
β β¦ ((expβ(i Β· π₯)) + (expβ(-i Β· π₯))))) = (π₯ β β β¦ (((expβ(i
Β· π₯)) Β· i) +
((expβ(-i Β· π₯)) Β· -i)))) |
92 | 2, 20, 90, 91, 66, 68 | dvmptdivc 25481 |
. . . 4
β’ (β€
β (β D (π₯ β
β β¦ (((expβ(i Β· π₯)) + (expβ(-i Β· π₯))) / 2))) = (π₯ β β β¦ ((((expβ(i
Β· π₯)) Β· i) +
((expβ(-i Β· π₯)) Β· -i)) / 2))) |
93 | 88 | oveq2d 7424 |
. . . 4
β’ (β€
β (β D cos) = (β D (π₯ β β β¦ (((expβ(i
Β· π₯)) +
(expβ(-i Β· π₯))) / 2)))) |
94 | 71, 4, 10 | divcld 11989 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) β
β) |
95 | 94, 72, 73 | divnegd 12002 |
. . . . . 6
β’
((β€ β§ π₯
β β) β -((((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) / 2) =
(-(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) / 2)) |
96 | | sinval 16064 |
. . . . . . . . 9
β’ (π₯ β β β
(sinβπ₯) =
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / (2 Β·
i))) |
97 | 96 | adantl 482 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β (sinβπ₯) = (((expβ(i Β· π₯)) β (expβ(-i
Β· π₯))) / (2 Β·
i))) |
98 | 97, 78 | eqtr4d 2775 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β (sinβπ₯) = ((((expβ(i Β· π₯)) β (expβ(-i
Β· π₯))) / i) /
2)) |
99 | 98 | negeqd 11453 |
. . . . . 6
β’
((β€ β§ π₯
β β) β -(sinβπ₯) = -((((expβ(i Β· π₯)) β (expβ(-i
Β· π₯))) / i) /
2)) |
100 | 3 | negnegi 11529 |
. . . . . . . . . 10
β’ --i =
i |
101 | 100 | oveq2i 7419 |
. . . . . . . . 9
β’
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β· --i) =
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β· i) |
102 | | mulneg2 11650 |
. . . . . . . . . 10
β’
((((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) β β β§ -i
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β· --i) =
-(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β·
-i)) |
103 | 71, 12, 102 | sylancl 586 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β· --i) =
-(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β·
-i)) |
104 | 101, 103 | eqtr3id 2786 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β· i) =
-(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β·
-i)) |
105 | | mulcl 11193 |
. . . . . . . . . . 11
β’
(((expβ(-i Β· π₯)) β β β§ i β β)
β ((expβ(-i Β· π₯)) Β· i) β
β) |
106 | 16, 3, 105 | sylancl 586 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β ((expβ(-i Β· π₯)) Β· i) β
β) |
107 | 21, 106 | negsubd 11576 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) Β· i) + -((expβ(-i Β·
π₯)) Β· i)) =
(((expβ(i Β· π₯)) Β· i) β ((expβ(-i
Β· π₯)) Β·
i))) |
108 | | mulneg2 11650 |
. . . . . . . . . . 11
β’
(((expβ(-i Β· π₯)) β β β§ i β β)
β ((expβ(-i Β· π₯)) Β· -i) = -((expβ(-i Β·
π₯)) Β·
i)) |
109 | 16, 3, 108 | sylancl 586 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β ((expβ(-i Β· π₯)) Β· -i) = -((expβ(-i Β·
π₯)) Β·
i)) |
110 | 109 | oveq2d 7424 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) Β· i) + ((expβ(-i Β·
π₯)) Β· -i)) =
(((expβ(i Β· π₯)) Β· i) + -((expβ(-i Β·
π₯)) Β·
i))) |
111 | 8, 16, 4 | subdird 11670 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β· i) =
(((expβ(i Β· π₯)) Β· i) β ((expβ(-i
Β· π₯)) Β·
i))) |
112 | 107, 110,
111 | 3eqtr4d 2782 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) Β· i) + ((expβ(-i Β·
π₯)) Β· -i)) =
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β·
i)) |
113 | 71, 4, 10 | divrecd 11992 |
. . . . . . . . . 10
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) = (((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) Β· (1 / i))) |
114 | | irec 14164 |
. . . . . . . . . . 11
β’ (1 / i) =
-i |
115 | 114 | oveq2i 7419 |
. . . . . . . . . 10
β’
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β· (1 / i)) =
(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) Β·
-i) |
116 | 113, 115 | eqtrdi 2788 |
. . . . . . . . 9
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) = (((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) Β· -i)) |
117 | 116 | negeqd 11453 |
. . . . . . . 8
β’
((β€ β§ π₯
β β) β -(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) = -(((expβ(i
Β· π₯)) β
(expβ(-i Β· π₯))) Β· -i)) |
118 | 104, 112,
117 | 3eqtr4d 2782 |
. . . . . . 7
β’
((β€ β§ π₯
β β) β (((expβ(i Β· π₯)) Β· i) + ((expβ(-i Β·
π₯)) Β· -i)) =
-(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i)) |
119 | 118 | oveq1d 7423 |
. . . . . 6
β’
((β€ β§ π₯
β β) β ((((expβ(i Β· π₯)) Β· i) + ((expβ(-i Β·
π₯)) Β· -i)) / 2) =
(-(((expβ(i Β· π₯)) β (expβ(-i Β· π₯))) / i) / 2)) |
120 | 95, 99, 119 | 3eqtr4d 2782 |
. . . . 5
β’
((β€ β§ π₯
β β) β -(sinβπ₯) = ((((expβ(i Β· π₯)) Β· i) + ((expβ(-i
Β· π₯)) Β· -i))
/ 2)) |
121 | 120 | mpteq2dva 5248 |
. . . 4
β’ (β€
β (π₯ β β
β¦ -(sinβπ₯)) =
(π₯ β β β¦
((((expβ(i Β· π₯)) Β· i) + ((expβ(-i Β·
π₯)) Β· -i)) /
2))) |
122 | 92, 93, 121 | 3eqtr4d 2782 |
. . 3
β’ (β€
β (β D cos) = (π₯
β β β¦ -(sinβπ₯))) |
123 | 89, 122 | jca 512 |
. 2
β’ (β€
β ((β D sin) = cos β§ (β D cos) = (π₯ β β β¦ -(sinβπ₯)))) |
124 | 123 | mptru 1548 |
1
β’ ((β
D sin) = cos β§ (β D cos) = (π₯ β β β¦ -(sinβπ₯))) |