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 ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑘 = 1 → ( 𝑀 · 𝑘 ) = ( 𝑀 · 1 ) )
2 1 oveq2d ⊢ ( 𝑘 = 1 → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = ( 𝑀 gcd ( 𝑀 · 1 ) ) )
3 2 eqeq1d ⊢ ( 𝑘 = 1 → ( ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ↔ ( 𝑀 gcd ( 𝑀 · 1 ) ) = 𝑀 ) )
4 3 imbi2d ⊢ ( 𝑘 = 1 → ( ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 1 ) ) = 𝑀 ) ) )
5 oveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝑀 · 𝑘 ) = ( 𝑀 · 𝑛 ) )
6 5 oveq2d ⊢ ( 𝑘 = 𝑛 → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) )
7 6 eqeq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ↔ ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = 𝑀 ) )
8 7 imbi2d ⊢ ( 𝑘 = 𝑛 → ( ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = 𝑀 ) ) )
9 oveq2 ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝑀 · 𝑘 ) = ( 𝑀 · ( 𝑛 + 1 ) ) )
10 9 oveq2d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) )
11 10 eqeq1d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ↔ ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) = 𝑀 ) )
12 11 imbi2d ⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) = 𝑀 ) ) )
13 oveq2 ⊢ ( 𝑘 = 𝑁 → ( 𝑀 · 𝑘 ) = ( 𝑀 · 𝑁 ) )
14 13 oveq2d ⊢ ( 𝑘 = 𝑁 → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) )
15 14 eqeq1d ⊢ ( 𝑘 = 𝑁 → ( ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ↔ ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 ) )
16 15 imbi2d ⊢ ( 𝑘 = 𝑁 → ( ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑘 ) ) = 𝑀 ) ↔ ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 ) ) )
17 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
18 17 mulid1d ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 · 1 ) = 𝑀 )
19 18 oveq2d ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 1 ) ) = ( 𝑀 gcd 𝑀 ) )
20 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
21 gcdid ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 𝑀 ) = ( abs ‘ 𝑀 ) )
22 20 21 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 gcd 𝑀 ) = ( abs ‘ 𝑀 ) )
23 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
24 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
25 24 nn0ge0d ⊢ ( 𝑀 ∈ ℕ → 0 ≤ 𝑀 )
26 23 25 absidd ⊢ ( 𝑀 ∈ ℕ → ( abs ‘ 𝑀 ) = 𝑀 )
27 22 26 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 gcd 𝑀 ) = 𝑀 )
28 19 27 eqtrd ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 1 ) ) = 𝑀 )
29 1z ⊢ 1 ∈ ℤ
30 nnz ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℤ )
31 zmulcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑀 · 𝑛 ) ∈ ℤ )
32 20 30 31 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑀 · 𝑛 ) ∈ ℤ )
33 gcdaddm ⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑀 · 𝑛 ) ∈ ℤ ) → ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = ( 𝑀 gcd ( ( 𝑀 · 𝑛 ) + ( 1 · 𝑀 ) ) ) )
34 29 20 32 33 mp3an2ani ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = ( 𝑀 gcd ( ( 𝑀 · 𝑛 ) + ( 1 · 𝑀 ) ) ) )
35 nncn ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℂ )
36 ax-1cn ⊢ 1 ∈ ℂ
37 adddi ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑀 · ( 𝑛 + 1 ) ) = ( ( 𝑀 · 𝑛 ) + ( 𝑀 · 1 ) ) )
38 36 37 mp3an3 ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑀 · ( 𝑛 + 1 ) ) = ( ( 𝑀 · 𝑛 ) + ( 𝑀 · 1 ) ) )
39 mulcom ⊢ ( ( 𝑀 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑀 · 1 ) = ( 1 · 𝑀 ) )
40 36 39 mpan2 ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 · 1 ) = ( 1 · 𝑀 ) )
41 40 adantr ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑀 · 1 ) = ( 1 · 𝑀 ) )
42 41 oveq2d ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( ( 𝑀 · 𝑛 ) + ( 𝑀 · 1 ) ) = ( ( 𝑀 · 𝑛 ) + ( 1 · 𝑀 ) ) )
43 38 42 eqtrd ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑛 ∈ ℂ ) → ( 𝑀 · ( 𝑛 + 1 ) ) = ( ( 𝑀 · 𝑛 ) + ( 1 · 𝑀 ) ) )
44 17 35 43 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑀 · ( 𝑛 + 1 ) ) = ( ( 𝑀 · 𝑛 ) + ( 1 · 𝑀 ) ) )
45 44 oveq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) = ( 𝑀 gcd ( ( 𝑀 · 𝑛 ) + ( 1 · 𝑀 ) ) ) )
46 34 45 eqtr4d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) )
47 46 eqeq1d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = 𝑀 ↔ ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) = 𝑀 ) )
48 47 biimpd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑛 ∈ ℕ ) → ( ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = 𝑀 → ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) = 𝑀 ) )
49 48 expcom ⊢ ( 𝑛 ∈ ℕ → ( 𝑀 ∈ ℕ → ( ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = 𝑀 → ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) = 𝑀 ) ) )
50 49 a2d ⊢ ( 𝑛 ∈ ℕ → ( ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑛 ) ) = 𝑀 ) → ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · ( 𝑛 + 1 ) ) ) = 𝑀 ) ) )
51 4 8 12 16 28 50 nnind ⊢ ( 𝑁 ∈ ℕ → ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 ) )
52 51 impcom ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )