rernegcl

Description: Closure law for negative reals. (Contributed by Steven Nguyen, 7-Jan-2023)

		Ref	Expression
	Assertion	rernegcl	$⊢ A \in ℝ \to 0 -_{ℝ} A \in ℝ$

Step	Hyp	Ref	Expression
1		elre0re	$⊢ A \in ℝ \to 0 \in ℝ$
2		resubval	$⊢ (0 \in ℝ \land A \in ℝ) \to 0 -_{ℝ} A = (ι x \in ℝ \| A + x = 0)$
3	1 2	mpancom	$⊢ A \in ℝ \to 0 -_{ℝ} A = (ι x \in ℝ \| A + x = 0)$
4		renegeu	$⊢ A \in ℝ \to \exists! x \in ℝ A + x = 0$
5		riotacl	$⊢ \exists! x \in ℝ A + x = 0 \to (ι x \in ℝ \| A + x = 0) \in ℝ$
6	4 5	syl	$⊢ A \in ℝ \to (ι x \in ℝ \| A + x = 0) \in ℝ$
7	3 6	eqeltrd	$⊢ A \in ℝ \to 0 -_{ℝ} A \in ℝ$

Metamath Proof Explorer