# Metamath Proof Explorer

## Theorem gcddiv

Description: Division law for GCD. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion gcddiv ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\wedge \left({C}\parallel {A}\wedge {C}\parallel {B}\right)\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)$

### Proof

Step Hyp Ref Expression
1 nnz ${⊢}{C}\in ℕ\to {C}\in ℤ$
2 1 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to {C}\in ℤ$
3 simp1 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to {A}\in ℤ$
4 divides ${⊢}\left({C}\in ℤ\wedge {A}\in ℤ\right)\to \left({C}\parallel {A}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}{C}={A}\right)$
5 2 3 4 syl2anc ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to \left({C}\parallel {A}↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}{C}={A}\right)$
6 simp2 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to {B}\in ℤ$
7 divides ${⊢}\left({C}\in ℤ\wedge {B}\in ℤ\right)\to \left({C}\parallel {B}↔\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}{C}={B}\right)$
8 2 6 7 syl2anc ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to \left({C}\parallel {B}↔\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}{C}={B}\right)$
9 5 8 anbi12d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to \left(\left({C}\parallel {A}\wedge {C}\parallel {B}\right)↔\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}{C}={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}{C}={B}\right)\right)$
10 reeanv ${⊢}\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}{C}={A}\wedge {b}{C}={B}\right)↔\left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}{a}{C}={A}\wedge \exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}{b}{C}={B}\right)$
11 9 10 syl6bbr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to \left(\left({C}\parallel {A}\wedge {C}\parallel {B}\right)↔\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}{C}={A}\wedge {b}{C}={B}\right)\right)$
12 gcdcl ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {a}\mathrm{gcd}{b}\in {ℕ}_{0}$
13 12 nn0cnd ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\right)\to {a}\mathrm{gcd}{b}\in ℂ$
14 13 3adant3 ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to {a}\mathrm{gcd}{b}\in ℂ$
15 nncn ${⊢}{C}\in ℕ\to {C}\in ℂ$
16 15 3ad2ant3 ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to {C}\in ℂ$
17 nnne0 ${⊢}{C}\in ℕ\to {C}\ne 0$
18 17 3ad2ant3 ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to {C}\ne 0$
19 14 16 18 divcan4d ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to \frac{\left({a}\mathrm{gcd}{b}\right){C}}{{C}}={a}\mathrm{gcd}{b}$
20 nnnn0 ${⊢}{C}\in ℕ\to {C}\in {ℕ}_{0}$
21 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}$
22 20 21 syl3an3 ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to {a}{C}\mathrm{gcd}{b}{C}=\left({a}\mathrm{gcd}{b}\right){C}$
23 22 oveq1d ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to \frac{{a}{C}\mathrm{gcd}{b}{C}}{{C}}=\frac{\left({a}\mathrm{gcd}{b}\right){C}}{{C}}$
24 zcn ${⊢}{a}\in ℤ\to {a}\in ℂ$
25 24 3ad2ant1 ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to {a}\in ℂ$
26 25 16 18 divcan4d ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to \frac{{a}{C}}{{C}}={a}$
27 zcn ${⊢}{b}\in ℤ\to {b}\in ℂ$
28 27 3ad2ant2 ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to {b}\in ℂ$
29 28 16 18 divcan4d ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to \frac{{b}{C}}{{C}}={b}$
30 26 29 oveq12d ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to \left(\frac{{a}{C}}{{C}}\right)\mathrm{gcd}\left(\frac{{b}{C}}{{C}}\right)={a}\mathrm{gcd}{b}$
31 19 23 30 3eqtr4d ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to \frac{{a}{C}\mathrm{gcd}{b}{C}}{{C}}=\left(\frac{{a}{C}}{{C}}\right)\mathrm{gcd}\left(\frac{{b}{C}}{{C}}\right)$
32 oveq12 ${⊢}\left({a}{C}={A}\wedge {b}{C}={B}\right)\to {a}{C}\mathrm{gcd}{b}{C}={A}\mathrm{gcd}{B}$
33 32 oveq1d ${⊢}\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \frac{{a}{C}\mathrm{gcd}{b}{C}}{{C}}=\frac{{A}\mathrm{gcd}{B}}{{C}}$
34 oveq1 ${⊢}{a}{C}={A}\to \frac{{a}{C}}{{C}}=\frac{{A}}{{C}}$
35 oveq1 ${⊢}{b}{C}={B}\to \frac{{b}{C}}{{C}}=\frac{{B}}{{C}}$
36 34 35 oveqan12d ${⊢}\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \left(\frac{{a}{C}}{{C}}\right)\mathrm{gcd}\left(\frac{{b}{C}}{{C}}\right)=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)$
37 33 36 eqeq12d ${⊢}\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \left(\frac{{a}{C}\mathrm{gcd}{b}{C}}{{C}}=\left(\frac{{a}{C}}{{C}}\right)\mathrm{gcd}\left(\frac{{b}{C}}{{C}}\right)↔\frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)\right)$
38 31 37 syl5ibcom ${⊢}\left({a}\in ℤ\wedge {b}\in ℤ\wedge {C}\in ℕ\right)\to \left(\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)\right)$
39 38 3expa ${⊢}\left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\wedge {C}\in ℕ\right)\to \left(\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)\right)$
40 39 expcom ${⊢}{C}\in ℕ\to \left(\left({a}\in ℤ\wedge {b}\in ℤ\right)\to \left(\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)\right)\right)$
41 40 rexlimdvv ${⊢}{C}\in ℕ\to \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)\right)$
42 41 3ad2ant3 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to \left(\exists {a}\in ℤ\phantom{\rule{.4em}{0ex}}\exists {b}\in ℤ\phantom{\rule{.4em}{0ex}}\left({a}{C}={A}\wedge {b}{C}={B}\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)\right)$
43 11 42 sylbid ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\to \left(\left({C}\parallel {A}\wedge {C}\parallel {B}\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)\right)$
44 43 imp ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\wedge {C}\in ℕ\right)\wedge \left({C}\parallel {A}\wedge {C}\parallel {B}\right)\right)\to \frac{{A}\mathrm{gcd}{B}}{{C}}=\left(\frac{{A}}{{C}}\right)\mathrm{gcd}\left(\frac{{B}}{{C}}\right)$