Metamath Proof Explorer

Theorem addgt0

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

Ref Expression
Assertion addgt0 
|- ( ( ( 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 lt2add 
 |-  ( ( ( 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 ) )