Metamath Proof Explorer

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 𝑁 ) ) )