Metamath Proof Explorer

Theorem xrge0addgt0

Description: The sum of nonnegative and positive numbers is positive. See addgtge0 . (Contributed by Thierry Arnoux, 6-Jul-2017)

Ref Expression
Assertion xrge0addgt0 
|- ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> 0 < ( A +e B ) )

Proof

Step Hyp Ref Expression
1 0xr 
 |-  0 e. RR*
2 xaddid1 
 |-  ( 0 e. RR* -> ( 0 +e 0 ) = 0 )
3 1 2 ax-mp 
 |-  ( 0 +e 0 ) = 0
4 simplr 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> 0 < A )
5 simpr 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> 0 < B )
6 1 a1i 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> 0 e. RR* )
7 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
8 simplll 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> A e. ( 0 [,] +oo ) )
9 7 8 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> A e. RR* )
10 simpllr 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> B e. ( 0 [,] +oo ) )
11 7 10 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> B e. RR* )
12 xlt2add 
 |-  ( ( ( 0 e. RR* /\ 0 e. RR* ) /\ ( A e. RR* /\ B e. RR* ) ) -> ( ( 0 < A /\ 0 < B ) -> ( 0 +e 0 ) < ( A +e B ) ) )
13 6 6 9 11 12 syl22anc 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> ( ( 0 < A /\ 0 < B ) -> ( 0 +e 0 ) < ( A +e B ) ) )
14 4 5 13 mp2and 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> ( 0 +e 0 ) < ( A +e B ) )
15 3 14 eqbrtrrid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 < B ) -> 0 < ( A +e B ) )
16 simplr 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> 0 < A )
17 oveq2 
 |-  ( 0 = B -> ( A +e 0 ) = ( A +e B ) )
18 17 adantl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> ( A +e 0 ) = ( A +e B ) )
19 18 breq2d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> ( 0 < ( A +e 0 ) <-> 0 < ( A +e B ) ) )
20 simplll 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> A e. ( 0 [,] +oo ) )
21 7 20 sselid 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> A e. RR* )
22 xaddid1 
 |-  ( A e. RR* -> ( A +e 0 ) = A )
23 21 22 syl 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> ( A +e 0 ) = A )
24 23 breq2d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> ( 0 < ( A +e 0 ) <-> 0 < A ) )
25 19 24 bitr3d 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> ( 0 < ( A +e B ) <-> 0 < A ) )
26 16 25 mpbird 
 |-  ( ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) /\ 0 = B ) -> 0 < ( A +e B ) )
27 1 a1i 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> 0 e. RR* )
28 simplr 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> B e. ( 0 [,] +oo ) )
29 7 28 sselid 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> B e. RR* )
30 pnfxr 
 |-  +oo e. RR*
31 30 a1i 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> +oo e. RR* )
32 iccgelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ B e. ( 0 [,] +oo ) ) -> 0 <_ B )
33 27 31 28 32 syl3anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> 0 <_ B )
34 xrleloe 
 |-  ( ( 0 e. RR* /\ B e. RR* ) -> ( 0 <_ B <-> ( 0 < B \/ 0 = B ) ) )
35 34 biimpa 
 |-  ( ( ( 0 e. RR* /\ B e. RR* ) /\ 0 <_ B ) -> ( 0 < B \/ 0 = B ) )
36 27 29 33 35 syl21anc 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> ( 0 < B \/ 0 = B ) )
37 15 26 36 mpjaodan 
 |-  ( ( ( A e. ( 0 [,] +oo ) /\ B e. ( 0 [,] +oo ) ) /\ 0 < A ) -> 0 < ( A +e B ) )