Theorem mulgcdr

Description: Reverse distribution law for the gcd operator. (Contributed by Scott Fenton, 2-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

	Ref	Expression
Assertion	mulgcdr	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 · 𝐶 ) gcd ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 gcd 𝐵 ) · 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		mulgcd	⊢ ( ( 𝐶 ∈ ℕ0 ∧ 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( ( 𝐶 · 𝐴 ) gcd ( 𝐶 · 𝐵 ) ) = ( 𝐶 · ( 𝐴 gcd 𝐵 ) ) )
2	1	3coml	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐶 · 𝐴 ) gcd ( 𝐶 · 𝐵 ) ) = ( 𝐶 · ( 𝐴 gcd 𝐵 ) ) )
3		zcn	⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℂ )
4	3	3ad2ant1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → 𝐴 ∈ ℂ )
5		nn0cn	⊢ ( 𝐶 ∈ ℕ0 → 𝐶 ∈ ℂ )
6	5	3ad2ant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
7	4 6	mulcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 · 𝐶 ) = ( 𝐶 · 𝐴 ) )
8		zcn	⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℂ )
9	8	3ad2ant2	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → 𝐵 ∈ ℂ )
10	9 6	mulcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
11	7 10	oveq12d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 · 𝐶 ) gcd ( 𝐵 · 𝐶 ) ) = ( ( 𝐶 · 𝐴 ) gcd ( 𝐶 · 𝐵 ) ) )
12		gcdcl	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 )
13	12	3adant3	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ∈ ℕ0 )
14	13	nn0cnd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( 𝐴 gcd 𝐵 ) ∈ ℂ )
15	14 6	mulcomd	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 gcd 𝐵 ) · 𝐶 ) = ( 𝐶 · ( 𝐴 gcd 𝐵 ) ) )
16	2 11 15	3eqtr4d	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝐴 · 𝐶 ) gcd ( 𝐵 · 𝐶 ) ) = ( ( 𝐴 gcd 𝐵 ) · 𝐶 ) )