Metamath Proof Explorer


Theorem relt0neg1

Description: Comparison of a real and its negative to zero. Compare lt0neg1 . (Contributed by SN, 13-Feb-2024)

Ref Expression
Assertion relt0neg1 ( 𝐴 ∈ ℝ → ( 𝐴 < 0 ↔ 0 < ( 0 − 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 0re 0 ∈ ℝ
2 reposdif ( ( 𝐴 ∈ ℝ ∧ 0 ∈ ℝ ) → ( 𝐴 < 0 ↔ 0 < ( 0 − 𝐴 ) ) )
3 1 2 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 < 0 ↔ 0 < ( 0 − 𝐴 ) ) )