Metamath Proof Explorer

Theorem absle

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

Ref Expression
Assertion absle ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 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 letrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( abs ‘ 𝐴 ) ≤ 𝐵 ) → - 𝐴 ≤ 𝐵 )
14 leabs ⊢ ( 𝐴 ∈ ℝ → 𝐴 ≤ ( abs ‘ 𝐴 ) )
15 14 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( abs ‘ 𝐴 ) ≤ 𝐵 ) → 𝐴 ≤ ( abs ‘ 𝐴 ) )
16 1 5 6 15 12 letrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 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 lenegcon1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( - 𝐴 ≤ 𝐵 ↔ - 𝐵 ≤ 𝐴 ) )
30 29 anbi1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( - 𝐴 ≤ 𝐵 ∧ 𝐴 ≤ 𝐵 ) ↔ ( - 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )
31 28 30 bitrd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ 𝐴 ) ≤ 𝐵 ↔ ( - 𝐵 ≤ 𝐴 ∧ 𝐴 ≤ 𝐵 ) ) )