Theorem dvdsgcd

Description: An integer which divides each of two others also divides their gcd. (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 30-May-2014)

	Ref	Expression
Assertion	dvdsgcd	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bezout	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) )
2	1	3adant1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) )
3		dvds2ln	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( ( 𝑥 · 𝑀 ) + ( 𝑦 · 𝑁 ) ) ) )
4	3	3impia	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → 𝐾 ∥ ( ( 𝑥 · 𝑀 ) + ( 𝑦 · 𝑁 ) ) )
5	4	3coml	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐾 ∥ ( ( 𝑥 · 𝑀 ) + ( 𝑦 · 𝑁 ) ) )
6		simp3l	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
7		simp12	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
8		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
9		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
10		mulcom	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑥 · 𝑀 ) = ( 𝑀 · 𝑥 ) )
11	8 9 10	syl2an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑥 · 𝑀 ) = ( 𝑀 · 𝑥 ) )
12	6 7 11	syl2anc	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑥 · 𝑀 ) = ( 𝑀 · 𝑥 ) )
13		simp3r	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑦 ∈ ℤ )
14		simp13	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
15		zcn	⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
16		zcn	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
17		mulcom	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑦 · 𝑁 ) = ( 𝑁 · 𝑦 ) )
18	15 16 17	syl2an	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑦 · 𝑁 ) = ( 𝑁 · 𝑦 ) )
19	13 14 18	syl2anc	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( 𝑦 · 𝑁 ) = ( 𝑁 · 𝑦 ) )
20	12 19	oveq12d	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑥 · 𝑀 ) + ( 𝑦 · 𝑁 ) ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) )
21	5 20	breqtrd	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → 𝐾 ∥ ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) )
22		breq2	⊢ ( ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) → ( 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ↔ 𝐾 ∥ ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) ) )
23	21 22	syl5ibrcom	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ∧ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) ) → ( ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) → 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) )
24	23	3expia	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) → 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) ) )
25	24	rexlimdvv	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) → 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) )
26	25	ex	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → ( ∃ 𝑥 ∈ ℤ ∃ 𝑦 ∈ ℤ ( 𝑀 gcd 𝑁 ) = ( ( 𝑀 · 𝑥 ) + ( 𝑁 · 𝑦 ) ) → 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) ) )
27	2 26	mpid	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 ∥ 𝑀 ∧ 𝐾 ∥ 𝑁 ) → 𝐾 ∥ ( 𝑀 gcd 𝑁 ) ) )