Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem sinadd 7393

Description: Sine addition formula for complex arguments. Equation 14 of [Gleason] p. 310.

Hypotheses

Ref	Expression
sinadd.1
sinadd.2

Assertion

Ref	Expression
sinadd

---

Proof of Theorem sinadd

Step	Hyp	Ref	Expression
1		sinadd.1	. . . 4
2		sinadd.2	. . . 4
3	1, 2	addcl 5292	. . 3
4		sinvalt 7371	. . 3
5	3, 4	ax-mp 7	. 2
6		cosclt 7374	. . . . . . . 8
7	1, 6	ax-mp 7	. . . . . . 7
8		cosclt 7374	. . . . . . . 8
9	2, 8	ax-mp 7	. . . . . . 7
10	7, 9	mulcl 5293	. . . . . 6
11		axicn 5242	. . . . . . . 8
12		sinclt 7373	. . . . . . . . 9
13	2, 12	ax-mp 7	. . . . . . . 8
14	11, 13	mulcl 5293	. . . . . . 7
15		sinclt 7373	. . . . . . . . 9
16	1, 15	ax-mp 7	. . . . . . . 8
17	11, 16	mulcl 5293	. . . . . . 7
18	14, 17	mulcl 5293	. . . . . 6
19	10, 18	addcl 5292	. . . . 5
20	7, 14	mulcl 5293	. . . . . 6
21	9, 17	mulcl 5293	. . . . . 6
22	20, 21	addcl 5292	. . . . 5
23	19, 22, 22	pnncan 5454	. . . 4
24	11, 1, 2	adddi 5298	. . . . . . 7
25	24	fveq2i 3712	. . . . . 6
26	11, 1	mulcl 5293	. . . . . . 7
27	11, 2	mulcl 5293	. . . . . . 7
28	26, 27	efadd 7308	. . . . . 6
29		efivalt 7389	. . . . . . . . 9
30	1, 29	ax-mp 7	. . . . . . . 8
31		efivalt 7389	. . . . . . . . 9
32	2, 31	ax-mp 7	. . . . . . . 8
33	30, 32	opreq12i 3958	. . . . . . 7
34	7, 17, 9, 14	muladd 5398	. . . . . . 7
35	33, 34	eqtr 1487	. . . . . 6
36	25, 28, 35	3eqtr 1491	. . . . 5
37	11	negcl 5341	. . . . . . . 8
38	37, 1, 2	adddi 5298	. . . . . . 7
39	38	fveq2i 3712	. . . . . 6
40	37, 1	mulcl 5293	. . . . . . 7
41	37, 2	mulcl 5293	. . . . . . 7
42	40, 41	efadd 7308	. . . . . 6
43		efmivalt 7390	. . . . . . . . 9
44	1, 43	ax-mp 7	. . . . . . . 8
45		efmivalt 7390	. . . . . . . . 9
46	2, 45	ax-mp 7	. . . . . . . 8
47	44, 46	opreq12i 3958	. . . . . . 7
48	7, 17	pm3.2i 285	. . . . . . . 8
49	9, 14	pm3.2i 285	. . . . . . . 8
50		mulsubt 5449	. . . . . . . 8
51	48, 49, 50	mp2an 695	. . . . . . 7
52	47, 51	eqtr 1487	. . . . . 6
53	39, 42, 52	3eqtr 1491	. . . . 5