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

Definition df-gcd 11563
Description: Define the  gcd operator. For example,  ( -u 6  gcd  9 )  =  3 (ex-gcd 12870). (Contributed by Paul Chapman, 21-Mar-2011.)
Assertion
Ref Expression
df-gcd  |-  gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  | 
( n  ||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
Distinct variable group:    x, n, y

Detailed syntax breakdown of Definition df-gcd
StepHypRef Expression
1 cgcd 11562 . 2  class  gcd
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cz 9022 . . 3  class  ZZ
52cv 1315 . . . . . 6  class  x
6 cc0 7588 . . . . . 6  class  0
75, 6wceq 1316 . . . . 5  wff  x  =  0
83cv 1315 . . . . . 6  class  y
98, 6wceq 1316 . . . . 5  wff  y  =  0
107, 9wa 103 . . . 4  wff  ( x  =  0  /\  y  =  0 )
11 vn . . . . . . . . 9  setvar  n
1211cv 1315 . . . . . . . 8  class  n
13 cdvds 11420 . . . . . . . 8  class  ||
1412, 5, 13wbr 3899 . . . . . . 7  wff  n  ||  x
1512, 8, 13wbr 3899 . . . . . . 7  wff  n  ||  y
1614, 15wa 103 . . . . . 6  wff  ( n 
||  x  /\  n  ||  y )
1716, 11, 4crab 2397 . . . . 5  class  { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) }
18 cr 7587 . . . . 5  class  RR
19 clt 7768 . . . . 5  class  <
2017, 18, 19csup 6837 . . . 4  class  sup ( { n  e.  ZZ  |  ( n  ||  x  /\  n  ||  y
) } ,  RR ,  <  )
2110, 6, 20cif 3444 . . 3  class  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) )
222, 3, 4, 4, 21cmpo 5744 . 2  class  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
231, 22wceq 1316 1  wff  gcd  =  ( x  e.  ZZ ,  y  e.  ZZ  |->  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  | 
( n  ||  x  /\  n  ||  y ) } ,  RR ,  <  ) ) )
Colors of variables: wff set class
This definition is referenced by:  gcdval  11575  gcdf  11588
  Copyright terms: Public domain W3C validator