Theorem xnegre

Description: An extended real is real if and only if its extended negative is real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

Step	Hyp	Ref	Expression
1		xnegrecl	⊢ ( 𝐴 ∈ ℝ → -𝑒 𝐴 ∈ ℝ )
2	1	adantl	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ∈ ℝ ) → -𝑒 𝐴 ∈ ℝ )
3		xnegrecl2	⊢ ( ( 𝐴 ∈ ℝ* ∧ -𝑒 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
4	2 3	impbida	⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ∈ ℝ ↔ -𝑒 𝐴 ∈ ℝ ) )