This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 ) · 𝐶 ) )