Metamath Proof Explorer

Theorem dvsincos

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

Ref Expression
Assertion dvsincos 
|- ( ( CC _D sin ) = cos /\ ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) ) )

Proof

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