Metamath Proof Explorer


Theorem lesub0i

Description: Lemma to show a nonnegative number is zero. (Contributed by NM, 8-Oct-1999) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Hypotheses lt2.1
|- A e. RR
lt2.2
|- B e. RR
Assertion lesub0i
|- ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 )

Proof

Step Hyp Ref Expression
1 lt2.1
 |-  A e. RR
2 lt2.2
 |-  B e. RR
3 lesub0
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 ) )
4 1 2 3 mp2an
 |-  ( ( 0 <_ A /\ B <_ ( B - A ) ) <-> A = 0 )