Metamath Proof Explorer

Theorem xaddge0

Description: The sum of nonnegative extended reals is nonnegative. (Contributed by Mario Carneiro, 21-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 1 a1i 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 e. RR* )
3 simplr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> B e. RR* )
4 xaddcl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A +e B ) e. RR* )
5 4 adantr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> ( A +e B ) e. RR* )
6 simprr 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ B )
7 xaddlid 
 |-  ( B e. RR* -> ( 0 +e B ) = B )
8 3 7 syl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> ( 0 +e B ) = B )
9 simpll 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> A e. RR* )
10 simprl 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ A )
11 xleadd1a 
 |-  ( ( ( 0 e. RR* /\ A e. RR* /\ B e. RR* ) /\ 0 <_ A ) -> ( 0 +e B ) <_ ( A +e B ) )
12 2 9 3 10 11 syl31anc 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> ( 0 +e B ) <_ ( A +e B ) )
13 8 12 eqbrtrrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> B <_ ( A +e B ) )
14 2 3 5 6 13 xrletrd 
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ ( 0 <_ A /\ 0 <_ B ) ) -> 0 <_ ( A +e B ) )