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 e. RR -> ( A < 0 <-> 0 < ( 0 -R A ) ) )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 reposdif 
 |-  ( ( A e. RR /\ 0 e. RR ) -> ( A < 0 <-> 0 < ( 0 -R A ) ) )
3 1 2 mpan2 
 |-  ( A e. RR -> ( A < 0 <-> 0 < ( 0 -R A ) ) )