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 ‘ ( 𝐴 − 𝐶 ) ) < 𝐵 )

Metamath Proof Explorer

Theorem iooabslt

Proof