Metamath Proof Explorer

Theorem dvsincos

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

Ref Expression
Assertion dvsincos ⊢ℂDsin=cos∧ℂDcos=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∈ℂ→ei⁢x∈ℂ
8 6 7 syl ⊢⊤∧x∈ℂ→ei⁢x∈ℂ
9 ine0 ⊢i≠0
10 9 a1i ⊢⊤∧x∈ℂ→i≠0
11 8 4 10 divcld ⊢⊤∧x∈ℂ→ei⁢xi∈ℂ
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⁢xi∈ℂ
18 17 negcld ⊢⊤∧x∈ℂ→−e−i⁢xi∈ℂ
19 11 18 addcld ⊢⊤∧x∈ℂ→ei⁢xi+−e−i⁢xi∈ℂ
20 8 16 addcld ⊢⊤∧x∈ℂ→ei⁢x+e−i⁢x∈ℂ
21 8 4 mulcld ⊢⊤∧x∈ℂ→ei⁢x⁢i∈ℂ
22 efcl ⊢y∈ℂ→ey∈ℂ
23 22 adantl ⊢⊤∧y∈ℂ→ey∈ℂ
24 1cnd ⊢⊤∧x∈ℂ→1∈ℂ
25 2 dvmptid ⊢⊤→dx∈ℂxdℂx=x∈ℂ⟼1
26 3 a1i ⊢⊤→i∈ℂ
27 2 5 24 25 26 dvmptcmul ⊢⊤→dx∈ℂi⁢xdℂx=x∈ℂ⟼i⋅1
28 3 mulridi ⊢i⋅1=i
29 28 mpteq2i ⊢x∈ℂ⟼i⋅1=x∈ℂ⟼i
30 27 29 eqtrdi ⊢⊤→dx∈ℂi⁢xdℂx=x∈ℂ⟼i
31 eff ⊢exp:ℂ⟶ℂ
32 31 a1i ⊢⊤→exp:ℂ⟶ℂ
33 32 feqmptd ⊢⊤→exp=y∈ℂ⟼ey
34 33 oveq2d ⊢⊤→ℂDexp=dy∈ℂeydℂy
35 dvef ⊢ℂDexp=exp
36 35 33 eqtrid ⊢⊤→ℂDexp=y∈ℂ⟼ey
37 34 36 eqtr3d ⊢⊤→dy∈ℂeydℂy=y∈ℂ⟼ey
38 fveq2 ⊢y=i⁢x→ey=ei⁢x
39 2 2 6 4 23 23 30 37 38 38 dvmptco ⊢⊤→dx∈ℂei⁢xdℂx=x∈ℂ⟼ei⁢x⁢i
40 9 a1i ⊢⊤→i≠0
41 2 8 21 39 26 40 dvmptdivc ⊢⊤→dx∈ℂei⁢xidℂx=x∈ℂ⟼ei⁢x⁢ii
42 8 4 10 divcan4d ⊢⊤∧x∈ℂ→ei⁢x⁢ii=ei⁢x
43 42 mpteq2dva ⊢⊤→x∈ℂ⟼ei⁢x⁢ii=x∈ℂ⟼ei⁢x
44 41 43 eqtrd ⊢⊤→dx∈ℂei⁢xidℂx=x∈ℂ⟼ei⁢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⁢−ii∈ℂ
48 12 a1i ⊢⊤∧x∈ℂ→−i∈ℂ
49 12 a1i ⊢⊤→−i∈ℂ
50 2 5 24 25 49 dvmptcmul ⊢⊤→dx∈ℂ−i⁢xdℂx=x∈ℂ⟼−i⋅1
51 12 mulridi ⊢−i⋅1=−i
52 51 mpteq2i ⊢x∈ℂ⟼−i⋅1=x∈ℂ⟼−i
53 50 52 eqtrdi ⊢⊤→dx∈ℂ−i⁢xdℂx=x∈ℂ⟼−i
54 fveq2 ⊢y=−i⁢x→ey=e−i⁢x
55 2 2 14 48 23 23 53 37 54 54 dvmptco ⊢⊤→dx∈ℂe−i⁢xdℂx=x∈ℂ⟼e−i⁢x⁢−i
56 2 16 46 55 26 40 dvmptdivc ⊢⊤→dx∈ℂe−i⁢xidℂx=x∈ℂ⟼e−i⁢x⁢−ii
57 2 17 47 56 dvmptneg ⊢⊤→dx∈ℂ−e−i⁢xidℂx=x∈ℂ⟼−e−i⁢x⁢−ii
58 46 4 10 divneg2d ⊢⊤∧x∈ℂ→−e−i⁢x⁢−ii=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⁢−ii=e−i⁢x
63 62 mpteq2dva ⊢⊤→x∈ℂ⟼−e−i⁢x⁢−ii=x∈ℂ⟼e−i⁢x
64 57 63 eqtrd ⊢⊤→dx∈ℂ−e−i⁢xidℂx=x∈ℂ⟼e−i⁢x
65 2 11 8 44 18 16 64 dvmptadd ⊢⊤→dx∈ℂei⁢xi+−e−i⁢xidℂx=x∈ℂ⟼ei⁢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∈ℂei⁢xi+−e−i⁢xi2dℂx=x∈ℂ⟼ei⁢x+e−i⁢x2
70 df-sin ⊢sin=x∈ℂ⟼ei⁢x−e−i⁢x2⁢i
71 8 16 subcld ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢x∈ℂ
72 2cnd ⊢⊤∧x∈ℂ→2∈ℂ
73 67 a1i ⊢⊤∧x∈ℂ→2≠0
74 71 4 72 10 73 divdiv1d ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi2=ei⁢x−e−i⁢xi⋅2
75 2cn ⊢2∈ℂ
76 3 75 mulcomi ⊢i⋅2=2⁢i
77 76 oveq2i ⊢ei⁢x−e−i⁢xi⋅2=ei⁢x−e−i⁢x2⁢i
78 74 77 eqtrdi ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi2=ei⁢x−e−i⁢x2⁢i
79 8 16 4 10 divsubdird ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi=ei⁢xi−e−i⁢xi
80 11 17 negsubd ⊢⊤∧x∈ℂ→ei⁢xi+−e−i⁢xi=ei⁢xi−e−i⁢xi
81 79 80 eqtr4d ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi=ei⁢xi+−e−i⁢xi
82 81 oveq1d ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi2=ei⁢xi+−e−i⁢xi2
83 78 82 eqtr3d ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢x2⁢i=ei⁢xi+−e−i⁢xi2
84 83 mpteq2dva ⊢⊤→x∈ℂ⟼ei⁢x−e−i⁢x2⁢i=x∈ℂ⟼ei⁢xi+−e−i⁢xi2
85 70 84 eqtrid ⊢⊤→sin=x∈ℂ⟼ei⁢xi+−e−i⁢xi2
86 85 oveq2d ⊢⊤→ℂDsin=dx∈ℂei⁢xi+−e−i⁢xi2dℂx
87 df-cos ⊢cos=x∈ℂ⟼ei⁢x+e−i⁢x2
88 87 a1i ⊢⊤→cos=x∈ℂ⟼ei⁢x+e−i⁢x2
89 69 86 88 3eqtr4d ⊢⊤→ℂDsin=cos
90 21 46 addcld ⊢⊤∧x∈ℂ→ei⁢x⁢i+e−i⁢x⁢−i∈ℂ
91 2 8 21 39 16 46 55 dvmptadd ⊢⊤→dx∈ℂei⁢x+e−i⁢xdℂx=x∈ℂ⟼ei⁢x⁢i+e−i⁢x⁢−i
92 2 20 90 91 66 68 dvmptdivc ⊢⊤→dx∈ℂei⁢x+e−i⁢x2dℂx=x∈ℂ⟼ei⁢x⁢i+e−i⁢x⁢−i2
93 88 oveq2d ⊢⊤→ℂDcos=dx∈ℂei⁢x+e−i⁢x2dℂx
94 71 4 10 divcld ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi∈ℂ
95 94 72 73 divnegd ⊢⊤∧x∈ℂ→−ei⁢x−e−i⁢xi2=−ei⁢x−e−i⁢xi2
96 sinval ⊢x∈ℂ→sin⁡x=ei⁢x−e−i⁢x2⁢i
97 96 adantl ⊢⊤∧x∈ℂ→sin⁡x=ei⁢x−e−i⁢x2⁢i
98 97 78 eqtr4d ⊢⊤∧x∈ℂ→sin⁡x=ei⁢x−e−i⁢xi2
99 98 negeqd ⊢⊤∧x∈ℂ→−sin⁡x=−ei⁢x−e−i⁢xi2
100 3 negnegi ⊢−−i=i
101 100 oveq2i ⊢ei⁢x−e−i⁢x⁢−−i=ei⁢x−e−i⁢x⁢i
102 mulneg2 ⊢ei⁢x−e−i⁢x∈ℂ∧−i∈ℂ→ei⁢x−e−i⁢x⁢−−i=−ei⁢x−e−i⁢x⁢−i
103 71 12 102 sylancl ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢x⁢−−i=−ei⁢x−e−i⁢x⁢−i
104 101 103 eqtr3id ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢x⁢i=−ei⁢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∈ℂ→ei⁢x⁢i+−e−i⁢x⁢i=ei⁢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∈ℂ→ei⁢x⁢i+e−i⁢x⁢−i=ei⁢x⁢i+−e−i⁢x⁢i
111 8 16 4 subdird ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢x⁢i=ei⁢x⁢i−e−i⁢x⁢i
112 107 110 111 3eqtr4d ⊢⊤∧x∈ℂ→ei⁢x⁢i+e−i⁢x⁢−i=ei⁢x−e−i⁢x⁢i
113 71 4 10 divrecd ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi=ei⁢x−e−i⁢x⁢1i
114 irec ⊢1i=−i
115 114 oveq2i ⊢ei⁢x−e−i⁢x⁢1i=ei⁢x−e−i⁢x⁢−i
116 113 115 eqtrdi ⊢⊤∧x∈ℂ→ei⁢x−e−i⁢xi=ei⁢x−e−i⁢x⁢−i
117 116 negeqd ⊢⊤∧x∈ℂ→−ei⁢x−e−i⁢xi=−ei⁢x−e−i⁢x⁢−i
118 104 112 117 3eqtr4d ⊢⊤∧x∈ℂ→ei⁢x⁢i+e−i⁢x⁢−i=−ei⁢x−e−i⁢xi
119 118 oveq1d ⊢⊤∧x∈ℂ→ei⁢x⁢i+e−i⁢x⁢−i2=−ei⁢x−e−i⁢xi2
120 95 99 119 3eqtr4d ⊢⊤∧x∈ℂ→−sin⁡x=ei⁢x⁢i+e−i⁢x⁢−i2
121 120 mpteq2dva ⊢⊤→x∈ℂ⟼−sin⁡x=x∈ℂ⟼ei⁢x⁢i+e−i⁢x⁢−i2
122 92 93 121 3eqtr4d ⊢⊤→ℂDcos=x∈ℂ⟼−sin⁡x
123 89 122 jca ⊢⊤→ℂDsin=cos∧ℂDcos=x∈ℂ⟼−sin⁡x
124 123 mptru ⊢ℂDsin=cos∧ℂDcos=x∈ℂ⟼−sin⁡x