Metamath Proof Explorer

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 ∈ ℕ
gcdaddmzz2nni.2 ⊢ N ∈ ℕ
gcdaddmzz2nni.3 ⊢ K ∈ ℤ
Assertion gcdaddmzz2nni ⊢ M gcd N = M gcd N + K ⋅ M

Proof

Step Hyp Ref Expression
1 gcdaddmzz2nni.1 ⊢ M ∈ ℕ
2 gcdaddmzz2nni.2 ⊢ N ∈ ℕ
3 gcdaddmzz2nni.3 ⊢ K ∈ ℤ
4 1 nnzi ⊢ M ∈ ℤ
5 2 nnzi ⊢ N ∈ ℤ
6 3 4 5 3pm3.2i ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ
7 gcdaddm ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N + K ⋅ M
8 6 7 ax-mp ⊢ M gcd N = M gcd N + K ⋅ M