Metamath Proof Explorer

Theorem xrge0subcld

Description: Condition for closure of nonnegative extended reals under subtraction. (Contributed by Thierry Arnoux, 27-May-2020)

Ref Expression
Hypotheses xrge0subcld.a ⊢ φ → A ∈ 0 +∞
xrge0subcld.b ⊢ φ → B ∈ 0 +∞
xrge0subcld.c ⊢ φ → B ≤ A
Assertion xrge0subcld ⊢ φ → A + 𝑒 − B ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 xrge0subcld.a ⊢ φ → A ∈ 0 +∞
2 xrge0subcld.b ⊢ φ → B ∈ 0 +∞
3 xrge0subcld.c ⊢ φ → B ≤ A
4 iccssxr ⊢ 0 +∞ ⊆ ℝ *
5 4 1 sselid ⊢ φ → A ∈ ℝ *
6 4 2 sselid ⊢ φ → B ∈ ℝ *
7 6 xnegcld ⊢ φ → − B ∈ ℝ *
8 5 7 xaddcld ⊢ φ → A + 𝑒 − B ∈ ℝ *
9 xsubge0 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → 0 ≤ A + 𝑒 − B ↔ B ≤ A
10 5 6 9 syl2anc ⊢ φ → 0 ≤ A + 𝑒 − B ↔ B ≤ A
11 3 10 mpbird ⊢ φ → 0 ≤ A + 𝑒 − B
12 8 11 jca ⊢ φ → A + 𝑒 − B ∈ ℝ * ∧ 0 ≤ A + 𝑒 − B
13 elxrge0 ⊢ A + 𝑒 − B ∈ 0 +∞ ↔ A + 𝑒 − B ∈ ℝ * ∧ 0 ≤ A + 𝑒 − B
14 12 13 sylibr ⊢ φ → A + 𝑒 − B ∈ 0 +∞