Step | Hyp | Ref
| Expression |
1 | | simpl2 1001 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ๐ต โ โ) |
2 | | simpl1 1000 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ๐ด โ โ) |
3 | 1, 2 | resubcld 8340 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ต โ ๐ด) โ โ) |
4 | | simpl3l 1052 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ๐ถ โ โ) |
5 | | simpr 110 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ๐ด โค ๐ต) |
6 | 1, 2 | subge0d 8494 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (0 โค (๐ต โ ๐ด) โ ๐ด โค ๐ต)) |
7 | 5, 6 | mpbird 167 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ 0 โค (๐ต โ ๐ด)) |
8 | | simpl3r 1053 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ 0 โค ๐ถ) |
9 | 3, 4, 7, 8 | mulge0d 8580 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ 0 โค ((๐ต โ ๐ด) ยท ๐ถ)) |
10 | 1 | recnd 7988 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ๐ต โ โ) |
11 | 2 | recnd 7988 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ๐ด โ โ) |
12 | 4 | recnd 7988 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ๐ถ โ โ) |
13 | 10, 11, 12 | subdird 8374 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ ((๐ต โ ๐ด) ยท ๐ถ) = ((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ))) |
14 | 9, 13 | breqtrd 4031 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ 0 โค ((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ))) |
15 | 1, 4 | remulcld 7990 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ต ยท ๐ถ) โ โ) |
16 | 2, 4 | remulcld 7990 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยท ๐ถ) โ โ) |
17 | 15, 16 | subge0d 8494 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (0 โค ((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ))) |
18 | 14, 17 | mpbid 147 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 โค
๐ถ)) โง ๐ด โค ๐ต) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ถ)) |