Database
REAL AND COMPLEX NUMBERS
Order sets
Infinity and the extended real number system (cont.)
xle0neg2
Next ⟩
xaddval
Metamath Proof Explorer
Ascii
Unicode
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