This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-gcd

Description: Define the gcd operator. For example, ( -u 6 gcd 9 ) = 3 ( ex-gcd ). For an alternate definition, based on the definition in ApostolNT p. 15, see dfgcd2 . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion df-gcd 
|- gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgcd 
 |-  gcd
1 vx 
 |-  x
2 cz 
 |-  ZZ
3 vy 
 |-  y
4 1 cv 
 |-  x
5 cc0 
 |-  0
6 4 5 wceq 
 |-  x = 0
7 3 cv 
 |-  y
8 7 5 wceq 
 |-  y = 0
9 6 8 wa 
 |-  ( x = 0 /\ y = 0 )
10 vn 
 |-  n
11 10 cv 
 |-  n
12 cdvds 
 |-  ||
13 11 4 12 wbr 
 |-  n || x
14 11 7 12 wbr 
 |-  n || y
15 13 14 wa 
 |-  ( n || x /\ n || y )
16 15 10 2 crab 
 |-  { n e. ZZ | ( n || x /\ n || y ) }
17 cr 
 |-  RR
18 clt 
 |-  <
19 16 17 18 csup 
 |-  sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < )
20 9 5 19 cif 
 |-  if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) )
21 1 3 2 2 20 cmpo 
 |-  ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
22 0 21 wceq 
 |-  gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )