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

Metamath Proof Explorer

Theorem gcdcld

Description: Closure of the gcd operator. (Contributed by Mario Carneiro, 29-May-2016)

Ref Expression
Hypotheses gcdcld.1 
|- ( ph -> M e. ZZ )
gcdcld.2 
|- ( ph -> N e. ZZ )
Assertion gcdcld 
|- ( ph -> ( M gcd N ) e. NN0 )

Proof

Step Hyp Ref Expression
1 gcdcld.1 
 |-  ( ph -> M e. ZZ )
2 gcdcld.2 
 |-  ( ph -> N e. ZZ )
3 gcdcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) e. NN0 )
4 1 2 3 syl2anc 
 |-  ( ph -> ( M gcd N ) e. NN0 )