Metamath Proof Explorer


Theorem gcdaddmzz2nncomi

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 gcdaddmzz2nncomi.1 M
gcdaddmzz2nncomi.2 N
gcdaddmzz2nncomi.3 K
Assertion gcdaddmzz2nncomi M gcd N = M gcd K M + N

Proof

Step Hyp Ref Expression
1 gcdaddmzz2nncomi.1 M
2 gcdaddmzz2nncomi.2 N
3 gcdaddmzz2nncomi.3 K
4 1 2 3 gcdaddmzz2nni M gcd N = M gcd N + K M
5 2 nncni N
6 zcn K K
7 3 6 ax-mp K
8 1 nncni M
9 7 8 mulcli K M
10 5 9 addcomi N + K M = K M + N
11 10 oveq2i M gcd N + K M = M gcd K M + N
12 4 11 eqtri M gcd N = M gcd K M + N