Step | Hyp | Ref
| Expression |
1 | | gt0ne0 11625 |
. . . . 5
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ 0) |
2 | | rereccl 11878 |
. . . . 5
โข ((๐ต โ โ โง ๐ต โ 0) โ (1 / ๐ต) โ
โ) |
3 | 1, 2 | syldan 592 |
. . . 4
โข ((๐ต โ โ โง 0 <
๐ต) โ (1 / ๐ต) โ
โ) |
4 | 3 | 3ad2ant2 1135 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (1 / ๐ต) โ โ) |
5 | | gt0ne0 11625 |
. . . . 5
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ 0) |
6 | | rereccl 11878 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) โ
โ) |
7 | 5, 6 | syldan 592 |
. . . 4
โข ((๐ด โ โ โง 0 <
๐ด) โ (1 / ๐ด) โ
โ) |
8 | 7 | 3ad2ant1 1134 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (1 / ๐ด) โ โ) |
9 | | simp3l 1202 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ๐ถ โ โ) |
10 | | simp3r 1203 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ 0 < ๐ถ) |
11 | | lemul2 12013 |
. . 3
โข (((1 /
๐ต) โ โ โง (1
/ ๐ด) โ โ โง
(๐ถ โ โ โง 0
< ๐ถ)) โ ((1 / ๐ต) โค (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) โค (๐ถ ยท (1 / ๐ด)))) |
12 | 4, 8, 9, 10, 11 | syl112anc 1375 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((1 / ๐ต) โค (1 / ๐ด) โ (๐ถ ยท (1 / ๐ต)) โค (๐ถ ยท (1 / ๐ด)))) |
13 | | lerec 12043 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ด โค ๐ต โ (1 / ๐ต) โค (1 / ๐ด))) |
14 | 13 | 3adant3 1133 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด โค ๐ต โ (1 / ๐ต) โค (1 / ๐ด))) |
15 | | recn 11146 |
. . . . . . 7
โข (๐ถ โ โ โ ๐ถ โ
โ) |
16 | | recn 11146 |
. . . . . . . . 9
โข (๐ต โ โ โ ๐ต โ
โ) |
17 | 16 | adantr 482 |
. . . . . . . 8
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ โ) |
18 | 17, 1 | jca 513 |
. . . . . . 7
โข ((๐ต โ โ โง 0 <
๐ต) โ (๐ต โ โ โง ๐ต โ 0)) |
19 | | divrec 11834 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
20 | 19 | 3expb 1121 |
. . . . . . 7
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
21 | 15, 18, 20 | syl2an 597 |
. . . . . 6
โข ((๐ถ โ โ โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
22 | 21 | 3adant2 1132 |
. . . . 5
โข ((๐ถ โ โ โง (๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ถ / ๐ต) = (๐ถ ยท (1 / ๐ต))) |
23 | | recn 11146 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
24 | 23 | adantr 482 |
. . . . . . . 8
โข ((๐ด โ โ โง 0 <
๐ด) โ ๐ด โ โ) |
25 | 24, 5 | jca 513 |
. . . . . . 7
โข ((๐ด โ โ โง 0 <
๐ด) โ (๐ด โ โ โง ๐ด โ 0)) |
26 | | divrec 11834 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ด โ โ โง ๐ด โ 0) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
27 | 26 | 3expb 1121 |
. . . . . . 7
โข ((๐ถ โ โ โง (๐ด โ โ โง ๐ด โ 0)) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
28 | 15, 25, 27 | syl2an 597 |
. . . . . 6
โข ((๐ถ โ โ โง (๐ด โ โ โง 0 <
๐ด)) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
29 | 28 | 3adant3 1133 |
. . . . 5
โข ((๐ถ โ โ โง (๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ (๐ถ / ๐ด) = (๐ถ ยท (1 / ๐ด))) |
30 | 22, 29 | breq12d 5119 |
. . . 4
โข ((๐ถ โ โ โง (๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต)) โ ((๐ถ / ๐ต) โค (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) โค (๐ถ ยท (1 / ๐ด)))) |
31 | 30 | 3coml 1128 |
. . 3
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง ๐ถ โ โ) โ ((๐ถ / ๐ต) โค (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) โค (๐ถ ยท (1 / ๐ด)))) |
32 | 31 | 3adant3r 1182 |
. 2
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ถ / ๐ต) โค (๐ถ / ๐ด) โ (๐ถ ยท (1 / ๐ต)) โค (๐ถ ยท (1 / ๐ด)))) |
33 | 12, 14, 32 | 3bitr4d 311 |
1
โข (((๐ด โ โ โง 0 <
๐ด) โง (๐ต โ โ โง 0 < ๐ต) โง (๐ถ โ โ โง 0 < ๐ถ)) โ (๐ด โค ๐ต โ (๐ถ / ๐ต) โค (๐ถ / ๐ด))) |