Metamath Proof Explorer

Theorem iooabslt

Description: An upper bound for the distance from the center of an open interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iooabslt.1 ⊢ φ → A ∈ ℝ
iooabslt.2 ⊢ φ → B ∈ ℝ
iooabslt.3 ⊢ φ → C ∈ A − B A + B
Assertion iooabslt ⊢ φ → A − C < B

Proof

Step Hyp Ref Expression
1 iooabslt.1 ⊢ φ → A ∈ ℝ
2 iooabslt.2 ⊢ φ → B ∈ ℝ
3 iooabslt.3 ⊢ φ → C ∈ A − B A + B
4 1 recnd ⊢ φ → A ∈ ℂ
5 elioore ⊢ C ∈ A − B A + B → C ∈ ℝ
6 3 5 syl ⊢ φ → C ∈ ℝ
7 6 recnd ⊢ φ → C ∈ ℂ
8 eqid ⊢ abs ∘ − = abs ∘ −
9 8 cnmetdval ⊢ A ∈ ℂ ∧ C ∈ ℂ → A abs ∘ − C = A − C
10 4 7 9 syl2anc ⊢ φ → A abs ∘ − C = A − C
11 eqid ⊢ abs ∘ − ↾ ℝ 2 = abs ∘ − ↾ ℝ 2
12 11 bl2ioo ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ball ⁡ abs ∘ − ↾ ℝ 2 B = A − B A + B
13 1 2 12 syl2anc ⊢ φ → A ball ⁡ abs ∘ − ↾ ℝ 2 B = A − B A + B
14 3 13 eleqtrrd ⊢ φ → C ∈ A ball ⁡ abs ∘ − ↾ ℝ 2 B
15 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
16 15 a1i ⊢ φ → abs ∘ − ∈ ∞Met ⁡ ℂ
17 4 1 elind ⊢ φ → A ∈ ℂ ∩ ℝ
18 2 rexrd ⊢ φ → B ∈ ℝ *
19 11 blres ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ A ∈ ℂ ∩ ℝ ∧ B ∈ ℝ * → A ball ⁡ abs ∘ − ↾ ℝ 2 B = A ball ⁡ abs ∘ − B ∩ ℝ
20 16 17 18 19 syl3anc ⊢ φ → A ball ⁡ abs ∘ − ↾ ℝ 2 B = A ball ⁡ abs ∘ − B ∩ ℝ
21 14 20 eleqtrd ⊢ φ → C ∈ A ball ⁡ abs ∘ − B ∩ ℝ
22 elin ⊢ C ∈ A ball ⁡ abs ∘ − B ∩ ℝ ↔ C ∈ A ball ⁡ abs ∘ − B ∧ C ∈ ℝ
23 21 22 sylib ⊢ φ → C ∈ A ball ⁡ abs ∘ − B ∧ C ∈ ℝ
24 23 simpld ⊢ φ → C ∈ A ball ⁡ abs ∘ − B
25 elbl ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ A ∈ ℂ ∧ B ∈ ℝ * → C ∈ A ball ⁡ abs ∘ − B ↔ C ∈ ℂ ∧ A abs ∘ − C < B
26 16 4 18 25 syl3anc ⊢ φ → C ∈ A ball ⁡ abs ∘ − B ↔ C ∈ ℂ ∧ A abs ∘ − C < B
27 24 26 mpbid ⊢ φ → C ∈ ℂ ∧ A abs ∘ − C < B
28 27 simprd ⊢ φ → A abs ∘ − C < B
29 10 28 eqbrtrrd ⊢ φ → A − C < B