Metamath Proof Explorer

Theorem dvdsmul1

Description: An integer divides a multiple of itself. (Contributed by Paul Chapman, 21-Mar-2011)

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

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( N e. ZZ -> N e. CC )
2 zcn 
 |-  ( M e. ZZ -> M e. CC )
3 mulcom 
 |-  ( ( N e. CC /\ M e. CC ) -> ( N x. M ) = ( M x. N ) )
4 1 2 3 syl2anr 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( N x. M ) = ( M x. N ) )
5 zmulcl 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M x. N ) e. ZZ )
6 dvds0lem 
 |-  ( ( ( N e. ZZ /\ M e. ZZ /\ ( M x. N ) e. ZZ ) /\ ( N x. M ) = ( M x. N ) ) -> M || ( M x. N ) )
7 6 ex 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( N x. M ) = ( M x. N ) -> M || ( M x. N ) ) )
8 7 3com12 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ ( M x. N ) e. ZZ ) -> ( ( N x. M ) = ( M x. N ) -> M || ( M x. N ) ) )
9 5 8 mpd3an3 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( N x. M ) = ( M x. N ) -> M || ( M x. N ) ) )
10 4 9 mpd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> M || ( M x. N ) )