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

Proof

Step Hyp Ref Expression
1 elre0re 
 |-  ( A e. RR -> 0 e. RR )
2 id 
 |-  ( A e. RR -> A e. RR )
3 reltsub1 
 |-  ( ( 0 e. RR /\ A e. RR /\ A e. RR ) -> ( 0 < A <-> ( 0 -R A ) < ( A -R A ) ) )
4 1 2 2 3 syl3anc 
 |-  ( A e. RR -> ( 0 < A <-> ( 0 -R A ) < ( A -R A ) ) )
5 resubid 
 |-  ( A e. RR -> ( A -R A ) = 0 )
6 5 breq2d 
 |-  ( A e. RR -> ( ( 0 -R A ) < ( A -R A ) <-> ( 0 -R A ) < 0 ) )
7 4 6 bitrd 
 |-  ( A e. RR -> ( 0 < A <-> ( 0 -R A ) < 0 ) )