Theorem dvdsmultr1d

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

	Ref	Expression
Hypotheses	dvdsmultr1d.1	$$⊢\phi \to K\in \mathbb{Z}$$
	dvdsmultr1d.2	$$⊢\phi \to M\in \mathbb{Z}$$
	dvdsmultr1d.3	$$⊢\phi \to N\in \mathbb{Z}$$
	dvdsmultr1d.4	$$⊢\phi \to K\parallel M$$
Assertion	dvdsmultr1d	$$⊢\phi \to K\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		dvdsmultr1d.1	$$⊢\phi \to K\in \mathbb{Z}$$
2		dvdsmultr1d.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		dvdsmultr1d.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		dvdsmultr1d.4	$$⊢\phi \to K\parallel M$$
5		dvdsmultr1	$$⊢\left(K\in \mathbb{Z}\wedge M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(K\parallel M\to K\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
6	1 2 3 5	syl3anc	$$⊢\phi \to \left(K\parallel M\to K\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)$$
7	4 6	mpd	$$⊢\phi \to K\parallel \mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$