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

Definition df-gcd 11478
Description: Define the  gcd operator. For example,  ( -u 6  gcd  9 )  =  3 (ex-gcd 12627). (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 11477 . 2  class  gcd
2 vx . . 3  setvar  x
3 vy . . 3  setvar  y
4 cz 8952 . . 3  class  ZZ
52cv 1311 . . . . . 6  class  x
6 cc0 7541 . . . . . 6  class  0
75, 6wceq 1312 . . . . 5  wff  x  =  0
83cv 1311 . . . . . 6  class  y
98, 6wceq 1312 . . . . 5  wff  y  =  0
107, 9wa 103 . . . 4  wff  ( x  =  0  /\  y  =  0 )
11 vn . . . . . . . . 9  setvar  n
1211cv 1311 . . . . . . . 8  class  n
13 cdvds 11335 . . . . . . . 8  class  ||
1412, 5, 13wbr 3893 . . . . . . 7  wff  n  ||  x
1512, 8, 13wbr 3893 . . . . . . 7  wff  n  ||  y
1614, 15wa 103 . . . . . 6  wff  ( n 
||  x  /\  n  ||  y )
1716, 11, 4crab 2392 . . . . 5  class  { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) }
18 cr 7540 . . . . 5  class  RR
19 clt 7718 . . . . 5  class  <
2017, 18, 19csup 6819 . . . 4  class  sup ( { n  e.  ZZ  |  ( n  ||  x  /\  n  ||  y
) } ,  RR ,  <  )
2110, 6, 20cif 3438 . . 3  class  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) )
222, 3, 4, 4, 21cmpo 5728 . 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 1312 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  11490  gcdf  11503
  Copyright terms: Public domain W3C validator