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

Metamath Proof Explorer

Theorem dvdsmultr2

Description: If an integer divides another, it divides a multiple of it. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Assertion dvdsmultr2 
|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || N -> K || ( M x. N ) ) )

Proof

Step Hyp Ref Expression
1 dvdsmul2 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> N || ( M x. N ) )
2 1 biantrud 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( K || N <-> ( K || N /\ N || ( M x. N ) ) ) )
3 2 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || N <-> ( K || N /\ N || ( M x. N ) ) ) )
4 simp1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
5 simp3 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> N e. ZZ )
6 zmulcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
7 6 3adant1 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
8 dvdstr 
 |-  ( ( K e. ZZ /\ N e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( K || N /\ N || ( M x. N ) ) -> K || ( M x. N ) ) )
9 4 5 7 8 syl3anc 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || N /\ N || ( M x. N ) ) -> K || ( M x. N ) ) )
10 3 9 sylbid 
 |-  ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || N -> K || ( M x. N ) ) )