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∈ℤ→MgcdN=MgcdN+K⋅ M

Proof

Step Hyp Ref Expression
1 oveq1 ⊢K=ifK∈ℤK0→K⋅ M=ifK∈ℤK0⋅ M
2 1 oveq1d ⊢K=ifK∈ℤK0→K⋅ M+N=ifK∈ℤK0⋅ M+N
3 2 oveq2d ⊢K=ifK∈ℤK0→MgcdK⋅ M+N=MgcdifK∈ℤK0⋅ M+N
4 3 eqeq2d ⊢K=ifK∈ℤK0→MgcdN=MgcdK⋅ M+N↔MgcdN=MgcdifK∈ℤK0⋅ M+N
5 oveq1 ⊢M=ifM∈ℤM0→MgcdN=ifM∈ℤM0gcdN
6 id ⊢M=ifM∈ℤM0→M=ifM∈ℤM0
7 oveq2 ⊢M=ifM∈ℤM0→ifK∈ℤK0⋅ M=ifK∈ℤK0⁢ifM∈ℤM0
8 7 oveq1d ⊢M=ifM∈ℤM0→ifK∈ℤK0⋅ M+N=ifK∈ℤK0⁢ifM∈ℤM0+N
9 6 8 oveq12d ⊢M=ifM∈ℤM0→MgcdifK∈ℤK0⋅ M+N=ifM∈ℤM0gcdifK∈ℤK0⁢ifM∈ℤM0+N
10 5 9 eqeq12d ⊢M=ifM∈ℤM0→MgcdN=MgcdifK∈ℤK0⋅ M+N↔ifM∈ℤM0gcdN=ifM∈ℤM0gcdifK∈ℤK0⁢ifM∈ℤM0+N
11 oveq2 ⊢N=ifN∈ℤN0→ifM∈ℤM0gcdN=ifM∈ℤM0gcdifN∈ℤN0
12 oveq2 ⊢N=ifN∈ℤN0→ifK∈ℤK0⁢ifM∈ℤM0+N=ifK∈ℤK0⁢ifM∈ℤM0+ifN∈ℤN0
13 12 oveq2d ⊢N=ifN∈ℤN0→ifM∈ℤM0gcdifK∈ℤK0⁢ifM∈ℤM0+N=ifM∈ℤM0gcdifK∈ℤK0⁢ifM∈ℤM0+ifN∈ℤN0
14 11 13 eqeq12d ⊢N=ifN∈ℤN0→ifM∈ℤM0gcdN=ifM∈ℤM0gcdifK∈ℤK0⁢ifM∈ℤM0+N↔ifM∈ℤM0gcdifN∈ℤN0=ifM∈ℤM0gcdifK∈ℤK0⁢ifM∈ℤM0+ifN∈ℤN0
15 0z ⊢0∈ℤ
16 15 elimel ⊢ifK∈ℤK0∈ℤ
17 15 elimel ⊢ifM∈ℤM0∈ℤ
18 15 elimel ⊢ifN∈ℤN0∈ℤ
19 16 17 18 gcdaddmlem ⊢ifM∈ℤM0gcdifN∈ℤN0=ifM∈ℤM0gcdifK∈ℤK0⁢ifM∈ℤM0+ifN∈ℤN0
20 4 10 14 19 dedth3h ⊢K∈ℤ∧M∈ℤ∧N∈ℤ→MgcdN=MgcdK⋅ 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∈ℤ→MgcdK⋅ M+N=MgcdN+K⋅ M
30 20 29 eqtrd ⊢K∈ℤ∧M∈ℤ∧N∈ℤ→MgcdN=MgcdN+K⋅ M