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 โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) โˆฅ ๐ธ )