Metamath Proof Explorer

Theorem ge0div

Description: Division of a nonnegative number by a positive number. (Contributed by NM, 28-Sep-2005)

Ref Expression
Assertion ge0div 
|- ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( 0 <_ A <-> 0 <_ ( A / B ) ) )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 lediv1 
 |-  ( ( 0 e. RR /\ A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( 0 <_ A <-> ( 0 / B ) <_ ( A / B ) ) )
3 1 2 mp3an1 
 |-  ( ( A e. RR /\ ( B e. RR /\ 0 < B ) ) -> ( 0 <_ A <-> ( 0 / B ) <_ ( A / B ) ) )
4 3 3impb 
 |-  ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( 0 <_ A <-> ( 0 / B ) <_ ( A / B ) ) )
5 recn 
 |-  ( B e. RR -> B e. CC )
6 gt0ne0 
 |-  ( ( B e. RR /\ 0 < B ) -> B =/= 0 )
7 div0 
 |-  ( ( B e. CC /\ B =/= 0 ) -> ( 0 / B ) = 0 )
8 5 6 7 syl2an2r 
 |-  ( ( B e. RR /\ 0 < B ) -> ( 0 / B ) = 0 )
9 8 breq1d 
 |-  ( ( B e. RR /\ 0 < B ) -> ( ( 0 / B ) <_ ( A / B ) <-> 0 <_ ( A / B ) ) )
10 9 3adant1 
 |-  ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( ( 0 / B ) <_ ( A / B ) <-> 0 <_ ( A / B ) ) )
11 4 10 bitrd 
 |-  ( ( A e. RR /\ B e. RR /\ 0 < B ) -> ( 0 <_ A <-> 0 <_ ( A / B ) ) )