Theorem 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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( sin ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐵 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐵 ) ) ) )

Proof

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