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

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 ( 𝐵 / 𝐶 ) ) )