dvasinbx

Description: Derivative exercise: the derivative with respect to y of A x sin(By), given two constants A and B . (Contributed by Glauco Siliprandi, 11-Dec-2019)

		Ref	Expression
	Assertion	dvasinbx	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{d (y \in ℂ⟼ A \sin B y)}{d_{ℂ} y} = (y \in ℂ ⟼ A B \cos B y)$

Proof

Step	Hyp	Ref	Expression
1		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
2	1	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to ℂ \in \{ℝ, ℂ\}$
3		simpll	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to A \in ℂ$
4		0cnd	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to 0 \in ℂ$
5	1	a1i	$⊢ A \in ℂ \to ℂ \in \{ℝ, ℂ\}$
6		id	$⊢ A \in ℂ \to A \in ℂ$
7	5 6	dvmptc	$⊢ A \in ℂ \to \frac{d (y \in ℂ⟼ A)}{d_{ℂ} y} = (y \in ℂ ⟼ 0)$
8	7	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{d (y \in ℂ⟼ A)}{d_{ℂ} y} = (y \in ℂ ⟼ 0)$
9		mulcl	$⊢ (B \in ℂ \land y \in ℂ) \to B y \in ℂ$
10	9	sincld	$⊢ (B \in ℂ \land y \in ℂ) \to \sin B y \in ℂ$
11	10	adantll	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to \sin B y \in ℂ$
12		simpl	$⊢ (B \in ℂ \land y \in ℂ) \to B \in ℂ$
13	9	coscld	$⊢ (B \in ℂ \land y \in ℂ) \to \cos B y \in ℂ$
14	12 13	mulcld	$⊢ (B \in ℂ \land y \in ℂ) \to B \cos B y \in ℂ$
15	14	adantll	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to B \cos B y \in ℂ$
16		dvsinax	$⊢ B \in ℂ \to \frac{d (y \in ℂ⟼ \sin B y)}{d_{ℂ} y} = (y \in ℂ ⟼ B \cos B y)$
17	16	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{d (y \in ℂ⟼ \sin B y)}{d_{ℂ} y} = (y \in ℂ ⟼ B \cos B y)$
18	2 3 4 8 11 15 17	dvmptmul	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{d (y \in ℂ⟼ A \sin B y)}{d_{ℂ} y} = (y \in ℂ ⟼ 0 \cdot \sin B y + B \cos B y A)$
19	11	mul02d	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to 0 \cdot \sin B y = 0$
20	12	adantll	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to B \in ℂ$
21	13	adantll	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to \cos B y \in ℂ$
22	20 21 3	mul32d	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to B \cos B y A = B A \cos B y$
23		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
24		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
25	23 24	mulcomd	$⊢ (A \in ℂ \land B \in ℂ) \to B A = A B$
26	25	adantr	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to B A = A B$
27	26	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to B A \cos B y = A B \cos B y$
28	22 27	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to B \cos B y A = A B \cos B y$
29	19 28	oveq12d	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to 0 \cdot \sin B y + B \cos B y A = 0 + A B \cos B y$
30	3 20	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to A B \in ℂ$
31	30 21	mulcld	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to A B \cos B y \in ℂ$
32	31	addid2d	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to 0 + A B \cos B y = A B \cos B y$
33	29 32	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ) \land y \in ℂ) \to 0 \cdot \sin B y + B \cos B y A = A B \cos B y$
34	33	mpteq2dva	$⊢ (A \in ℂ \land B \in ℂ) \to (y \in ℂ ⟼ 0 \cdot \sin B y + B \cos B y A) = (y \in ℂ ⟼ A B \cos B y)$
35	18 34	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{d (y \in ℂ⟼ A \sin B y)}{d_{ℂ} y} = (y \in ℂ ⟼ A B \cos B y)$

Metamath Proof Explorer

Theorem dvasinbx

Proof