Definition df-cos 13806

Description: Define the cosine function. (Contributed by NM, 14-Mar-2005.)

Assertion

Ref	Expression
df-cos

Detailed syntax breakdown of Definition df-cos

Step	Hyp	Ref	Expression
1		ccos 13800	. 2
2		vx	. . 3
3		cc 9511	. . 3
4		ci 9515	. . . . . . 7
5	2	cv 1394	. . . . . . 7
6		cmul 9518	. . . . . . 7
7	4, 5, 6	co 6296	. . . . . 6
8		ce 13797	. . . . . 6
9	7, 8	cfv 5593	. . . . 5
10	4	cneg 9829	. . . . . . 7
11	10, 5, 6	co 6296	. . . . . 6
12	11, 8	cfv 5593	. . . . 5
13		caddc 9516	. . . . 5
14	9, 12, 13	co 6296	. . . 4
15		c2 10610	. . . 4
16		cdiv 10231	. . . 4
17	14, 15, 16	co 6296	. . 3
18	2, 3, 17	cmpt 4510	. 2
19	1, 18	wceq 1395	1

This definition is referenced by:  cosval  13858  cosf  13860  dvsincos  22382  coscn  22840