Metamath Proof Explorer


Theorem ltmul1

Description: Multiplication of both sides of 'less than' by a positive number. Theorem I.19 of Apostol p. 20. (Contributed by NM, 13-Feb-2005) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

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