Metamath Proof Explorer

Theorem lesub0

Description: Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 0red 
 |-  ( B e. RR -> 0 e. RR )
2 letri3 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) )
3 1 2 sylan2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A = 0 <-> ( A <_ 0 /\ 0 <_ A ) ) )
4 ancom 
 |-  ( ( A <_ 0 /\ 0 <_ A ) <-> ( 0 <_ A /\ A <_ 0 ) )
5 simpr 
 |-  ( ( B e. RR /\ A e. RR ) -> A e. RR )
6 0red 
 |-  ( ( B e. RR /\ A e. RR ) -> 0 e. RR )
7 simpl 
 |-  ( ( B e. RR /\ A e. RR ) -> B e. RR )
8 lesub2 
 |-  ( ( A e. RR /\ 0 e. RR /\ B e. RR ) -> ( A <_ 0 <-> ( B - 0 ) <_ ( B - A ) ) )
9 5 6 7 8 syl3anc 
 |-  ( ( B e. RR /\ A e. RR ) -> ( A <_ 0 <-> ( B - 0 ) <_ ( B - A ) ) )
10 7 recnd 
 |-  ( ( B e. RR /\ A e. RR ) -> B e. CC )
11 10 subid1d 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B - 0 ) = B )
12 11 breq1d 
 |-  ( ( B e. RR /\ A e. RR ) -> ( ( B - 0 ) <_ ( B - A ) <-> B <_ ( B - A ) ) )
13 9 12 bitrd 
 |-  ( ( B e. RR /\ A e. RR ) -> ( A <_ 0 <-> B <_ ( B - A ) ) )
14 13 ancoms 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A <_ 0 <-> B <_ ( B - A ) ) )
15 14 anbi2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ A <_ 0 ) <-> ( 0 <_ A /\ B <_ ( B - A ) ) ) )
16 4 15 syl5bb 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( A <_ 0 /\ 0 <_ A ) <-> ( 0 <_ A /\ B <_ ( B - A ) ) ) )
17 3 16 bitr2d 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 ) )