ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-dvds Unicode version

Definition df-dvds 10341
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
StepHypRef Expression
1 cdvds 10340 . 2  class  ||
2 vx . . . . . . 7  setvar  x
32cv 1284 . . . . . 6  class  x
4 cz 8432 . . . . . 6  class  ZZ
53, 4wcel 1434 . . . . 5  wff  x  e.  ZZ
6 vy . . . . . . 7  setvar  y
76cv 1284 . . . . . 6  class  y
87, 4wcel 1434 . . . . 5  wff  y  e.  ZZ
95, 8wa 102 . . . 4  wff  ( x  e.  ZZ  /\  y  e.  ZZ )
10 vn . . . . . . . 8  setvar  n
1110cv 1284 . . . . . . 7  class  n
12 cmul 7048 . . . . . . 7  class  x.
1311, 3, 12co 5543 . . . . . 6  class  ( n  x.  x )
1413, 7wceq 1285 . . . . 5  wff  ( n  x.  x )  =  y
1514, 10, 4wrex 2350 . . . 4  wff  E. n  e.  ZZ  ( n  x.  x )  =  y
169, 15wa 102 . . 3  wff  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x
)  =  y )
1716, 2, 6copab 3846 . 2  class  { <. x ,  y >.  |  ( ( x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x )  =  y ) }
181, 17wceq 1285 1  wff  ||  =  { <. x ,  y
>.  |  ( (
x  e.  ZZ  /\  y  e.  ZZ )  /\  E. n  e.  ZZ  ( n  x.  x
)  =  y ) }
Colors of variables: wff set class
This definition is referenced by:  divides  10342  dvdszrcl  10345
  Copyright terms: Public domain W3C validator