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 ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→AB∈01↔A≤B

Proof

Step Hyp Ref Expression
1 elicc01 ⊢AB∈01↔AB∈ℝ∧0≤AB∧AB≤1
2 df-3an ⊢AB∈ℝ∧0≤AB∧AB≤1↔AB∈ℝ∧0≤AB∧AB≤1
3 1 2 bitri ⊢AB∈01↔AB∈ℝ∧0≤AB∧AB≤1
4 1re ⊢1∈ℝ
5 ledivmul ⊢A∈ℝ∧1∈ℝ∧B∈ℝ∧0<B→AB≤1↔A≤B⋅1
6 4 5 mp3an2 ⊢A∈ℝ∧B∈ℝ∧0<B→AB≤1↔A≤B⋅1
7 6 adantlr ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→AB≤1↔A≤B⋅1
8 simpll ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→A∈ℝ
9 simprl ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→B∈ℝ
10 gt0ne0 ⊢B∈ℝ∧0<B→B≠0
11 10 adantl ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→B≠0
12 8 9 11 redivcld ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→AB∈ℝ
13 divge0 ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→0≤AB
14 12 13 jca ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→AB∈ℝ∧0≤AB
15 14 biantrurd ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→AB≤1↔AB∈ℝ∧0≤AB∧AB≤1
16 recn ⊢B∈ℝ→B∈ℂ
17 16 ad2antrl ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→B∈ℂ
18 17 mulridd ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→B⋅1=B
19 18 breq2d ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→A≤B⋅1↔A≤B
20 7 15 19 3bitr3d ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→AB∈ℝ∧0≤AB∧AB≤1↔A≤B
21 3 20 bitrid ⊢A∈ℝ∧0≤A∧B∈ℝ∧0<B→AB∈01↔A≤B