Theorem dvds2subd

Description: Deduction form of dvds2sub . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	dvds2subd.k	$$⊢\phi \to K\in \mathbb{Z}$$
	dvds2subd.m	$$⊢\phi \to M\in \mathbb{Z}$$
	dvds2subd.n	$$⊢\phi \to N\in \mathbb{Z}$$
	dvds2subd.1	$$⊢\phi \to K\parallel M$$
	dvds2subd.2	$$⊢\phi \to K\parallel N$$
Assertion	dvds2subd	$$⊢\phi \to K\parallel \left(M-N\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvds2subd.k	$$⊢\phi \to K\in \mathbb{Z}$$
2		dvds2subd.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		dvds2subd.n	$$⊢\phi \to N\in \mathbb{Z}$$
4		dvds2subd.1	$$⊢\phi \to K\parallel M$$
5		dvds2subd.2	$$⊢\phi \to K\parallel N$$
6		dvds2sub	$$⊢\left(K\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(\left(K\parallel M\wedge K\parallel N\right)\to K\parallel \left(M-N\right)\right)$$
7	1 2 3 6	syl3anc	$$⊢\phi \to \left(\left(K\parallel M\wedge K\parallel N\right)\to K\parallel \left(M-N\right)\right)$$
8	4 5 7	mp2and	$$⊢\phi \to K\parallel \left(M-N\right)$$