Metamath Proof Explorer


Theorem xlt0neg1

Description: Extended real version of lt0neg1 . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xlt0neg1 ( 𝐴 ∈ ℝ* → ( 𝐴 < 0 ↔ 0 < -𝑒 𝐴 ) )

Proof

Step Hyp Ref Expression
1 0xr 0 ∈ ℝ*
2 xltneg ( ( 𝐴 ∈ ℝ* ∧ 0 ∈ ℝ* ) → ( 𝐴 < 0 ↔ -𝑒 0 < -𝑒 𝐴 ) )
3 1 2 mpan2 ( 𝐴 ∈ ℝ* → ( 𝐴 < 0 ↔ -𝑒 0 < -𝑒 𝐴 ) )
4 xneg0 -𝑒 0 = 0
5 4 breq1i ( -𝑒 0 < -𝑒 𝐴 ↔ 0 < -𝑒 𝐴 )
6 3 5 bitrdi ( 𝐴 ∈ ℝ* → ( 𝐴 < 0 ↔ 0 < -𝑒 𝐴 ) )