This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvsincos

Description: Derivative of the sine and cosine functions. (Contributed by Mario Carneiro, 21-May-2016)

Ref Expression
Assertion dvsincos ( ( ℂ D sin ) = cos ∧ ( ℂ D cos ) = ( 𝑥 ∈ ℂ ↦ - ( sin ‘ 𝑥 ) ) )

Proof

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 ‘ 𝑥 ) ) )