# Metamath Proof Explorer

## Theorem ledivmul

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

Ref Expression
Assertion ledivmul ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(\frac{{A}}{{C}}\le {B}↔{A}\le {C}{B}\right)$

### Proof

Step Hyp Ref Expression
1 remulcl ${⊢}\left({C}\in ℝ\wedge {B}\in ℝ\right)\to {C}{B}\in ℝ$
2 1 ancoms ${⊢}\left({B}\in ℝ\wedge {C}\in ℝ\right)\to {C}{B}\in ℝ$
3 2 adantrr ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}{B}\in ℝ$
4 3 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}{B}\in ℝ$
5 lediv1 ${⊢}\left({A}\in ℝ\wedge {C}{B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}\le {C}{B}↔\frac{{A}}{{C}}\le \frac{{C}{B}}{{C}}\right)$
6 4 5 syld3an2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left({A}\le {C}{B}↔\frac{{A}}{{C}}\le \frac{{C}{B}}{{C}}\right)$
7 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
8 7 adantr ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {B}\in ℂ$
9 recn ${⊢}{C}\in ℝ\to {C}\in ℂ$
10 9 ad2antrl ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}\in ℂ$
11 gt0ne0 ${⊢}\left({C}\in ℝ\wedge 0<{C}\right)\to {C}\ne 0$
12 11 adantl ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to {C}\ne 0$
13 8 10 12 divcan3d ${⊢}\left({B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \frac{{C}{B}}{{C}}={B}$
14 13 3adant1 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \frac{{C}{B}}{{C}}={B}$
15 14 breq2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(\frac{{A}}{{C}}\le \frac{{C}{B}}{{C}}↔\frac{{A}}{{C}}\le {B}\right)$
16 6 15 bitr2d ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge \left({C}\in ℝ\wedge 0<{C}\right)\right)\to \left(\frac{{A}}{{C}}\le {B}↔{A}\le {C}{B}\right)$