Theorem renegcl

Description: Closure law for negative of reals. The weak deduction theorem dedth is used to convert hypothesis of the inference (deduction) form of this theorem, renegcli , to an antecedent. (Contributed by NM, 20-Jan-1997) (Proof modification is discouraged.)

	Ref	Expression
Assertion	renegcl	$$⊢A\in ℝ\to -A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		negeq	$$⊢A=if\left(A\in ℝ,A,1\right)\to -A=-if\left(A\in ℝ,A,1\right)$$
2	1	eleq1d	$$⊢A=if\left(A\in ℝ,A,1\right)\to \left(-A\in ℝ\leftrightarrow -if\left(A\in ℝ,A,1\right)\in ℝ\right)$$
3		1re	$$⊢1\in ℝ$$
4	3	elimel	$$⊢if\left(A\in ℝ,A,1\right)\in ℝ$$
5	4	renegcli	$$⊢-if\left(A\in ℝ,A,1\right)\in ℝ$$
6	2 5	dedth	$$⊢A\in ℝ\to -A\in ℝ$$