Theorem dvdstrd

Description: The divides relation is transitive, a deduction version of dvdstr . (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	dvdstrd.1	$$⊢\phi \to K\in \mathbb{Z}$$
	dvdstrd.2	$$⊢\phi \to M\in \mathbb{Z}$$
	dvdstrd.3	$$⊢\phi \to N\in \mathbb{Z}$$
	dvdstrd.4	$$⊢\phi \to K\parallel M$$
	dvdstrd.5	$$⊢\phi \to M\parallel N$$
Assertion	dvdstrd	$$⊢\phi \to K\parallel N$$

Proof

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