Metamath Proof Explorer

Theorem addge0

Description: The sum of 2 nonnegative numbers is nonnegative. (Contributed by NM, 17-Mar-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

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

Proof

Step Hyp Ref Expression
1 00id 
 |-  ( 0 + 0 ) = 0
2 0re 
 |-  0 e. RR
3 le2add 
 |-  ( ( ( 0 e. RR /\ 0 e. RR ) /\ ( A e. RR /\ B e. RR ) ) -> ( ( 0 <_ A /\ 0 <_ B ) -> ( 0 + 0 ) <_ ( A + B ) ) )
4 2 2 3 mpanl12 
 |-  ( ( A e. RR /\ B e. RR ) -> ( ( 0 <_ A /\ 0 <_ B ) -> ( 0 + 0 ) <_ ( A + B ) ) )
5 4 imp 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> ( 0 + 0 ) <_ ( A + B ) )
6 1 5 eqbrtrrid 
 |-  ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A + B ) )