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 e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) e. ( 0 [,] 1 ) <-> A <_ B ) )

Proof

Step Hyp Ref Expression
1 elicc01 
 |-  ( ( A / B ) e. ( 0 [,] 1 ) <-> ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) )
2 df-3an 
 |-  ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) <-> ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) ) /\ ( A / B ) <_ 1 ) )
3 1 2 bitri 
 |-  ( ( A / B ) e. ( 0 [,] 1 ) <-> ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) ) /\ ( A / B ) <_ 1 ) )
4 1re 
 |-  1 e. RR
5 ledivmul 
 |-  ( ( A e. RR /\ 1 e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) <_ 1 <-> A <_ ( B x. 1 ) ) )
6 4 5 mp3an2 
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) <_ 1 <-> A <_ ( B x. 1 ) ) )
7 6 adantlr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) <_ 1 <-> A <_ ( B x. 1 ) ) )
8 simpll 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> A e. RR )
9 simprl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> B e. RR )
10 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
11 10 adantl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> B =/= 0 )
12 8 9 11 redivcld 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A / B ) e. RR )
13 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) )
14 12 13 jca 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) e. RR /\ 0 <_ ( A / B ) ) )
15 14 biantrurd 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) <_ 1 <-> ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) ) /\ ( A / B ) <_ 1 ) ) )
16 recn 
 |-  ( B e. RR -> B e. CC )
17 16 ad2antrl 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> B e. CC )
18 17 mulid1d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( B x. 1 ) = B )
19 18 breq2d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( A <_ ( B x. 1 ) <-> A <_ B ) )
20 7 15 19 3bitr3d 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) ) /\ ( A / B ) <_ 1 ) <-> A <_ B ) )
21 3 20 syl5bb 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) e. ( 0 [,] 1 ) <-> A <_ B ) )