Definition df-dvds 11970

Description: Define the divides relation, see definition in [ApostolNT] p. 14. (Contributed by Paul Chapman, 21-Mar-2011.)

Assertion

Ref	Expression
df-dvds	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }

Distinct variable group:   x, n, y

Detailed syntax breakdown of Definition df-dvds

Step	Hyp	Ref	Expression
1		cdvds 11969	. 2 class ||
2		vx	. . . . . . 7 setvar x
3	2	cv 1363	. . . . . 6 class x
4		cz 9343	. . . . . 6 class ZZ
5	3, 4	wcel 2167	. . . . 5 wff x e. ZZ
6		vy	. . . . . . 7 setvar y
7	6	cv 1363	. . . . . 6 class y
8	7, 4	wcel 2167	. . . . 5 wff y e. ZZ
9	5, 8	wa 104	. . . 4 wff ( x e. ZZ /\ y e. ZZ )
10		vn	. . . . . . . 8 setvar n
11	10	cv 1363	. . . . . . 7 class n
12		cmul 7901	. . . . . . 7 class x.
13	11, 3, 12	co 5925	. . . . . 6 class ( n x. x )
14	13, 7	wceq 1364	. . . . 5 wff ( n x. x ) = y
15	14, 10, 4	wrex 2476	. . . 4 wff E. n e. ZZ ( n x. x ) = y
16	9, 15	wa 104	. . 3 wff ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y )
17	16, 2, 6	copab 4094	. 2 class { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
18	1, 17	wceq 1364	1 wff || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }

This definition is referenced by:  divides  11971  dvdszrcl  11974  dvdsrzring  14235