Step | Hyp | Ref
| Expression |
1 | | ltrec 12045 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) |
2 | 1 | 3adant3 1133 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) |
3 | | gt0ne0 11628 |
. . . . . 6
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ 0) |
4 | | rereccl 11881 |
. . . . . 6
โข ((๐ต โ โ โง ๐ต โ 0) โ (1 / ๐ต) โ
โ) |
5 | 3, 4 | syldan 592 |
. . . . 5
โข ((๐ต โ โ โง 0 <
๐ต) โ (1 / ๐ต) โ
โ) |
6 | | gt0ne0 11628 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ 0) |
7 | | rereccl 11881 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) โ
โ) |
8 | 6, 7 | syldan 592 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด) โ (1 / ๐ด) โ
โ) |
9 | | ltmul2 12014 |
. . . . . 6
โข (((1 /
๐ต) โ โ โง (1
/ ๐ด) โ โ โง
(๐ถ โ โ โง 0
< ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
10 | 8, 9 | syl3an2 1165 |
. . . . 5
โข (((1 /
๐ต) โ โ โง
(๐ด โ โ โง 0
< ๐ด) โง (๐ถ โ โ โง 0 <
๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
11 | 5, 10 | syl3an1 1164 |
. . . 4
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ด โ โ โง 0 < ๐ด) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
12 | | recn 11149 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โ) |
13 | 12 | adantr 482 |
. . . . . 6
โข ((๐ถ โ โ โง 0 <
๐ถ) โ ๐ถ โ โ) |
14 | | recn 11149 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ) |
15 | 14 | adantr 482 |
. . . . . . 7
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ โ) |
16 | 15, 3 | jca 513 |
. . . . . 6
โข ((๐ต โ โ โง 0 <
๐ต) โ (๐ต โ โ โง ๐ต โ 0)) |
17 | | recn 11149 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
18 | 17 | adantr 482 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ โ) |
19 | 18, 6 | jca 513 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด โ โ โง ๐ด โ 0)) |
20 | | divrec 11837 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
21 | 20 | 3expb 1121 |
. . . . . . . 8
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
22 | 21 | 3adant3 1133 |
. . . . . . 7
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
23 | | divrec 11837 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ด โ 0) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
24 | 23 | 3expb 1121 |
. . . . . . . 8
โข ((๐ถ โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
25 | 24 | 3adant2 1132 |
. . . . . . 7
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
26 | 22, 25 | breq12d 5122 |
. . . . . 6
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ถ / ๐ต) < (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
27 | 13, 16, 19, 26 | syl3an 1161 |
. . . . 5
โข (((๐ถ โ โ โง 0 <
๐ถ) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ด โ โ โง 0 < ๐ด)) โ ((๐ถ / ๐ต) < (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
28 | 27 | 3coml 1128 |
. . . 4
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ด โ โ โง 0 < ๐ด) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ถ / ๐ต) < (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
29 | 11, 28 | bitr4d 282 |
. . 3
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ด โ โ โง 0 < ๐ด) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) |
30 | 29 | 3com12 1124 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) |
31 | 2, 30 | bitrd 279 |
1
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) |