Metamath Proof Explorer

Theorem addgegt0i

Description: Addition of nonnegative and positive numbers is positive. (Contributed by NM, 25-Sep-1999) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

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