Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem cosadd 7394

Description: Addition formula for cosine. Equation 15 of [Gleason] p. 310.

Hypotheses

Ref	Expression
sinadd.1
sinadd.2

Assertion

Ref	Expression
cosadd

---

Proof of Theorem cosadd

Step	Hyp	Ref	Expression
1		sinadd.1	. . . 4
2		sinadd.2	. . . 4
3	1, 2	addcl 5292	. . 3
4		cosvalt 7372	. . 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		ppncant 5453	. . . . 5
24	19, 22, 19, 23	mp3an 913	. . . 4
25	11, 1, 2	adddi 5298	. . . . . . 7
26	25	fveq2i 3712	. . . . . 6
27	11, 1	mulcl 5293	. . . . . . 7
28	11, 2	mulcl 5293	. . . . . . 7
29	27, 28	efadd 7308	. . . . . 6
30		efivalt 7389	. . . . . . . . 9
31	1, 30	ax-mp 7	. . . . . . . 8
32		efivalt 7389	. . . . . . . . 9
33	2, 32	ax-mp 7	. . . . . . . 8
34	31, 33	opreq12i 3958	. . . . . . 7
35	7, 17, 9, 14	muladd 5398	. . . . . . 7
36	34, 35	eqtr 1487	. . . . . 6
37	26, 29, 36	3eqtr 1491	. . . . 5
38	11	negcl 5341	. . . . . . . 8
39	38, 1, 2	adddi 5298	. . . . . . 7
40	39	fveq2i 3712	. . . . . 6
41	38, 1	mulcl 5293	. . . . . . 7
42	38, 2	mulcl 5293	. . . . . . 7
43	41, 42	efadd 7308	. . . . . 6
44		efmivalt 7390	. . . . . . . . 9
45	1, 44	ax-mp 7	. . . . . . . 8
46		efmivalt 7390	. . . . . . . . 9
47	2, 46	ax-mp 7	. . . . . . . 8
48	45, 47	opreq12i 3958	. . . . . . 7
49	7, 17	pm3.2i 285	. . . . . . . 8
50	9, 14	pm3.2i 285	. . . . . . . 8
51		mulsubt 5449	. . . . . . . 8