This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Real and complex numbers - basic operations Ordering on reals (cont.) ltneg
Description: Negative of both sides of 'less than'. Theorem I.23 of Apostol p. 20.
(Contributed by NM , 27-Aug-1999) (Proof shortened by Mario Carneiro , 27-May-2016)
Ref
Expression
Assertion
ltneg ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < − A
Proof
Step
Hyp
Ref
Expression
1
0re ⊢ 0 ∈ ℝ
2
ltsub2 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ∈ ℝ → A < B ↔ 0 − B < 0 − A
3
1 2
mp3an3 ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ 0 − B < 0 − A
4
df-neg ⊢ − B = 0 − B
5
df-neg ⊢ − A = 0 − A
6
4 5
breq12i ⊢ − B < − A ↔ 0 − B < 0 − A
7
3 6
bitr4di ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < − A