This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvdscmulr

Description: Cancellation law for the divides relation. Theorem 1.1(e) in ApostolNT p. 14. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvdscmulr ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ↔ 𝑀 ∥ 𝑁 ) )

Proof

Step Hyp Ref Expression
1 zmulcl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
2 1 3adant3 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑀 ) ∈ ℤ )
3 zmulcl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
4 3 3adant2 ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 · 𝑁 ) ∈ ℤ )
5 2 4 jca ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) )
6 5 3coml ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) )
7 6 3adant3r ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∈ ℤ ∧ ( 𝐾 · 𝑁 ) ∈ ℤ ) )
8 3simpa ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
9 simpr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → 𝑥 ∈ ℤ )
10 zcn ⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
11 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
12 10 11 anim12i ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) )
13 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
14 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
15 14 anim1i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) → ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) )
16 mul12 ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
17 16 3adant1r ⊢ ( ( ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ∧ 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
18 17 3expb ⊢ ( ( ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
19 18 ancoms ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
20 19 3adant2 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝑥 · ( 𝐾 · 𝑀 ) ) )
21 20 eqeq1d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ) )
22 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝑥 · 𝑀 ) ∈ ℂ )
23 mulcan ⊢ ( ( ( 𝑥 · 𝑀 ) ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
24 22 23 syl3an1 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · ( 𝑥 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
25 21 24 bitr3d ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑀 ∈ ℂ ) ∧ 𝑁 ∈ ℂ ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
26 12 13 15 25 syl3an ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
27 26 3expb ⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ) ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
28 27 3impa ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
29 28 3coml ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
30 29 3expia ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ) → ( 𝑥 ∈ ℤ → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) ) )
31 30 3impb ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( 𝑥 ∈ ℤ → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) ) )
32 31 imp ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) ↔ ( 𝑥 · 𝑀 ) = 𝑁 ) )
33 32 biimpd ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) ∧ 𝑥 ∈ ℤ ) → ( ( 𝑥 · ( 𝐾 · 𝑀 ) ) = ( 𝐾 · 𝑁 ) → ( 𝑥 · 𝑀 ) = 𝑁 ) )
34 7 8 9 33 dvds1lem ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) → 𝑀 ∥ 𝑁 ) )
35 dvdscmul ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 → ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ) )
36 35 3adant3r ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( 𝑀 ∥ 𝑁 → ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ) )
37 34 36 impbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ ( 𝐾 ∈ ℤ ∧ 𝐾 ≠ 0 ) ) → ( ( 𝐾 · 𝑀 ) ∥ ( 𝐾 · 𝑁 ) ↔ 𝑀 ∥ 𝑁 ) )