Metamath Proof Explorer


Theorem absmulgcd

Description: Distribute absolute value of multiplication over gcd. Theorem 1.4(c) in ApostolNT p. 16. (Contributed by Paul Chapman, 22-Jun-2011)

Ref Expression
Assertion absmulgcd ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( abs ‘ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )

Proof

Step Hyp Ref Expression
1 gcdcl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℕ0 )
2 nn0re ( ( 𝑀 gcd 𝑁 ) ∈ ℕ0 → ( 𝑀 gcd 𝑁 ) ∈ ℝ )
3 nn0ge0 ( ( 𝑀 gcd 𝑁 ) ∈ ℕ0 → 0 ≤ ( 𝑀 gcd 𝑁 ) )
4 2 3 absidd ( ( 𝑀 gcd 𝑁 ) ∈ ℕ0 → ( abs ‘ ( 𝑀 gcd 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
5 1 4 syl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝑀 gcd 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
6 5 oveq2d ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝐾 ) · ( abs ‘ ( 𝑀 gcd 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( 𝑀 gcd 𝑁 ) ) )
7 6 3adant1 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝐾 ) · ( abs ‘ ( 𝑀 gcd 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( 𝑀 gcd 𝑁 ) ) )
8 zcn ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
9 1 nn0cnd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 gcd 𝑁 ) ∈ ℂ )
10 absmul ( ( 𝐾 ∈ ℂ ∧ ( 𝑀 gcd 𝑁 ) ∈ ℂ ) → ( abs ‘ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( abs ‘ ( 𝑀 gcd 𝑁 ) ) ) )
11 8 9 10 syl2an ( ( 𝐾 ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( abs ‘ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( abs ‘ ( 𝑀 gcd 𝑁 ) ) ) )
12 11 3impb ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( abs ‘ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( abs ‘ ( 𝑀 gcd 𝑁 ) ) ) )
13 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
14 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
15 absmul ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( abs ‘ ( 𝐾 · 𝑀 ) ) = ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑀 ) ) )
16 absmul ( ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( abs ‘ ( 𝐾 · 𝑁 ) ) = ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑁 ) ) )
17 15 16 oveqan12d ( ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) ) → ( ( abs ‘ ( 𝐾 · 𝑀 ) ) gcd ( abs ‘ ( 𝐾 · 𝑁 ) ) ) = ( ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑀 ) ) gcd ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑁 ) ) ) )
18 17 3impdi ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( abs ‘ ( 𝐾 · 𝑀 ) ) gcd ( abs ‘ ( 𝐾 · 𝑁 ) ) ) = ( ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑀 ) ) gcd ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑁 ) ) ) )
19 8 13 14 18 syl3an ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ ( 𝐾 · 𝑀 ) ) gcd ( abs ‘ ( 𝐾 · 𝑁 ) ) ) = ( ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑀 ) ) gcd ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑁 ) ) ) )
20 zmulcl ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
21 zmulcl ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
22 gcdabs ( ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) → ( ( abs ‘ ( 𝐾 · 𝑀 ) ) gcd ( abs ‘ ( 𝐾 · 𝑁 ) ) ) = ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) )
23 20 21 22 syl2an ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( abs ‘ ( 𝐾 · 𝑀 ) ) gcd ( abs ‘ ( 𝐾 · 𝑁 ) ) ) = ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) )
24 23 3impdi ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ ( 𝐾 · 𝑀 ) ) gcd ( abs ‘ ( 𝐾 · 𝑁 ) ) ) = ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) )
25 nn0abscl ( 𝐾 ∈ ℤ → ( abs ‘ 𝐾 ) ∈ ℕ0 )
26 zabscl ( 𝑀 ∈ ℤ → ( abs ‘ 𝑀 ) ∈ ℤ )
27 zabscl ( 𝑁 ∈ ℤ → ( abs ‘ 𝑁 ) ∈ ℤ )
28 mulgcd ( ( ( abs ‘ 𝐾 ) ∈ ℕ0 ∧ ( abs ‘ 𝑀 ) ∈ ℤ ∧ ( abs ‘ 𝑁 ) ∈ ℤ ) → ( ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑀 ) ) gcd ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) ) )
29 25 26 27 28 syl3an ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑀 ) ) gcd ( ( abs ‘ 𝐾 ) · ( abs ‘ 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) ) )
30 19 24 29 3eqtr3d ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( ( abs ‘ 𝐾 ) · ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) ) )
31 gcdabs ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
32 31 3adant1 ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) = ( 𝑀 gcd 𝑁 ) )
33 32 oveq2d ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝐾 ) · ( ( abs ‘ 𝑀 ) gcd ( abs ‘ 𝑁 ) ) ) = ( ( abs ‘ 𝐾 ) · ( 𝑀 gcd 𝑁 ) ) )
34 30 33 eqtrd ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( ( abs ‘ 𝐾 ) · ( 𝑀 gcd 𝑁 ) ) )
35 7 12 34 3eqtr4rd ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) gcd ( 𝐾 · 𝑁 ) ) = ( abs ‘ ( 𝐾 · ( 𝑀 gcd 𝑁 ) ) ) )