Definition df-dvds

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdvds	|- ||
1		vx	|- x
2		vy	|- y
3	1	cv	|- x
4		cz	|- ZZ
5	3 4	wcel	|- x e. ZZ
6	2	cv	|- y
7	6 4	wcel	|- y e. ZZ
8	5 7	wa	|- ( x e. ZZ /\ y e. ZZ )
9		vn	|- n
10	9	cv	|- n
11		cmul	|- x.
12	10 3 11	co	|- ( n x. x )
13	12 6	wceq	|- ( n x. x ) = y
14	13 9 4	wrex	|- E. n e. ZZ ( n x. x ) = y
15	8 14	wa	|- ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y )
16	15 1 2	copab	|- { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }
17	0 16	wceq	|- || = { <. x , y >. | ( ( x e. ZZ /\ y e. ZZ ) /\ E. n e. ZZ ( n x. x ) = y ) }