Metamath Proof Explorer


Theorem xle0neg1

Description: Extended real version of le0neg1 . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Assertion xle0neg1 A*A00A

Proof

Step Hyp Ref Expression
1 0xr 0*
2 xleneg A*0*A00A
3 1 2 mpan2 A*A00A
4 xneg0 0=0
5 4 breq1i 0A0A
6 3 5 bitrdi A*A00A