Metamath Proof Explorer


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 ( 𝐴 ∈ ℝ* → ( 𝐴 ∈ ℝ ↔ -𝑒 𝐴 ∈ ℝ ) )