Metamath Proof Explorer

Theorem xrge0addcld

Description: Nonnegative extended reals are closed under addition. (Contributed by Thierry Arnoux, 16-Sep-2019)

Ref Expression
Hypotheses xrge0addcld.a ⊢ φ → A ∈ 0 +∞
xrge0addcld.b ⊢ φ → B ∈ 0 +∞
Assertion xrge0addcld ⊢ φ → A + 𝑒 B ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 xrge0addcld.a ⊢ φ → A ∈ 0 +∞
2 xrge0addcld.b ⊢ φ → B ∈ 0 +∞
3 elxrge0 ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ * ∧ 0 ≤ A
4 1 3 sylib ⊢ φ → A ∈ ℝ * ∧ 0 ≤ A
5 4 simpld ⊢ φ → A ∈ ℝ *
6 elxrge0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ * ∧ 0 ≤ B
7 2 6 sylib ⊢ φ → B ∈ ℝ * ∧ 0 ≤ B
8 7 simpld ⊢ φ → B ∈ ℝ *
9 5 8 xaddcld ⊢ φ → A + 𝑒 B ∈ ℝ *
10 4 simprd ⊢ φ → 0 ≤ A
11 7 simprd ⊢ φ → 0 ≤ B
12 xaddge0 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ 0 ≤ A ∧ 0 ≤ B → 0 ≤ A + 𝑒 B
13 5 8 10 11 12 syl22anc ⊢ φ → 0 ≤ A + 𝑒 B
14 elxrge0 ⊢ A + 𝑒 B ∈ 0 +∞ ↔ A + 𝑒 B ∈ ℝ * ∧ 0 ≤ A + 𝑒 B
15 9 13 14 sylanbrc ⊢ φ → A + 𝑒 B ∈ 0 +∞