Metamath Proof Explorer

Theorem addgt0ii

Description: Addition of 2 positive numbers is positive. (Contributed by NM, 18-May-1999)

Ref Expression
Hypotheses lt2.1 
|- A e. RR
lt2.2 
|- B e. RR
addgt0i.3 
|- 0 < A
addgt0i.4 
|- 0 < B
Assertion addgt0ii 
|- 0 < ( A + B )

Proof

Step Hyp Ref Expression
1 lt2.1 
 |-  A e. RR
2 lt2.2 
 |-  B e. RR
3 addgt0i.3 
 |-  0 < A
4 addgt0i.4 
 |-  0 < B
5 1 2 addgt0i 
 |-  ( ( 0 < A /\ 0 < B ) -> 0 < ( A + B ) )
6 3 4 5 mp2an 
 |-  0 < ( A + B )