Description: Comparison of a number and its negative to zero. (Contributed by NM, 24-Aug-1999)
Ref | Expression | ||
---|---|---|---|
Assertion | le0neg2 | ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ 0 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re | ⊢ 0 ∈ ℝ | |
2 | leneg | ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ - 0 ) ) | |
3 | 1 2 | mpan | ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ - 0 ) ) |
4 | neg0 | ⊢ - 0 = 0 | |
5 | 4 | breq2i | ⊢ ( - 𝐴 ≤ - 0 ↔ - 𝐴 ≤ 0 ) |
6 | 3 5 | bitrdi | ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ - 𝐴 ≤ 0 ) ) |