Theorem lcmineqlem14

Description: Technical lemma for inequality estimate. (Contributed by metakunt, 12-May-2024)

	Ref	Expression
Hypotheses	lcmineqlem14.1	$$⊢\phi \to A\in \mathbb{N}$$
	lcmineqlem14.2	$$⊢\phi \to B\in \mathbb{N}$$
	lcmineqlem14.3	$$⊢\phi \to C\in \mathbb{N}$$
	lcmineqlem14.4	$$⊢\phi \to D\in \mathbb{N}$$
	lcmineqlem14.5	$$⊢\phi \to E\in \mathbb{N}$$
	lcmineqlem14.6	$$⊢\phi \to AC\parallel D$$
	lcmineqlem14.7	$$⊢\phi \to BC\parallel E$$
	lcmineqlem14.8	$$⊢\phi \to D\parallel E$$
	lcmineqlem14.9	$$⊢\phi \to A\gcd B=1$$
Assertion	lcmineqlem14	$$⊢\phi \to ABC\parallel E$$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem14.1	$$⊢\phi \to A\in \mathbb{N}$$
2		lcmineqlem14.2	$$⊢\phi \to B\in \mathbb{N}$$
3		lcmineqlem14.3	$$⊢\phi \to C\in \mathbb{N}$$
4		lcmineqlem14.4	$$⊢\phi \to D\in \mathbb{N}$$
5		lcmineqlem14.5	$$⊢\phi \to E\in \mathbb{N}$$
6		lcmineqlem14.6	$$⊢\phi \to AC\parallel D$$
7		lcmineqlem14.7	$$⊢\phi \to BC\parallel E$$
8		lcmineqlem14.8	$$⊢\phi \to D\parallel E$$
9		lcmineqlem14.9	$$⊢\phi \to A\gcd B=1$$
10	1	nnzd	$$⊢\phi \to A\in \mathbb{Z}$$
11	2	nnzd	$$⊢\phi \to B\in \mathbb{Z}$$
12	2 3 5	nnproddivdvdsd	$$⊢\phi \to \left(BC\parallel E\leftrightarrow B\parallel \left(\frac{E}{C}\right)\right)$$
13	7 12	mpbid	$$⊢\phi \to B\parallel \left(\frac{E}{C}\right)$$
14		dvdszrcl	$$⊢B\parallel \left(\frac{E}{C}\right)\to \left(B\in \mathbb{Z}\wedge \frac{E}{C}\in \mathbb{Z}\right)$$
15	13 14	syl	$$⊢\phi \to \left(B\in \mathbb{Z}\wedge \frac{E}{C}\in \mathbb{Z}\right)$$
16	15	simprd	$$⊢\phi \to \frac{E}{C}\in \mathbb{Z}$$
17	3	nnzd	$$⊢\phi \to C\in \mathbb{Z}$$
18	10 17	zmulcld	$$⊢\phi \to AC\in \mathbb{Z}$$
19	4	nnzd	$$⊢\phi \to D\in \mathbb{Z}$$
20	5	nnzd	$$⊢\phi \to E\in \mathbb{Z}$$
21	18 19 20 6 8	dvdstrd	$$⊢\phi \to AC\parallel E$$
22	1 3 5	nnproddivdvdsd	$$⊢\phi \to \left(AC\parallel E\leftrightarrow A\parallel \left(\frac{E}{C}\right)\right)$$
23	21 22	mpbid	$$⊢\phi \to A\parallel \left(\frac{E}{C}\right)$$
24	10 11 16 9 23 13	coprmdvds2d	$$⊢\phi \to AB\parallel \left(\frac{E}{C}\right)$$
25	1 2	nnmulcld	$$⊢\phi \to AB\in \mathbb{N}$$
26	25 3 5	nnproddivdvdsd	$$⊢\phi \to \left(ABC\parallel E\leftrightarrow AB\parallel \left(\frac{E}{C}\right)\right)$$
27	24 26	mpbird	$$⊢\phi \to ABC\parallel E$$