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 |
โข ( ๐ โ ( ( ๐ด ยท ๐ต ) ยท ๐ถ ) โฅ ๐ธ ) |