Step | Hyp | Ref
| Expression |
1 | | ltrec 12095 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) |
2 | 1 | 3adant3 1132 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (1 / ๐ต) < (1 / ๐ด))) |
3 | | gt0ne0 11678 |
. . . . . 6
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ 0) |
4 | | rereccl 11931 |
. . . . . 6
โข ((๐ต โ โ โง ๐ต โ 0) โ (1 / ๐ต) โ
โ) |
5 | 3, 4 | syldan 591 |
. . . . 5
โข ((๐ต โ โ โง 0 <
๐ต) โ (1 / ๐ต) โ
โ) |
6 | | gt0ne0 11678 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ 0) |
7 | | rereccl 11931 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) โ
โ) |
8 | 6, 7 | syldan 591 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด) โ (1 / ๐ด) โ
โ) |
9 | | ltmul2 12064 |
. . . . . 6
โข (((1 /
๐ต) โ โ โง (1
/ ๐ด) โ โ โง
(๐ถ โ โ โง 0
< ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
10 | 8, 9 | syl3an2 1164 |
. . . . 5
โข (((1 /
๐ต) โ โ โง
(๐ด โ โ โง 0
< ๐ด) โง (๐ถ โ โ โง 0 <
๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
11 | 5, 10 | syl3an1 1163 |
. . . 4
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ด โ โ โง 0 < ๐ด) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
12 | | recn 11199 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โ) |
13 | 12 | adantr 481 |
. . . . . 6
โข ((๐ถ โ โ โง 0 <
๐ถ) โ ๐ถ โ โ) |
14 | | recn 11199 |
. . . . . . . 8
โข (๐ต โ โ โ ๐ต โ
โ) |
15 | 14 | adantr 481 |
. . . . . . 7
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ โ) |
16 | 15, 3 | jca 512 |
. . . . . 6
โข ((๐ต โ โ โง 0 <
๐ต) โ (๐ต โ โ โง ๐ต โ 0)) |
17 | | recn 11199 |
. . . . . . . 8
โข (๐ด โ โ โ ๐ด โ
โ) |
18 | 17 | adantr 481 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ โ) |
19 | 18, 6 | jca 512 |
. . . . . 6
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด โ โ โง ๐ด โ 0)) |
20 | | divrec 11887 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
21 | 20 | 3expb 1120 |
. . . . . . . 8
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
22 | 21 | 3adant3 1132 |
. . . . . . 7
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
23 | | divrec 11887 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ด โ 0) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
24 | 23 | 3expb 1120 |
. . . . . . . 8
โข ((๐ถ โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
25 | 24 | 3adant2 1131 |
. . . . . . 7
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
26 | 22, 25 | breq12d 5161 |
. . . . . 6
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0) โง (๐ด โ โ โง ๐ด โ 0)) โ ((๐ถ / ๐ต) < (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
27 | 13, 16, 19, 26 | syl3an 1160 |
. . . . 5
โข (((๐ถ โ โ โง 0 <
๐ถ) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ด โ โ โง 0 < ๐ด)) โ ((๐ถ / ๐ต) < (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
28 | 27 | 3coml 1127 |
. . . 4
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ด โ โ โง 0 < ๐ด) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ถ / ๐ต) < (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) < (๐ถ ยท (1 / ๐ด)))) |
29 | 11, 28 | bitr4d 281 |
. . 3
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ด โ โ โง 0 < ๐ด) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) |
30 | 29 | 3com12 1123 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((1 / ๐ต) < (1 / ๐ด) โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) |
31 | 2, 30 | bitrd 278 |
1
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด < ๐ต โ (๐ถ / ๐ต) < (๐ถ / ๐ด))) |