cosadd

Description: Addition formula for cosine. Equation 15 of Gleason p. 310. (Contributed by NM, 15-Jan-2006) (Revised by Mario Carneiro, 30-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		addcl	$⊢ (A \in ℂ \land B \in ℂ) \to A + B \in ℂ$
2		cosval	$⊢ A + B \in ℂ \to \cos (A + B) = \frac{e^{i (A + B)} + e^{(- i) (A + B)}}{2}$
3	1 2	syl	$⊢ (A \in ℂ \land B \in ℂ) \to \cos (A + B) = \frac{e^{i (A + B)} + e^{(- i) (A + B)}}{2}$
4		coscl	$⊢ A \in ℂ \to \cos A \in ℂ$
5	4	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \in ℂ$
6		coscl	$⊢ B \in ℂ \to \cos B \in ℂ$
7	6	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \cos B \in ℂ$
8	5 7	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \cos B \in ℂ$
9		ax-icn	$⊢ i \in ℂ$
10		sincl	$⊢ B \in ℂ \to \sin B \in ℂ$
11	10	adantl	$⊢ (A \in ℂ \land B \in ℂ) \to \sin B \in ℂ$
12		mulcl	$⊢ (i \in ℂ \land \sin B \in ℂ) \to i \sin B \in ℂ$
13	9 11 12	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin B \in ℂ$
14		sincl	$⊢ A \in ℂ \to \sin A \in ℂ$
15	14	adantr	$⊢ (A \in ℂ \land B \in ℂ) \to \sin A \in ℂ$
16		mulcl	$⊢ (i \in ℂ \land \sin A \in ℂ) \to i \sin A \in ℂ$
17	9 15 16	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin A \in ℂ$
18	13 17	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin B i \sin A \in ℂ$
19	8 18	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \cos B + i \sin B i \sin A \in ℂ$
20	5 13	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A i \sin B \in ℂ$
21	7 17	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos B i \sin A \in ℂ$
22	20 21	addcld	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A i \sin B + \cos B i \sin A \in ℂ$
23	19 22 19	ppncand	$⊢ (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 \cos B + i \sin B i \sin A + \cos A \cos B + i \sin B i \sin A$
24		adddi	$⊢ (i \in ℂ \land A \in ℂ \land B \in ℂ) \to i (A + B) = i A + i B$
25	9 24	mp3an1	$⊢ (A \in ℂ \land B \in ℂ) \to i (A + B) = i A + i B$
26	25	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i (A + B)} = e^{i A + i B}$
27		simpl	$⊢ (A \in ℂ \land B \in ℂ) \to A \in ℂ$
28		mulcl	$⊢ (i \in ℂ \land A \in ℂ) \to i A \in ℂ$
29	9 27 28	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i A \in ℂ$
30		simpr	$⊢ (A \in ℂ \land B \in ℂ) \to B \in ℂ$
31		mulcl	$⊢ (i \in ℂ \land B \in ℂ) \to i B \in ℂ$
32	9 30 31	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to i B \in ℂ$
33		efadd	$⊢ (i A \in ℂ \land i B \in ℂ) \to e^{i A + i B} = e^{i A} e^{i B}$
34	29 32 33	syl2anc	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i A + i B} = e^{i A} e^{i B}$
35		efival	$⊢ A \in ℂ \to e^{i A} = \cos A + i \sin A$
36		efival	$⊢ B \in ℂ \to e^{i B} = \cos B + i \sin B$
37	35 36	oveqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i A} e^{i B} = (\cos A + i \sin A) (\cos B + i \sin B)$
38	5 17 7 13	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$
39	37 38	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$
40	26 34 39	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$
41		negicn	$⊢ - i \in ℂ$
42		adddi	$⊢ (- i \in ℂ \land A \in ℂ \land B \in ℂ) \to (- i) (A + B) = (- i) A + (- i) B$
43	41 42	mp3an1	$⊢ (A \in ℂ \land B \in ℂ) \to (- i) (A + B) = (- i) A + (- i) B$
44	43	fveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) (A + B)} = e^{(- i) A + (- i) B}$
45		mulcl	$⊢ (- i \in ℂ \land A \in ℂ) \to (- i) A \in ℂ$
46	41 27 45	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to (- i) A \in ℂ$
47		mulcl	$⊢ (- i \in ℂ \land B \in ℂ) \to (- i) B \in ℂ$
48	41 30 47	sylancr	$⊢ (A \in ℂ \land B \in ℂ) \to (- i) B \in ℂ$
49		efadd	$⊢ ((- i) A \in ℂ \land (- i) B \in ℂ) \to e^{(- i) A + (- i) B} = e^{(- i) A} e^{(- i) B}$
50	46 48 49	syl2anc	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) A + (- i) B} = e^{(- i) A} e^{(- i) B}$
51		efmival	$⊢ A \in ℂ \to e^{(- i) A} = \cos A - i \sin A$
52		efmival	$⊢ B \in ℂ \to e^{(- i) B} = \cos B - i \sin B$
53	51 52	oveqan12d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{(- i) A} e^{(- i) B} = (\cos A - i \sin A) (\cos B - i \sin B)$
54	5 17 7 13	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)$
55	53 54	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)$
56	44 50 55	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)$
57	40 56	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))$
58	19	2timesd	$⊢ (A \in ℂ \land B \in ℂ) \to 2 (\cos A \cos B + i \sin B i \sin A) = \cos A \cos B + i \sin B i \sin A + \cos A \cos B + i \sin B i \sin A$
59	23 57 58	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ) \to e^{i (A + B)} + e^{(- i) (A + B)} = 2 (\cos A \cos B + i \sin B i \sin A)$
60	59	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{e^{i (A + B)} + e^{(- i) (A + B)}}{2} = \frac{2 (\cos A \cos B + i \sin B i \sin A)}{2}$
61		2cn	$⊢ 2 \in ℂ$
62		2ne0	$⊢ 2 \neq 0$
63		divcan3	$⊢ (\cos A \cos B + i \sin B i \sin A \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 (\cos A \cos B + i \sin B i \sin A)}{2} = \cos A \cos B + i \sin B i \sin A$
64	61 62 63	mp3an23	$⊢ \cos A \cos B + i \sin B i \sin A \in ℂ \to \frac{2 (\cos A \cos B + i \sin B i \sin A)}{2} = \cos A \cos B + i \sin B i \sin A$
65	19 64	syl	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{2 (\cos A \cos B + i \sin B i \sin A)}{2} = \cos A \cos B + i \sin B i \sin A$
66	9	a1i	$⊢ (A \in ℂ \land B \in ℂ) \to i \in ℂ$
67	66 11 66 15	mul4d	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin B i \sin A = i i \sin B \sin A$
68		ixi	$⊢ i i = - 1$
69	68	oveq1i	$⊢ i i \sin B \sin A = -1 \sin B \sin A$
70	11 15	mulcomd	$⊢ (A \in ℂ \land B \in ℂ) \to \sin B \sin A = \sin A \sin B$
71	70	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to -1 \sin B \sin A = -1 \sin A \sin B$
72	69 71	syl5eq	$⊢ (A \in ℂ \land B \in ℂ) \to i i \sin B \sin A = -1 \sin A \sin B$
73	15 11	mulcld	$⊢ (A \in ℂ \land B \in ℂ) \to \sin A \sin B \in ℂ$
74	73	mulm1d	$⊢ (A \in ℂ \land B \in ℂ) \to -1 \sin A \sin B = - \sin A \sin B$
75	67 72 74	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to i \sin B i \sin A = - \sin A \sin B$
76	75	oveq2d	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \cos B + i \sin B i \sin A = \cos A \cos B + (- \sin A \sin B)$
77	8 73	negsubd	$⊢ (A \in ℂ \land B \in ℂ) \to \cos A \cos B + (- \sin A \sin B) = \cos A \cos B - \sin A \sin B$
78	65 76 77	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{2 (\cos A \cos B + i \sin B i \sin A)}{2} = \cos A \cos B - \sin A \sin B$
79	3 60 78	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ) \to \cos (A + B) = \cos A \cos B - \sin A \sin B$

Metamath Proof Explorer

Theorem cosadd

Proof