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 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℕ 0 → A ⁢ C gcd B ⁢ C = A gcd B ⁢ C

Proof

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