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 = x sin x

Proof

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