Step | Hyp | Ref
| Expression |
1 | | resubcl 11473 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต) โ โ) |
2 | 1 | 3adant3 1133 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด โ ๐ต) โ โ) |
3 | | resubcl 11473 |
. . . . 5
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ โ ๐ต) โ โ) |
4 | 3 | ancoms 460 |
. . . 4
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ต) โ โ) |
5 | 4 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ โ ๐ต) โ โ) |
6 | | mulle0b 12034 |
. . 3
โข (((๐ด โ ๐ต) โ โ โง (๐ถ โ ๐ต) โ โ) โ (((๐ด โ ๐ต) ยท (๐ถ โ ๐ต)) โค 0 โ (((๐ด โ ๐ต) โค 0 โง 0 โค (๐ถ โ ๐ต)) โจ (0 โค (๐ด โ ๐ต) โง (๐ถ โ ๐ต) โค 0)))) |
7 | 2, 5, 6 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด โ ๐ต) ยท (๐ถ โ ๐ต)) โค 0 โ (((๐ด โ ๐ต) โค 0 โง 0 โค (๐ถ โ ๐ต)) โจ (0 โค (๐ด โ ๐ต) โง (๐ถ โ ๐ต) โค 0)))) |
8 | | suble0 11677 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ) โ ((๐ด โ ๐ต) โค 0 โ ๐ด โค ๐ต)) |
9 | 8 | 3adant3 1133 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ต) โค 0 โ ๐ด โค ๐ต)) |
10 | | subge0 11676 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ต โ โ) โ (0 โค
(๐ถ โ ๐ต) โ ๐ต โค ๐ถ)) |
11 | 10 | ancoms 460 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ (0 โค
(๐ถ โ ๐ต) โ ๐ต โค ๐ถ)) |
12 | 11 | 3adant1 1131 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (0 โค
(๐ถ โ ๐ต) โ ๐ต โค ๐ถ)) |
13 | 9, 12 | anbi12d 632 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด โ ๐ต) โค 0 โง 0 โค (๐ถ โ ๐ต)) โ (๐ด โค ๐ต โง ๐ต โค ๐ถ))) |
14 | | subge0 11676 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ) โ (0 โค
(๐ด โ ๐ต) โ ๐ต โค ๐ด)) |
15 | 14 | 3adant3 1133 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (0 โค
(๐ด โ ๐ต) โ ๐ต โค ๐ด)) |
16 | | suble0 11677 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ต โ โ) โ ((๐ถ โ ๐ต) โค 0 โ ๐ถ โค ๐ต)) |
17 | 16 | ancoms 460 |
. . . . . 6
โข ((๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ โ ๐ต) โค 0 โ ๐ถ โค ๐ต)) |
18 | 17 | 3adant1 1131 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ โ ๐ต) โค 0 โ ๐ถ โค ๐ต)) |
19 | 15, 18 | anbi12d 632 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((0 โค
(๐ด โ ๐ต) โง (๐ถ โ ๐ต) โค 0) โ (๐ต โค ๐ด โง ๐ถ โค ๐ต))) |
20 | 19 | biancomd 465 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((0 โค
(๐ด โ ๐ต) โง (๐ถ โ ๐ต) โค 0) โ (๐ถ โค ๐ต โง ๐ต โค ๐ด))) |
21 | 13, 20 | orbi12d 918 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
((((๐ด โ ๐ต) โค 0 โง 0 โค (๐ถ โ ๐ต)) โจ (0 โค (๐ด โ ๐ต) โง (๐ถ โ ๐ต) โค 0)) โ ((๐ด โค ๐ต โง ๐ต โค ๐ถ) โจ (๐ถ โค ๐ต โง ๐ต โค ๐ด)))) |
22 | 7, 21 | bitrd 279 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด โ ๐ต) ยท (๐ถ โ ๐ต)) โค 0 โ ((๐ด โค ๐ต โง ๐ต โค ๐ถ) โจ (๐ถ โค ๐ต โง ๐ต โค ๐ด)))) |