Step |
Hyp |
Ref |
Expression |
1 |
|
resubcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ ) |
2 |
1
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ ) |
3 |
2
|
rexrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 − 𝐵 ) ∈ ℝ* ) |
4 |
|
readdcl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ ) |
5 |
4
|
3adant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ ) |
6 |
5
|
rexrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ* ) |
7 |
|
rexr |
⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℝ* ) |
8 |
7
|
3ad2ant3 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → 𝐶 ∈ ℝ* ) |
9 |
|
elicc4 |
⊢ ( ( ( 𝐴 − 𝐵 ) ∈ ℝ* ∧ ( 𝐴 + 𝐵 ) ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) → ( 𝐶 ∈ ( ( 𝐴 − 𝐵 ) [,] ( 𝐴 + 𝐵 ) ) ↔ ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) ) |
10 |
3 6 8 9
|
syl3anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( ( 𝐴 − 𝐵 ) [,] ( 𝐴 + 𝐵 ) ) ↔ ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) ) |
11 |
|
absdifle |
⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( abs ‘ ( 𝐶 − 𝐴 ) ) ≤ 𝐵 ↔ ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) ) |
12 |
11
|
3coml |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( abs ‘ ( 𝐶 − 𝐴 ) ) ≤ 𝐵 ↔ ( ( 𝐴 − 𝐵 ) ≤ 𝐶 ∧ 𝐶 ≤ ( 𝐴 + 𝐵 ) ) ) ) |
13 |
10 12
|
bitr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 ∈ ( ( 𝐴 − 𝐵 ) [,] ( 𝐴 + 𝐵 ) ) ↔ ( abs ‘ ( 𝐶 − 𝐴 ) ) ≤ 𝐵 ) ) |