Metamath Proof Explorer


Theorem neggcdnni

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

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

Proof

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