Theorem gcdcomnni

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

	Ref	Expression
Hypotheses	gcdcomnni.1	$$⊢M\in \mathbb{N}$$
	gcdcomnni.2	$$⊢N\in \mathbb{N}$$
Assertion	gcdcomnni	$$⊢M\gcd N=N\gcd M$$

Proof

Step	Hyp	Ref	Expression
1		gcdcomnni.1	$$⊢M\in \mathbb{N}$$
2		gcdcomnni.2	$$⊢N\in \mathbb{N}$$
3	1	nnzi	$$⊢M\in \mathbb{Z}$$
4	2	nnzi	$$⊢N\in \mathbb{Z}$$
5	3 4	pm3.2i	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)$$
6		gcdcom	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\gcd N=N\gcd M$$
7	5 6	ax-mp	$$⊢M\gcd N=N\gcd M$$