Definition df-dvds 14984

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 14983	. 2 class ||
2		vx	. . . . . . 7 setvar x
3	2	cv 1482	. . . . . 6 class x
4		cz 11377	. . . . . 6 class ZZ
5	3, 4	wcel 1990	. . . . 5 wff x e. ZZ
6		vy	. . . . . . 7 setvar y
7	6	cv 1482	. . . . . 6 class y
8	7, 4	wcel 1990	. . . . 5 wff y e. ZZ
9	5, 8	wa 384	. . . 4 wff ( x e. ZZ /\ y e. ZZ )
10		vn	. . . . . . . 8 setvar n
11	10	cv 1482	. . . . . . 7 class n
12		cmul 9941	. . . . . . 7 class x.
13	11, 3, 12	co 6650	. . . . . 6 class ( n x. x )
14	13, 7	wceq 1483	. . . . 5 wff ( n x. x ) = y
15	14, 10, 4	wrex 2913	. . . 4 wff E. n e. ZZ ( n x. x ) = y
16	9, 15	wa 384	. . 3 wff ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y )
17	16, 2, 6	copab 4712	. 2 class { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
18	1, 17	wceq 1483	1 wff || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }

This definition is referenced by:  divides  14985  dvdszrcl  14988  dvdsrzring  19831  reldvds  38514