Theorem gcdaddmzz2nni

Description: Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by metakunt, 25-Apr-2024)

	Ref	Expression
Hypotheses	gcdaddmzz2nni.1	$$⊢M\in \mathbb{N}$$
	gcdaddmzz2nni.2	$$⊢N\in \mathbb{N}$$
	gcdaddmzz2nni.3	$$⊢K\in \mathbb{Z}$$
Assertion	gcdaddmzz2nni	$$⊢M\gcd N=M\gcd \left(N+K\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$

Proof

Step	Hyp	Ref	Expression
1		gcdaddmzz2nni.1	$$⊢M\in \mathbb{N}$$
2		gcdaddmzz2nni.2	$$⊢N\in \mathbb{N}$$
3		gcdaddmzz2nni.3	$$⊢K\in \mathbb{Z}$$
4	1	nnzi	$$⊢M\in \mathbb{Z}$$
5	2	nnzi	$$⊢N\in \mathbb{Z}$$
6	3 4 5	3pm3.2i	$$⊢\left(K\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)$$
7		gcdaddm	$$⊢\left(K\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to M\gcd N=M\gcd \left(N+K\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
8	6 7	ax-mp	$$⊢M\gcd N=M\gcd \left(N+K\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$