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 ) → ( ( 𝑀 ∥ 𝐾 ∧ 𝑁 ∥ 𝐾 ) → ( 𝑀 · 𝑁 ) ∥ 𝐾 ) )