Metamath Proof Explorer


Theorem dvdsmul1

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

Ref Expression
Assertion dvdsmul1 ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐‘€ โˆฅ ( ๐‘€ ยท ๐‘ ) )

Proof

Step Hyp Ref Expression
1 zcn โŠข ( ๐‘ โˆˆ โ„ค โ†’ ๐‘ โˆˆ โ„‚ )
2 zcn โŠข ( ๐‘€ โˆˆ โ„ค โ†’ ๐‘€ โˆˆ โ„‚ )
3 mulcom โŠข ( ( ๐‘ โˆˆ โ„‚ โˆง ๐‘€ โˆˆ โ„‚ ) โ†’ ( ๐‘ ยท ๐‘€ ) = ( ๐‘€ ยท ๐‘ ) )
4 1 2 3 syl2anr โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ ยท ๐‘€ ) = ( ๐‘€ ยท ๐‘ ) )
5 zmulcl โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘€ ยท ๐‘ ) โˆˆ โ„ค )
6 dvds0lem โŠข ( ( ( ๐‘ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ( ๐‘€ ยท ๐‘ ) โˆˆ โ„ค ) โˆง ( ๐‘ ยท ๐‘€ ) = ( ๐‘€ ยท ๐‘ ) ) โ†’ ๐‘€ โˆฅ ( ๐‘€ ยท ๐‘ ) )
7 6 ex โŠข ( ( ๐‘ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ( ๐‘€ ยท ๐‘ ) โˆˆ โ„ค ) โ†’ ( ( ๐‘ ยท ๐‘€ ) = ( ๐‘€ ยท ๐‘ ) โ†’ ๐‘€ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )
8 7 3com12 โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ( ๐‘€ ยท ๐‘ ) โˆˆ โ„ค ) โ†’ ( ( ๐‘ ยท ๐‘€ ) = ( ๐‘€ ยท ๐‘ ) โ†’ ๐‘€ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )
9 5 8 mpd3an3 โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘ ยท ๐‘€ ) = ( ๐‘€ ยท ๐‘ ) โ†’ ๐‘€ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )
10 4 9 mpd โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐‘€ โˆฅ ( ๐‘€ ยท ๐‘ ) )