Metamath Proof Explorer


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