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

Metamath Proof Explorer

Theorem relt0neg2

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

Ref Expression
Assertion relt0neg2 ⊢ A ∈ ℝ → 0 < A ↔ 0 - ℝ A < 0

Proof

Step Hyp Ref Expression
1 elre0re ⊢ A ∈ ℝ → 0 ∈ ℝ
2 id ⊢ A ∈ ℝ → A ∈ ℝ
3 reltsub1 ⊢ 0 ∈ ℝ ∧ A ∈ ℝ ∧ A ∈ ℝ → 0 < A ↔ 0 - ℝ A < A - ℝ A
4 1 2 2 3 syl3anc ⊢ A ∈ ℝ → 0 < A ↔ 0 - ℝ A < A - ℝ A
5 resubid ⊢ A ∈ ℝ → A - ℝ A = 0
6 5 breq2d ⊢ A ∈ ℝ → 0 - ℝ A < A - ℝ A ↔ 0 - ℝ A < 0
7 4 6 bitrd ⊢ A ∈ ℝ → 0 < A ↔ 0 - ℝ A < 0