Theorem dvdsmultr1

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

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

Proof

Step	Hyp	Ref	Expression
1		dvdsmul1	|- ( ( M e. ZZ /\ N e. ZZ ) -> M || ( M x. N ) )
2	1	3adant1	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> M || ( M x. N ) )
3		zmulcl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
4	3	3adant1	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
5		dvdstr	|- ( ( K e. ZZ /\ M e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( K || M /\ M || ( M x. N ) ) -> K || ( M x. N ) ) )
6	4 5	syld3an3	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K || M /\ M || ( M x. N ) ) -> K || ( M x. N ) ) )
7	2 6	mpan2d	|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K || M -> K || ( M x. N ) ) )