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