Theorem minvecolem4c

Description: Lemma for minveco . The infimum of the distances to A is a real number. (Contributed by Mario Carneiro, 16-Jun-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	minveco.m	$$⊢M={-}_v\left(U\right)$$
	minveco.n	$$⊢N={norm}_{CV}\left(U\right)$$
	minveco.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
	minveco.u	$$⊢\phi \to U\in {CPreHil}_{\mathrm{OLD}}$$
	minveco.w	$$⊢\phi \to W\in \left(\mathrm{SubSp}\left(U\right)\cap \mathrm{CBan}\right)$$
	minveco.a	$$⊢\phi \to A\in X$$
	minveco.d	$$⊢D=\mathrm{IndMet}\left(U\right)$$
	minveco.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	minveco.r	$$⊢R=\mathrm{ran}\left(y\in Y⟼N\left(AMy\right)\right)$$
	minveco.s	$$⊢S=inf\left(R,ℝ,<\right)$$
	minveco.f	$$⊢\phi \to F:\mathbb{N}⟶Y$$
	minveco.1	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to {\left(ADF\left(n\right)\right)}^2\le S^2+\left(\frac{1}{n}\right)$$
Assertion	minvecolem4c	$$⊢\phi \to S\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		minveco.x	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		minveco.m	$$⊢M={-}_v\left(U\right)$$
3		minveco.n	$$⊢N={norm}_{CV}\left(U\right)$$
4		minveco.y	$$⊢Y=\mathrm{BaseSet}\left(W\right)$$
5		minveco.u	$$⊢\phi \to U\in {CPreHil}_{\mathrm{OLD}}$$
6		minveco.w	$$⊢\phi \to W\in \left(\mathrm{SubSp}\left(U\right)\cap \mathrm{CBan}\right)$$
7		minveco.a	$$⊢\phi \to A\in X$$
8		minveco.d	$$⊢D=\mathrm{IndMet}\left(U\right)$$
9		minveco.j	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
10		minveco.r	$$⊢R=\mathrm{ran}\left(y\in Y⟼N\left(AMy\right)\right)$$
11		minveco.s	$$⊢S=inf\left(R,ℝ,<\right)$$
12		minveco.f	$$⊢\phi \to F:\mathbb{N}⟶Y$$
13		minveco.1	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to {\left(ADF\left(n\right)\right)}^2\le S^2+\left(\frac{1}{n}\right)$$
14	1 2 3 4 5 6 7 8 9 10	minvecolem1	$$⊢\phi \to \left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \forall w\in R0\le w\right)$$
15	14	simp1d	$$⊢\phi \to R\subseteq ℝ$$
16	14	simp2d	$$⊢\phi \to R\ne \varnothing$$
17		0re	$$⊢0\in ℝ$$
18	14	simp3d	$$⊢\phi \to \forall w\in R0\le w$$
19		breq1	$$⊢x=0\to \left(x\le w\leftrightarrow 0\le w\right)$$
20	19	ralbidv	$$⊢x=0\to \left(\forall w\in Rx\le w\leftrightarrow \forall w\in R0\le w\right)$$
21	20	rspcev	$$⊢\left(0\in ℝ\wedge \forall w\in R0\le w\right)\to \exists x\in ℝ\forall w\in Rx\le w$$
22	17 18 21	sylancr	$$⊢\phi \to \exists x\in ℝ\forall w\in Rx\le w$$
23		infrecl	$$⊢\left(R\subseteq ℝ\wedge R\ne \varnothing \wedge \exists x\in ℝ\forall w\in Rx\le w\right)\to inf\left(R,ℝ,<\right)\in ℝ$$
24	15 16 22 23	syl3anc	$$⊢\phi \to inf\left(R,ℝ,<\right)\in ℝ$$
25	11 24	eqeltrid	$$⊢\phi \to S\in ℝ$$