Metamath Proof Explorer

Theorem abslt

Description: Absolute value and 'less than' relation. (Contributed by NM, 6-Apr-2005) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abslt ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < A ∧ A < B

Proof

Step Hyp Ref Expression
1 simpll ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A ∈ ℝ
2 1 renegcld ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → − A ∈ ℝ
3 1 recnd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A ∈ ℂ
4 abscl ⊢ A ∈ ℂ → A ∈ ℝ
5 3 4 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A ∈ ℝ
6 simplr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → B ∈ ℝ
7 leabs ⊢ − A ∈ ℝ → − A ≤ − A
8 2 7 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → − A ≤ − A
9 absneg ⊢ A ∈ ℂ → − A = A
10 3 9 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → − A = A
11 8 10 breqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → − A ≤ A
12 simpr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A < B
13 2 5 6 11 12 lelttrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → − A < B
14 leabs ⊢ A ∈ ℝ → A ≤ A
15 14 ad2antrr ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A ≤ A
16 1 5 6 15 12 lelttrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → A < B
17 13 16 jca ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ A < B → − A < B ∧ A < B
18 17 ex ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → − A < B ∧ A < B
19 absor ⊢ A ∈ ℝ → A = A ∨ A = − A
20 19 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → A = A ∨ A = − A
21 breq1 ⊢ A = A → A < B ↔ A < B
22 21 biimprd ⊢ A = A → A < B → A < B
23 breq1 ⊢ A = − A → A < B ↔ − A < B
24 23 biimprd ⊢ A = − A → − A < B → A < B
25 22 24 jaoa ⊢ A = A ∨ A = − A → A < B ∧ − A < B → A < B
26 25 ancomsd ⊢ A = A ∨ A = − A → − A < B ∧ A < B → A < B
27 20 26 syl ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A < B ∧ A < B → A < B
28 18 27 impbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − A < B ∧ A < B
29 ltnegcon1 ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A < B ↔ − B < A
30 29 anbi1d ⊢ A ∈ ℝ ∧ B ∈ ℝ → − A < B ∧ A < B ↔ − B < A ∧ A < B
31 28 30 bitrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B ↔ − B < A ∧ A < B