xnegcl

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

		Ref	Expression
	Assertion	xnegcl	$⊢ A \in ℝ^{} \to - A \in ℝ^{}$

Step	Hyp	Ref	Expression
1		elxr	$⊢ A \in ℝ^{*} \leftrightarrow (A \in ℝ \lor A = +∞ \lor A = −∞)$
2		rexneg	$⊢ A \in ℝ \to - A = - A$
3		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
4	2 3	eqeltrd	$⊢ A \in ℝ \to - A \in ℝ$
5	4	rexrd	$⊢ A \in ℝ \to - A \in ℝ^{*}$
6		xnegeq	$⊢ A = +∞ \to - A = - +∞$
7		xnegpnf	$⊢ - +∞ = −∞$
8		mnfxr	$⊢ −∞ \in ℝ^{*}$
9	7 8	eqeltri	$⊢ - +∞ \in ℝ^{*}$
10	6 9	eqeltrdi	$⊢ A = +∞ \to - A \in ℝ^{*}$
11		xnegeq	$⊢ A = −∞ \to - A = - −∞$
12		xnegmnf	$⊢ - −∞ = +∞$
13		pnfxr	$⊢ +∞ \in ℝ^{*}$
14	12 13	eqeltri	$⊢ - −∞ \in ℝ^{*}$
15	11 14	eqeltrdi	$⊢ A = −∞ \to - A \in ℝ^{*}$
16	5 10 15	3jaoi	$⊢ (A \in ℝ \lor A = +∞ \lor A = −∞) \to - A \in ℝ^{*}$
17	1 16	sylbi	$⊢ A \in ℝ^{} \to - A \in ℝ^{}$

Metamath Proof Explorer