Step |
Hyp |
Ref |
Expression |
1 |
|
ltp1d.1 |
โข ( ๐ โ ๐ด โ โ ) |
2 |
|
divgt0d.2 |
โข ( ๐ โ ๐ต โ โ ) |
3 |
|
lemul1ad.3 |
โข ( ๐ โ ๐ถ โ โ ) |
4 |
|
lemul1ad.4 |
โข ( ๐ โ 0 โค ๐ถ ) |
5 |
|
lemul1ad.5 |
โข ( ๐ โ ๐ด โค ๐ต ) |
6 |
3 4
|
jca |
โข ( ๐ โ ( ๐ถ โ โ โง 0 โค ๐ถ ) ) |
7 |
|
lemul2a |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 โค ๐ถ ) ) โง ๐ด โค ๐ต ) โ ( ๐ถ ยท ๐ด ) โค ( ๐ถ ยท ๐ต ) ) |
8 |
1 2 6 5 7
|
syl31anc |
โข ( ๐ โ ( ๐ถ ยท ๐ด ) โค ( ๐ถ ยท ๐ต ) ) |