This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ∧ K ∥ N → K ∥ M − N

Proof

Step Hyp Ref Expression
1 3simpa ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ ∧ M ∈ ℤ
2 3simpb ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ ∧ N ∈ ℤ
3 zsubcl ⊢ M ∈ ℤ ∧ N ∈ ℤ → M − N ∈ ℤ
4 3 anim2i ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ ∧ M − N ∈ ℤ
5 4 3impb ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ ∧ M − N ∈ ℤ
6 zsubcl ⊢ x ∈ ℤ ∧ y ∈ ℤ → x − y ∈ ℤ
7 6 adantl ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ x ∈ ℤ ∧ y ∈ ℤ → x − y ∈ ℤ
8 zcn ⊢ x ∈ ℤ → x ∈ ℂ
9 zcn ⊢ y ∈ ℤ → y ∈ ℂ
10 zcn ⊢ K ∈ ℤ → K ∈ ℂ
11 subdir ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ K ∈ ℂ → x − y ⁢ K = x ⁢ K − y ⁢ K
12 8 9 10 11 syl3an ⊢ x ∈ ℤ ∧ y ∈ ℤ ∧ K ∈ ℤ → x − y ⁢ K = x ⁢ K − y ⁢ K
13 12 3comr ⊢ K ∈ ℤ ∧ x ∈ ℤ ∧ y ∈ ℤ → x − y ⁢ K = x ⁢ K − y ⁢ K
14 13 3expb ⊢ K ∈ ℤ ∧ x ∈ ℤ ∧ y ∈ ℤ → x − y ⁢ K = x ⁢ K − y ⁢ K
15 oveq12 ⊢ x ⁢ K = M ∧ y ⁢ K = N → x ⁢ K − y ⁢ K = M − N
16 14 15 sylan9eq ⊢ K ∈ ℤ ∧ x ∈ ℤ ∧ y ∈ ℤ ∧ x ⁢ K = M ∧ y ⁢ K = N → x − y ⁢ K = M − N
17 16 ex ⊢ K ∈ ℤ ∧ x ∈ ℤ ∧ y ∈ ℤ → x ⁢ K = M ∧ y ⁢ K = N → x − y ⁢ K = M − N
18 17 3ad2antl1 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ ∧ x ∈ ℤ ∧ y ∈ ℤ → x ⁢ K = M ∧ y ⁢ K = N → x − y ⁢ K = M − N
19 1 2 5 7 18 dvds2lem ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∥ M ∧ K ∥ N → K ∥ M − N