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 ( ( ( 𝐴 ∈ ( 0 [,] +∞ ) ∧ 𝐵 ∈ ( 0 [,] +∞ ) ) ∧ 0 < 𝐴 ) → 0 < ( 𝐴 +𝑒 𝐵 ) )

Proof

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