This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = BaseSet ⁡ U
minveco.m ⊢ M = - v ⁡ U
minveco.n ⊢ N = norm CV ⁡ U
minveco.y ⊢ Y = BaseSet ⁡ W
minveco.u ⊢ φ → U ∈ CPreHil OLD
minveco.w ⊢ φ → W ∈ SubSp ⁡ U ∩ CBan
minveco.a ⊢ φ → A ∈ X
minveco.d ⊢ D = IndMet ⁡ U
minveco.j ⊢ J = MetOpen ⁡ D
minveco.r ⊢ R = ran ⁡ y ∈ Y ⟼ N ⁡ A M y
minveco.s ⊢ S = inf R ℝ <
minveco.f ⊢ φ → F : ℕ ⟶ Y
minveco.1 ⊢ φ ∧ n ∈ ℕ → A D F ⁡ n 2 ≤ S 2 + 1 n
Assertion minvecolem4c ⊢ φ → S ∈ ℝ

Proof

Step Hyp Ref Expression
1 minveco.x ⊢ X = BaseSet ⁡ U
2 minveco.m ⊢ M = - v ⁡ U
3 minveco.n ⊢ N = norm CV ⁡ U
4 minveco.y ⊢ Y = BaseSet ⁡ W
5 minveco.u ⊢ φ → U ∈ CPreHil OLD
6 minveco.w ⊢ φ → W ∈ SubSp ⁡ U ∩ CBan
7 minveco.a ⊢ φ → A ∈ X
8 minveco.d ⊢ D = IndMet ⁡ U
9 minveco.j ⊢ J = MetOpen ⁡ D
10 minveco.r ⊢ R = ran ⁡ y ∈ Y ⟼ N ⁡ A M y
11 minveco.s ⊢ S = inf R ℝ <
12 minveco.f ⊢ φ → F : ℕ ⟶ Y
13 minveco.1 ⊢ φ ∧ n ∈ ℕ → A D F ⁡ n 2 ≤ S 2 + 1 n
14 1 2 3 4 5 6 7 8 9 10 minvecolem1 ⊢ φ → R ⊆ ℝ ∧ R ≠ ∅ ∧ ∀ w ∈ R 0 ≤ w
15 14 simp1d ⊢ φ → R ⊆ ℝ
16 14 simp2d ⊢ φ → R ≠ ∅
17 0re ⊢ 0 ∈ ℝ
18 14 simp3d ⊢ φ → ∀ w ∈ R 0 ≤ w
19 breq1 ⊢ x = 0 → x ≤ w ↔ 0 ≤ w
20 19 ralbidv ⊢ x = 0 → ∀ w ∈ R x ≤ w ↔ ∀ w ∈ R 0 ≤ w
21 20 rspcev ⊢ 0 ∈ ℝ ∧ ∀ w ∈ R 0 ≤ w → ∃ x ∈ ℝ ∀ w ∈ R x ≤ w
22 17 18 21 sylancr ⊢ φ → ∃ x ∈ ℝ ∀ w ∈ R x ≤ w
23 infrecl ⊢ R ⊆ ℝ ∧ R ≠ ∅ ∧ ∃ x ∈ ℝ ∀ w ∈ R x ≤ w → inf R ℝ < ∈ ℝ
24 15 16 22 23 syl3anc ⊢ φ → inf R ℝ < ∈ ℝ
25 11 24 eqeltrid ⊢ φ → S ∈ ℝ