Metamath Proof Explorer

Theorem coprmdvds2

Description: If an integer is divisible by two coprime integers, then it is divisible by their product. (Contributed by Mario Carneiro, 24-Feb-2014)

Ref Expression
Assertion coprmdvds2 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) )

Proof

Step Hyp Ref Expression
1 divides ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∥ 𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 ) )
2 1 3adant1 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∥ 𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 ) )
3 2 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 ∥ 𝐾 ↔ ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 ) )
4 simprr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → 𝑥 ∈ ℤ )
5 simpl2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
6 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
7 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
8 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑥 · 𝑁 ) = ( 𝑁 · 𝑥 ) )
9 6 7 8 syl2an ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑥 · 𝑁 ) = ( 𝑁 · 𝑥 ) )
10 4 5 9 syl2anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑥 · 𝑁 ) = ( 𝑁 · 𝑥 ) )
11 10 breq2d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) ↔ 𝑀 ∥ ( 𝑁 · 𝑥 ) ) )
12 simprl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
13 simpl1 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
14 coprmdvds ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( ( 𝑀 ∥ ( 𝑁 · 𝑥 ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀 ∥ 𝑥 ) )
15 13 5 4 14 syl3anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝑀 ∥ ( 𝑁 · 𝑥 ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → 𝑀 ∥ 𝑥 ) )
16 12 15 mpan2d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑁 · 𝑥 ) → 𝑀 ∥ 𝑥 ) )
17 11 16 sylbid ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) → 𝑀 ∥ 𝑥 ) )
18 dvdsmulc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑥 → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) )
19 13 4 5 18 syl3anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ 𝑥 → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) )
20 17 19 syld ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) )
21 breq2 ⊢ ( ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀 ∥ ( 𝑥 · 𝑁 ) ↔ 𝑀 ∥ 𝐾 ) )
22 breq2 ⊢ ( ( 𝑥 · 𝑁 ) = 𝐾 → ( ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ↔ ( 𝑀 · 𝑁 ) ∥ 𝐾 ) )
23 21 22 imbi12d ⊢ ( ( 𝑥 · 𝑁 ) = 𝐾 → ( ( 𝑀 ∥ ( 𝑥 · 𝑁 ) → ( 𝑀 · 𝑁 ) ∥ ( 𝑥 · 𝑁 ) ) ↔ ( 𝑀 ∥ 𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
24 20 23 syl5ibcom ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( ( 𝑀 gcd 𝑁 ) = 1 ∧ 𝑥 ∈ ℤ ) ) → ( ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀 ∥ 𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
25 24 anassrs ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀 ∥ 𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
26 25 rexlimdva ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ∃ 𝑥 ∈ ℤ ( 𝑥 · 𝑁 ) = 𝐾 → ( 𝑀 ∥ 𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
27 3 26 sylbid ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( 𝑁 ∥ 𝐾 → ( 𝑀 ∥ 𝐾 → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) ) )
28 27 impcomd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ∧ ( 𝑀 gcd 𝑁 ) = 1 ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) )