Metamath Proof Explorer


Theorem xle0neg2

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

Ref Expression
Assertion xle0neg2 ( 𝐴 ∈ ℝ* → ( 0 ≤ 𝐴 ↔ -𝑒 𝐴 ≤ 0 ) )

Proof

Step Hyp Ref Expression
1 0xr 0 ∈ ℝ*
2 xleneg ( ( 0 ∈ ℝ*𝐴 ∈ ℝ* ) → ( 0 ≤ 𝐴 ↔ -𝑒 𝐴 ≤ -𝑒 0 ) )
3 1 2 mpan ( 𝐴 ∈ ℝ* → ( 0 ≤ 𝐴 ↔ -𝑒 𝐴 ≤ -𝑒 0 ) )
4 xneg0 -𝑒 0 = 0
5 4 breq2i ( -𝑒 𝐴 ≤ -𝑒 0 ↔ -𝑒 𝐴 ≤ 0 )
6 3 5 bitrdi ( 𝐴 ∈ ℝ* → ( 0 ≤ 𝐴 ↔ -𝑒 𝐴 ≤ 0 ) )