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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
iooabslt.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
iooabslt.3 ⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐴 − 𝐵 ) (,) ( 𝐴 + 𝐵 ) ) )
Assertion iooabslt ( 𝜑 → ( abs ‘ ( 𝐴 − 𝐶 ) ) < 𝐵 )

Proof

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