Metamath Proof Explorer

Theorem gcdaddm

Description: Adding a multiple of one operand of the gcd operator to the other does not alter the result. (Contributed by Paul Chapman, 31-Mar-2011)

Ref Expression
Assertion gcdaddm ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N + K ⋅ M

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ K = if K ∈ ℤ K 0 → K ⋅ M = if K ∈ ℤ K 0 ⋅ M
2 1 oveq1d ⊢ K = if K ∈ ℤ K 0 → K ⋅ M + N = if K ∈ ℤ K 0 ⋅ M + N
3 2 oveq2d ⊢ K = if K ∈ ℤ K 0 → M gcd K ⋅ M + N = M gcd if K ∈ ℤ K 0 ⋅ M + N
4 3 eqeq2d ⊢ K = if K ∈ ℤ K 0 → M gcd N = M gcd K ⋅ M + N ↔ M gcd N = M gcd if K ∈ ℤ K 0 ⋅ M + N
5 oveq1 ⊢ M = if M ∈ ℤ M 0 → M gcd N = if M ∈ ℤ M 0 gcd N
6 id ⊢ M = if M ∈ ℤ M 0 → M = if M ∈ ℤ M 0
7 oveq2 ⊢ M = if M ∈ ℤ M 0 → if K ∈ ℤ K 0 ⋅ M = if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0
8 7 oveq1d ⊢ M = if M ∈ ℤ M 0 → if K ∈ ℤ K 0 ⋅ M + N = if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + N
9 6 8 oveq12d ⊢ M = if M ∈ ℤ M 0 → M gcd if K ∈ ℤ K 0 ⋅ M + N = if M ∈ ℤ M 0 gcd if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + N
10 5 9 eqeq12d ⊢ M = if M ∈ ℤ M 0 → M gcd N = M gcd if K ∈ ℤ K 0 ⋅ M + N ↔ if M ∈ ℤ M 0 gcd N = if M ∈ ℤ M 0 gcd if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + N
11 oveq2 ⊢ N = if N ∈ ℤ N 0 → if M ∈ ℤ M 0 gcd N = if M ∈ ℤ M 0 gcd if N ∈ ℤ N 0
12 oveq2 ⊢ N = if N ∈ ℤ N 0 → if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + N = if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + if N ∈ ℤ N 0
13 12 oveq2d ⊢ N = if N ∈ ℤ N 0 → if M ∈ ℤ M 0 gcd if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + N = if M ∈ ℤ M 0 gcd if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + if N ∈ ℤ N 0
14 11 13 eqeq12d ⊢ N = if N ∈ ℤ N 0 → if M ∈ ℤ M 0 gcd N = if M ∈ ℤ M 0 gcd if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + N ↔ if M ∈ ℤ M 0 gcd if N ∈ ℤ N 0 = if M ∈ ℤ M 0 gcd if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + if N ∈ ℤ N 0
15 0z ⊢ 0 ∈ ℤ
16 15 elimel ⊢ if K ∈ ℤ K 0 ∈ ℤ
17 15 elimel ⊢ if M ∈ ℤ M 0 ∈ ℤ
18 15 elimel ⊢ if N ∈ ℤ N 0 ∈ ℤ
19 16 17 18 gcdaddmlem ⊢ if M ∈ ℤ M 0 gcd if N ∈ ℤ N 0 = if M ∈ ℤ M 0 gcd if K ∈ ℤ K 0 ⁢ if M ∈ ℤ M 0 + if N ∈ ℤ N 0
20 4 10 14 19 dedth3h ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd K ⋅ M + N
21 zcn ⊢ K ∈ ℤ → K ∈ ℂ
22 zcn ⊢ M ∈ ℤ → M ∈ ℂ
23 mulcl ⊢ K ∈ ℂ ∧ M ∈ ℂ → K ⋅ M ∈ ℂ
24 21 22 23 syl2an ⊢ K ∈ ℤ ∧ M ∈ ℤ → K ⋅ M ∈ ℂ
25 zcn ⊢ N ∈ ℤ → N ∈ ℂ
26 addcom ⊢ K ⋅ M ∈ ℂ ∧ N ∈ ℂ → K ⋅ M + N = N + K ⋅ M
27 24 25 26 syl2an ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ⋅ M + N = N + K ⋅ M
28 27 3impa ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ⋅ M + N = N + K ⋅ M
29 28 oveq2d ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M gcd K ⋅ M + N = M gcd N + K ⋅ M
30 20 29 eqtrd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → M gcd N = M gcd N + K ⋅ M