Description: Extended real version of le0neg2 . (Contributed by Mario Carneiro, 9-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | xle0neg2 | ⊢ ( 𝐴 ∈ ℝ* → ( 0 ≤ 𝐴 ↔ -𝑒 𝐴 ≤ 0 ) ) |
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 ) ) |