Metamath Proof Explorer


Theorem xle0neg2

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

Ref Expression
Assertion xle0neg2 A * 0 A A 0

Proof

Step Hyp Ref Expression
1 0xr 0 *
2 xleneg 0 * A * 0 A A 0
3 1 2 mpan A * 0 A A 0
4 xneg0 0 = 0
5 4 breq2i A 0 A 0
6 3 5 bitrdi A * 0 A A 0