| Step |
Hyp |
Ref |
Expression |
| 1 |
|
cnelprrecn |
⊢ ℂ ∈ { ℝ , ℂ } |
| 2 |
1
|
a1i |
⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } ) |
| 3 |
|
ax-icn |
⊢ i ∈ ℂ |
| 4 |
3
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → i ∈ ℂ ) |
| 5 |
|
simpr |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ ) |
| 6 |
4 5
|
mulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( i · 𝑥 ) ∈ ℂ ) |
| 7 |
|
efcl |
⊢ ( ( i · 𝑥 ) ∈ ℂ → ( exp ‘ ( i · 𝑥 ) ) ∈ ℂ ) |
| 8 |
6 7
|
syl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( exp ‘ ( i · 𝑥 ) ) ∈ ℂ ) |
| 9 |
|
ine0 |
⊢ i ≠ 0 |
| 10 |
9
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → i ≠ 0 ) |
| 11 |
8 4 10
|
divcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( i · 𝑥 ) ) / i ) ∈ ℂ ) |
| 12 |
|
negicn |
⊢ - i ∈ ℂ |
| 13 |
|
mulcl |
⊢ ( ( - i ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - i · 𝑥 ) ∈ ℂ ) |
| 14 |
12 5 13
|
sylancr |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( - i · 𝑥 ) ∈ ℂ ) |
| 15 |
|
efcl |
⊢ ( ( - i · 𝑥 ) ∈ ℂ → ( exp ‘ ( - i · 𝑥 ) ) ∈ ℂ ) |
| 16 |
14 15
|
syl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( exp ‘ ( - i · 𝑥 ) ) ∈ ℂ ) |
| 17 |
16 4 10
|
divcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ∈ ℂ ) |
| 18 |
17
|
negcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ∈ ℂ ) |
| 19 |
11 18
|
addcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ∈ ℂ ) |
| 20 |
8 16
|
addcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ ) |
| 21 |
8 4
|
mulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( i · 𝑥 ) ) · i ) ∈ ℂ ) |
| 22 |
|
efcl |
⊢ ( 𝑦 ∈ ℂ → ( exp ‘ 𝑦 ) ∈ ℂ ) |
| 23 |
22
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℂ ) → ( exp ‘ 𝑦 ) ∈ ℂ ) |
| 24 |
|
1cnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 1 ∈ ℂ ) |
| 25 |
2
|
dvmptid |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ 1 ) ) |
| 26 |
3
|
a1i |
⊢ ( ⊤ → i ∈ ℂ ) |
| 27 |
2 5 24 25 26
|
dvmptcmul |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( i · 1 ) ) ) |
| 28 |
3
|
mulridi |
⊢ ( i · 1 ) = i |
| 29 |
28
|
mpteq2i |
⊢ ( 𝑥 ∈ ℂ ↦ ( i · 1 ) ) = ( 𝑥 ∈ ℂ ↦ i ) |
| 30 |
27 29
|
eqtrdi |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( i · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ i ) ) |
| 31 |
|
eff |
⊢ exp : ℂ ⟶ ℂ |
| 32 |
31
|
a1i |
⊢ ( ⊤ → exp : ℂ ⟶ ℂ ) |
| 33 |
32
|
feqmptd |
⊢ ( ⊤ → exp = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) |
| 34 |
33
|
oveq2d |
⊢ ( ⊤ → ( ℂ D exp ) = ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) ) |
| 35 |
|
dvef |
⊢ ( ℂ D exp ) = exp |
| 36 |
35 33
|
eqtrid |
⊢ ( ⊤ → ( ℂ D exp ) = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) |
| 37 |
34 36
|
eqtr3d |
⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( exp ‘ 𝑦 ) ) ) |
| 38 |
|
fveq2 |
⊢ ( 𝑦 = ( i · 𝑥 ) → ( exp ‘ 𝑦 ) = ( exp ‘ ( i · 𝑥 ) ) ) |
| 39 |
2 2 6 4 23 23 30 37 38 38
|
dvmptco |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( i · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) · i ) ) ) |
| 40 |
9
|
a1i |
⊢ ( ⊤ → i ≠ 0 ) |
| 41 |
2 8 21 39 26 40
|
dvmptdivc |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) / i ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) / i ) ) ) |
| 42 |
8 4 10
|
divcan4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) / i ) = ( exp ‘ ( i · 𝑥 ) ) ) |
| 43 |
42
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) / i ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( i · 𝑥 ) ) ) ) |
| 44 |
41 43
|
eqtrd |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) / i ) ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( i · 𝑥 ) ) ) ) |
| 45 |
|
mulcl |
⊢ ( ( ( exp ‘ ( - i · 𝑥 ) ) ∈ ℂ ∧ - i ∈ ℂ ) → ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ∈ ℂ ) |
| 46 |
16 12 45
|
sylancl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ∈ ℂ ) |
| 47 |
46 4 10
|
divcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / i ) ∈ ℂ ) |
| 48 |
12
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - i ∈ ℂ ) |
| 49 |
12
|
a1i |
⊢ ( ⊤ → - i ∈ ℂ ) |
| 50 |
2 5 24 25 49
|
dvmptcmul |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( - i · 1 ) ) ) |
| 51 |
12
|
mulridi |
⊢ ( - i · 1 ) = - i |
| 52 |
51
|
mpteq2i |
⊢ ( 𝑥 ∈ ℂ ↦ ( - i · 1 ) ) = ( 𝑥 ∈ ℂ ↦ - i ) |
| 53 |
50 52
|
eqtrdi |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( - i · 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ - i ) ) |
| 54 |
|
fveq2 |
⊢ ( 𝑦 = ( - i · 𝑥 ) → ( exp ‘ 𝑦 ) = ( exp ‘ ( - i · 𝑥 ) ) ) |
| 55 |
2 2 14 48 23 23 53 37 54 54
|
dvmptco |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( - i · 𝑥 ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) ) |
| 56 |
2 16 46 55 26 40
|
dvmptdivc |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / i ) ) ) |
| 57 |
2 17 47 56
|
dvmptneg |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ) = ( 𝑥 ∈ ℂ ↦ - ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / i ) ) ) |
| 58 |
46 4 10
|
divneg2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / i ) = ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / - i ) ) |
| 59 |
3 9
|
negne0i |
⊢ - i ≠ 0 |
| 60 |
59
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - i ≠ 0 ) |
| 61 |
16 48 60
|
divcan4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / - i ) = ( exp ‘ ( - i · 𝑥 ) ) ) |
| 62 |
58 61
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / i ) = ( exp ‘ ( - i · 𝑥 ) ) ) |
| 63 |
62
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ - ( ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) / i ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( - i · 𝑥 ) ) ) ) |
| 64 |
57 63
|
eqtrd |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ) = ( 𝑥 ∈ ℂ ↦ ( exp ‘ ( - i · 𝑥 ) ) ) ) |
| 65 |
2 11 8 44 18 16 64
|
dvmptadd |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) ) |
| 66 |
|
2cnd |
⊢ ( ⊤ → 2 ∈ ℂ ) |
| 67 |
|
2ne0 |
⊢ 2 ≠ 0 |
| 68 |
67
|
a1i |
⊢ ( ⊤ → 2 ≠ 0 ) |
| 69 |
2 19 20 65 66 68
|
dvmptdivc |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) / 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) ) |
| 70 |
|
df-sin |
⊢ sin = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) |
| 71 |
8 16
|
subcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ ) |
| 72 |
|
2cnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 2 ∈ ℂ ) |
| 73 |
67
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → 2 ≠ 0 ) |
| 74 |
71 4 72 10 73
|
divdiv1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( i · 2 ) ) ) |
| 75 |
|
2cn |
⊢ 2 ∈ ℂ |
| 76 |
3 75
|
mulcomi |
⊢ ( i · 2 ) = ( 2 · i ) |
| 77 |
76
|
oveq2i |
⊢ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( i · 2 ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) |
| 78 |
74 77
|
eqtrdi |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) |
| 79 |
8 16 4 10
|
divsubdird |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) = ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) − ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ) |
| 80 |
11 17
|
negsubd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) − ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ) |
| 81 |
79 80
|
eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) = ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) ) |
| 82 |
81
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) = ( ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) / 2 ) ) |
| 83 |
78 82
|
eqtr3d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) = ( ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) / 2 ) ) |
| 84 |
83
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) / 2 ) ) ) |
| 85 |
70 84
|
eqtrid |
⊢ ( ⊤ → sin = ( 𝑥 ∈ ℂ ↦ ( ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) / 2 ) ) ) |
| 86 |
85
|
oveq2d |
⊢ ( ⊤ → ( ℂ D sin ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( ( ( exp ‘ ( i · 𝑥 ) ) / i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) / i ) ) / 2 ) ) ) ) |
| 87 |
|
df-cos |
⊢ cos = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) |
| 88 |
87
|
a1i |
⊢ ( ⊤ → cos = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) ) |
| 89 |
69 86 88
|
3eqtr4d |
⊢ ( ⊤ → ( ℂ D sin ) = cos ) |
| 90 |
21 46
|
addcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) ∈ ℂ ) |
| 91 |
2 8 21 39 16 46 55
|
dvmptadd |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) ) ) |
| 92 |
2 20 90 91 66 68
|
dvmptdivc |
⊢ ( ⊤ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) / 2 ) ) ) |
| 93 |
88
|
oveq2d |
⊢ ( ⊤ → ( ℂ D cos ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( ( exp ‘ ( i · 𝑥 ) ) + ( exp ‘ ( - i · 𝑥 ) ) ) / 2 ) ) ) ) |
| 94 |
71 4 10
|
divcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) ∈ ℂ ) |
| 95 |
94 72 73
|
divnegd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) = ( - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) ) |
| 96 |
|
sinval |
⊢ ( 𝑥 ∈ ℂ → ( sin ‘ 𝑥 ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) |
| 97 |
96
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( sin ‘ 𝑥 ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / ( 2 · i ) ) ) |
| 98 |
97 78
|
eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( sin ‘ 𝑥 ) = ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) ) |
| 99 |
98
|
negeqd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( sin ‘ 𝑥 ) = - ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) ) |
| 100 |
3
|
negnegi |
⊢ - - i = i |
| 101 |
100
|
oveq2i |
⊢ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - - i ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · i ) |
| 102 |
|
mulneg2 |
⊢ ( ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) ∈ ℂ ∧ - i ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - - i ) = - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - i ) ) |
| 103 |
71 12 102
|
sylancl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - - i ) = - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - i ) ) |
| 104 |
101 103
|
eqtr3id |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · i ) = - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - i ) ) |
| 105 |
|
mulcl |
⊢ ( ( ( exp ‘ ( - i · 𝑥 ) ) ∈ ℂ ∧ i ∈ ℂ ) → ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ∈ ℂ ) |
| 106 |
16 3 105
|
sylancl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ∈ ℂ ) |
| 107 |
21 106
|
negsubd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) − ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ) ) |
| 108 |
|
mulneg2 |
⊢ ( ( ( exp ‘ ( - i · 𝑥 ) ) ∈ ℂ ∧ i ∈ ℂ ) → ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) = - ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ) |
| 109 |
16 3 108
|
sylancl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) = - ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ) |
| 110 |
109
|
oveq2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + - ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ) ) |
| 111 |
8 16 4
|
subdird |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · i ) = ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) − ( ( exp ‘ ( - i · 𝑥 ) ) · i ) ) ) |
| 112 |
107 110 111
|
3eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · i ) ) |
| 113 |
71 4 10
|
divrecd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · ( 1 / i ) ) ) |
| 114 |
|
irec |
⊢ ( 1 / i ) = - i |
| 115 |
114
|
oveq2i |
⊢ ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · ( 1 / i ) ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - i ) |
| 116 |
113 115
|
eqtrdi |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) = ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - i ) ) |
| 117 |
116
|
negeqd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) = - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) · - i ) ) |
| 118 |
104 112 117
|
3eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) = - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) ) |
| 119 |
118
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) / 2 ) = ( - ( ( ( exp ‘ ( i · 𝑥 ) ) − ( exp ‘ ( - i · 𝑥 ) ) ) / i ) / 2 ) ) |
| 120 |
95 99 119
|
3eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → - ( sin ‘ 𝑥 ) = ( ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) / 2 ) ) |
| 121 |
120
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) = ( 𝑥 ∈ ℂ ↦ ( ( ( ( exp ‘ ( i · 𝑥 ) ) · i ) + ( ( exp ‘ ( - i · 𝑥 ) ) · - i ) ) / 2 ) ) ) |
| 122 |
92 93 121
|
3eqtr4d |
⊢ ( ⊤ → ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ) |
| 123 |
89 122
|
jca |
⊢ ( ⊤ → ( ( ℂ D sin ) = cos ∧ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ) ) |
| 124 |
123
|
mptru |
⊢ ( ( ℂ D sin ) = cos ∧ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) ) |