Theorem gcdnegnni

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

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

Proof

Step	Hyp	Ref	Expression
1		gcdnegnni.1	|- M e. NN
2		gcdnegnni.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		gcdneg	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M gcd -u N ) = ( M gcd N ) )
7	5 6	ax-mp	|- ( M gcd -u N ) = ( M gcd N )