Theorem dvdsmultr2d

Description: Deduction form of dvdsmultr2 . (Contributed by SN, 23-Aug-2024)

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

Proof

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