Theorem dvcosax

Description: Derivative exercise: the derivative with respect to x of cos(Ax), given a constant A . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	dvcosax	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼\cos Ax\right)}{d_{ℂ}x}=\left(x\in ℂ⟼A\left(-\sin Ax\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mulcl	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to Ax\in ℂ$$
2		eqidd	$$⊢A\in ℂ\to \left(x\in ℂ⟼Ax\right)=\left(x\in ℂ⟼Ax\right)$$
3		cosf	$$⊢\cos :ℂ⟶ℂ$$
4	3	a1i	$$⊢A\in ℂ\to \cos :ℂ⟶ℂ$$
5	4	feqmptd	$$⊢A\in ℂ\to \cos =\left(y\in ℂ⟼\cos y\right)$$
6		fveq2	$$⊢y=Ax\to \cos y=\cos Ax$$
7	1 2 5 6	fmptco	$$⊢A\in ℂ\to \cos \circ \left(x\in ℂ⟼Ax\right)=\left(x\in ℂ⟼\cos Ax\right)$$
8	7	eqcomd	$$⊢A\in ℂ\to \left(x\in ℂ⟼\cos Ax\right)=\cos \circ \left(x\in ℂ⟼Ax\right)$$
9	8	oveq2d	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼\cos Ax\right)}{d_{ℂ}x}=ℂ\mathrm{D}\left(\cos \circ \left(x\in ℂ⟼Ax\right)\right)$$
10		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
11	10	a1i	$$⊢A\in ℂ\to ℂ\in \left\{ℝ,ℂ\right\}$$
12	1	fmpttd	$$⊢A\in ℂ\to \left(x\in ℂ⟼Ax\right):ℂ⟶ℂ$$
13		dvcos	$$⊢ℂ\mathrm{D}\cos =\left(x\in ℂ⟼-\sin x\right)$$
14	13	dmeqi	$$⊢\mathrm{dom}{\cos }_{ℂ}^{\prime }=\mathrm{dom}\left(x\in ℂ⟼-\sin x\right)$$
15		dmmptg	$$⊢\forall x\in ℂ-\sin x\in ℂ\to \mathrm{dom}\left(x\in ℂ⟼-\sin x\right)=ℂ$$
16		sincl	$$⊢x\in ℂ\to \sin x\in ℂ$$
17	16	negcld	$$⊢x\in ℂ\to -\sin x\in ℂ$$
18	15 17	mprg	$$⊢\mathrm{dom}\left(x\in ℂ⟼-\sin x\right)=ℂ$$
19	14 18	eqtri	$$⊢\mathrm{dom}{\cos }_{ℂ}^{\prime }=ℂ$$
20	19	a1i	$$⊢A\in ℂ\to \mathrm{dom}{\cos }_{ℂ}^{\prime }=ℂ$$
21		simpl	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to A\in ℂ$$
22		0red	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to 0\in ℝ$$
23		id	$$⊢A\in ℂ\to A\in ℂ$$
24	11 23	dvmptc	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼A\right)}{d_{ℂ}x}=\left(x\in ℂ⟼0\right)$$
25		simpr	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to x\in ℂ$$
26		1red	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to 1\in ℝ$$
27	11	dvmptid	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼1\right)$$
28	11 21 22 24 25 26 27	dvmptmul	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\left(x\in ℂ⟼0\cdot x+1A\right)$$
29	28	dmeqd	$$⊢A\in ℂ\to \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\mathrm{dom}\left(x\in ℂ⟼0\cdot x+1A\right)$$
30		dmmptg	$$⊢\forall x\in ℂ0\cdot x+1A\in \mathrm{V}\to \mathrm{dom}\left(x\in ℂ⟼0\cdot x+1A\right)=ℂ$$
31		ovex	$$⊢0\cdot x+1A\in \mathrm{V}$$
32	31	a1i	$$⊢x\in ℂ\to 0\cdot x+1A\in \mathrm{V}$$
33	30 32	mprg	$$⊢\mathrm{dom}\left(x\in ℂ⟼0\cdot x+1A\right)=ℂ$$
34	29 33	eqtrdi	$$⊢A\in ℂ\to \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=ℂ$$
35	11 11 4 12 20 34	dvcof	$$⊢A\in ℂ\to ℂ\mathrm{D}\left(\cos \circ \left(x\in ℂ⟼Ax\right)\right)=\left({\cos }_{ℂ}^{\prime }\circ \left(x\in ℂ⟼Ax\right)\right){\times }_f\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}$$
36		dvcos	$$⊢ℂ\mathrm{D}\cos =\left(y\in ℂ⟼-\sin y\right)$$
37	36	a1i	$$⊢A\in ℂ\to ℂ\mathrm{D}\cos =\left(y\in ℂ⟼-\sin y\right)$$
38		fveq2	$$⊢y=Ax\to \sin y=\sin Ax$$
39	38	negeqd	$$⊢y=Ax\to -\sin y=-\sin Ax$$
40	1 2 37 39	fmptco	$$⊢A\in ℂ\to {\cos }_{ℂ}^{\prime }\circ \left(x\in ℂ⟼Ax\right)=\left(x\in ℂ⟼-\sin Ax\right)$$
41	40	oveq1d	$$⊢A\in ℂ\to \left({\cos }_{ℂ}^{\prime }\circ \left(x\in ℂ⟼Ax\right)\right){\times }_f\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\left(x\in ℂ⟼-\sin Ax\right){\times }_f\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}$$
42		cnex	$$⊢ℂ\in \mathrm{V}$$
43	42	mptex	$$⊢\left(x\in ℂ⟼-\sin Ax\right)\in \mathrm{V}$$
44		ovex	$$⊢\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\in \mathrm{V}$$
45		offval3	$$⊢\left(\left(x\in ℂ⟼-\sin Ax\right)\in \mathrm{V}\wedge \frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\in \mathrm{V}\right)\to \left(x\in ℂ⟼-\sin Ax\right){\times }_f\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\left(y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)⟼\left(x\in ℂ⟼-\sin Ax\right)\left(y\right)\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)\right)$$
46	43 44 45	mp2an	$$⊢\left(x\in ℂ⟼-\sin Ax\right){\times }_f\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\left(y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)⟼\left(x\in ℂ⟼-\sin Ax\right)\left(y\right)\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)\right)$$
47	46	a1i	$$⊢A\in ℂ\to \left(x\in ℂ⟼-\sin Ax\right){\times }_f\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\left(y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)⟼\left(x\in ℂ⟼-\sin Ax\right)\left(y\right)\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)\right)$$
48	1	sincld	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to \sin Ax\in ℂ$$
49	48	negcld	$$⊢\left(A\in ℂ\wedge x\in ℂ\right)\to -\sin Ax\in ℂ$$
50	49	ralrimiva	$$⊢A\in ℂ\to \forall x\in ℂ-\sin Ax\in ℂ$$
51		dmmptg	$$⊢\forall x\in ℂ-\sin Ax\in ℂ\to \mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)=ℂ$$
52	50 51	syl	$$⊢A\in ℂ\to \mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)=ℂ$$
53	52 34	ineq12d	$$⊢A\in ℂ\to \mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=ℂ\cap ℂ$$
54		inidm	$$⊢ℂ\cap ℂ=ℂ$$
55	53 54	eqtrdi	$$⊢A\in ℂ\to \mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=ℂ$$
56		simpr	$$⊢\left(A\in ℂ\wedge y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)\right)\to y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)$$
57	55	adantr	$$⊢\left(A\in ℂ\wedge y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)\right)\to \mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=ℂ$$
58	56 57	eleqtrd	$$⊢\left(A\in ℂ\wedge y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)\right)\to y\in ℂ$$
59		eqidd	$$⊢y\in ℂ\to \left(x\in ℂ⟼-\sin Ax\right)=\left(x\in ℂ⟼-\sin Ax\right)$$
60		oveq2	$$⊢x=y\to Ax=Ay$$
61	60	fveq2d	$$⊢x=y\to \sin Ax=\sin Ay$$
62	61	negeqd	$$⊢x=y\to -\sin Ax=-\sin Ay$$
63	62	adantl	$$⊢\left(y\in ℂ\wedge x=y\right)\to -\sin Ax=-\sin Ay$$
64		id	$$⊢y\in ℂ\to y\in ℂ$$
65		negex	$$⊢-\sin Ay\in \mathrm{V}$$
66	65	a1i	$$⊢y\in ℂ\to -\sin Ay\in \mathrm{V}$$
67	59 63 64 66	fvmptd	$$⊢y\in ℂ\to \left(x\in ℂ⟼-\sin Ax\right)\left(y\right)=-\sin Ay$$
68	67	adantl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to \left(x\in ℂ⟼-\sin Ax\right)\left(y\right)=-\sin Ay$$
69	28	adantr	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to \frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\left(x\in ℂ⟼0\cdot x+1A\right)$$
70		oveq2	$$⊢x=y\to 0\cdot x=0\cdot y$$
71	70	oveq1d	$$⊢x=y\to 0\cdot x+1A=0\cdot y+1A$$
72		mul02	$$⊢y\in ℂ\to 0\cdot y=0$$
73		mulid2	$$⊢A\in ℂ\to 1A=A$$
74	72 73	oveqan12rd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to 0\cdot y+1A=0+A$$
75		addid2	$$⊢A\in ℂ\to 0+A=A$$
76	75	adantr	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to 0+A=A$$
77	74 76	eqtrd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to 0\cdot y+1A=A$$
78	71 77	sylan9eqr	$$⊢\left(\left(A\in ℂ\wedge y\in ℂ\right)\wedge x=y\right)\to 0\cdot x+1A=A$$
79		simpr	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to y\in ℂ$$
80		simpl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to A\in ℂ$$
81	69 78 79 80	fvmptd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to \frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)=A$$
82	68 81	oveq12d	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to \left(x\in ℂ⟼-\sin Ax\right)\left(y\right)\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)=\left(-\sin Ay\right)A$$
83		mulcl	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to Ay\in ℂ$$
84	83	sincld	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to \sin Ay\in ℂ$$
85	84	negcld	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to -\sin Ay\in ℂ$$
86	85 80	mulcomd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to \left(-\sin Ay\right)A=A\left(-\sin Ay\right)$$
87	82 86	eqtrd	$$⊢\left(A\in ℂ\wedge y\in ℂ\right)\to \left(x\in ℂ⟼-\sin Ax\right)\left(y\right)\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)=A\left(-\sin Ay\right)$$
88	58 87	syldan	$$⊢\left(A\in ℂ\wedge y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)\right)\to \left(x\in ℂ⟼-\sin Ax\right)\left(y\right)\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)=A\left(-\sin Ay\right)$$
89	55 88	mpteq12dva	$$⊢A\in ℂ\to \left(y\in \left(\mathrm{dom}\left(x\in ℂ⟼-\sin Ax\right)\cap \mathrm{dom}\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\right)⟼\left(x\in ℂ⟼-\sin Ax\right)\left(y\right)\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}\left(y\right)\right)=\left(y\in ℂ⟼A\left(-\sin Ay\right)\right)$$
90	41 47 89	3eqtrd	$$⊢A\in ℂ\to \left({\cos }_{ℂ}^{\prime }\circ \left(x\in ℂ⟼Ax\right)\right){\times }_f\frac{d\left(x\in ℂ⟼Ax\right)}{d_{ℂ}x}=\left(y\in ℂ⟼A\left(-\sin Ay\right)\right)$$
91	9 35 90	3eqtrd	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼\cos Ax\right)}{d_{ℂ}x}=\left(y\in ℂ⟼A\left(-\sin Ay\right)\right)$$
92		oveq2	$$⊢y=x\to Ay=Ax$$
93	92	fveq2d	$$⊢y=x\to \sin Ay=\sin Ax$$
94	93	negeqd	$$⊢y=x\to -\sin Ay=-\sin Ax$$
95	94	oveq2d	$$⊢y=x\to A\left(-\sin Ay\right)=A\left(-\sin Ax\right)$$
96	95	cbvmptv	$$⊢\left(y\in ℂ⟼A\left(-\sin Ay\right)\right)=\left(x\in ℂ⟼A\left(-\sin Ax\right)\right)$$
97	91 96	eqtrdi	$$⊢A\in ℂ\to \frac{d\left(x\in ℂ⟼\cos Ax\right)}{d_{ℂ}x}=\left(x\in ℂ⟼A\left(-\sin Ax\right)\right)$$