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