Step |
Hyp |
Ref |
Expression |
1 |
|
ltp1d.1 |
โข ( ๐ โ ๐ด โ โ ) |
2 |
|
divgt0d.2 |
โข ( ๐ โ ๐ต โ โ ) |
3 |
|
lemul1ad.3 |
โข ( ๐ โ ๐ถ โ โ ) |
4 |
|
ltmul12ad.3 |
โข ( ๐ โ ๐ท โ โ ) |
5 |
|
lemul12bd.4 |
โข ( ๐ โ 0 โค ๐ด ) |
6 |
|
lemul12bd.5 |
โข ( ๐ โ 0 โค ๐ท ) |
7 |
|
lemul12bd.6 |
โข ( ๐ โ ๐ด โค ๐ต ) |
8 |
|
lemul12bd.7 |
โข ( ๐ โ ๐ถ โค ๐ท ) |
9 |
1 5
|
jca |
โข ( ๐ โ ( ๐ด โ โ โง 0 โค ๐ด ) ) |
10 |
4 6
|
jca |
โข ( ๐ โ ( ๐ท โ โ โง 0 โค ๐ท ) ) |
11 |
|
lemul12b |
โข ( ( ( ( ๐ด โ โ โง 0 โค ๐ด ) โง ๐ต โ โ ) โง ( ๐ถ โ โ โง ( ๐ท โ โ โง 0 โค ๐ท ) ) ) โ ( ( ๐ด โค ๐ต โง ๐ถ โค ๐ท ) โ ( ๐ด ยท ๐ถ ) โค ( ๐ต ยท ๐ท ) ) ) |
12 |
9 2 3 10 11
|
syl22anc |
โข ( ๐ โ ( ( ๐ด โค ๐ต โง ๐ถ โค ๐ท ) โ ( ๐ด ยท ๐ถ ) โค ( ๐ต ยท ๐ท ) ) ) |
13 |
7 8 12
|
mp2and |
โข ( ๐ โ ( ๐ด ยท ๐ถ ) โค ( ๐ต ยท ๐ท ) ) |