MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-gcd Unicode version

Definition df-gcd 12681
Description: Define the  gcd operator. (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 12680 . 2  class  gcd
2 vx . . 3  set  x
3 vy . . 3  set  y
4 cz 10020 . . 3  class  ZZ
52cv 1623 . . . . . 6  class  x
6 cc0 8733 . . . . . 6  class  0
75, 6wceq 1624 . . . . 5  wff  x  =  0
83cv 1623 . . . . . 6  class  y
98, 6wceq 1624 . . . . 5  wff  y  =  0
107, 9wa 360 . . . 4  wff  ( x  =  0  /\  y  =  0 )
11 vn . . . . . . . . 9  set  n
1211cv 1623 . . . . . . . 8  class  n
13 cdivides 12526 . . . . . . . 8  class  ||
1412, 5, 13wbr 4025 . . . . . . 7  wff  n  ||  x
1512, 8, 13wbr 4025 . . . . . . 7  wff  n  ||  y
1614, 15wa 360 . . . . . 6  wff  ( n 
||  x  /\  n  ||  y )
1716, 11, 4crab 2549 . . . . 5  class  { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) }
18 cr 8732 . . . . 5  class  RR
19 clt 8863 . . . . 5  class  <
2017, 18, 19csup 7189 . . . 4  class  sup ( { n  e.  ZZ  |  ( n  ||  x  /\  n  ||  y
) } ,  RR ,  <  )
2110, 6, 20cif 3567 . . 3  class  if ( ( x  =  0  /\  y  =  0 ) ,  0 ,  sup ( { n  e.  ZZ  |  ( n 
||  x  /\  n  ||  y ) } ,  RR ,  <  ) )
222, 3, 4, 4, 21cmpt2 5822 . 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 1624 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  12682  gcdf  12693
  Copyright terms: Public domain W3C validator