Metamath Proof Explorer

Theorem gcd0val

Description: The value, by convention, of the gcd operator when both operands are 0. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcd0val 
|- ( 0 gcd 0 ) = 0

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 gcdval 
 |-  ( ( 0 e. ZZ /\ 0 e. ZZ ) -> ( 0 gcd 0 ) = if ( ( 0 = 0 /\ 0 = 0 ) , 0 , sup ( { n e. ZZ | ( n || 0 /\ n || 0 ) } , RR , < ) ) )
3 1 1 2 mp2an 
 |-  ( 0 gcd 0 ) = if ( ( 0 = 0 /\ 0 = 0 ) , 0 , sup ( { n e. ZZ | ( n || 0 /\ n || 0 ) } , RR , < ) )
4 eqid 
 |-  0 = 0
5 iftrue 
 |-  ( ( 0 = 0 /\ 0 = 0 ) -> if ( ( 0 = 0 /\ 0 = 0 ) , 0 , sup ( { n e. ZZ | ( n || 0 /\ n || 0 ) } , RR , < ) ) = 0 )
6 4 4 5 mp2an 
 |-  if ( ( 0 = 0 /\ 0 = 0 ) , 0 , sup ( { n e. ZZ | ( n || 0 /\ n || 0 ) } , RR , < ) ) = 0
7 3 6 eqtri 
 |-  ( 0 gcd 0 ) = 0