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−BA+B
Assertion iooabslt ⊢φ→A−C<B

Proof

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