Metamath Proof Explorer

Theorem ge0xaddcl

Description: The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ge0xaddcl ⊢A∈0+∞∧B∈0+∞→A+𝑒B∈0+∞

Proof

Step Hyp Ref Expression
1 elxrge0 ⊢A∈0+∞↔A∈ℝ*∧0≤A
2 elxrge0 ⊢B∈0+∞↔B∈ℝ*∧0≤B
3 xaddcl ⊢A∈ℝ*∧B∈ℝ*→A+𝑒B∈ℝ*
4 3 ad2ant2r ⊢A∈ℝ*∧0≤A∧B∈ℝ*∧0≤B→A+𝑒B∈ℝ*
5 xaddge0 ⊢A∈ℝ*∧B∈ℝ*∧0≤A∧0≤B→0≤A+𝑒B
6 5 an4s ⊢A∈ℝ*∧0≤A∧B∈ℝ*∧0≤B→0≤A+𝑒B
7 elxrge0 ⊢A+𝑒B∈0+∞↔A+𝑒B∈ℝ*∧0≤A+𝑒B
8 4 6 7 sylanbrc ⊢A∈ℝ*∧0≤A∧B∈ℝ*∧0≤B→A+𝑒B∈0+∞
9 1 2 8 syl2anb ⊢A∈0+∞∧B∈0+∞→A+𝑒B∈0+∞