Metamath Proof Explorer


Theorem addgegt0

Description: The sum of nonnegative and positive numbers is positive. (Contributed by NM, 28-Dec-2005) (Proof shortened by Andrew Salmon, 19-Nov-2011)

Ref Expression
Assertion addgegt0
|- ( ( ( 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 leltadd
 |-  ( ( ( 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 ) )