Metamath Proof Explorer


Theorem dvds2sub

Description: If an integer divides each of two other integers, it divides their difference. (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion dvds2sub ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐พ โˆฅ ๐‘€ โˆง ๐พ โˆฅ ๐‘ ) โ†’ ๐พ โˆฅ ( ๐‘€ โˆ’ ๐‘ ) ) )

Proof

Step Hyp Ref Expression
1 3simpa โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค ) )
2 3simpb โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐พ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) )
3 zsubcl โŠข ( ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘€ โˆ’ ๐‘ ) โˆˆ โ„ค )
4 3 anim2i โŠข ( ( ๐พ โˆˆ โ„ค โˆง ( ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) ) โ†’ ( ๐พ โˆˆ โ„ค โˆง ( ๐‘€ โˆ’ ๐‘ ) โˆˆ โ„ค ) )
5 4 3impb โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐พ โˆˆ โ„ค โˆง ( ๐‘€ โˆ’ ๐‘ ) โˆˆ โ„ค ) )
6 zsubcl โŠข ( ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„ค )
7 6 adantl โŠข ( ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ๐‘ฅ โˆ’ ๐‘ฆ ) โˆˆ โ„ค )
8 zcn โŠข ( ๐‘ฅ โˆˆ โ„ค โ†’ ๐‘ฅ โˆˆ โ„‚ )
9 zcn โŠข ( ๐‘ฆ โˆˆ โ„ค โ†’ ๐‘ฆ โˆˆ โ„‚ )
10 zcn โŠข ( ๐พ โˆˆ โ„ค โ†’ ๐พ โˆˆ โ„‚ )
11 subdir โŠข ( ( ๐‘ฅ โˆˆ โ„‚ โˆง ๐‘ฆ โˆˆ โ„‚ โˆง ๐พ โˆˆ โ„‚ ) โ†’ ( ( ๐‘ฅ โˆ’ ๐‘ฆ ) ยท ๐พ ) = ( ( ๐‘ฅ ยท ๐พ ) โˆ’ ( ๐‘ฆ ยท ๐พ ) ) )
12 8 9 10 11 syl3an โŠข ( ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค โˆง ๐พ โˆˆ โ„ค ) โ†’ ( ( ๐‘ฅ โˆ’ ๐‘ฆ ) ยท ๐พ ) = ( ( ๐‘ฅ ยท ๐พ ) โˆ’ ( ๐‘ฆ ยท ๐พ ) ) )
13 12 3comr โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) โ†’ ( ( ๐‘ฅ โˆ’ ๐‘ฆ ) ยท ๐พ ) = ( ( ๐‘ฅ ยท ๐พ ) โˆ’ ( ๐‘ฆ ยท ๐พ ) ) )
14 13 3expb โŠข ( ( ๐พ โˆˆ โ„ค โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ๐‘ฅ โˆ’ ๐‘ฆ ) ยท ๐พ ) = ( ( ๐‘ฅ ยท ๐พ ) โˆ’ ( ๐‘ฆ ยท ๐พ ) ) )
15 oveq12 โŠข ( ( ( ๐‘ฅ ยท ๐พ ) = ๐‘€ โˆง ( ๐‘ฆ ยท ๐พ ) = ๐‘ ) โ†’ ( ( ๐‘ฅ ยท ๐พ ) โˆ’ ( ๐‘ฆ ยท ๐พ ) ) = ( ๐‘€ โˆ’ ๐‘ ) )
16 14 15 sylan9eq โŠข ( ( ( ๐พ โˆˆ โ„ค โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) ) โˆง ( ( ๐‘ฅ ยท ๐พ ) = ๐‘€ โˆง ( ๐‘ฆ ยท ๐พ ) = ๐‘ ) ) โ†’ ( ( ๐‘ฅ โˆ’ ๐‘ฆ ) ยท ๐พ ) = ( ๐‘€ โˆ’ ๐‘ ) )
17 16 ex โŠข ( ( ๐พ โˆˆ โ„ค โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ( ๐‘ฅ ยท ๐พ ) = ๐‘€ โˆง ( ๐‘ฆ ยท ๐พ ) = ๐‘ ) โ†’ ( ( ๐‘ฅ โˆ’ ๐‘ฆ ) ยท ๐พ ) = ( ๐‘€ โˆ’ ๐‘ ) ) )
18 17 3ad2antl1 โŠข ( ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โˆง ( ๐‘ฅ โˆˆ โ„ค โˆง ๐‘ฆ โˆˆ โ„ค ) ) โ†’ ( ( ( ๐‘ฅ ยท ๐พ ) = ๐‘€ โˆง ( ๐‘ฆ ยท ๐พ ) = ๐‘ ) โ†’ ( ( ๐‘ฅ โˆ’ ๐‘ฆ ) ยท ๐พ ) = ( ๐‘€ โˆ’ ๐‘ ) ) )
19 1 2 5 7 18 dvds2lem โŠข ( ( ๐พ โˆˆ โ„ค โˆง ๐‘€ โˆˆ โ„ค โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐พ โˆฅ ๐‘€ โˆง ๐พ โˆฅ ๐‘ ) โ†’ ๐พ โˆฅ ( ๐‘€ โˆ’ ๐‘ ) ) )