Definition df-dvds 13987

Description: Define the divides relation. (Contributed by Paul Chapman, 21-Mar-2011.)

Assertion

Ref	Expression
df-dvds

Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-dvds

Step	Hyp	Ref	Expression
1		cdvds 13986	. 2
2		vx	. . . . . . 7
3	2	cv 1394	. . . . . 6
4		cz 10889	. . . . . 6
5	3, 4	wcel 1818	. . . . 5
6		vy	. . . . . . 7
7	6	cv 1394	. . . . . 6
8	7, 4	wcel 1818	. . . . 5
9	5, 8	wa 369	. . . 4
10		vn	. . . . . . . 8
11	10	cv 1394	. . . . . . 7
12		cmul 9518	. . . . . . 7
13	11, 3, 12	co 6296	. . . . . 6
14	13, 7	wceq 1395	. . . . 5
15	14, 10, 4	wrex 2808	. . . 4
16	9, 15	wa 369	. . 3
17	16, 2, 6	copab 4509	. 2
18	1, 17	wceq 1395	1

This definition is referenced by:  divides  13988  dvdszrcl  13991  dvdsrzring  18507  dvdsrz  18508  reldvds  31220