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

Theorem minvecolem4 28043
Description: Lemma for minveco 28047. The convergent point of the cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in 𝑌. (Contributed by Mario Carneiro, 7-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(𝑅, ℝ, < )
minveco.f (𝜑𝐹:ℕ⟶𝑌)
minveco.1 ((𝜑𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
minveco.t 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
Assertion
Ref Expression
minvecolem4 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Distinct variable groups:   𝑥,𝑛,𝑦,𝐹   𝑛,𝐽,𝑥,𝑦   𝑥,𝑀,𝑦   𝑥,𝑁,𝑦   𝜑,𝑛,𝑥,𝑦   𝑥,𝑅   𝑆,𝑛,𝑥,𝑦   𝐴,𝑛,𝑥,𝑦   𝐷,𝑛,𝑥,𝑦   𝑥,𝑈,𝑦   𝑥,𝑊,𝑦   𝑇,𝑛   𝑛,𝑋,𝑥   𝑛,𝑌,𝑥,𝑦
Allowed substitution hints:   𝑅(𝑦,𝑛)   𝑇(𝑥,𝑦)   𝑈(𝑛)   𝑀(𝑛)   𝑁(𝑛)   𝑊(𝑛)   𝑋(𝑦)

Proof of Theorem minvecolem4
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 minveco.u . . . . . 6 (𝜑𝑈 ∈ CPreHilOLD)
2 phnv 27976 . . . . . 6 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
3 minveco.x . . . . . . 7 𝑋 = (BaseSet‘𝑈)
4 minveco.d . . . . . . 7 𝐷 = (IndMet‘𝑈)
53, 4imsxmet 27854 . . . . . 6 (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋))
61, 2, 53syl 18 . . . . 5 (𝜑𝐷 ∈ (∞Met‘𝑋))
7 minveco.j . . . . . 6 𝐽 = (MetOpen‘𝐷)
87methaus 22524 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
9 lmfun 21385 . . . . 5 (𝐽 ∈ Haus → Fun (⇝𝑡𝐽))
106, 8, 93syl 18 . . . 4 (𝜑 → Fun (⇝𝑡𝐽))
11 minveco.m . . . . . 6 𝑀 = ( −𝑣𝑈)
12 minveco.n . . . . . 6 𝑁 = (normCV𝑈)
13 minveco.y . . . . . 6 𝑌 = (BaseSet‘𝑊)
14 minveco.w . . . . . 6 (𝜑𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))
15 minveco.a . . . . . 6 (𝜑𝐴𝑋)
16 minveco.r . . . . . 6 𝑅 = ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
17 minveco.s . . . . . 6 𝑆 = inf(𝑅, ℝ, < )
18 minveco.f . . . . . 6 (𝜑𝐹:ℕ⟶𝑌)
19 minveco.1 . . . . . 6 ((𝜑𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
203, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4a 28040 . . . . 5 (𝜑𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
21 eqid 2758 . . . . . . 7 (𝐽t 𝑌) = (𝐽t 𝑌)
22 nnuz 11914 . . . . . . 7 ℕ = (ℤ‘1)
23 fvex 6360 . . . . . . . . 9 (BaseSet‘𝑊) ∈ V
2413, 23eqeltri 2833 . . . . . . . 8 𝑌 ∈ V
2524a1i 11 . . . . . . 7 (𝜑𝑌 ∈ V)
261, 2syl 17 . . . . . . . 8 (𝜑𝑈 ∈ NrmCVec)
277mopntop 22444 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2826, 5, 273syl 18 . . . . . . 7 (𝜑𝐽 ∈ Top)
29 elin 3937 . . . . . . . . . . . . 13 (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
3014, 29sylib 208 . . . . . . . . . . . 12 (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
3130simpld 477 . . . . . . . . . . 11 (𝜑𝑊 ∈ (SubSp‘𝑈))
32 eqid 2758 . . . . . . . . . . . 12 (SubSp‘𝑈) = (SubSp‘𝑈)
333, 13, 32sspba 27889 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
3426, 31, 33syl2anc 696 . . . . . . . . . 10 (𝜑𝑌𝑋)
35 xmetres2 22365 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
366, 34, 35syl2anc 696 . . . . . . . . 9 (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
37 eqid 2758 . . . . . . . . . 10 (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
3837mopntopon 22443 . . . . . . . . 9 ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
3936, 38syl 17 . . . . . . . 8 (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
40 lmcl 21301 . . . . . . . 8 (((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
4139, 20, 40syl2anc 696 . . . . . . 7 (𝜑 → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
42 1zzd 11598 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
4321, 22, 25, 28, 41, 42, 18lmss 21302 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
44 eqid 2758 . . . . . . . . . 10 (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
4544, 7, 37metrest 22528 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
466, 34, 45syl2anc 696 . . . . . . . 8 (𝜑 → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
4746fveq2d 6354 . . . . . . 7 (𝜑 → (⇝𝑡‘(𝐽t 𝑌)) = (⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))))
4847breqd 4813 . . . . . 6 (𝜑 → (𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4943, 48bitrd 268 . . . . 5 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
5020, 49mpbird 247 . . . 4 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
51 funbrfv 6393 . . . 4 (Fun (⇝𝑡𝐽) → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
5210, 50, 51sylc 65 . . 3 (𝜑 → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
5352, 41eqeltrd 2837 . 2 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑌)
543, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4b 28041 . . . . . 6 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋)
553, 11, 12, 4imsdval 27848 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5626, 15, 54, 55syl3anc 1477 . . . . 5 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5756adantr 472 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
583, 4imsmet 27853 . . . . . . . 8 (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
591, 2, 583syl 18 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
60 metcl 22336 . . . . . . 7 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6159, 15, 54, 60syl3anc 1477 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6261adantr 472 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
633, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4c 28042 . . . . . 6 (𝜑𝑆 ∈ ℝ)
6463adantr 472 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ∈ ℝ)
6526adantr 472 . . . . . 6 ((𝜑𝑦𝑌) → 𝑈 ∈ NrmCVec)
6615adantr 472 . . . . . . 7 ((𝜑𝑦𝑌) → 𝐴𝑋)
6734sselda 3742 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑦𝑋)
683, 11nvmcl 27808 . . . . . . 7 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝑀𝑦) ∈ 𝑋)
6965, 66, 67, 68syl3anc 1477 . . . . . 6 ((𝜑𝑦𝑌) → (𝐴𝑀𝑦) ∈ 𝑋)
703, 12nvcl 27823 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7165, 69, 70syl2anc 696 . . . . 5 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7263, 61ltnled 10374 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
73 eqid 2758 . . . . . . . . . . 11 (ℤ‘((⌊‘𝑇) + 1)) = (ℤ‘((⌊‘𝑇) + 1))
746adantr 472 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋))
75 minveco.t . . . . . . . . . . . . . . 15 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
7661, 63readdcld 10259 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ)
7776rehalfcld 11469 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
7877resqcld 13227 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
7963resqcld 13227 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆↑2) ∈ ℝ)
8078, 79resubcld 10648 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8180adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8263, 61, 63ltadd1d 10810 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
8363recnd 10258 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆 ∈ ℂ)
84832timesd 11465 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
8584breq1d 4812 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
86 2re 11280 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
87 2pos 11302 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
8886, 87pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
8988a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
90 ltmuldiv2 11087 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9163, 76, 89, 90syl3anc 1477 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9282, 85, 913bitr2d 296 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
933, 11, 12, 13, 1, 14, 15, 4, 7, 16minvecolem1 28037 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
9493simp3d 1139 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝑅 0 ≤ 𝑤)
9593simp1d 1137 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ⊆ ℝ)
9693simp2d 1138 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ≠ ∅)
97 0re 10230 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℝ
98 breq1 4805 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
9998ralbidv 3122 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10099rspcev 3447 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10197, 94, 100sylancr 698 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10297a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ∈ ℝ)
103 infregelb 11197 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10495, 96, 101, 102, 103syl31anc 1480 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10594, 104mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
106105, 17syl6breqr 4844 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ 𝑆)
107 metge0 22349 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10859, 15, 54, 107syl3anc 1477 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10961, 63, 108, 106addge0d 10793 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆))
110 divge0 11082 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11176, 109, 89, 110syl21anc 1476 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11263, 77, 106, 111lt2sqd 13235 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
11379, 78posdifd 10804 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
11492, 112, 1133bitrd 294 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
115114biimpa 502 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
11681, 115elrpd 12060 . . . . . . . . . . . . . . . 16 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ+)
117116rpreccld 12073 . . . . . . . . . . . . . . 15 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈ ℝ+)
11875, 117syl5eqel 2841 . . . . . . . . . . . . . 14 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝑇 ∈ ℝ+)
119118rprege0d 12070 . . . . . . . . . . . . 13 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇))
120 flge0nn0 12813 . . . . . . . . . . . . 13 ((𝑇 ∈ ℝ ∧ 0 ≤ 𝑇) → (⌊‘𝑇) ∈ ℕ0)
121 nn0p1nn 11522 . . . . . . . . . . . . 13 ((⌊‘𝑇) ∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ)
122119, 120, 1213syl 18 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ)
123122nnzd 11671 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ)
12450, 52breqtrrd 4830 . . . . . . . . . . . 12 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
125124adantr 472 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
12615adantr 472 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐴𝑋)
12777adantr 472 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
128127rexrd 10279 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ*)
129 simpll 807 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝜑)
130 eluznn 11949 . . . . . . . . . . . . . . . 16 ((((⌊‘𝑇) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
131122, 130sylan 489 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
13259adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
13315adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐴𝑋)
13418, 34fssd 6216 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:ℕ⟶𝑋)
135134ffvelrnda 6520 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑋)
136 metcl 22336 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
137132, 133, 135, 136syl3anc 1477 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
138129, 131, 137syl2anc 696 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
139138resqcld 13227 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ∈ ℝ)
14063ad2antrr 764 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ)
141140resqcld 13227 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ)
142131nnrecred 11256 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ)
143141, 142readdcld 10259 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ)
14478ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
145129, 131, 19syl2anc 696 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
146118adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ+)
147146rpred 12063 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ)
148 reflcl 12789 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → (⌊‘𝑇) ∈ ℝ)
149 peano2re 10399 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑇) ∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ)
150147, 148, 1493syl 18 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈ ℝ)
151131nnred 11225 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ)
152 fllep1 12794 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1))
153147, 152syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1))
154 eluzle 11890 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛)
155154adantl 473 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛)
156147, 150, 151, 153, 155letrd 10384 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇𝑛)
15775, 156syl5eqbrr 4838 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛)
158 1red 10245 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 1 ∈ ℝ)
15980ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
160115adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
161131nngt0d 11254 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < 𝑛)
162 lediv23 11105 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ ((((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ ∧ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
163158, 159, 160, 151, 161, 162syl122anc 1486 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
164157, 163mpbid 222 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
165141, 142, 144leaddsub2d 10819 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
166164, 165mpbird 247 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
167139, 143, 144, 145, 166letrd 10384 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
16877ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
169 metge0 22349 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
170132, 133, 135, 169syl3anc 1477 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
171129, 131, 170syl2anc 696 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
172111ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
173138, 168, 171, 172le2sqd 13236 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
174167, 173mpbird 247 . . . . . . . . . . 11 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17573, 7, 74, 123, 125, 126, 128, 174lmle 23297 . . . . . . . . . 10 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17661, 63, 61leadd2d 10812 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
17761recnd 10258 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℂ)
1781772timesd 11465 . . . . . . . . . . . . 13 (𝜑 → (2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))))
179178breq1d 4812 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
180 lemuldiv2 11094 . . . . . . . . . . . . . 14 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18188, 180mp3an3 1560 . . . . . . . . . . . . 13 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18261, 76, 181syl2anc 696 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
183176, 179, 1823bitr2d 296 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
184183biimpar 503 . . . . . . . . . 10 ((𝜑 ∧ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
185175, 184syldan 488 . . . . . . . . 9 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
186185ex 449 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
18772, 186sylbird 250 . . . . . . 7 (𝜑 → (¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
188187pm2.18d 124 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
189188adantr 472 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
19095adantr 472 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑅 ⊆ ℝ)
191101adantr 472 . . . . . . 7 ((𝜑𝑦𝑌) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
192 simpr 479 . . . . . . . . 9 ((𝜑𝑦𝑌) → 𝑦𝑌)
193 fvex 6360 . . . . . . . . 9 (𝑁‘(𝐴𝑀𝑦)) ∈ V
194 eqid 2758 . . . . . . . . . 10 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
195194elrnmpt1 5527 . . . . . . . . 9 ((𝑦𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
196192, 193, 195sylancl 697 . . . . . . . 8 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
197196, 16syl6eleqr 2848 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅)
198 infrelb 11198 . . . . . . 7 ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
199190, 191, 197, 198syl3anc 1477 . . . . . 6 ((𝜑𝑦𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
20017, 199syl5eqbr 4837 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦)))
20162, 64, 71, 189, 200letrd 10384 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20257, 201eqbrtrrd 4826 . . 3 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
203202ralrimiva 3102 . 2 (𝜑 → ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
204 oveq2 6819 . . . . . 6 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡𝐽)‘𝐹)))
205204fveq2d 6354 . . . . 5 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
206205breq1d 4812 . . . 4 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
207206ralbidv 3122 . . 3 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (∀𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
208207rspcev 3447 . 2 ((((⇝𝑡𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20953, 203, 208syl2anc 696 1 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1630  wcel 2137  wne 2930  wral 3048  wrex 3049  Vcvv 3338  cin 3712  wss 3713  c0 4056   class class class wbr 4802  cmpt 4879   × cxp 5262  ran crn 5265  cres 5266  Fun wfun 6041  wf 6043  cfv 6047  (class class class)co 6811  infcinf 8510  cr 10125  0cc0 10126  1c1 10127   + caddc 10129   · cmul 10131   < clt 10264  cle 10265  cmin 10456   / cdiv 10874  cn 11210  2c2 11260  0cn0 11482  cuz 11877  +crp 12023  cfl 12783  cexp 13052  t crest 16281  ∞Metcxmt 19931  Metcme 19932  MetOpencmopn 19936  Topctop 20898  TopOnctopon 20915  𝑡clm 21230  Hauscha 21312  NrmCVeccnv 27746  BaseSetcba 27748  𝑣 cnsb 27751  normCVcnmcv 27752  IndMetcims 27753  SubSpcss 27883  CPreHilOLDccphlo 27974  CBanccbn 28025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-rep 4921  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112  ax-cnex 10182  ax-resscn 10183  ax-1cn 10184  ax-icn 10185  ax-addcl 10186  ax-addrcl 10187  ax-mulcl 10188  ax-mulrcl 10189  ax-mulcom 10190  ax-addass 10191  ax-mulass 10192  ax-distr 10193  ax-i2m1 10194  ax-1ne0 10195  ax-1rid 10196  ax-rnegex 10197  ax-rrecex 10198  ax-cnre 10199  ax-pre-lttri 10200  ax-pre-lttrn 10201  ax-pre-ltadd 10202  ax-pre-mulgt0 10203  ax-pre-sup 10204  ax-addf 10205  ax-mulf 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-nel 3034  df-ral 3053  df-rex 3054  df-reu 3055  df-rmo 3056  df-rab 3057  df-v 3340  df-sbc 3575  df-csb 3673  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-pss 3729  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-tp 4324  df-op 4326  df-uni 4587  df-int 4626  df-iun 4672  df-iin 4673  df-br 4803  df-opab 4863  df-mpt 4880  df-tr 4903  df-id 5172  df-eprel 5177  df-po 5185  df-so 5186  df-fr 5223  df-we 5225  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-pred 5839  df-ord 5885  df-on 5886  df-lim 5887  df-suc 5888  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-f1 6052  df-fo 6053  df-f1o 6054  df-fv 6055  df-riota 6772  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-om 7229  df-1st 7331  df-2nd 7332  df-wrecs 7574  df-recs 7635  df-rdg 7673  df-oadd 7731  df-er 7909  df-map 8023  df-pm 8024  df-en 8120  df-dom 8121  df-sdom 8122  df-fin 8123  df-fi 8480  df-sup 8511  df-inf 8512  df-pnf 10266  df-mnf 10267  df-xr 10268  df-ltxr 10269  df-le 10270  df-sub 10458  df-neg 10459  df-div 10875  df-nn 11211  df-2 11269  df-3 11270  df-4 11271  df-n0 11483  df-z 11568  df-uz 11878  df-q 11980  df-rp 12024  df-xneg 12137  df-xadd 12138  df-xmul 12139  df-ico 12372  df-icc 12373  df-fl 12785  df-seq 12994  df-exp 13053  df-cj 14036  df-re 14037  df-im 14038  df-sqrt 14172  df-abs 14173  df-rest 16283  df-topgen 16304  df-psmet 19938  df-xmet 19939  df-met 19940  df-bl 19941  df-mopn 19942  df-fbas 19943  df-fg 19944  df-top 20899  df-topon 20916  df-bases 20950  df-cld 21023  df-ntr 21024  df-cls 21025  df-nei 21102  df-lm 21233  df-haus 21319  df-fil 21849  df-fm 21941  df-flim 21942  df-flf 21943  df-cfil 23251  df-cau 23252  df-cmet 23253  df-grpo 27654  df-gid 27655  df-ginv 27656  df-gdiv 27657  df-ablo 27706  df-vc 27721  df-nv 27754  df-va 27757  df-ba 27758  df-sm 27759  df-0v 27760  df-vs 27761  df-nmcv 27762  df-ims 27763  df-ssp 27884  df-ph 27975  df-cbn 28026
This theorem is referenced by:  minvecolem5  28044
  Copyright terms: Public domain W3C validator