sinadd

Description: Addition formula for sine. Equation 14 of Gleason p. 310. (Contributed by Steve Rodriguez, 10-Nov-2006) (Revised by Mario Carneiro, 30-Apr-2014)

		Ref	Expression
	Assertion	sinadd	$⊢ (A \in ℂ \land B \in ℂ) \to \sin (A + B) = \sin A \cos B + \cos A \sin B$

Proof

Step	Hyp	Ref	Expression
1		addcl	$⊢ (A \in ℂ \land B \in ℂ) \to A + B \in ℂ$
2		sinval	$⊢ A + B \in ℂ \to \sin (A + B) = \frac{e^{i (A + B)} - e^{(- i) (A + B)}}{2 i}$
3	1 2	syl	$⊢ (A \in ℂ \land B \in ℂ) \to \sin (A + B) = \frac{e^{i (A + B)} - e^{(- i) (A + B)}}{2 i}$
4		2cn	$⊢ 2 \in ℂ$
5	4	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to 2 \in ℂ$
6		ax-icn	$⊢ i \in ℂ$
7	6	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to i \in ℂ$
8		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
9	8	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \in ℂ$
10		sincl	$⊢ B \in ℂ \to \sin B \in ℂ$
11	10	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \sin B \in ℂ$
12	9 11	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \sin B \in ℂ$
13		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
14	13	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to \sin A \in ℂ$
15		coscl	$⊢ B \in ℂ \to \cos B \in ℂ$
16	15	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \cos B \in ℂ$
17	14 16	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \sin A \cos B \in ℂ$
18	12 17	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \sin B + \sin A \cos B \in ℂ$
19	5 7 18	mulassd	$⊢ (A \in ℂ \land B \in ℂ) \to 2 i (\cos A \sin B + \sin A \cos B) = 2 i (\cos A \sin B + \sin A \cos B)$
20	7 12 17	adddid	$⊢ (A \in ℂ \land B \in ℂ) \to i (\cos A \sin B + \sin A \cos B) = i \cos A \sin B + i \sin A \cos B$
21	7 9 11	mul12d	$⊢ (A \in ℂ \land B \in ℂ) \to i \cos A \sin B = \cos A i \sin B$
22	14 16	mulcomd	$⊢ (A \in ℂ \land B \in ℂ) \to \sin A \cos B = \cos B \sin A$
23	22	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin A \cos B = i \cos B \sin A$
24	7 16 14	mul12d	$⊢ (A \in ℂ \land B \in ℂ) \to i \cos B \sin A = \cos B i \sin A$
25	23 24	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin A \cos B = \cos B i \sin A$
26	21 25	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to i \cos A \sin B + i \sin A \cos B = \cos A i \sin B + \cos B i \sin A$
27	20 26	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to i (\cos A \sin B + \sin A \cos B) = \cos A i \sin B + \cos B i \sin A$
28	27	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to 2 i (\cos A \sin B + \sin A \cos B) = 2 (\cos A i \sin B + \cos B i \sin A)$
29	19 28	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to 2 i (\cos A \sin B + \sin A \cos B) = 2 (\cos A i \sin B + \cos B i \sin A)$
30		mulcl	$⊢ (i \in ℂ \land \sin B \in ℂ) \to i \sin B \in ℂ$
31	6 11 30	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin B \in ℂ$
32	9 31	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A i \sin B \in ℂ$
33		mulcl	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i \sin A \in ℂ$
34	6 14 33	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin A \in ℂ$
35	16 34	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos B i \sin A \in ℂ$
36	32 35	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A i \sin B + \cos B i \sin A \in ℂ$
37		mulcl	$⊢ (2 \in ℂ \land \cos A i \sin B + \cos B i \sin A \in ℂ) \to 2 (\cos A i \sin B + \cos B i \sin A) \in ℂ$
38	4 36 37	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to 2 (\cos A i \sin B + \cos B i \sin A) \in ℂ$
39		2mulicn	$⊢ 2 i \in ℂ$
40	39	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to 2 i \in ℂ$
41		2muline0	$⊢ 2 i \neq 0$
42	41	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to 2 i \neq 0$
43	38 40 18 42	divmuld	$⊢ (A \in ℂ \land B \in ℂ) \to (\frac{2 (\cos A i \sin B + \cos B i \sin A)}{2 i} = \cos A \sin B + \sin A \cos B \leftrightarrow 2 i (\cos A \sin B + \sin A \cos B) = 2 (\cos A i \sin B + \cos B i \sin A))$
44	29 43	mpbird	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{2 (\cos A i \sin B + \cos B i \sin A)}{2 i} = \cos A \sin B + \sin A \cos B$
45	9 16	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \cos B \in ℂ$
46	31 34	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin B i \sin A \in ℂ$
47	45 46	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \cos B + i \sin B i \sin A \in ℂ$
48	47 36 36	pnncand	$⊢ (A \in ℂ \land B \in ℂ) \to (\cos A \cos B + i \sin B i \sin A) + (\cos A i \sin B + \cos B i \sin A) - (\cos A \cos B + i \sin B i \sin A - (\cos A i \sin B + \cos B i \sin A)) = \cos A i \sin B + \cos B i \sin A + \cos A i \sin B + \cos B i \sin A$
49		adddi	$⊢ (i \in ℂ \land A \in ℂ \land B \in ℂ) \to i (A + B) = i A + i B$
50	6 49	mp3an1	$⊢ (A \in ℂ \land B \in ℂ) \to i (A + B) = i A + i B$
51	50	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i (A + B)} = e^{i A + i B}$
52		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
53		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
54	6 52 53	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i A \in ℂ$
55		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
56		mulcl	$⊢ (i \in ℂ \land B \in ℂ) \to i B \in ℂ$
57	6 55 56	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i B \in ℂ$
58		efadd	$⊢ (i A \in ℂ \land i B \in ℂ) \to e^{i A + i B} = e^{i A} e^{i B}$
59	54 57 58	syl2anc	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i A + i B} = e^{i A} e^{i B}$
60		efival	$⊢ A \in ℂ \to e^{i A} = \cos A + i \sin A$
61		efival	$⊢ B \in ℂ \to e^{i B} = \cos B + i \sin B$
62	60 61	oveqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i A} e^{i B} = (\cos A + i \sin A) (\cos B + i \sin B)$
63	9 34 16 31	muladdd	$⊢ (A \in ℂ \land B \in ℂ) \to (\cos A + i \sin A) (\cos B + i \sin B) = \cos A \cos B + i \sin B i \sin A + \cos A i \sin B + \cos B i \sin A$
64	62 63	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i A} e^{i B} = \cos A \cos B + i \sin B i \sin A + \cos A i \sin B + \cos B i \sin A$
65	51 59 64	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i (A + B)} = \cos A \cos B + i \sin B i \sin A + \cos A i \sin B + \cos B i \sin A$
66		negicn	$⊢ - i \in ℂ$
67		adddi	$⊢ (- i \in ℂ \land A \in ℂ \land B \in ℂ) \to (- i) (A + B) = (- i) A + (- i) B$
68	66 67	mp3an1	$⊢ (A \in ℂ \land B \in ℂ) \to (- i) (A + B) = (- i) A + (- i) B$
69	68	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) (A + B)} = e^{(- i) A + (- i) B}$
70		mulcl	$⊢ (- i \in ℂ \land A \in ℂ) \to (- i) A \in ℂ$
71	66 52 70	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to (- i) A \in ℂ$
72		mulcl	$⊢ (- i \in ℂ \land B \in ℂ) \to (- i) B \in ℂ$
73	66 55 72	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to (- i) B \in ℂ$
74		efadd	$⊢ ((- i) A \in ℂ \land (- i) B \in ℂ) \to e^{(- i) A + (- i) B} = e^{(- i) A} e^{(- i) B}$
75	71 73 74	syl2anc	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) A + (- i) B} = e^{(- i) A} e^{(- i) B}$
76		efmival	$⊢ A \in ℂ \to e^{(- i) A} = \cos A - i \sin A$
77		efmival	$⊢ B \in ℂ \to e^{(- i) B} = \cos B - i \sin B$
78	76 77	oveqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) A} e^{(- i) B} = (\cos A - i \sin A) (\cos B - i \sin B)$
79	9 34 16 31	mulsubd	$⊢ (A \in ℂ \land B \in ℂ) \to (\cos A - i \sin A) (\cos B - i \sin B) = \cos A \cos B + i \sin B i \sin A - (\cos A i \sin B + \cos B i \sin A)$
80	78 79	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) A} e^{(- i) B} = \cos A \cos B + i \sin B i \sin A - (\cos A i \sin B + \cos B i \sin A)$
81	69 75 80	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) (A + B)} = \cos A \cos B + i \sin B i \sin A - (\cos A i \sin B + \cos B i \sin A)$
82	65 81	oveq12d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i (A + B)} - e^{(- i) (A + B)} = (\cos A \cos B + i \sin B i \sin A) + (\cos A i \sin B + \cos B i \sin A) - (\cos A \cos B + i \sin B i \sin A - (\cos A i \sin B + \cos B i \sin A))$
83	36	2timesd	$⊢ (A \in ℂ \land B \in ℂ) \to 2 (\cos A i \sin B + \cos B i \sin A) = \cos A i \sin B + \cos B i \sin A + \cos A i \sin B + \cos B i \sin A$
84	48 82 83	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i (A + B)} - e^{(- i) (A + B)} = 2 (\cos A i \sin B + \cos B i \sin A)$
85	84	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{e^{i (A + B)} - e^{(- i) (A + B)}}{2 i} = \frac{2 (\cos A i \sin B + \cos B i \sin A)}{2 i}$
86	17 12	addcomd	$⊢ (A \in ℂ \land B \in ℂ) \to \sin A \cos B + \cos A \sin B = \cos A \sin B + \sin A \cos B$
87	44 85 86	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{e^{i (A + B)} - e^{(- i) (A + B)}}{2 i} = \sin A \cos B + \cos A \sin B$
88	3 87	eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \sin (A + B) = \sin A \cos B + \cos A \sin B$

Metamath Proof Explorer

Theorem sinadd

Proof