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 ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐พ โˆฅ ๐‘ โ†’ ๐พ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 dvdsmul2 โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐‘ โˆฅ ( ๐‘€ ยท ๐‘ ) )
2 1 biantrud โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐พ โˆฅ ๐‘ โ†” ( ๐พ โˆฅ ๐‘ โˆง ๐‘ โˆฅ ( ๐‘€ ยท ๐‘ ) ) ) )
3 2 3adant1 โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐พ โˆฅ ๐‘ โ†” ( ๐พ โˆฅ ๐‘ โˆง ๐‘ โˆฅ ( ๐‘€ ยท ๐‘ ) ) ) )
4 simp1 โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐พ โˆˆ โ„ค )
5 simp3 โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ๐‘ โˆˆ โ„ค )
6 zmulcl โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘€ ยท ๐‘ ) โˆˆ โ„ค )
7 6 3adant1 โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘€ ยท ๐‘ ) โˆˆ โ„ค )
8 dvdstr โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค โˆง ( ๐‘€ ยท ๐‘ ) โˆˆ โ„ค ) โ†’ ( ( ๐พ โˆฅ ๐‘ โˆง ๐‘ โˆฅ ( ๐‘€ ยท ๐‘ ) ) โ†’ ๐พ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )
9 4 5 7 8 syl3anc โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐พ โˆฅ ๐‘ โˆง ๐‘ โˆฅ ( ๐‘€ ยท ๐‘ ) ) โ†’ ๐พ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )
10 3 9 sylbid โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐พ โˆฅ ๐‘ โ†’ ๐พ โˆฅ ( ๐‘€ ยท ๐‘ ) ) )