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∈0+∞∧B∈0+∞∧0<A→0<A+𝑒B

Proof

Step Hyp Ref Expression
1 0xr ⊢0∈ℝ*
2 xaddrid ⊢0∈ℝ*→0+𝑒0=0
3 1 2 ax-mp ⊢0+𝑒0=0
4 simplr ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→0<A
5 simpr ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→0<B
6 1 a1i ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→0∈ℝ*
7 iccssxr ⊢0+∞⊆ℝ*
8 simplll ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→A∈0+∞
9 7 8 sselid ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→A∈ℝ*
10 simpllr ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→B∈0+∞
11 7 10 sselid ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→B∈ℝ*
12 xlt2add ⊢0∈ℝ*∧0∈ℝ*∧A∈ℝ*∧B∈ℝ*→0<A∧0<B→0+𝑒0<A+𝑒B
13 6 6 9 11 12 syl22anc ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→0<A∧0<B→0+𝑒0<A+𝑒B
14 4 5 13 mp2and ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→0+𝑒0<A+𝑒B
15 3 14 eqbrtrrid ⊢A∈0+∞∧B∈0+∞∧0<A∧0<B→0<A+𝑒B
16 simplr ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→0<A
17 oveq2 ⊢0=B→A+𝑒0=A+𝑒B
18 17 adantl ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→A+𝑒0=A+𝑒B
19 18 breq2d ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→0<A+𝑒0↔0<A+𝑒B
20 simplll ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→A∈0+∞
21 7 20 sselid ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→A∈ℝ*
22 xaddrid ⊢A∈ℝ*→A+𝑒0=A
23 21 22 syl ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→A+𝑒0=A
24 23 breq2d ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→0<A+𝑒0↔0<A
25 19 24 bitr3d ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→0<A+𝑒B↔0<A
26 16 25 mpbird ⊢A∈0+∞∧B∈0+∞∧0<A∧0=B→0<A+𝑒B
27 1 a1i ⊢A∈0+∞∧B∈0+∞∧0<A→0∈ℝ*
28 simplr ⊢A∈0+∞∧B∈0+∞∧0<A→B∈0+∞
29 7 28 sselid ⊢A∈0+∞∧B∈0+∞∧0<A→B∈ℝ*
30 pnfxr ⊢+∞∈ℝ*
31 30 a1i ⊢A∈0+∞∧B∈0+∞∧0<A→+∞∈ℝ*
32 iccgelb ⊢0∈ℝ*∧+∞∈ℝ*∧B∈0+∞→0≤B
33 27 31 28 32 syl3anc ⊢A∈0+∞∧B∈0+∞∧0<A→0≤B
34 xrleloe ⊢0∈ℝ*∧B∈ℝ*→0≤B↔0<B∨0=B
35 34 biimpa ⊢0∈ℝ*∧B∈ℝ*∧0≤B→0<B∨0=B
36 27 29 33 35 syl21anc ⊢A∈0+∞∧B∈0+∞∧0<A→0<B∨0=B
37 15 26 36 mpjaodan ⊢A∈0+∞∧B∈0+∞∧0<A→0<A+𝑒B