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

Metamath Proof Explorer

Theorem gcdf

Description: Domain and codomain of the gcd operator. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Assertion gcdf 
|- gcd : ( ZZ X. ZZ ) --> NN0

Proof

Step Hyp Ref Expression
1 gcdval 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x gcd y ) = if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
2 gcdcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x gcd y ) e. NN0 )
3 1 2 eqeltrrd 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) e. NN0 )
4 3 rgen2 
 |-  A. x e. ZZ A. y e. ZZ if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) e. NN0
5 df-gcd 
 |-  gcd = ( x e. ZZ , y e. ZZ |-> if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) )
6 5 fmpo 
 |-  ( A. x e. ZZ A. y e. ZZ if ( ( x = 0 /\ y = 0 ) , 0 , sup ( { n e. ZZ | ( n || x /\ n || y ) } , RR , < ) ) e. NN0 <-> gcd : ( ZZ X. ZZ ) --> NN0 )
7 4 6 mpbi 
 |-  gcd : ( ZZ X. ZZ ) --> NN0