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	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		negeq	⊢ ( 𝐴 = if ( 𝐴 ∈ ℝ , 𝐴 , 1 ) → - 𝐴 = - if ( 𝐴 ∈ ℝ , 𝐴 , 1 ) )
2	1	eleq1d	⊢ ( 𝐴 = if ( 𝐴 ∈ ℝ , 𝐴 , 1 ) → ( - 𝐴 ∈ ℝ ↔ - if ( 𝐴 ∈ ℝ , 𝐴 , 1 ) ∈ ℝ ) )
3		1re	⊢ 1 ∈ ℝ
4	3	elimel	⊢ if ( 𝐴 ∈ ℝ , 𝐴 , 1 ) ∈ ℝ
5	4	renegcli	⊢ - if ( 𝐴 ∈ ℝ , 𝐴 , 1 ) ∈ ℝ
6	2 5	dedth	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )