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

Theorem minvecolem4 29596
Description: Lemma for minveco 29600. 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 29530 . . . . . 6 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
3 minveco.x . . . . . . 7 𝑋 = (BaseSet‘𝑈)
4 minveco.d . . . . . . 7 𝐷 = (IndMet‘𝑈)
53, 4imsxmet 29408 . . . . . 6 (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋))
61, 2, 53syl 18 . . . . 5 (𝜑𝐷 ∈ (∞Met‘𝑋))
7 minveco.j . . . . . 6 𝐽 = (MetOpen‘𝐷)
87methaus 23786 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
9 lmfun 22642 . . . . 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 29593 . . . . 5 (𝜑𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
21 eqid 2737 . . . . . . 7 (𝐽t 𝑌) = (𝐽t 𝑌)
22 nnuz 12731 . . . . . . 7 ℕ = (ℤ‘1)
2313fvexi 6848 . . . . . . . 8 𝑌 ∈ V
2423a1i 11 . . . . . . 7 (𝜑𝑌 ∈ V)
251, 2syl 17 . . . . . . . 8 (𝜑𝑈 ∈ NrmCVec)
267mopntop 23703 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2725, 5, 263syl 18 . . . . . . 7 (𝜑𝐽 ∈ Top)
28 elin 3921 . . . . . . . . . . . . 13 (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
2914, 28sylib 217 . . . . . . . . . . . 12 (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
3029simpld 496 . . . . . . . . . . 11 (𝜑𝑊 ∈ (SubSp‘𝑈))
31 eqid 2737 . . . . . . . . . . . 12 (SubSp‘𝑈) = (SubSp‘𝑈)
323, 13, 31sspba 29443 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
3325, 30, 32syl2anc 585 . . . . . . . . . 10 (𝜑𝑌𝑋)
34 xmetres2 23624 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
356, 33, 34syl2anc 585 . . . . . . . . 9 (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
36 eqid 2737 . . . . . . . . . 10 (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
3736mopntopon 23702 . . . . . . . . 9 ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
3835, 37syl 17 . . . . . . . 8 (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
39 lmcl 22558 . . . . . . . 8 (((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
4038, 20, 39syl2anc 585 . . . . . . 7 (𝜑 → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
41 1zzd 12461 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
4221, 22, 24, 27, 40, 41, 18lmss 22559 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
43 eqid 2737 . . . . . . . . . 10 (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
4443, 7, 36metrest 23790 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
456, 33, 44syl2anc 585 . . . . . . . 8 (𝜑 → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
4645fveq2d 6838 . . . . . . 7 (𝜑 → (⇝𝑡‘(𝐽t 𝑌)) = (⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))))
4746breqd 5111 . . . . . 6 (𝜑 → (𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4842, 47bitrd 279 . . . . 5 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4920, 48mpbird 257 . . . 4 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
50 funbrfv 6885 . . . 4 (Fun (⇝𝑡𝐽) → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
5110, 49, 50sylc 65 . . 3 (𝜑 → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
5251, 40eqeltrd 2838 . 2 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑌)
533, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4b 29594 . . . . . 6 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋)
543, 11, 12, 4imsdval 29402 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5525, 15, 53, 54syl3anc 1371 . . . . 5 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5655adantr 482 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
573, 4imsmet 29407 . . . . . . . 8 (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
581, 2, 573syl 18 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
59 metcl 23595 . . . . . . 7 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6058, 15, 53, 59syl3anc 1371 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6160adantr 482 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
623, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4c 29595 . . . . . 6 (𝜑𝑆 ∈ ℝ)
6362adantr 482 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ∈ ℝ)
6425adantr 482 . . . . . 6 ((𝜑𝑦𝑌) → 𝑈 ∈ NrmCVec)
6515adantr 482 . . . . . . 7 ((𝜑𝑦𝑌) → 𝐴𝑋)
6633sselda 3939 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑦𝑋)
673, 11nvmcl 29362 . . . . . . 7 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝑀𝑦) ∈ 𝑋)
6864, 65, 66, 67syl3anc 1371 . . . . . 6 ((𝜑𝑦𝑌) → (𝐴𝑀𝑦) ∈ 𝑋)
693, 12nvcl 29377 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7064, 68, 69syl2anc 585 . . . . 5 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7162, 60ltnled 11232 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
72 eqid 2737 . . . . . . . . . . 11 (ℤ‘((⌊‘𝑇) + 1)) = (ℤ‘((⌊‘𝑇) + 1))
736adantr 482 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋))
74 minveco.t . . . . . . . . . . . . . . 15 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
7560, 62readdcld 11114 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ)
7675rehalfcld 12330 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
7776resqcld 14075 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
7862resqcld 14075 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆↑2) ∈ ℝ)
7977, 78resubcld 11513 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8079adantr 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8162, 60, 62ltadd1d 11678 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
8262recnd 11113 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆 ∈ ℂ)
83822timesd 12326 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
8483breq1d 5110 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
85 2re 12157 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
86 2pos 12186 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
8785, 86pm3.2i 472 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
8887a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
89 ltmuldiv2 11959 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9062, 75, 88, 89syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9181, 84, 903bitr2d 307 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
923, 11, 12, 13, 1, 14, 15, 4, 7, 16minvecolem1 29590 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
9392simp3d 1144 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝑅 0 ≤ 𝑤)
9492simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ⊆ ℝ)
9592simp2d 1143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ≠ ∅)
96 0re 11087 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℝ
97 breq1 5103 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
9897ralbidv 3172 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
9998rspcev 3576 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10096, 93, 99sylancr 588 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10196a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ∈ ℝ)
102 infregelb 12069 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10394, 95, 100, 101, 102syl31anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10493, 103mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
105104, 17breqtrrdi 5142 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ 𝑆)
106 metge0 23608 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10758, 15, 53, 106syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10860, 62, 107, 105addge0d 11661 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆))
109 divge0 11954 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11075, 108, 88, 109syl21anc 836 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11162, 76, 105, 110lt2sqd 14083 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
11278, 77posdifd 11672 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
11391, 111, 1123bitrd 305 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
114113biimpa 478 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
11580, 114elrpd 12879 . . . . . . . . . . . . . . . 16 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ+)
116115rpreccld 12892 . . . . . . . . . . . . . . 15 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈ ℝ+)
11774, 116eqeltrid 2842 . . . . . . . . . . . . . 14 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝑇 ∈ ℝ+)
118117rprege0d 12889 . . . . . . . . . . . . 13 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇))
119 flge0nn0 13650 . . . . . . . . . . . . 13 ((𝑇 ∈ ℝ ∧ 0 ≤ 𝑇) → (⌊‘𝑇) ∈ ℕ0)
120 nn0p1nn 12382 . . . . . . . . . . . . 13 ((⌊‘𝑇) ∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ)
121118, 119, 1203syl 18 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ)
122121nnzd 12535 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ)
12349, 51breqtrrd 5128 . . . . . . . . . . . 12 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
124123adantr 482 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
12515adantr 482 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐴𝑋)
12676adantr 482 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
127126rexrd 11135 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ*)
128 simpll 765 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝜑)
129 eluznn 12768 . . . . . . . . . . . . . . . 16 ((((⌊‘𝑇) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
130121, 129sylan 581 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
13158adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
13215adantr 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐴𝑋)
13318, 33fssd 6678 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:ℕ⟶𝑋)
134133ffvelcdmda 7026 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑋)
135 metcl 23595 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
136131, 132, 134, 135syl3anc 1371 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
137128, 130, 136syl2anc 585 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
138137resqcld 14075 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ∈ ℝ)
13962ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ)
140139resqcld 14075 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ)
141130nnrecred 12134 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ)
142140, 141readdcld 11114 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ)
14377ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
144128, 130, 19syl2anc 585 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
145117adantr 482 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ+)
146145rpred 12882 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ)
147 reflcl 13626 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → (⌊‘𝑇) ∈ ℝ)
148 peano2re 11258 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑇) ∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ)
149146, 147, 1483syl 18 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈ ℝ)
150130nnred 12098 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ)
151 fllep1 13631 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1))
152146, 151syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1))
153 eluzle 12705 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛)
154153adantl 483 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛)
155146, 149, 150, 152, 154letrd 11242 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇𝑛)
15674, 155eqbrtrrid 5136 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛)
157 1red 11086 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 1 ∈ ℝ)
15879ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
159114adantr 482 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
160130nngt0d 12132 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < 𝑛)
161 lediv23 11977 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ ((((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ ∧ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
162157, 158, 159, 150, 160, 161syl122anc 1379 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
163156, 162mpbid 231 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
164140, 141, 143leaddsub2d 11687 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
165163, 164mpbird 257 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
166138, 142, 143, 144, 165letrd 11242 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
16776ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
168 metge0 23608 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
169131, 132, 134, 168syl3anc 1371 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
170128, 130, 169syl2anc 585 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
171110ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
172137, 167, 170, 171le2sqd 14084 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
173166, 172mpbird 257 . . . . . . . . . . 11 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17472, 7, 73, 122, 124, 125, 127, 173lmle 24575 . . . . . . . . . 10 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17560, 62, 60leadd2d 11680 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
17660recnd 11113 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℂ)
1771762timesd 12326 . . . . . . . . . . . . 13 (𝜑 → (2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))))
178177breq1d 5110 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
179 lemuldiv2 11966 . . . . . . . . . . . . . 14 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18087, 179mp3an3 1450 . . . . . . . . . . . . 13 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18160, 75, 180syl2anc 585 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
182175, 178, 1813bitr2d 307 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
183182biimpar 479 . . . . . . . . . 10 ((𝜑 ∧ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
184174, 183syldan 592 . . . . . . . . 9 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
185184ex 414 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
18671, 185sylbird 260 . . . . . . 7 (𝜑 → (¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
187186pm2.18d 127 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
188187adantr 482 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
18994adantr 482 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑅 ⊆ ℝ)
190100adantr 482 . . . . . . 7 ((𝜑𝑦𝑌) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
191 simpr 486 . . . . . . . . 9 ((𝜑𝑦𝑌) → 𝑦𝑌)
192 fvex 6847 . . . . . . . . 9 (𝑁‘(𝐴𝑀𝑦)) ∈ V
193 eqid 2737 . . . . . . . . . 10 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
194193elrnmpt1 5906 . . . . . . . . 9 ((𝑦𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
195191, 192, 194sylancl 587 . . . . . . . 8 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
196195, 16eleqtrrdi 2849 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅)
197 infrelb 12070 . . . . . . 7 ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
198189, 190, 196, 197syl3anc 1371 . . . . . 6 ((𝜑𝑦𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
19917, 198eqbrtrid 5135 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦)))
20061, 63, 70, 188, 199letrd 11242 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20156, 200eqbrtrrd 5124 . . 3 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
202201ralrimiva 3141 . 2 (𝜑 → ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
203 oveq2 7354 . . . . . 6 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡𝐽)‘𝐹)))
204203fveq2d 6838 . . . . 5 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
205204breq1d 5110 . . . 4 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
206205ralbidv 3172 . . 3 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (∀𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
207206rspcev 3576 . 2 ((((⇝𝑡𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20852, 202, 207syl2anc 585 1 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1541  wcel 2106  wne 2941  wral 3062  wrex 3071  Vcvv 3443  cin 3904  wss 3905  c0 4277   class class class wbr 5100  cmpt 5183   × cxp 5625  ran crn 5628  cres 5629  Fun wfun 6482  wf 6484  cfv 6488  (class class class)co 7346  infcinf 9307  cr 10980  0cc0 10981  1c1 10982   + caddc 10984   · cmul 10986   < clt 11119  cle 11120  cmin 11315   / cdiv 11742  cn 12083  2c2 12138  0cn0 12343  cuz 12692  +crp 12840  cfl 13620  cexp 13892  t crest 17233  ∞Metcxmet 20692  Metcmet 20693  MetOpencmopn 20697  Topctop 22152  TopOnctopon 22169  𝑡clm 22487  Hauscha 22569  NrmCVeccnv 29300  BaseSetcba 29302  𝑣 cnsb 29305  normCVcnmcv 29306  IndMetcims 29307  SubSpcss 29437  CPreHilOLDccphlo 29528  CBanccbn 29578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-rep 5237  ax-sep 5251  ax-nul 5258  ax-pow 5315  ax-pr 5379  ax-un 7659  ax-cnex 11037  ax-resscn 11038  ax-1cn 11039  ax-icn 11040  ax-addcl 11041  ax-addrcl 11042  ax-mulcl 11043  ax-mulrcl 11044  ax-mulcom 11045  ax-addass 11046  ax-mulass 11047  ax-distr 11048  ax-i2m1 11049  ax-1ne0 11050  ax-1rid 11051  ax-rnegex 11052  ax-rrecex 11053  ax-cnre 11054  ax-pre-lttri 11055  ax-pre-lttrn 11056  ax-pre-ltadd 11057  ax-pre-mulgt0 11058  ax-pre-sup 11059  ax-addf 11060  ax-mulf 11061
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3351  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3735  df-csb 3851  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3924  df-nul 4278  df-if 4482  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-int 4903  df-iun 4951  df-iin 4952  df-br 5101  df-opab 5163  df-mpt 5184  df-tr 5218  df-id 5525  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5582  df-we 5584  df-xp 5633  df-rel 5634  df-cnv 5635  df-co 5636  df-dm 5637  df-rn 5638  df-res 5639  df-ima 5640  df-pred 6246  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6440  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-riota 7302  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7790  df-1st 7908  df-2nd 7909  df-frecs 8176  df-wrecs 8207  df-recs 8281  df-rdg 8320  df-er 8578  df-map 8697  df-pm 8698  df-en 8814  df-dom 8815  df-sdom 8816  df-fin 8817  df-fi 9277  df-sup 9308  df-inf 9309  df-pnf 11121  df-mnf 11122  df-xr 11123  df-ltxr 11124  df-le 11125  df-sub 11317  df-neg 11318  df-div 11743  df-nn 12084  df-2 12146  df-3 12147  df-4 12148  df-n0 12344  df-z 12430  df-uz 12693  df-q 12799  df-rp 12841  df-xneg 12958  df-xadd 12959  df-xmul 12960  df-ico 13195  df-icc 13196  df-fl 13622  df-seq 13832  df-exp 13893  df-cj 14914  df-re 14915  df-im 14916  df-sqrt 15050  df-abs 15051  df-rest 17235  df-topgen 17256  df-psmet 20699  df-xmet 20700  df-met 20701  df-bl 20702  df-mopn 20703  df-fbas 20704  df-fg 20705  df-top 22153  df-topon 22170  df-bases 22206  df-cld 22280  df-ntr 22281  df-cls 22282  df-nei 22359  df-lm 22490  df-haus 22576  df-fil 23107  df-fm 23199  df-flim 23200  df-flf 23201  df-cfil 24529  df-cau 24530  df-cmet 24531  df-grpo 29209  df-gid 29210  df-ginv 29211  df-gdiv 29212  df-ablo 29261  df-vc 29275  df-nv 29308  df-va 29311  df-ba 29312  df-sm 29313  df-0v 29314  df-vs 29315  df-nmcv 29316  df-ims 29317  df-ssp 29438  df-ph 29529  df-cbn 29579
This theorem is referenced by:  minvecolem5  29597
  Copyright terms: Public domain W3C validator