Metamath Proof Explorer


Theorem neggcdnni

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

Ref Expression
Hypotheses neggcdnni.1 M
neggcdnni.2 N
Assertion neggcdnni -M gcd N = M gcd N

Proof

Step Hyp Ref Expression
1 neggcdnni.1 M
2 neggcdnni.2 N
3 1 nnzi M
4 2 nnzi N
5 3 4 pm3.2i M N
6 neggcd M N -M gcd N = M gcd N
7 5 6 ax-mp -M gcd N = M gcd N