Theorem dvds2subd

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

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

Proof

Step	Hyp	Ref	Expression
1		dvds2subd.1	$$⊢\phi \to K\in \mathbb{Z}$$
2		dvds2subd.2	$$⊢\phi \to K\parallel M$$
3		dvds2subd.3	$$⊢\phi \to K\parallel N$$
4		dvds2subd.4	$$⊢\phi \to M\in \mathbb{Z}$$
5		dvds2subd.5	$$⊢\phi \to N\in \mathbb{Z}$$
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 4 5 6	syl3anc	$$⊢\phi \to \left(\left(K\parallel M\wedge K\parallel N\right)\to K\parallel \left(M-N\right)\right)$$
8	2 3 7	mp2and	$$⊢\phi \to K\parallel \left(M-N\right)$$