Theorem gcdnegnni

Description: Negation invariance for gcd. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Hypotheses	gcdnegnni.1	$$⊢M\in \mathbb{N}$$
	gcdnegnni.2	$$⊢N\in \mathbb{N}$$
Assertion	gcdnegnni	$$⊢M\gcd \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=M\gcd N$$

Proof

Step	Hyp	Ref	Expression
1		gcdnegnni.1	$$⊢M\in \mathbb{N}$$
2		gcdnegnni.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		gcdneg	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\gcd \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=M\gcd N$$
7	5 6	ax-mp	$$⊢M\gcd \mathrm{-\; <mi\; mathcolor="\#808">N</mi>}=M\gcd N$$