Step |
Hyp |
Ref |
Expression |
1 |
|
ltmul1a |
โข ( ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โง ๐ด < ๐ต ) โ ( ๐ด ยท ๐ถ ) < ( ๐ต ยท ๐ถ ) ) |
2 |
1
|
ex |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด < ๐ต โ ( ๐ด ยท ๐ถ ) < ( ๐ต ยท ๐ถ ) ) ) |
3 |
|
oveq1 |
โข ( ๐ด = ๐ต โ ( ๐ด ยท ๐ถ ) = ( ๐ต ยท ๐ถ ) ) |
4 |
3
|
a1i |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด = ๐ต โ ( ๐ด ยท ๐ถ ) = ( ๐ต ยท ๐ถ ) ) ) |
5 |
|
ltmul1a |
โข ( ( ( ๐ต โ โ โง ๐ด โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โง ๐ต < ๐ด ) โ ( ๐ต ยท ๐ถ ) < ( ๐ด ยท ๐ถ ) ) |
6 |
5
|
ex |
โข ( ( ๐ต โ โ โง ๐ด โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ต < ๐ด โ ( ๐ต ยท ๐ถ ) < ( ๐ด ยท ๐ถ ) ) ) |
7 |
6
|
3com12 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ต < ๐ด โ ( ๐ต ยท ๐ถ ) < ( ๐ด ยท ๐ถ ) ) ) |
8 |
4 7
|
orim12d |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ( ๐ด = ๐ต โจ ๐ต < ๐ด ) โ ( ( ๐ด ยท ๐ถ ) = ( ๐ต ยท ๐ถ ) โจ ( ๐ต ยท ๐ถ ) < ( ๐ด ยท ๐ถ ) ) ) ) |
9 |
8
|
con3d |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ยฌ ( ( ๐ด ยท ๐ถ ) = ( ๐ต ยท ๐ถ ) โจ ( ๐ต ยท ๐ถ ) < ( ๐ด ยท ๐ถ ) ) โ ยฌ ( ๐ด = ๐ต โจ ๐ต < ๐ด ) ) ) |
10 |
|
simp1 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ด โ โ ) |
11 |
|
simp3l |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ถ โ โ ) |
12 |
10 11
|
remulcld |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด ยท ๐ถ ) โ โ ) |
13 |
|
simp2 |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ๐ต โ โ ) |
14 |
13 11
|
remulcld |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ต ยท ๐ถ ) โ โ ) |
15 |
12 14
|
lttrid |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ( ๐ด ยท ๐ถ ) < ( ๐ต ยท ๐ถ ) โ ยฌ ( ( ๐ด ยท ๐ถ ) = ( ๐ต ยท ๐ถ ) โจ ( ๐ต ยท ๐ถ ) < ( ๐ด ยท ๐ถ ) ) ) ) |
16 |
10 13
|
lttrid |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด < ๐ต โ ยฌ ( ๐ด = ๐ต โจ ๐ต < ๐ด ) ) ) |
17 |
9 15 16
|
3imtr4d |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ( ๐ด ยท ๐ถ ) < ( ๐ต ยท ๐ถ ) โ ๐ด < ๐ต ) ) |
18 |
2 17
|
impbid |
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ( ๐ถ โ โ โง 0 < ๐ถ ) ) โ ( ๐ด < ๐ต โ ( ๐ด ยท ๐ถ ) < ( ๐ต ยท ๐ถ ) ) ) |