Theorem xnegcl

Description: Closure of extended real negative. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xnegcl	⊢ ( 𝐴 ∈ ℝ* → -𝑒 𝐴 ∈ ℝ* )

Proof

Step	Hyp	Ref	Expression
1		elxr	⊢ ( 𝐴 ∈ ℝ* ↔ ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) )
2		rexneg	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 = - 𝐴 )
3		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
4	2 3	eqeltrd	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 ∈ ℝ )
5	4	rexrd	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 ∈ ℝ* )
6		xnegeq	⊢ ( 𝐴 = +∞ → -𝑒 𝐴 = -𝑒 +∞ )
7		xnegpnf	⊢ -𝑒 +∞ = -∞
8		mnfxr	⊢ -∞ ∈ ℝ*
9	7 8	eqeltri	⊢ -𝑒 +∞ ∈ ℝ*
10	6 9	eqeltrdi	⊢ ( 𝐴 = +∞ → -𝑒 𝐴 ∈ ℝ* )
11		xnegeq	⊢ ( 𝐴 = -∞ → -𝑒 𝐴 = -𝑒 -∞ )
12		xnegmnf	⊢ -𝑒 -∞ = +∞
13		pnfxr	⊢ +∞ ∈ ℝ*
14	12 13	eqeltri	⊢ -𝑒 -∞ ∈ ℝ*
15	11 14	eqeltrdi	⊢ ( 𝐴 = -∞ → -𝑒 𝐴 ∈ ℝ* )
16	5 10 15	3jaoi	⊢ ( ( 𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞ ) → -𝑒 𝐴 ∈ ℝ* )
17	1 16	sylbi	⊢ ( 𝐴 ∈ ℝ* → -𝑒 𝐴 ∈ ℝ* )