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