Metamath Proof Explorer


Theorem gcdcomnni

Description: Commutative law for gcd. (Contributed by metakunt, 25-Apr-2024)

Ref Expression
Hypotheses gcdcomnni.1
|- M e. NN
gcdcomnni.2
|- N e. NN
Assertion gcdcomnni
|- ( M gcd N ) = ( N gcd M )

Proof

Step Hyp Ref Expression
1 gcdcomnni.1
 |-  M e. NN
2 gcdcomnni.2
 |-  N e. NN
3 1 nnzi
 |-  M e. ZZ
4 2 nnzi
 |-  N e. ZZ
5 3 4 pm3.2i
 |-  ( M e. ZZ /\ N e. ZZ )
6 gcdcom
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd N ) = ( N gcd M ) )
7 5 6 ax-mp
 |-  ( M gcd N ) = ( N gcd M )