Metamath Proof Explorer


Theorem gcdcomnni

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

Ref Expression
Hypotheses gcdcomnni.1 M
gcdcomnni.2 N
Assertion gcdcomnni M gcd N = N gcd M

Proof

Step Hyp Ref Expression
1 gcdcomnni.1 M
2 gcdcomnni.2 N
3 1 nnzi M
4 2 nnzi N
5 3 4 pm3.2i M N
6 gcdcom M N M gcd N = N gcd M
7 5 6 ax-mp M gcd N = N gcd M