Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  minvecolem5 Structured version   Visualization version   GIF version

Theorem minvecolem5 27598
 Description: Lemma for minveco 27601. Discharge the assumption about the sequence 𝐹 by applying countable choice ax-cc 9204. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)
Hypotheses
Ref Expression
minveco.x 𝑋 = (BaseSet‘𝑈)
minveco.m 𝑀 = ( −𝑣𝑈)
minveco.n 𝑁 = (normCV𝑈)
minveco.y 𝑌 = (BaseSet‘𝑊)
minveco.u (𝜑𝑈 ∈ CPreHilOLD)
minveco.w (𝜑𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))
minveco.a (𝜑𝐴𝑋)
minveco.d 𝐷 = (IndMet‘𝑈)
minveco.j 𝐽 = (MetOpen‘𝐷)
minveco.r 𝑅 = ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
minveco.s 𝑆 = inf(𝑅, ℝ, < )
Assertion
Ref Expression
minvecolem5 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Distinct variable groups:   𝑥,𝑦,𝐽   𝑥,𝑀,𝑦   𝑥,𝑁,𝑦   𝜑,𝑥,𝑦   𝑥,𝑅   𝑥,𝑆,𝑦   𝑥,𝐴,𝑦   𝑥,𝐷,𝑦   𝑥,𝑈,𝑦   𝑥,𝑊,𝑦   𝑥,𝑋   𝑥,𝑌,𝑦
Allowed substitution hints:   𝑅(𝑦)   𝑋(𝑦)

