dvsincos

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

		Ref	Expression
	Assertion	dvsincos	$⊢ (ℂ D \sin = \cos \land ℂ D \cos = (x \in ℂ ⟼ - \sin x))$

Proof

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

Metamath Proof Explorer

Theorem dvsincos

Proof