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 𝑁 ) ) ) )