Step |
Hyp |
Ref |
Expression |
1 |
|
simp1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ด โ โ ) |
2 |
|
simp2 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ต โ โ ) |
3 |
|
simp3l |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ถ โ โ ) |
4 |
|
simp3r |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ 0 < ๐ถ ) |
5 |
4
|
gt0ne0d |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ถ โ 0 ) |
6 |
3 5
|
rereccld |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( 1 / ๐ถ ) โ โ ) |
7 |
|
recgt0 |
โข ( ( ๐ถ โ โ โง 0 < ๐ถ ) โ 0 < ( 1 / ๐ถ ) ) |
8 |
7
|
3ad2ant3 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ 0 < ( 1 / ๐ถ ) ) |
9 |
|
ltmul1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ( 1 / ๐ถ ) โ โ โง 0 < ( 1 / ๐ถ ) ) ) โ ( ๐ด < ๐ต โ ( ๐ด ยท ( 1 / ๐ถ ) ) < ( ๐ต ยท ( 1 / ๐ถ ) ) ) ) |
10 |
1 2 6 8 9
|
syl112anc |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด < ๐ต โ ( ๐ด ยท ( 1 / ๐ถ ) ) < ( ๐ต ยท ( 1 / ๐ถ ) ) ) ) |
11 |
1
|
recnd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ด โ โ ) |
12 |
3
|
recnd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ถ โ โ ) |
13 |
11 12 5
|
divrecd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด / ๐ถ ) = ( ๐ด ยท ( 1 / ๐ถ ) ) ) |
14 |
2
|
recnd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ต โ โ ) |
15 |
14 12 5
|
divrecd |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ต / ๐ถ ) = ( ๐ต ยท ( 1 / ๐ถ ) ) ) |
16 |
13 15
|
breq12d |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ( ๐ด / ๐ถ ) < ( ๐ต / ๐ถ ) โ ( ๐ด ยท ( 1 / ๐ถ ) ) < ( ๐ต ยท ( 1 / ๐ถ ) ) ) ) |
17 |
10 16
|
bitr4d |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด < ๐ต โ ( ๐ด / ๐ถ ) < ( ๐ต / ๐ถ ) ) ) |