Metamath Proof Explorer

Theorem unitdivcld

Description: Necessary conditions for a quotient to be in the closed unit interval. (somewhat too strong, it would be sufficient that A and B are in RR+) (Contributed by Thierry Arnoux, 20-Dec-2016)

Ref Expression
Assertion unitdivcld 
|- ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( A <_ B <-> ( A / B ) e. ( 0 [,] 1 ) ) )

Proof

Step Hyp Ref Expression
1 elunitrn 
 |-  ( A e. ( 0 [,] 1 ) -> A e. RR )
2 1 3ad2ant1 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> A e. RR )
3 elunitrn 
 |-  ( B e. ( 0 [,] 1 ) -> B e. RR )
4 3 3ad2ant2 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> B e. RR )
5 simp3 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> B =/= 0 )
6 2 4 5 redivcld 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( A / B ) e. RR )
7 6 adantr 
 |-  ( ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) /\ A <_ B ) -> ( A / B ) e. RR )
8 elunitge0 
 |-  ( A e. ( 0 [,] 1 ) -> 0 <_ A )
9 8 3ad2ant1 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> 0 <_ A )
10 elunitge0 
 |-  ( B e. ( 0 [,] 1 ) -> 0 <_ B )
11 10 adantr 
 |-  ( ( B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> 0 <_ B )
12 0re 
 |-  0 e. RR
13 ltlen 
 |-  ( ( 0 e. RR /\ B e. RR ) -> ( 0 < B <-> ( 0 <_ B /\ B =/= 0 ) ) )
14 12 3 13 sylancr 
 |-  ( B e. ( 0 [,] 1 ) -> ( 0 < B <-> ( 0 <_ B /\ B =/= 0 ) ) )
15 14 biimpar 
 |-  ( ( B e. ( 0 [,] 1 ) /\ ( 0 <_ B /\ B =/= 0 ) ) -> 0 < B )
16 15 3impb 
 |-  ( ( B e. ( 0 [,] 1 ) /\ 0 <_ B /\ B =/= 0 ) -> 0 < B )
17 16 3com23 
 |-  ( ( B e. ( 0 [,] 1 ) /\ B =/= 0 /\ 0 <_ B ) -> 0 < B )
18 11 17 mpd3an3 
 |-  ( ( B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> 0 < B )
19 18 3adant1 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> 0 < B )
20 divge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( B e. RR /\ 0 < B ) ) -> 0 <_ ( A / B ) )
21 2 9 4 19 20 syl22anc 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> 0 <_ ( A / B ) )
22 21 adantr 
 |-  ( ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) /\ A <_ B ) -> 0 <_ ( A / B ) )
23 1red 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> 1 e. RR )
24 ledivmul 
 |-  ( ( A e. RR /\ 1 e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( ( A / B ) <_ 1 <-> A <_ ( B x. 1 ) ) )
25 2 23 4 19 24 syl112anc 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( ( A / B ) <_ 1 <-> A <_ ( B x. 1 ) ) )
26 ax-1rid 
 |-  ( B e. RR -> ( B x. 1 ) = B )
27 26 breq2d 
 |-  ( B e. RR -> ( A <_ ( B x. 1 ) <-> A <_ B ) )
28 4 27 syl 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( A <_ ( B x. 1 ) <-> A <_ B ) )
29 25 28 bitr2d 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( A <_ B <-> ( A / B ) <_ 1 ) )
30 29 biimpa 
 |-  ( ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) /\ A <_ B ) -> ( A / B ) <_ 1 )
31 7 22 30 3jca 
 |-  ( ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) /\ A <_ B ) -> ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) )
32 31 ex 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( A <_ B -> ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) ) )
33 simp3 
 |-  ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) -> ( A / B ) <_ 1 )
34 33 29 syl5ibr 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) -> A <_ B ) )
35 32 34 impbid 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( A <_ B <-> ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) ) )
36 elicc01 
 |-  ( ( A / B ) e. ( 0 [,] 1 ) <-> ( ( A / B ) e. RR /\ 0 <_ ( A / B ) /\ ( A / B ) <_ 1 ) )
37 35 36 bitr4di 
 |-  ( ( A e. ( 0 [,] 1 ) /\ B e. ( 0 [,] 1 ) /\ B =/= 0 ) -> ( A <_ B <-> ( A / B ) e. ( 0 [,] 1 ) ) )