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 +∞