Step | Hyp | Ref
| Expression |
1 | | recn 11148 |
. . . . . . . . 9
โข (๐ถ โ โ โ ๐ถ โ
โ) |
2 | | recn 11148 |
. . . . . . . . 9
โข (๐ท โ โ โ ๐ท โ
โ) |
3 | | mulcom 11144 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ท โ โ) โ (๐ถ ยท ๐ท) = (๐ท ยท ๐ถ)) |
4 | 1, 2, 3 | syl2an 597 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ท โ โ) โ (๐ถ ยท ๐ท) = (๐ท ยท ๐ถ)) |
5 | 4 | oveq1d 7377 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ท โ โ) โ ((๐ถ ยท ๐ท) / ๐ต) = ((๐ท ยท ๐ถ) / ๐ต)) |
6 | 5 | adantl 483 |
. . . . . 6
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ถ ยท ๐ท) / ๐ต) = ((๐ท ยท ๐ถ) / ๐ต)) |
7 | 2 | ad2antll 728 |
. . . . . . 7
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ท โ โ) |
8 | 1 | ad2antrl 727 |
. . . . . . 7
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ถ โ โ โง ๐ท โ โ)) โ ๐ถ โ โ) |
9 | | recn 11148 |
. . . . . . . . . 10
โข (๐ต โ โ โ ๐ต โ
โ) |
10 | 9 | adantr 482 |
. . . . . . . . 9
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ โ) |
11 | | gt0ne0 11627 |
. . . . . . . . 9
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ 0) |
12 | 10, 11 | jca 513 |
. . . . . . . 8
โข ((๐ต โ โ โง 0 <
๐ต) โ (๐ต โ โ โง ๐ต โ 0)) |
13 | 12 | adantr 482 |
. . . . . . 7
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต โ โ โง ๐ต โ 0)) |
14 | | divass 11838 |
. . . . . . 7
โข ((๐ท โ โ โง ๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ท ยท ๐ถ) / ๐ต) = (๐ท ยท (๐ถ / ๐ต))) |
15 | 7, 8, 13, 14 | syl3anc 1372 |
. . . . . 6
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ท ยท ๐ถ) / ๐ต) = (๐ท ยท (๐ถ / ๐ต))) |
16 | 6, 15 | eqtrd 2777 |
. . . . 5
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ถ ยท ๐ท) / ๐ต) = (๐ท ยท (๐ถ / ๐ต))) |
17 | 16 | adantrrr 724 |
. . . 4
โข (((๐ต โ โ โง 0 <
๐ต) โง (๐ถ โ โ โง (๐ท โ โ โง 0 < ๐ท))) โ ((๐ถ ยท ๐ท) / ๐ต) = (๐ท ยท (๐ถ / ๐ต))) |
18 | 17 | adantll 713 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ ((๐ถ ยท ๐ท) / ๐ต) = (๐ท ยท (๐ถ / ๐ต))) |
19 | 18 | breq2d 5122 |
. 2
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ (๐ด < ((๐ถ ยท ๐ท) / ๐ต) โ ๐ด < (๐ท ยท (๐ถ / ๐ต)))) |
20 | | simpll 766 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ ๐ด โ
โ) |
21 | | remulcl 11143 |
. . . . 5
โข ((๐ถ โ โ โง ๐ท โ โ) โ (๐ถ ยท ๐ท) โ โ) |
22 | 21 | adantrr 716 |
. . . 4
โข ((๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท)) โ (๐ถ ยท ๐ท) โ โ) |
23 | 22 | adantl 483 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ (๐ถ ยท ๐ท) โ โ) |
24 | | simplr 768 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ (๐ต โ โ โง 0 <
๐ต)) |
25 | | ltmuldiv 12035 |
. . 3
โข ((๐ด โ โ โง (๐ถ ยท ๐ท) โ โ โง (๐ต โ โ โง 0 < ๐ต)) โ ((๐ด ยท ๐ต) < (๐ถ ยท ๐ท) โ ๐ด < ((๐ถ ยท ๐ท) / ๐ต))) |
26 | 20, 23, 24, 25 | syl3anc 1372 |
. 2
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ ((๐ด ยท ๐ต) < (๐ถ ยท ๐ท) โ ๐ด < ((๐ถ ยท ๐ท) / ๐ต))) |
27 | | simpl 484 |
. . . . . . 7
โข ((๐ต โ โ โง 0 <
๐ต) โ ๐ต โ โ) |
28 | 27, 11 | jca 513 |
. . . . . 6
โข ((๐ต โ โ โง 0 <
๐ต) โ (๐ต โ โ โง ๐ต โ 0)) |
29 | | redivcl 11881 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ถ / ๐ต) โ โ) |
30 | 29 | 3expb 1121 |
. . . . . 6
โข ((๐ถ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (๐ถ / ๐ต) โ โ) |
31 | 28, 30 | sylan2 594 |
. . . . 5
โข ((๐ถ โ โ โง (๐ต โ โ โง 0 <
๐ต)) โ (๐ถ / ๐ต) โ โ) |
32 | 31 | ancoms 460 |
. . . 4
โข (((๐ต โ โ โง 0 <
๐ต) โง ๐ถ โ โ) โ (๐ถ / ๐ต) โ โ) |
33 | 32 | ad2ant2lr 747 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ (๐ถ / ๐ต) โ โ) |
34 | | simprr 772 |
. . 3
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ (๐ท โ โ โง 0 <
๐ท)) |
35 | | ltdivmul 12037 |
. . 3
โข ((๐ด โ โ โง (๐ถ / ๐ต) โ โ โง (๐ท โ โ โง 0 < ๐ท)) โ ((๐ด / ๐ท) < (๐ถ / ๐ต) โ ๐ด < (๐ท ยท (๐ถ / ๐ต)))) |
36 | 20, 33, 34, 35 | syl3anc 1372 |
. 2
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ ((๐ด / ๐ท) < (๐ถ / ๐ต) โ ๐ด < (๐ท ยท (๐ถ / ๐ต)))) |
37 | 19, 26, 36 | 3bitr4d 311 |
1
โข (((๐ด โ โ โง (๐ต โ โ โง 0 <
๐ต)) โง (๐ถ โ โ โง (๐ท โ โ โง 0 <
๐ท))) โ ((๐ด ยท ๐ต) < (๐ถ ยท ๐ท) โ (๐ด / ๐ท) < (๐ถ / ๐ต))) |