Theorem neggcdnni

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

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

Proof

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