# Metamath Proof Explorer

## Theorem gcdmultipleOLD

Description: Obsolete proof of gcdmultiple as of 12-Jan-2024. The GCD of a multiple of a number is the number itself. (Contributed by Scott Fenton, 12-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion gcdmultipleOLD ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\right)\to {M}\mathrm{gcd}{M}\cdot {N}={M}$

### Proof

Step Hyp Ref Expression
1 oveq2 ${⊢}{k}=1\to {M}{k}={M}\cdot 1$
2 1 oveq2d ${⊢}{k}=1\to {M}\mathrm{gcd}{M}{k}={M}\mathrm{gcd}{M}\cdot 1$
3 2 eqeq1d ${⊢}{k}=1\to \left({M}\mathrm{gcd}{M}{k}={M}↔{M}\mathrm{gcd}{M}\cdot 1={M}\right)$
4 3 imbi2d ${⊢}{k}=1\to \left(\left({M}\in ℕ\to {M}\mathrm{gcd}{M}{k}={M}\right)↔\left({M}\in ℕ\to {M}\mathrm{gcd}{M}\cdot 1={M}\right)\right)$
5 oveq2 ${⊢}{k}={n}\to {M}{k}={M}{n}$
6 5 oveq2d ${⊢}{k}={n}\to {M}\mathrm{gcd}{M}{k}={M}\mathrm{gcd}{M}{n}$
7 6 eqeq1d ${⊢}{k}={n}\to \left({M}\mathrm{gcd}{M}{k}={M}↔{M}\mathrm{gcd}{M}{n}={M}\right)$
8 7 imbi2d ${⊢}{k}={n}\to \left(\left({M}\in ℕ\to {M}\mathrm{gcd}{M}{k}={M}\right)↔\left({M}\in ℕ\to {M}\mathrm{gcd}{M}{n}={M}\right)\right)$
9 oveq2 ${⊢}{k}={n}+1\to {M}{k}={M}\left({n}+1\right)$
10 9 oveq2d ${⊢}{k}={n}+1\to {M}\mathrm{gcd}{M}{k}={M}\mathrm{gcd}{M}\left({n}+1\right)$
11 10 eqeq1d ${⊢}{k}={n}+1\to \left({M}\mathrm{gcd}{M}{k}={M}↔{M}\mathrm{gcd}{M}\left({n}+1\right)={M}\right)$
12 11 imbi2d ${⊢}{k}={n}+1\to \left(\left({M}\in ℕ\to {M}\mathrm{gcd}{M}{k}={M}\right)↔\left({M}\in ℕ\to {M}\mathrm{gcd}{M}\left({n}+1\right)={M}\right)\right)$
13 oveq2 ${⊢}{k}={N}\to {M}{k}={M}\cdot {N}$
14 13 oveq2d ${⊢}{k}={N}\to {M}\mathrm{gcd}{M}{k}={M}\mathrm{gcd}{M}\cdot {N}$
15 14 eqeq1d ${⊢}{k}={N}\to \left({M}\mathrm{gcd}{M}{k}={M}↔{M}\mathrm{gcd}{M}\cdot {N}={M}\right)$
16 15 imbi2d ${⊢}{k}={N}\to \left(\left({M}\in ℕ\to {M}\mathrm{gcd}{M}{k}={M}\right)↔\left({M}\in ℕ\to {M}\mathrm{gcd}{M}\cdot {N}={M}\right)\right)$
17 nncn ${⊢}{M}\in ℕ\to {M}\in ℂ$
18 17 mulid1d ${⊢}{M}\in ℕ\to {M}\cdot 1={M}$
19 18 oveq2d ${⊢}{M}\in ℕ\to {M}\mathrm{gcd}{M}\cdot 1={M}\mathrm{gcd}{M}$
20 nnz ${⊢}{M}\in ℕ\to {M}\in ℤ$
21 gcdid ${⊢}{M}\in ℤ\to {M}\mathrm{gcd}{M}=\left|{M}\right|$
22 20 21 syl ${⊢}{M}\in ℕ\to {M}\mathrm{gcd}{M}=\left|{M}\right|$
23 nnre ${⊢}{M}\in ℕ\to {M}\in ℝ$
24 nnnn0 ${⊢}{M}\in ℕ\to {M}\in {ℕ}_{0}$
25 24 nn0ge0d ${⊢}{M}\in ℕ\to 0\le {M}$
26 23 25 absidd ${⊢}{M}\in ℕ\to \left|{M}\right|={M}$
27 22 26 eqtrd ${⊢}{M}\in ℕ\to {M}\mathrm{gcd}{M}={M}$
28 19 27 eqtrd ${⊢}{M}\in ℕ\to {M}\mathrm{gcd}{M}\cdot 1={M}$
29 1z ${⊢}1\in ℤ$
30 nnz ${⊢}{n}\in ℕ\to {n}\in ℤ$
31 zmulcl ${⊢}\left({M}\in ℤ\wedge {n}\in ℤ\right)\to {M}{n}\in ℤ$
32 20 30 31 syl2an ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to {M}{n}\in ℤ$
33 gcdaddm ${⊢}\left(1\in ℤ\wedge {M}\in ℤ\wedge {M}{n}\in ℤ\right)\to {M}\mathrm{gcd}{M}{n}={M}\mathrm{gcd}\left({M}{n}+1\cdot {M}\right)$
34 29 20 32 33 mp3an2ani ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to {M}\mathrm{gcd}{M}{n}={M}\mathrm{gcd}\left({M}{n}+1\cdot {M}\right)$
35 nncn ${⊢}{n}\in ℕ\to {n}\in ℂ$
36 ax-1cn ${⊢}1\in ℂ$
37 adddi ${⊢}\left({M}\in ℂ\wedge {n}\in ℂ\wedge 1\in ℂ\right)\to {M}\left({n}+1\right)={M}{n}+{M}\cdot 1$
38 36 37 mp3an3 ${⊢}\left({M}\in ℂ\wedge {n}\in ℂ\right)\to {M}\left({n}+1\right)={M}{n}+{M}\cdot 1$
39 mulcom ${⊢}\left({M}\in ℂ\wedge 1\in ℂ\right)\to {M}\cdot 1=1\cdot {M}$
40 36 39 mpan2 ${⊢}{M}\in ℂ\to {M}\cdot 1=1\cdot {M}$
41 40 adantr ${⊢}\left({M}\in ℂ\wedge {n}\in ℂ\right)\to {M}\cdot 1=1\cdot {M}$
42 41 oveq2d ${⊢}\left({M}\in ℂ\wedge {n}\in ℂ\right)\to {M}{n}+{M}\cdot 1={M}{n}+1\cdot {M}$
43 38 42 eqtrd ${⊢}\left({M}\in ℂ\wedge {n}\in ℂ\right)\to {M}\left({n}+1\right)={M}{n}+1\cdot {M}$
44 17 35 43 syl2an ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to {M}\left({n}+1\right)={M}{n}+1\cdot {M}$
45 44 oveq2d ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to {M}\mathrm{gcd}{M}\left({n}+1\right)={M}\mathrm{gcd}\left({M}{n}+1\cdot {M}\right)$
46 34 45 eqtr4d ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to {M}\mathrm{gcd}{M}{n}={M}\mathrm{gcd}{M}\left({n}+1\right)$
47 46 eqeq1d ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to \left({M}\mathrm{gcd}{M}{n}={M}↔{M}\mathrm{gcd}{M}\left({n}+1\right)={M}\right)$
48 47 biimpd ${⊢}\left({M}\in ℕ\wedge {n}\in ℕ\right)\to \left({M}\mathrm{gcd}{M}{n}={M}\to {M}\mathrm{gcd}{M}\left({n}+1\right)={M}\right)$
49 48 expcom ${⊢}{n}\in ℕ\to \left({M}\in ℕ\to \left({M}\mathrm{gcd}{M}{n}={M}\to {M}\mathrm{gcd}{M}\left({n}+1\right)={M}\right)\right)$
50 49 a2d ${⊢}{n}\in ℕ\to \left(\left({M}\in ℕ\to {M}\mathrm{gcd}{M}{n}={M}\right)\to \left({M}\in ℕ\to {M}\mathrm{gcd}{M}\left({n}+1\right)={M}\right)\right)$
51 4 8 12 16 28 50 nnind ${⊢}{N}\in ℕ\to \left({M}\in ℕ\to {M}\mathrm{gcd}{M}\cdot {N}={M}\right)$
52 51 impcom ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\right)\to {M}\mathrm{gcd}{M}\cdot {N}={M}$