Metamath Proof Explorer

Theorem gcdcl

Description: Closure of the gcd operator. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion gcdcl 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )

Proof

Step Hyp Ref Expression
1 oveq12 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) = ( 0 gcd 0 ) )
2 gcd0val 
 |-  ( 0 gcd 0 ) = 0
3 1 2 eqtrdi 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) = 0 )
4 0nn0 
 |-  0 e. NN0
5 3 4 eqeltrdi 
 |-  ( ( M = 0 /\ N = 0 ) -> ( M gcd N ) e. NN0 )
6 5 adantl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN0 )
7 gcdn0cl 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN )
8 7 nnnn0d 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ -. ( M = 0 /\ N = 0 ) ) -> ( M gcd N ) e. NN0 )
9 6 8 pm2.61dan 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )