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 ⊢ 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 letrd ⊢ 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 letrd ⊢ 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 lenegcon1 ⊢ 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