Metamath Proof Explorer

Theorem elicc4abs

Description: Membership in a symmetric closed real interval. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Assertion elicc4abs ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ A − B A + B ↔ C − A ≤ B

Proof

Step Hyp Ref Expression
1 resubcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A − B ∈ ℝ
2 1 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ∈ ℝ
3 2 rexrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A − B ∈ ℝ *
4 readdcl ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + B ∈ ℝ
5 4 3adant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ∈ ℝ
6 5 rexrd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B ∈ ℝ *
7 rexr ⊢ C ∈ ℝ → C ∈ ℝ *
8 7 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ ℝ *
9 elicc4 ⊢ A − B ∈ ℝ * ∧ A + B ∈ ℝ * ∧ C ∈ ℝ * → C ∈ A − B A + B ↔ A − B ≤ C ∧ C ≤ A + B
10 3 6 8 9 syl3anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ A − B A + B ↔ A − B ≤ C ∧ C ≤ A + B
11 absdifle ⊢ C ∈ ℝ ∧ A ∈ ℝ ∧ B ∈ ℝ → C − A ≤ B ↔ A − B ≤ C ∧ C ≤ A + B
12 11 3coml ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C − A ≤ B ↔ A − B ≤ C ∧ C ≤ A + B
13 10 12 bitr4d ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C ∈ A − B A + B ↔ C − A ≤ B