Metamath Proof Explorer


Theorem lcmineqlem14

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

Ref Expression
Hypotheses lcmineqlem14.1 φ A
lcmineqlem14.2 φ B
lcmineqlem14.3 φ C
lcmineqlem14.4 φ D
lcmineqlem14.5 φ E
lcmineqlem14.6 φ A C D
lcmineqlem14.7 φ B C E
lcmineqlem14.8 φ D E
lcmineqlem14.9 φ A gcd B = 1
Assertion lcmineqlem14 φ A B C E

Proof

Step Hyp Ref Expression
1 lcmineqlem14.1 φ A
2 lcmineqlem14.2 φ B
3 lcmineqlem14.3 φ C
4 lcmineqlem14.4 φ D
5 lcmineqlem14.5 φ E
6 lcmineqlem14.6 φ A C D
7 lcmineqlem14.7 φ B C E
8 lcmineqlem14.8 φ D E
9 lcmineqlem14.9 φ A gcd B = 1
10 1 nnzd φ A
11 2 nnzd φ B
12 2 3 5 nnproddivdvdsd φ B C E B E C
13 7 12 mpbid φ B E C
14 dvdszrcl B E C B E C
15 13 14 syl φ B E C
16 15 simprd φ E C
17 3 nnzd φ C
18 10 17 zmulcld φ A C
19 4 nnzd φ D
20 5 nnzd φ E
21 18 19 20 6 8 dvdstrd φ A C E
22 1 3 5 nnproddivdvdsd φ A C E A E C
23 21 22 mpbid φ A E C
24 10 11 16 9 23 13 coprmdvds2d φ A B E C
25 1 2 nnmulcld φ A B
26 25 3 5 nnproddivdvdsd φ A B C E A B E C
27 24 26 mpbird φ A B C E