This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,] +∞ ) )
xrge0subcld.b ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
xrge0subcld.c ⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
Assertion xrge0subcld ( 𝜑 → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )

Proof

Step Hyp Ref Expression
1 xrge0subcld.a ⊢ ( 𝜑 → 𝐴 ∈ ( 0 [,] +∞ ) )
2 xrge0subcld.b ⊢ ( 𝜑 → 𝐵 ∈ ( 0 [,] +∞ ) )
3 xrge0subcld.c ⊢ ( 𝜑 → 𝐵 ≤ 𝐴 )
4 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
5 4 1 sselid ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
6 4 2 sselid ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
7 6 xnegcld ⊢ ( 𝜑 → -𝑒 𝐵 ∈ ℝ* )
8 5 7 xaddcld ⊢ ( 𝜑 → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* )
9 xsubge0 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ ( 𝐴 +𝑒 -𝑒 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )
10 5 6 9 syl2anc ⊢ ( 𝜑 → ( 0 ≤ ( 𝐴 +𝑒 -𝑒 𝐵 ) ↔ 𝐵 ≤ 𝐴 ) )
11 3 10 mpbird ⊢ ( 𝜑 → 0 ≤ ( 𝐴 +𝑒 -𝑒 𝐵 ) )
12 8 11 jca ⊢ ( 𝜑 → ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )
13 elxrge0 ⊢ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( 𝐴 +𝑒 -𝑒 𝐵 ) ) )
14 12 13 sylibr ⊢ ( 𝜑 → ( 𝐴 +𝑒 -𝑒 𝐵 ) ∈ ( 0 [,] +∞ ) )