# 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 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel {M}\wedge {K}\parallel {N}\right)\to {K}\parallel \left({M}-{N}\right)\right)$

### Proof

Step Hyp Ref Expression
1 3simpa ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in ℤ\wedge {M}\in ℤ\right)$
2 3simpb ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in ℤ\wedge {N}\in ℤ\right)$
3 zsubcl ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to {M}-{N}\in ℤ$
4 3 anim2i ${⊢}\left({K}\in ℤ\wedge \left({M}\in ℤ\wedge {N}\in ℤ\right)\right)\to \left({K}\in ℤ\wedge {M}-{N}\in ℤ\right)$
5 4 3impb ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in ℤ\wedge {M}-{N}\in ℤ\right)$
6 zsubcl ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\right)\to {x}-{y}\in ℤ$
7 6 adantl ${⊢}\left(\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\to {x}-{y}\in ℤ$
8 zcn ${⊢}{x}\in ℤ\to {x}\in ℂ$
9 zcn ${⊢}{y}\in ℤ\to {y}\in ℂ$
10 zcn ${⊢}{K}\in ℤ\to {K}\in ℂ$
11 subdir ${⊢}\left({x}\in ℂ\wedge {y}\in ℂ\wedge {K}\in ℂ\right)\to \left({x}-{y}\right){K}={x}{K}-{y}{K}$
12 8 9 10 11 syl3an ${⊢}\left({x}\in ℤ\wedge {y}\in ℤ\wedge {K}\in ℤ\right)\to \left({x}-{y}\right){K}={x}{K}-{y}{K}$
13 12 3comr ${⊢}\left({K}\in ℤ\wedge {x}\in ℤ\wedge {y}\in ℤ\right)\to \left({x}-{y}\right){K}={x}{K}-{y}{K}$
14 13 3expb ${⊢}\left({K}\in ℤ\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\to \left({x}-{y}\right){K}={x}{K}-{y}{K}$
15 oveq12 ${⊢}\left({x}{K}={M}\wedge {y}{K}={N}\right)\to {x}{K}-{y}{K}={M}-{N}$
16 14 15 sylan9eq ${⊢}\left(\left({K}\in ℤ\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\wedge \left({x}{K}={M}\wedge {y}{K}={N}\right)\right)\to \left({x}-{y}\right){K}={M}-{N}$
17 16 ex ${⊢}\left({K}\in ℤ\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\to \left(\left({x}{K}={M}\wedge {y}{K}={N}\right)\to \left({x}-{y}\right){K}={M}-{N}\right)$
18 17 3ad2antl1 ${⊢}\left(\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({x}\in ℤ\wedge {y}\in ℤ\right)\right)\to \left(\left({x}{K}={M}\wedge {y}{K}={N}\right)\to \left({x}-{y}\right){K}={M}-{N}\right)$
19 1 2 5 7 18 dvds2lem ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\parallel {M}\wedge {K}\parallel {N}\right)\to {K}\parallel \left({M}-{N}\right)\right)$