Step | Hyp | Ref
| Expression |
1 | | 0re 7970 |
. . . 4
โข 0 โ
โ |
2 | | 1re 7969 |
. . . 4
โข 1 โ
โ |
3 | 1, 2 | elicc2i 9952 |
. . 3
โข ((๐ด / ๐ต) โ (0[,]1) โ ((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1)) |
4 | | df-3an 981 |
. . 3
โข (((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต) โง (๐ด / ๐ต) โค 1) โ (((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต)) โง (๐ด / ๐ต) โค 1)) |
5 | 3, 4 | bitri 184 |
. 2
โข ((๐ด / ๐ต) โ (0[,]1) โ (((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต)) โง (๐ด / ๐ต) โค 1)) |
6 | | ledivmul 8847 |
. . . . 5
โข ((๐ด โ โ โง 1 โ
โ โง (๐ต โ
โ โง 0 < ๐ต))
โ ((๐ด / ๐ต) โค 1 โ ๐ด โค (๐ต ยท 1))) |
7 | 2, 6 | mp3an2 1335 |
. . . 4
โข ((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โ ((๐ด / ๐ต) โค 1 โ ๐ด โค (๐ต ยท 1))) |
8 | 7 | adantlr 477 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((๐ด / ๐ต) โค 1 โ ๐ด โค (๐ต ยท 1))) |
9 | | simpll 527 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ด โ โ) |
10 | | simprl 529 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ต โ โ) |
11 | | gt0ap0 8596 |
. . . . . . 7
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต # 0) |
12 | 11 | adantl 277 |
. . . . . 6
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ต # 0) |
13 | 9, 10, 12 | redivclapd 8805 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด / ๐ต) โ โ) |
14 | | divge0 8843 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ 0 โค (๐ด / ๐ต)) |
15 | 13, 14 | jca 306 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต))) |
16 | 15 | biantrurd 305 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((๐ด / ๐ต) โค 1 โ (((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต)) โง (๐ด / ๐ต) โค 1))) |
17 | | recn 7957 |
. . . . . 6
โข (๐ต โ โ โ ๐ต โ
โ) |
18 | 17 | ad2antrl 490 |
. . . . 5
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ๐ต โ โ) |
19 | 18 | mulridd 7987 |
. . . 4
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ต ยท 1) = ๐ต) |
20 | 19 | breq2d 4027 |
. . 3
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด โค (๐ต ยท 1) โ ๐ด โค ๐ต)) |
21 | 8, 16, 20 | 3bitr3d 218 |
. 2
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((((๐ด / ๐ต) โ โ โง 0 โค (๐ด / ๐ต)) โง (๐ด / ๐ต) โค 1) โ ๐ด โค ๐ต)) |
22 | 5, 21 | bitrid 192 |
1
โข (((๐ด โ โ โง 0 โค
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((๐ด / ๐ต) โ (0[,]1) โ ๐ด โค ๐ต)) |