Metamath Proof Explorer

Theorem ge0addcl

Description: The nonnegative reals are closed under addition. (Contributed by Mario Carneiro, 19-Jun-2014)

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

Proof

Step Hyp Ref Expression
1 elrege0 ⊢A∈0+∞↔A∈ℝ∧0≤A
2 elrege0 ⊢B∈0+∞↔B∈ℝ∧0≤B
3 readdcl ⊢A∈ℝ∧B∈ℝ→A+B∈ℝ
4 3 ad2ant2r ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→A+B∈ℝ
5 addge0 ⊢A∈ℝ∧B∈ℝ∧0≤A∧0≤B→0≤A+B
6 5 an4s ⊢A∈ℝ∧0≤A∧B∈ℝ∧0≤B→0≤A+B
7 elrege0 ⊢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+∞