Metamath Proof Explorer

Theorem gcdmultiplezOLD

Description: Obsolete proof of gcdmultiplez as of 12-Jan-2024. Extend gcdmultiple so N can be an integer. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion gcdmultiplezOLD ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑁 = 0 → ( 𝑀 · 𝑁 ) = ( 𝑀 · 0 ) )
2 1 oveq2d ⊢ ( 𝑁 = 0 → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = ( 𝑀 gcd ( 𝑀 · 0 ) ) )
3 2 eqeq1d ⊢ ( 𝑁 = 0 → ( ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 ↔ ( 𝑀 gcd ( 𝑀 · 0 ) ) = 𝑀 ) )
4 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
5 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
6 absmul ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( ( abs ‘ 𝑀 ) · ( abs ‘ 𝑁 ) ) )
7 4 5 6 syl2an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( ( abs ‘ 𝑀 ) · ( abs ‘ 𝑁 ) ) )
8 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
9 nnnn0 ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℕ0 )
10 9 nn0ge0d ⊢ ( 𝑀 ∈ ℕ → 0 ≤ 𝑀 )
11 8 10 absidd ⊢ ( 𝑀 ∈ ℕ → ( abs ‘ 𝑀 ) = 𝑀 )
12 11 oveq1d ⊢ ( 𝑀 ∈ ℕ → ( ( abs ‘ 𝑀 ) · ( abs ‘ 𝑁 ) ) = ( 𝑀 · ( abs ‘ 𝑁 ) ) )
13 12 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) · ( abs ‘ 𝑁 ) ) = ( 𝑀 · ( abs ‘ 𝑁 ) ) )
14 7 13 eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝑀 · 𝑁 ) ) = ( 𝑀 · ( abs ‘ 𝑁 ) ) )
15 14 oveq2d ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( abs ‘ ( 𝑀 · 𝑁 ) ) ) = ( 𝑀 gcd ( 𝑀 · ( abs ‘ 𝑁 ) ) ) )
16 15 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( 𝑀 gcd ( abs ‘ ( 𝑀 · 𝑁 ) ) ) = ( 𝑀 gcd ( 𝑀 · ( abs ‘ 𝑁 ) ) ) )
17 simpll ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → 𝑀 ∈ ℕ )
18 17 nnzd ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → 𝑀 ∈ ℤ )
19 nnz ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℤ )
20 zmulcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
21 19 20 sylan ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
22 21 adantr ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( 𝑀 · 𝑁 ) ∈ ℤ )
23 gcdabs2 ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑀 · 𝑁 ) ∈ ℤ ) → ( 𝑀 gcd ( abs ‘ ( 𝑀 · 𝑁 ) ) ) = ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) )
24 18 22 23 syl2anc ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( 𝑀 gcd ( abs ‘ ( 𝑀 · 𝑁 ) ) ) = ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) )
25 nnabscl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) → ( abs ‘ 𝑁 ) ∈ ℕ )
26 gcdmultiple ⊢ ( ( 𝑀 ∈ ℕ ∧ ( abs ‘ 𝑁 ) ∈ ℕ ) → ( 𝑀 gcd ( 𝑀 · ( abs ‘ 𝑁 ) ) ) = 𝑀 )
27 25 26 sylan2 ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝑁 ∈ ℤ ∧ 𝑁 ≠ 0 ) ) → ( 𝑀 gcd ( 𝑀 · ( abs ‘ 𝑁 ) ) ) = 𝑀 )
28 27 anassrs ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( 𝑀 gcd ( 𝑀 · ( abs ‘ 𝑁 ) ) ) = 𝑀 )
29 16 24 28 3eqtr3d ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) ∧ 𝑁 ≠ 0 ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )
30 mul01 ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 · 0 ) = 0 )
31 30 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 gcd ( 𝑀 · 0 ) ) = ( 𝑀 gcd 0 ) )
32 4 31 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 gcd ( 𝑀 · 0 ) ) = ( 𝑀 gcd 0 ) )
33 32 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( 𝑀 · 0 ) ) = ( 𝑀 gcd 0 ) )
34 nn0gcdid0 ⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 gcd 0 ) = 𝑀 )
35 9 34 syl ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 gcd 0 ) = 𝑀 )
36 35 adantr ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 0 ) = 𝑀 )
37 33 36 eqtrd ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( 𝑀 · 0 ) ) = 𝑀 )
38 3 29 37 pm2.61ne ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd ( 𝑀 · 𝑁 ) ) = 𝑀 )