# Metamath Proof Explorer

## Theorem divelunit

Description: A condition for a ratio to be a member of the closed unit interval. (Contributed by Scott Fenton, 11-Jun-2013)

Ref Expression
Assertion divelunit ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}\in \left[0,1\right]↔{A}\le {B}\right)$

### Proof

Step Hyp Ref Expression
1 elicc01 ${⊢}\frac{{A}}{{B}}\in \left[0,1\right]↔\left(\frac{{A}}{{B}}\in ℝ\wedge 0\le \frac{{A}}{{B}}\wedge \frac{{A}}{{B}}\le 1\right)$
2 df-3an ${⊢}\left(\frac{{A}}{{B}}\in ℝ\wedge 0\le \frac{{A}}{{B}}\wedge \frac{{A}}{{B}}\le 1\right)↔\left(\left(\frac{{A}}{{B}}\in ℝ\wedge 0\le \frac{{A}}{{B}}\right)\wedge \frac{{A}}{{B}}\le 1\right)$
3 1 2 bitri ${⊢}\frac{{A}}{{B}}\in \left[0,1\right]↔\left(\left(\frac{{A}}{{B}}\in ℝ\wedge 0\le \frac{{A}}{{B}}\right)\wedge \frac{{A}}{{B}}\le 1\right)$
4 1re ${⊢}1\in ℝ$
5 ledivmul ${⊢}\left({A}\in ℝ\wedge 1\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}\le 1↔{A}\le {B}\cdot 1\right)$
6 4 5 mp3an2 ${⊢}\left({A}\in ℝ\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}\le 1↔{A}\le {B}\cdot 1\right)$
7 6 adantlr ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}\le 1↔{A}\le {B}\cdot 1\right)$
8 simpll ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {A}\in ℝ$
9 simprl ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\in ℝ$
10 gt0ne0 ${⊢}\left({B}\in ℝ\wedge 0<{B}\right)\to {B}\ne 0$
11 10 adantl ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\ne 0$
12 8 9 11 redivcld ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \frac{{A}}{{B}}\in ℝ$
13 divge0 ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 0\le \frac{{A}}{{B}}$
14 12 13 jca ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}\in ℝ\wedge 0\le \frac{{A}}{{B}}\right)$
15 14 biantrurd ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}\le 1↔\left(\left(\frac{{A}}{{B}}\in ℝ\wedge 0\le \frac{{A}}{{B}}\right)\wedge \frac{{A}}{{B}}\le 1\right)\right)$
16 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
17 16 ad2antrl ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\in ℂ$
18 17 mulid1d ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to {B}\cdot 1={B}$
19 18 breq2d ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left({A}\le {B}\cdot 1↔{A}\le {B}\right)$
20 7 15 19 3bitr3d ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\left(\left(\frac{{A}}{{B}}\in ℝ\wedge 0\le \frac{{A}}{{B}}\right)\wedge \frac{{A}}{{B}}\le 1\right)↔{A}\le {B}\right)$
21 3 20 syl5bb ${⊢}\left(\left({A}\in ℝ\wedge 0\le {A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to \left(\frac{{A}}{{B}}\in \left[0,1\right]↔{A}\le {B}\right)$