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 ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ ( 𝐶𝐴𝐶𝐵 ) ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 nnz ( 𝐶 ∈ ℕ → 𝐶 ∈ ℤ )
2 1 3ad2ant3 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℤ )
3 simp1 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐴 ∈ ℤ )
4 divides ( ( 𝐶 ∈ ℤ ∧ 𝐴 ∈ ℤ ) → ( 𝐶𝐴 ↔ ∃ 𝑎 ∈ ℤ ( 𝑎 · 𝐶 ) = 𝐴 ) )
5 2 3 4 syl2anc ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐶𝐴 ↔ ∃ 𝑎 ∈ ℤ ( 𝑎 · 𝐶 ) = 𝐴 ) )
6 simp2 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐵 ∈ ℤ )
7 divides ( ( 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 𝐶𝐵 ↔ ∃ 𝑏 ∈ ℤ ( 𝑏 · 𝐶 ) = 𝐵 ) )
8 2 6 7 syl2anc ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐶𝐵 ↔ ∃ 𝑏 ∈ ℤ ( 𝑏 · 𝐶 ) = 𝐵 ) )
9 5 8 anbi12d ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶𝐴𝐶𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( 𝑎 · 𝐶 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( 𝑏 · 𝐶 ) = 𝐵 ) ) )
10 reeanv ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) ↔ ( ∃ 𝑎 ∈ ℤ ( 𝑎 · 𝐶 ) = 𝐴 ∧ ∃ 𝑏 ∈ ℤ ( 𝑏 · 𝐶 ) = 𝐵 ) )
11 9 10 bitr4di ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶𝐴𝐶𝐵 ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) ) )
12 gcdcl ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 gcd 𝑏 ) ∈ ℕ0 )
13 12 nn0cnd ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 gcd 𝑏 ) ∈ ℂ )
14 13 3adant3 ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝑎 gcd 𝑏 ) ∈ ℂ )
15 nncn ( 𝐶 ∈ ℕ → 𝐶 ∈ ℂ )
16 15 3ad2ant3 ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐶 ∈ ℂ )
17 nnne0 ( 𝐶 ∈ ℕ → 𝐶 ≠ 0 )
18 17 3ad2ant3 ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝐶 ≠ 0 )
19 14 16 18 divcan4d ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝑎 gcd 𝑏 ) · 𝐶 ) / 𝐶 ) = ( 𝑎 gcd 𝑏 ) )
20 nnnn0 ( 𝐶 ∈ ℕ → 𝐶 ∈ ℕ0 )
21 mulgcdr ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ0 ) → ( ( 𝑎 · 𝐶 ) gcd ( 𝑏 · 𝐶 ) ) = ( ( 𝑎 gcd 𝑏 ) · 𝐶 ) )
22 20 21 syl3an3 ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 𝑎 · 𝐶 ) gcd ( 𝑏 · 𝐶 ) ) = ( ( 𝑎 gcd 𝑏 ) · 𝐶 ) )
23 22 oveq1d ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝑎 · 𝐶 ) gcd ( 𝑏 · 𝐶 ) ) / 𝐶 ) = ( ( ( 𝑎 gcd 𝑏 ) · 𝐶 ) / 𝐶 ) )
24 zcn ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
25 24 3ad2ant1 ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝑎 ∈ ℂ )
26 25 16 18 divcan4d ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 𝑎 · 𝐶 ) / 𝐶 ) = 𝑎 )
27 zcn ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
28 27 3ad2ant2 ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → 𝑏 ∈ ℂ )
29 28 16 18 divcan4d ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 𝑏 · 𝐶 ) / 𝐶 ) = 𝑏 )
30 26 29 oveq12d ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝑎 · 𝐶 ) / 𝐶 ) gcd ( ( 𝑏 · 𝐶 ) / 𝐶 ) ) = ( 𝑎 gcd 𝑏 ) )
31 19 23 30 3eqtr4d ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝑎 · 𝐶 ) gcd ( 𝑏 · 𝐶 ) ) / 𝐶 ) = ( ( ( 𝑎 · 𝐶 ) / 𝐶 ) gcd ( ( 𝑏 · 𝐶 ) / 𝐶 ) ) )
32 oveq12 ( ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( 𝑎 · 𝐶 ) gcd ( 𝑏 · 𝐶 ) ) = ( 𝐴 gcd 𝐵 ) )
33 32 oveq1d ( ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( ( 𝑎 · 𝐶 ) gcd ( 𝑏 · 𝐶 ) ) / 𝐶 ) = ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) )
34 oveq1 ( ( 𝑎 · 𝐶 ) = 𝐴 → ( ( 𝑎 · 𝐶 ) / 𝐶 ) = ( 𝐴 / 𝐶 ) )
35 oveq1 ( ( 𝑏 · 𝐶 ) = 𝐵 → ( ( 𝑏 · 𝐶 ) / 𝐶 ) = ( 𝐵 / 𝐶 ) )
36 34 35 oveqan12d ( ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( ( 𝑎 · 𝐶 ) / 𝐶 ) gcd ( ( 𝑏 · 𝐶 ) / 𝐶 ) ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) )
37 33 36 eqeq12d ( ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( ( ( 𝑎 · 𝐶 ) gcd ( 𝑏 · 𝐶 ) ) / 𝐶 ) = ( ( ( 𝑎 · 𝐶 ) / 𝐶 ) gcd ( ( 𝑏 · 𝐶 ) / 𝐶 ) ) ↔ ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) ) )
38 31 37 syl5ibcom ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) ) )
39 38 3expa ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) ) )
40 39 expcom ( 𝐶 ∈ ℕ → ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) ) ) )
41 40 rexlimdvv ( 𝐶 ∈ ℕ → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) ) )
42 41 3ad2ant3 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ ( ( 𝑎 · 𝐶 ) = 𝐴 ∧ ( 𝑏 · 𝐶 ) = 𝐵 ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) ) )
43 11 42 sylbid ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 𝐶𝐴𝐶𝐵 ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) ) )
44 43 imp ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) ∧ ( 𝐶𝐴𝐶𝐵 ) ) → ( ( 𝐴 gcd 𝐵 ) / 𝐶 ) = ( ( 𝐴 / 𝐶 ) gcd ( 𝐵 / 𝐶 ) ) )