Theorem lcmineqlem14

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

	Ref	Expression
Hypotheses	lcmineqlem14.1	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	lcmineqlem14.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	lcmineqlem14.3	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	lcmineqlem14.4	⊢ ( 𝜑 → 𝐷 ∈ ℕ )
	lcmineqlem14.5	⊢ ( 𝜑 → 𝐸 ∈ ℕ )
	lcmineqlem14.6	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∥ 𝐷 )
	lcmineqlem14.7	⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∥ 𝐸 )
	lcmineqlem14.8	⊢ ( 𝜑 → 𝐷 ∥ 𝐸 )
	lcmineqlem14.9	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
Assertion	lcmineqlem14	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · 𝐶 ) ∥ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem14.1	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
2		lcmineqlem14.2	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
3		lcmineqlem14.3	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
4		lcmineqlem14.4	⊢ ( 𝜑 → 𝐷 ∈ ℕ )
5		lcmineqlem14.5	⊢ ( 𝜑 → 𝐸 ∈ ℕ )
6		lcmineqlem14.6	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∥ 𝐷 )
7		lcmineqlem14.7	⊢ ( 𝜑 → ( 𝐵 · 𝐶 ) ∥ 𝐸 )
8		lcmineqlem14.8	⊢ ( 𝜑 → 𝐷 ∥ 𝐸 )
9		lcmineqlem14.9	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
10	1	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
11	2	nnzd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
12	2 3 5	nnproddivdvdsd	⊢ ( 𝜑 → ( ( 𝐵 · 𝐶 ) ∥ 𝐸 ↔ 𝐵 ∥ ( 𝐸 / 𝐶 ) ) )
13	7 12	mpbid	⊢ ( 𝜑 → 𝐵 ∥ ( 𝐸 / 𝐶 ) )
14		dvdszrcl	⊢ ( 𝐵 ∥ ( 𝐸 / 𝐶 ) → ( 𝐵 ∈ ℤ ∧ ( 𝐸 / 𝐶 ) ∈ ℤ ) )
15	13 14	syl	⊢ ( 𝜑 → ( 𝐵 ∈ ℤ ∧ ( 𝐸 / 𝐶 ) ∈ ℤ ) )
16	15	simprd	⊢ ( 𝜑 → ( 𝐸 / 𝐶 ) ∈ ℤ )
17	3	nnzd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
18	10 17	zmulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℤ )
19	4	nnzd	⊢ ( 𝜑 → 𝐷 ∈ ℤ )
20	5	nnzd	⊢ ( 𝜑 → 𝐸 ∈ ℤ )
21	18 19 20 6 8	dvdstrd	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∥ 𝐸 )
22	1 3 5	nnproddivdvdsd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) ∥ 𝐸 ↔ 𝐴 ∥ ( 𝐸 / 𝐶 ) ) )
23	21 22	mpbid	⊢ ( 𝜑 → 𝐴 ∥ ( 𝐸 / 𝐶 ) )
24	10 11 16 9 23 13	coprmdvds2d	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∥ ( 𝐸 / 𝐶 ) )
25	1 2	nnmulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℕ )
26	25 3 5	nnproddivdvdsd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐵 ) · 𝐶 ) ∥ 𝐸 ↔ ( 𝐴 · 𝐵 ) ∥ ( 𝐸 / 𝐶 ) ) )
27	24 26	mpbird	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) · 𝐶 ) ∥ 𝐸 )