Theorem muldvds1

Description: If a product divides an integer, so does one of its factors. (Contributed by Paul Chapman, 21-Mar-2011)

	Ref	Expression
Assertion	muldvds1	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → 𝐾 ∥ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		zmulcl	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
2	1	anim1i	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
3	2	3impa	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
4		3simpb	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
5		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑥 · 𝑀 ) ∈ ℤ )
6	5	ancoms	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝑀 ) ∈ ℤ )
7	6	3ad2antl2	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · 𝑀 ) ∈ ℤ )
8		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
9		zcn	⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
10		zcn	⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
11		mulass	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑥 · 𝐾 ) · 𝑀 ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
12		mul32	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( ( 𝑥 · 𝐾 ) · 𝑀 ) = ( ( 𝑥 · 𝑀 ) · 𝐾 ) )
13	11 12	eqtr3d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( ( 𝑥 · 𝑀 ) · 𝐾 ) )
14	8 9 10 13	syl3an	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( ( 𝑥 · 𝑀 ) · 𝐾 ) )
15	14	3coml	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( ( 𝑥 · 𝑀 ) · 𝐾 ) )
16	15	3expa	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( ( 𝑥 · 𝑀 ) · 𝐾 ) )
17	16	3adantl3	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( ( 𝑥 · 𝑀 ) · 𝐾 ) )
18	17	eqeq1d	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = 𝑁 ↔ ( ( 𝑥 · 𝑀 ) · 𝐾 ) = 𝑁 ) )
19	18	biimpd	⊢ ( ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = 𝑁 → ( ( 𝑥 · 𝑀 ) · 𝐾 ) = 𝑁 ) )
20	3 4 7 19	dvds1lem	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∥ 𝑁 → 𝐾 ∥ 𝑁 ) )