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 [,] +∞ ) )