Metamath Proof Explorer


Theorem neggcdnni

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

Ref Expression
Hypotheses neggcdnni.1 𝑀 ∈ ℕ
neggcdnni.2 𝑁 ∈ ℕ
Assertion neggcdnni ( - 𝑀 gcd 𝑁 ) = ( 𝑀 gcd 𝑁 )

Proof

Step Hyp Ref Expression
1 neggcdnni.1 𝑀 ∈ ℕ
2 neggcdnni.2 𝑁 ∈ ℕ
3 1 nnzi 𝑀 ∈ ℤ
4 2 nnzi 𝑁 ∈ ℤ
5 3 4 pm3.2i ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ )
6 neggcd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( - 𝑀 gcd 𝑁 ) = ( 𝑀 gcd 𝑁 ) )
7 5 6 ax-mp ( - 𝑀 gcd 𝑁 ) = ( 𝑀 gcd 𝑁 )