Metamath Proof Explorer


Theorem ledivmul2

Description: 'Less than or equal to' relationship between division and multiplication. (Contributed by NM, 9-Dec-2005)

Ref Expression
Assertion ledivmul2 A B C 0 < C A C B A B C

Proof

Step Hyp Ref Expression
1 ledivmul A B C 0 < C A C B A C B
2 recn B B
3 recn C C
4 mulcom B C B C = C B
5 2 3 4 syl2an B C B C = C B
6 5 adantrr B C 0 < C B C = C B
7 6 3adant1 A B C 0 < C B C = C B
8 7 breq2d A B C 0 < C A B C A C B
9 1 8 bitr4d A B C 0 < C A C B A B C