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