# 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {A}{C}\mathrm{gcd}{B}{C}=\left({A}\mathrm{gcd}{B}\right){C}$

### Proof

Step Hyp Ref Expression
1 mulgcd ${⊢}\left({C}\in {ℕ}_{0}\wedge {A}\in ℤ\wedge {B}\in ℤ\right)\to {C}{A}\mathrm{gcd}{C}{B}={C}\left({A}\mathrm{gcd}{B}\right)$
2 1 3coml ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {C}{A}\mathrm{gcd}{C}{B}={C}\left({A}\mathrm{gcd}{B}\right)$
3 zcn ${⊢}{A}\in ℤ\to {A}\in ℂ$
4 3 3ad2ant1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {A}\in ℂ$
5 nn0cn ${⊢}{C}\in {ℕ}_{0}\to {C}\in ℂ$
6 5 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {C}\in ℂ$
7 4 6 mulcomd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {A}{C}={C}{A}$
8 zcn ${⊢}{B}\in ℤ\to {B}\in ℂ$
9 8 3ad2ant2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {B}\in ℂ$
10 9 6 mulcomd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {B}{C}={C}{B}$
11 7 10 oveq12d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {A}{C}\mathrm{gcd}{B}{C}={C}{A}\mathrm{gcd}{C}{B}$
12 gcdcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\mathrm{gcd}{B}\in {ℕ}_{0}$
13 12 3adant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {A}\mathrm{gcd}{B}\in {ℕ}_{0}$
14 13 nn0cnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {A}\mathrm{gcd}{B}\in ℂ$
15 14 6 mulcomd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to \left({A}\mathrm{gcd}{B}\right){C}={C}\left({A}\mathrm{gcd}{B}\right)$
16 2 11 15 3eqtr4d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in {ℕ}_{0}\right)\to {A}{C}\mathrm{gcd}{B}{C}=\left({A}\mathrm{gcd}{B}\right){C}$