Metamath Proof Explorer


Theorem ltdiv1

Description: Division of both sides of 'less than' by a positive number. (Contributed by NM, 10-Oct-2004) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion ltdiv1 ( ( ๐ด โˆˆ โ„ โˆง ๐ต โˆˆ โ„ โˆง ( ๐ถ โˆˆ โ„ โˆง 0 < ๐ถ ) ) โ†’ ( ๐ด < ๐ต โ†” ( ๐ด / ๐ถ ) < ( ๐ต / ๐ถ ) ) )

Proof

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 < ๐ถ ) ) โ†’ ( ๐ด < ๐ต โ†” ( ๐ด / ๐ถ ) < ( ๐ต / ๐ถ ) ) )