Step |
Hyp |
Ref |
Expression |
1 |
|
remulcl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยท ๐ต ) โ โ ) |
2 |
1
|
le0neg1d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( ๐ด ยท ๐ต ) โค 0 โ 0 โค - ( ๐ด ยท ๐ต ) ) ) |
3 |
|
le0neg2 |
โข ( ๐ต โ โ โ ( 0 โค ๐ต โ - ๐ต โค 0 ) ) |
4 |
3
|
anbi2d |
โข ( ๐ต โ โ โ ( ( ๐ด โค 0 โง 0 โค ๐ต ) โ ( ๐ด โค 0 โง - ๐ต โค 0 ) ) ) |
5 |
|
le0neg1 |
โข ( ๐ต โ โ โ ( ๐ต โค 0 โ 0 โค - ๐ต ) ) |
6 |
5
|
anbi2d |
โข ( ๐ต โ โ โ ( ( 0 โค ๐ด โง ๐ต โค 0 ) โ ( 0 โค ๐ด โง 0 โค - ๐ต ) ) ) |
7 |
4 6
|
orbi12d |
โข ( ๐ต โ โ โ ( ( ( ๐ด โค 0 โง 0 โค ๐ต ) โจ ( 0 โค ๐ด โง ๐ต โค 0 ) ) โ ( ( ๐ด โค 0 โง - ๐ต โค 0 ) โจ ( 0 โค ๐ด โง 0 โค - ๐ต ) ) ) ) |
8 |
7
|
adantl |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( ( ๐ด โค 0 โง 0 โค ๐ต ) โจ ( 0 โค ๐ด โง ๐ต โค 0 ) ) โ ( ( ๐ด โค 0 โง - ๐ต โค 0 ) โจ ( 0 โค ๐ด โง 0 โค - ๐ต ) ) ) ) |
9 |
|
renegcl |
โข ( ๐ต โ โ โ - ๐ต โ โ ) |
10 |
|
mulge0b |
โข ( ( ๐ด โ โ โง - ๐ต โ โ ) โ ( 0 โค ( ๐ด ยท - ๐ต ) โ ( ( ๐ด โค 0 โง - ๐ต โค 0 ) โจ ( 0 โค ๐ด โง 0 โค - ๐ต ) ) ) ) |
11 |
9 10
|
sylan2 |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( 0 โค ( ๐ด ยท - ๐ต ) โ ( ( ๐ด โค 0 โง - ๐ต โค 0 ) โจ ( 0 โค ๐ด โง 0 โค - ๐ต ) ) ) ) |
12 |
|
recn |
โข ( ๐ด โ โ โ ๐ด โ โ ) |
13 |
|
recn |
โข ( ๐ต โ โ โ ๐ต โ โ ) |
14 |
|
mulneg2 |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ๐ด ยท - ๐ต ) = - ( ๐ด ยท ๐ต ) ) |
15 |
14
|
breq2d |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( 0 โค ( ๐ด ยท - ๐ต ) โ 0 โค - ( ๐ด ยท ๐ต ) ) ) |
16 |
12 13 15
|
syl2an |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( 0 โค ( ๐ด ยท - ๐ต ) โ 0 โค - ( ๐ด ยท ๐ต ) ) ) |
17 |
8 11 16
|
3bitr2rd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( 0 โค - ( ๐ด ยท ๐ต ) โ ( ( ๐ด โค 0 โง 0 โค ๐ต ) โจ ( 0 โค ๐ด โง ๐ต โค 0 ) ) ) ) |
18 |
2 17
|
bitrd |
โข ( ( ๐ด โ โ โง ๐ต โ โ ) โ ( ( ๐ด ยท ๐ต ) โค 0 โ ( ( ๐ด โค 0 โง 0 โค ๐ต ) โจ ( 0 โค ๐ด โง ๐ต โค 0 ) ) ) ) |