Metamath Proof Explorer


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 ( 𝜑 → ( ( 𝐴 · 𝐵 ) · 𝐶 ) ∥ 𝐸 )