Theorem gcdnegnni

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

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

Proof

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