This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ A ∈ ℝ → A < 0 ↔ 0 < 0 - ℝ A

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 reposdif ⊢ A ∈ ℝ ∧ 0 ∈ ℝ → A < 0 ↔ 0 < 0 - ℝ A
3 1 2 mpan2 ⊢ A ∈ ℝ → A < 0 ↔ 0 < 0 - ℝ A