Step | Hyp | Ref
| Expression |
1 | | simpl2 1192 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ๐ต โ โ) |
2 | | simpl1 1191 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ๐ด โ โ) |
3 | 1, 2 | resubcld 11641 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ (๐ต โ ๐ด) โ โ) |
4 | | simpl3l 1228 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ๐ถ โ โ) |
5 | | simpr 485 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ๐ด < ๐ต) |
6 | 2, 1 | posdifd 11800 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ (๐ด < ๐ต โ 0 < (๐ต โ ๐ด))) |
7 | 5, 6 | mpbid 231 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ 0 < (๐ต โ ๐ด)) |
8 | | simpl3r 1229 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ 0 < ๐ถ) |
9 | 3, 4, 7, 8 | mulgt0d 11368 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ 0 < ((๐ต โ ๐ด) ยท ๐ถ)) |
10 | 1 | recnd 11241 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ๐ต โ โ) |
11 | 2 | recnd 11241 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ๐ด โ โ) |
12 | 4 | recnd 11241 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ๐ถ โ โ) |
13 | 10, 11, 12 | subdird 11670 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ((๐ต โ ๐ด) ยท ๐ถ) = ((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ))) |
14 | 9, 13 | breqtrd 5174 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ 0 < ((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ))) |
15 | 2, 4 | remulcld 11243 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ (๐ด ยท ๐ถ) โ โ) |
16 | 1, 4 | remulcld 11243 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ (๐ต ยท ๐ถ) โ โ) |
17 | 15, 16 | posdifd 11800 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ ((๐ด ยท ๐ถ) < (๐ต ยท ๐ถ) โ 0 < ((๐ต ยท ๐ถ) โ (๐ด ยท ๐ถ)))) |
18 | 14, 17 | mpbird 256 |
1
โข (((๐ด โ โ โง ๐ต โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โง ๐ด < ๐ต) โ (๐ด ยท ๐ถ) < (๐ต ยท ๐ถ)) |