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 ) ) )