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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) < 𝐵 ↔ ( - 𝐵 < 𝐴𝐴 < 𝐵 ) ) )

Proof

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