Step | Hyp | Ref
| Expression |
1 | | 1red 7974 |
. . . 4
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 1 โ
โ) |
2 | | simprl 529 |
. . . 4
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ต โ โ) |
3 | | simpll 527 |
. . . 4
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ด โ โ) |
4 | | simplr 528 |
. . . 4
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 < ๐ด) |
5 | | ltmuldiv 8833 |
. . . 4
โข ((1
โ โ โง ๐ต
โ โ โง (๐ด
โ โ โง 0 < ๐ด)) โ ((1 ยท ๐ด) < ๐ต โ 1 < (๐ต / ๐ด))) |
6 | 1, 2, 3, 4, 5 | syl112anc 1242 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((1 ยท ๐ด) < ๐ต โ 1 < (๐ต / ๐ด))) |
7 | 3 | recnd 7988 |
. . . . 5
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ด โ โ) |
8 | 7 | mulid2d 7978 |
. . . 4
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (1 ยท ๐ด) = ๐ด) |
9 | 8 | breq1d 4015 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((1 ยท ๐ด) < ๐ต โ ๐ด < ๐ต)) |
10 | 2 | recnd 7988 |
. . . . 5
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ต โ โ) |
11 | 3, 4 | gt0ap0d 8588 |
. . . . 5
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ด # 0) |
12 | 10, 7, 11 | divrecapd 8752 |
. . . 4
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ต / ๐ด) = (๐ต ยท (1 / ๐ด))) |
13 | 12 | breq2d 4017 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (1 < (๐ต / ๐ด) โ 1 < (๐ต ยท (1 / ๐ด)))) |
14 | 6, 9, 13 | 3bitr3d 218 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด < ๐ต โ 1 < (๐ต ยท (1 / ๐ด)))) |
15 | 3, 11 | rerecclapd 8793 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (1 / ๐ด) โ โ) |
16 | | simprr 531 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 < ๐ต) |
17 | | ltdivmul 8835 |
. . 3
โข ((1
โ โ โง (1 / ๐ด) โ โ โง (๐ต โ โ โง 0 < ๐ต)) โ ((1 / ๐ต) < (1 / ๐ด) โ 1 < (๐ต ยท (1 / ๐ด)))) |
18 | 1, 15, 2, 16, 17 | syl112anc 1242 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((1 / ๐ต) < (1 / ๐ด) โ 1 < (๐ต ยท (1 / ๐ด)))) |
19 | 14, 18 | bitr4d 191 |
1
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) |