Proof of Theorem minvecolem5
Dummy variables 𝑛 𝑘 𝑤 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnrecgt0 11005 . . . . . . . . . . . 12 (𝑛 ∈ ℕ → 0 < (1 / 𝑛))
21adantl 482 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 0 < (1 / 𝑛))
3 nnrecre 11004 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
43adantl 482 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
5 minveco.s . . . . . . . . . . . . . 14 𝑆 = inf(𝑅, ℝ, < )
6 minveco.x . . . . . . . . . . . . . . . . . 18 𝑋 = (BaseSet‘𝑈)
7 minveco.m . . . . . . . . . . . . . . . . . 18 𝑀 = ( −𝑣𝑈)
8 minveco.n . . . . . . . . . . . . . . . . . 18 𝑁 = (normCV𝑈)
9 minveco.y . . . . . . . . . . . . . . . . . 18 𝑌 = (BaseSet‘𝑊)
10 minveco.u . . . . . . . . . . . . . . . . . 18 (𝜑𝑈 ∈ CPreHilOLD)
11 minveco.w . . . . . . . . . . . . . . . . . 18 (𝜑𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))
12 minveco.a . . . . . . . . . . . . . . . . . 18 (𝜑𝐴𝑋)
13 minveco.d . . . . . . . . . . . . . . . . . 18 𝐷 = (IndMet‘𝑈)
14 minveco.j . . . . . . . . . . . . . . . . . 18 𝐽 = (MetOpen‘𝐷)
15 minveco.r . . . . . . . . . . . . . . . . . 18 𝑅 = ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
166, 7, 8, 9, 10, 11, 12, 13, 14, 15minvecolem1 27591 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
1716adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
1817simp1d 1071 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑅 ⊆ ℝ)
1917simp2d 1072 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → 𝑅 ≠ ∅)
20 0re 9987 . . . . . . . . . . . . . . . 16 0 ∈ ℝ
2117simp3d 1073 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → ∀𝑤𝑅 0 ≤ 𝑤)
22 breq1 4618 . . . . . . . . . . . . . . . . . 18 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
2322ralbidv 2980 . . . . . . . . . . . . . . . . 17 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
2423rspcev 3295 . . . . . . . . . . . . . . . 16 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
2520, 21, 24sylancr 694 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
26 infrecl 10952 . . . . . . . . . . . . . . 15 ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
2718, 19, 25, 26syl3anc 1323 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → inf(𝑅, ℝ, < ) ∈ ℝ)
285, 27syl5eqel 2702 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑆 ∈ ℝ)
2928resqcld 12978 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝑆↑2) ∈ ℝ)
304, 29ltaddposd 10558 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (0 < (1 / 𝑛) ↔ (𝑆↑2) < ((𝑆↑2) + (1 / 𝑛))))
312, 30mpbid 222 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (𝑆↑2) < ((𝑆↑2) + (1 / 𝑛)))
3229, 4readdcld 10016 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ)
3328sqge0d 12979 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝑆↑2))
3429, 4, 33, 2addgegt0d 10548 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 0 < ((𝑆↑2) + (1 / 𝑛)))
3532, 34elrpd 11816 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ+)
3635rpge0d 11823 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 0 ≤ ((𝑆↑2) + (1 / 𝑛)))
37 resqrtth 13933 . . . . . . . . . . 11 ((((𝑆↑2) + (1 / 𝑛)) ∈ ℝ ∧ 0 ≤ ((𝑆↑2) + (1 / 𝑛))) → ((√‘((𝑆↑2) + (1 / 𝑛)))↑2) = ((𝑆↑2) + (1 / 𝑛)))
3832, 36, 37syl2anc 692 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → ((√‘((𝑆↑2) + (1 / 𝑛)))↑2) = ((𝑆↑2) + (1 / 𝑛)))
3931, 38breqtrrd 4643 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑆↑2) < ((√‘((𝑆↑2) + (1 / 𝑛)))↑2))
4035rpsqrtcld 14087 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → (√‘((𝑆↑2) + (1 / 𝑛))) ∈ ℝ+)
4140rpred 11819 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → (√‘((𝑆↑2) + (1 / 𝑛))) ∈ ℝ)
42 0red 9988 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 0 ∈ ℝ)
43 infregelb 10954 . . . . . . . . . . . . 13 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
4418, 19, 25, 42, 43syl31anc 1326 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
4521, 44mpbird 247 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → 0 ≤ inf(𝑅, ℝ, < ))
4645, 5syl6breqr 4657 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 0 ≤ 𝑆)
4732, 36sqrtge0d 14096 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (√‘((𝑆↑2) + (1 / 𝑛))))
4828, 41, 46, 47lt2sqd 12986 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → (𝑆 < (√‘((𝑆↑2) + (1 / 𝑛))) ↔ (𝑆↑2) < ((√‘((𝑆↑2) + (1 / 𝑛)))↑2)))
4939, 48mpbird 247 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → 𝑆 < (√‘((𝑆↑2) + (1 / 𝑛))))
5028, 41ltnled 10131 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → (𝑆 < (√‘((𝑆↑2) + (1 / 𝑛))) ↔ ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑆))
5149, 50mpbid 222 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑆)
525breq2i 4623 . . . . . . . . 9 ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑆 ↔ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ inf(𝑅, ℝ, < ))
53 infregelb 10954 . . . . . . . . . 10 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ (√‘((𝑆↑2) + (1 / 𝑛))) ∈ ℝ) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤))
5418, 19, 25, 41, 53syl31anc 1326 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤))
5552, 54syl5bb 272 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑆 ↔ ∀𝑤𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤))
5615raleqi 3131 . . . . . . . . 9 (∀𝑤𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑤 ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤)
57 fvex 6160 . . . . . . . . . . 11 (𝑁‘(𝐴𝑀𝑦)) ∈ V
5857rgenw 2919 . . . . . . . . . 10 𝑦𝑌 (𝑁‘(𝐴𝑀𝑦)) ∈ V
59 eqid 2621 . . . . . . . . . . 11 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
60 breq2 4619 . . . . . . . . . . 11 (𝑤 = (𝑁‘(𝐴𝑀𝑦)) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))))
6159, 60ralrnmpt 6326 . . . . . . . . . 10 (∀𝑦𝑌 (𝑁‘(𝐴𝑀𝑦)) ∈ V → (∀𝑤 ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑦𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))))
6258, 61ax-mp 5 . . . . . . . . 9 (∀𝑤 ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))(√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑦𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))
6356, 62bitri 264 . . . . . . . 8 (∀𝑤𝑅 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑤 ↔ ∀𝑦𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))
6455, 63syl6bb 276 . . . . . . 7 ((𝜑𝑛 ∈ ℕ) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ 𝑆 ↔ ∀𝑦𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦))))
6551, 64mtbid 314 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ¬ ∀𝑦𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))
66 rexnal 2989 . . . . . 6 (∃𝑦𝑌 ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ¬ ∀𝑦𝑌 (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))
6765, 66sylibr 224 . . . . 5 ((𝜑𝑛 ∈ ℕ) → ∃𝑦𝑌 ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)))
6832adantr 481 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ)
69 phnv 27530 . . . . . . . . . . . . 13 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
7010, 69syl 17 . . . . . . . . . . . 12 (𝜑𝑈 ∈ NrmCVec)
7170ad2antrr 761 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → 𝑈 ∈ NrmCVec)
7212ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → 𝐴𝑋)
73 inss1 3813 . . . . . . . . . . . . . . . 16 ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
7473, 11sseldi 3582 . . . . . . . . . . . . . . 15 (𝜑𝑊 ∈ (SubSp‘𝑈))
75 eqid 2621 . . . . . . . . . . . . . . . 16 (SubSp‘𝑈) = (SubSp‘𝑈)
766, 9, 75sspba 27443 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
7770, 74, 76syl2anc 692 . . . . . . . . . . . . . 14 (𝜑𝑌𝑋)
7877adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → 𝑌𝑋)
7978sselda 3584 . . . . . . . . . . . 12 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → 𝑦𝑋)
806, 7nvmcl 27362 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝑀𝑦) ∈ 𝑋)
8171, 72, 79, 80syl3anc 1323 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (𝐴𝑀𝑦) ∈ 𝑋)
826, 8nvcl 27377 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
8371, 81, 82syl2anc 692 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
8483resqcld 12978 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → ((𝑁‘(𝐴𝑀𝑦))↑2) ∈ ℝ)
8568, 84letrid 10136 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2) ∨ ((𝑁‘(𝐴𝑀𝑦))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
8685ord 392 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (¬ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2) → ((𝑁‘(𝐴𝑀𝑦))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
8741adantr 481 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (√‘((𝑆↑2) + (1 / 𝑛))) ∈ ℝ)
8847adantr 481 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → 0 ≤ (√‘((𝑆↑2) + (1 / 𝑛))))
896, 8nvge0 27389 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → 0 ≤ (𝑁‘(𝐴𝑀𝑦)))
9071, 81, 89syl2anc 692 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → 0 ≤ (𝑁‘(𝐴𝑀𝑦)))
9187, 83, 88, 90le2sqd 12987 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ((√‘((𝑆↑2) + (1 / 𝑛)))↑2) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2)))
9238adantr 481 . . . . . . . . . 10 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → ((√‘((𝑆↑2) + (1 / 𝑛)))↑2) = ((𝑆↑2) + (1 / 𝑛)))
9392breq1d 4625 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (((√‘((𝑆↑2) + (1 / 𝑛)))↑2) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2) ↔ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2)))
9491, 93bitrd 268 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → ((√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2)))
9594notbid 308 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ¬ ((𝑆↑2) + (1 / 𝑛)) ≤ ((𝑁‘(𝐴𝑀𝑦))↑2)))
966, 7, 8, 13imsdval 27402 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝐷𝑦) = (𝑁‘(𝐴𝑀𝑦)))
9771, 72, 79, 96syl3anc 1323 . . . . . . . . 9 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (𝐴𝐷𝑦) = (𝑁‘(𝐴𝑀𝑦)))
9897oveq1d 6622 . . . . . . . 8 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → ((𝐴𝐷𝑦)↑2) = ((𝑁‘(𝐴𝑀𝑦))↑2))
9998breq1d 4625 . . . . . . 7 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ↔ ((𝑁‘(𝐴𝑀𝑦))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
10086, 95, 993imtr4d 283 . . . . . 6 (((𝜑𝑛 ∈ ℕ) ∧ 𝑦𝑌) → (¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) → ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
101100reximdva 3011 . . . . 5 ((𝜑𝑛 ∈ ℕ) → (∃𝑦𝑌 ¬ (√‘((𝑆↑2) + (1 / 𝑛))) ≤ (𝑁‘(𝐴𝑀𝑦)) → ∃𝑦𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
10267, 101mpd 15 . . . 4 ((𝜑𝑛 ∈ ℕ) → ∃𝑦𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
103102ralrimiva 2960 . . 3 (𝜑 → ∀𝑛 ∈ ℕ ∃𝑦𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
104 fvex 6160 . . . . 5 (BaseSet‘𝑊) ∈ V
1059, 104eqeltri 2694 . . . 4 𝑌 ∈ V
106 nnenom 12722 . . . 4 ℕ ≈ ω
107 oveq2 6615 . . . . . 6 (𝑦 = (𝑓𝑛) → (𝐴𝐷𝑦) = (𝐴𝐷(𝑓𝑛)))
108107oveq1d 6622 . . . . 5 (𝑦 = (𝑓𝑛) → ((𝐴𝐷𝑦)↑2) = ((𝐴𝐷(𝑓𝑛))↑2))
109108breq1d 4625 . . . 4 (𝑦 = (𝑓𝑛) → (((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ↔ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
110105, 106, 109axcc4 9208 . . 3 (∀𝑛 ∈ ℕ ∃𝑦𝑌 ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) → ∃𝑓(𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
111103, 110syl 17 . 2 (𝜑 → ∃𝑓(𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))))
11210adantr 481 . . 3 ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝑈 ∈ CPreHilOLD)
11311adantr 481 . . 3 ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))
11412adantr 481 . . 3 ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝐴𝑋)
115 simprl 793 . . 3 ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → 𝑓:ℕ⟶𝑌)
116 simprr 795 . . . 4 ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
117 fveq2 6150 . . . . . . . 8 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
118117oveq2d 6623 . . . . . . 7 (𝑛 = 𝑘 → (𝐴𝐷(𝑓𝑛)) = (𝐴𝐷(𝑓𝑘)))
119118oveq1d 6622 . . . . . 6 (𝑛 = 𝑘 → ((𝐴𝐷(𝑓𝑛))↑2) = ((𝐴𝐷(𝑓𝑘))↑2))
120 oveq2 6615 . . . . . . 7 (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
121120oveq2d 6623 . . . . . 6 (𝑛 = 𝑘 → ((𝑆↑2) + (1 / 𝑛)) = ((𝑆↑2) + (1 / 𝑘)))
122119, 121breq12d 4628 . . . . 5 (𝑛 = 𝑘 → (((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ↔ ((𝐴𝐷(𝑓𝑘))↑2) ≤ ((𝑆↑2) + (1 / 𝑘))))
123122rspccva 3294 . . . 4 ((∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)) ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝑓𝑘))↑2) ≤ ((𝑆↑2) + (1 / 𝑘)))
124116, 123sylan 488 . . 3 (((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) ∧ 𝑘 ∈ ℕ) → ((𝐴𝐷(𝑓𝑘))↑2) ≤ ((𝑆↑2) + (1 / 𝑘)))
125 eqid 2621 . . 3 (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝑓)) + 𝑆) / 2)↑2) − (𝑆↑2))) = (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝑓)) + 𝑆) / 2)↑2) − (𝑆↑2)))
1266, 7, 8, 9, 112, 113, 114, 13, 14, 15, 5, 115, 124, 125minvecolem4 27597 . 2 ((𝜑 ∧ (𝑓:ℕ⟶𝑌 ∧ ∀𝑛 ∈ ℕ ((𝐴𝐷(𝑓𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))) → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
127111, 126exlimddv 1860 1 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480  ∃wex 1701   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∩ cin 3555   ⊆ wss 3556  ∅c0 3893   class class class wbr 4615   ↦ cmpt 4675  ran crn 5077  ⟶wf 5845  ‘cfv 5849  (class class class)co 6607  infcinf 8294  ℝcr 9882  0cc0 9883  1c1 9884   + caddc 9886   < clt 10021   ≤ cle 10022   − cmin 10213   / cdiv 10631  ℕcn 10967  2c2 11017  ↑cexp 12803  √csqrt 13910  MetOpencmopn 19658  ⇝𝑡clm 20943  NrmCVeccnv 27300  BaseSetcba 27302   −𝑣 cnsb 27305  normCVcnmcv 27306  IndMetcims 27307  SubSpcss 27437  CPreHilOLDccphlo 27528  CBanccbn 27579 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-cc 9204  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961  ax-addf 9962  ax-mulf 9963 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-oadd 7512  df-er 7690  df-map 7807  df-pm 7808  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-fi 8264  df-sup 8295  df-inf 8296  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-n0 11240  df-z 11325  df-uz 11635  df-q 11736  df-rp 11780  df-xneg 11893  df-xadd 11894  df-xmul 11895  df-ico 12126  df-icc 12127  df-fl 12536  df-seq 12745  df-exp 12804  df-cj 13776  df-re 13777  df-im 13778  df-sqrt 13912  df-abs 13913  df-rest 16007  df-topgen 16028  df-psmet 19660  df-xmet 19661  df-met 19662  df-bl 19663  df-mopn 19664  df-fbas 19665  df-fg 19666  df-top 20621  df-topon 20638  df-bases 20664  df-cld 20736  df-ntr 20737  df-cls 20738  df-nei 20815  df-lm 20946  df-haus 21032  df-fil 21563  df-fm 21655  df-flim 21656  df-flf 21657  df-cfil 22966  df-cau 22967  df-cmet 22968  df-grpo 27208  df-gid 27209  df-ginv 27210  df-gdiv 27211  df-ablo 27260  df-vc 27275  df-nv 27308  df-va 27311  df-ba 27312  df-sm 27313  df-0v 27314  df-vs 27315  df-nmcv 27316  df-ims 27317  df-ssp 27438  df-ph 27529  df-cbn 27580 This theorem is referenced by:  minvecolem7  27600
 Copyright terms: Public domain W3C validator