Theorem relt0neg2

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

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

Proof

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