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

Theorem minvecolem4 30900
Description: Lemma for minveco 30904. 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 30834 . . . . . 6 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
3 minveco.x . . . . . . 7 𝑋 = (BaseSet‘𝑈)
4 minveco.d . . . . . . 7 𝐷 = (IndMet‘𝑈)
53, 4imsxmet 30712 . . . . . 6 (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋))
61, 2, 53syl 18 . . . . 5 (𝜑𝐷 ∈ (∞Met‘𝑋))
7 minveco.j . . . . . 6 𝐽 = (MetOpen‘𝐷)
87methaus 24534 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
9 lmfun 23390 . . . . 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 30897 . . . . 5 (𝜑𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
21 eqid 2736 . . . . . . 7 (𝐽t 𝑌) = (𝐽t 𝑌)
22 nnuz 12922 . . . . . . 7 ℕ = (ℤ‘1)
2313fvexi 6919 . . . . . . . 8 𝑌 ∈ V
2423a1i 11 . . . . . . 7 (𝜑𝑌 ∈ V)
251, 2syl 17 . . . . . . . 8 (𝜑𝑈 ∈ NrmCVec)
267mopntop 24451 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2725, 5, 263syl 18 . . . . . . 7 (𝜑𝐽 ∈ Top)
28 elin 3966 . . . . . . . . . . . . 13 (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
2914, 28sylib 218 . . . . . . . . . . . 12 (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
3029simpld 494 . . . . . . . . . . 11 (𝜑𝑊 ∈ (SubSp‘𝑈))
31 eqid 2736 . . . . . . . . . . . 12 (SubSp‘𝑈) = (SubSp‘𝑈)
323, 13, 31sspba 30747 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
3325, 30, 32syl2anc 584 . . . . . . . . . 10 (𝜑𝑌𝑋)
34 xmetres2 24372 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
356, 33, 34syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
36 eqid 2736 . . . . . . . . . 10 (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
3736mopntopon 24450 . . . . . . . . 9 ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
3835, 37syl 17 . . . . . . . 8 (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
39 lmcl 23306 . . . . . . . 8 (((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
4038, 20, 39syl2anc 584 . . . . . . 7 (𝜑 → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
41 1zzd 12650 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
4221, 22, 24, 27, 40, 41, 18lmss 23307 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
43 eqid 2736 . . . . . . . . . 10 (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
4443, 7, 36metrest 24538 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
456, 33, 44syl2anc 584 . . . . . . . 8 (𝜑 → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
4645fveq2d 6909 . . . . . . 7 (𝜑 → (⇝𝑡‘(𝐽t 𝑌)) = (⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))))
4746breqd 5153 . . . . . 6 (𝜑 → (𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4842, 47bitrd 279 . . . . 5 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4920, 48mpbird 257 . . . 4 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
50 funbrfv 6956 . . . 4 (Fun (⇝𝑡𝐽) → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
5110, 49, 50sylc 65 . . 3 (𝜑 → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
5251, 40eqeltrd 2840 . 2 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑌)
533, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4b 30898 . . . . . 6 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋)
543, 11, 12, 4imsdval 30706 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5525, 15, 53, 54syl3anc 1372 . . . . 5 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5655adantr 480 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
573, 4imsmet 30711 . . . . . . . 8 (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
581, 2, 573syl 18 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
59 metcl 24343 . . . . . . 7 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6058, 15, 53, 59syl3anc 1372 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6160adantr 480 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
623, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4c 30899 . . . . . 6 (𝜑𝑆 ∈ ℝ)
6362adantr 480 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ∈ ℝ)
6425adantr 480 . . . . . 6 ((𝜑𝑦𝑌) → 𝑈 ∈ NrmCVec)
6515adantr 480 . . . . . . 7 ((𝜑𝑦𝑌) → 𝐴𝑋)
6633sselda 3982 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑦𝑋)
673, 11nvmcl 30666 . . . . . . 7 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝑀𝑦) ∈ 𝑋)
6864, 65, 66, 67syl3anc 1372 . . . . . 6 ((𝜑𝑦𝑌) → (𝐴𝑀𝑦) ∈ 𝑋)
693, 12nvcl 30681 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7064, 68, 69syl2anc 584 . . . . 5 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7162, 60ltnled 11409 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
72 eqid 2736 . . . . . . . . . . 11 (ℤ‘((⌊‘𝑇) + 1)) = (ℤ‘((⌊‘𝑇) + 1))
736adantr 480 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋))
74 minveco.t . . . . . . . . . . . . . . 15 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
7560, 62readdcld 11291 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ)
7675rehalfcld 12515 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
7776resqcld 14166 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
7862resqcld 14166 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆↑2) ∈ ℝ)
7977, 78resubcld 11692 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8079adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8162, 60, 62ltadd1d 11857 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
8262recnd 11290 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆 ∈ ℂ)
83822timesd 12511 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
8483breq1d 5152 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
85 2re 12341 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
86 2pos 12370 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
8785, 86pm3.2i 470 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
8887a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
89 ltmuldiv2 12143 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9062, 75, 88, 89syl3anc 1372 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9181, 84, 903bitr2d 307 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
923, 11, 12, 13, 1, 14, 15, 4, 7, 16minvecolem1 30894 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
9392simp3d 1144 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝑅 0 ≤ 𝑤)
9492simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ⊆ ℝ)
9592simp2d 1143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ≠ ∅)
96 0re 11264 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℝ
97 breq1 5145 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
9897ralbidv 3177 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
9998rspcev 3621 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10096, 93, 99sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10196a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ∈ ℝ)
102 infregelb 12253 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10394, 95, 100, 101, 102syl31anc 1374 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10493, 103mpbird 257 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
105104, 17breqtrrdi 5184 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ 𝑆)
106 metge0 24356 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10758, 15, 53, 106syl3anc 1372 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10860, 62, 107, 105addge0d 11840 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆))
109 divge0 12138 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11075, 108, 88, 109syl21anc 837 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11162, 76, 105, 110lt2sqd 14296 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
11278, 77posdifd 11851 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
11391, 111, 1123bitrd 305 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
114113biimpa 476 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
11580, 114elrpd 13075 . . . . . . . . . . . . . . . 16 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ+)
116115rpreccld 13088 . . . . . . . . . . . . . . 15 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈ ℝ+)
11774, 116eqeltrid 2844 . . . . . . . . . . . . . 14 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝑇 ∈ ℝ+)
118117rprege0d 13085 . . . . . . . . . . . . 13 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇))
119 flge0nn0 13861 . . . . . . . . . . . . 13 ((𝑇 ∈ ℝ ∧ 0 ≤ 𝑇) → (⌊‘𝑇) ∈ ℕ0)
120 nn0p1nn 12567 . . . . . . . . . . . . 13 ((⌊‘𝑇) ∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ)
121118, 119, 1203syl 18 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ)
122121nnzd 12642 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ)
12349, 51breqtrrd 5170 . . . . . . . . . . . 12 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
124123adantr 480 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
12515adantr 480 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐴𝑋)
12676adantr 480 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
127126rexrd 11312 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ*)
128 simpll 766 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝜑)
129 eluznn 12961 . . . . . . . . . . . . . . . 16 ((((⌊‘𝑇) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
130121, 129sylan 580 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
13158adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
13215adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐴𝑋)
13318, 33fssd 6752 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:ℕ⟶𝑋)
134133ffvelcdmda 7103 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑋)
135 metcl 24343 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
136131, 132, 134, 135syl3anc 1372 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
137128, 130, 136syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
138137resqcld 14166 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ∈ ℝ)
13962ad2antrr 726 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ)
140139resqcld 14166 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ)
141130nnrecred 12318 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ)
142140, 141readdcld 11291 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ)
14377ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
144128, 130, 19syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
145117adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ+)
146145rpred 13078 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ)
147 reflcl 13837 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → (⌊‘𝑇) ∈ ℝ)
148 peano2re 11435 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑇) ∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ)
149146, 147, 1483syl 18 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈ ℝ)
150130nnred 12282 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ)
151 fllep1 13842 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1))
152146, 151syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1))
153 eluzle 12892 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛)
154153adantl 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛)
155146, 149, 150, 152, 154letrd 11419 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇𝑛)
15674, 155eqbrtrrid 5178 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛)
157 1red 11263 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 1 ∈ ℝ)
15879ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
159114adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
160130nngt0d 12316 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < 𝑛)
161 lediv23 12161 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ ((((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ ∧ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
162157, 158, 159, 150, 160, 161syl122anc 1380 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
163156, 162mpbid 232 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
164140, 141, 143leaddsub2d 11866 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
165163, 164mpbird 257 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
166138, 142, 143, 144, 165letrd 11419 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
16776ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
168 metge0 24356 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
169131, 132, 134, 168syl3anc 1372 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
170128, 130, 169syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
171110ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
172137, 167, 170, 171le2sqd 14297 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
173166, 172mpbird 257 . . . . . . . . . . 11 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17472, 7, 73, 122, 124, 125, 127, 173lmle 25336 . . . . . . . . . 10 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17560, 62, 60leadd2d 11859 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
17660recnd 11290 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℂ)
1771762timesd 12511 . . . . . . . . . . . . 13 (𝜑 → (2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))))
178177breq1d 5152 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
179 lemuldiv2 12150 . . . . . . . . . . . . . 14 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18087, 179mp3an3 1451 . . . . . . . . . . . . 13 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18160, 75, 180syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
182175, 178, 1813bitr2d 307 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
183182biimpar 477 . . . . . . . . . 10 ((𝜑 ∧ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
184174, 183syldan 591 . . . . . . . . 9 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
185184ex 412 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
18671, 185sylbird 260 . . . . . . 7 (𝜑 → (¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
187186pm2.18d 127 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
188187adantr 480 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
18994adantr 480 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑅 ⊆ ℝ)
190100adantr 480 . . . . . . 7 ((𝜑𝑦𝑌) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
191 simpr 484 . . . . . . . . 9 ((𝜑𝑦𝑌) → 𝑦𝑌)
192 fvex 6918 . . . . . . . . 9 (𝑁‘(𝐴𝑀𝑦)) ∈ V
193 eqid 2736 . . . . . . . . . 10 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
194193elrnmpt1 5970 . . . . . . . . 9 ((𝑦𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
195191, 192, 194sylancl 586 . . . . . . . 8 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
196195, 16eleqtrrdi 2851 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅)
197 infrelb 12254 . . . . . . 7 ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
198189, 190, 196, 197syl3anc 1372 . . . . . 6 ((𝜑𝑦𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
19917, 198eqbrtrid 5177 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦)))
20061, 63, 70, 188, 199letrd 11419 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20156, 200eqbrtrrd 5166 . . 3 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
202201ralrimiva 3145 . 2 (𝜑 → ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
203 oveq2 7440 . . . . . 6 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡𝐽)‘𝐹)))
204203fveq2d 6909 . . . . 5 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
205204breq1d 5152 . . . 4 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
206205ralbidv 3177 . . 3 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (∀𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
207206rspcev 3621 . 2 ((((⇝𝑡𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20852, 202, 207syl2anc 584 1 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1539  wcel 2107  wne 2939  wral 3060  wrex 3069  Vcvv 3479  cin 3949  wss 3950  c0 4332   class class class wbr 5142  cmpt 5224   × cxp 5682  ran crn 5685  cres 5686  Fun wfun 6554  wf 6556  cfv 6560  (class class class)co 7432  infcinf 9482  cr 11155  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161   < clt 11296  cle 11297  cmin 11493   / cdiv 11921  cn 12267  2c2 12322  0cn0 12528  cuz 12879  +crp 13035  cfl 13831  cexp 14103  t crest 17466  ∞Metcxmet 21350  Metcmet 21351  MetOpencmopn 21355  Topctop 22900  TopOnctopon 22917  𝑡clm 23235  Hauscha 23317  NrmCVeccnv 30604  BaseSetcba 30606  𝑣 cnsb 30609  normCVcnmcv 30610  IndMetcims 30611  SubSpcss 30741  CPreHilOLDccphlo 30832  CBanccbn 30882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234  ax-addf 11235  ax-mulf 11236
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-int 4946  df-iun 4992  df-iin 4993  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-er 8746  df-map 8869  df-pm 8870  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-fi 9452  df-sup 9483  df-inf 9484  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-n0 12529  df-z 12616  df-uz 12880  df-q 12992  df-rp 13036  df-xneg 13155  df-xadd 13156  df-xmul 13157  df-ico 13394  df-icc 13395  df-fl 13833  df-seq 14044  df-exp 14104  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-rest 17468  df-topgen 17489  df-psmet 21357  df-xmet 21358  df-met 21359  df-bl 21360  df-mopn 21361  df-fbas 21362  df-fg 21363  df-top 22901  df-topon 22918  df-bases 22954  df-cld 23028  df-ntr 23029  df-cls 23030  df-nei 23107  df-lm 23238  df-haus 23324  df-fil 23855  df-fm 23947  df-flim 23948  df-flf 23949  df-cfil 25290  df-cau 25291  df-cmet 25292  df-grpo 30513  df-gid 30514  df-ginv 30515  df-gdiv 30516  df-ablo 30565  df-vc 30579  df-nv 30612  df-va 30615  df-ba 30616  df-sm 30617  df-0v 30618  df-vs 30619  df-nmcv 30620  df-ims 30621  df-ssp 30742  df-ph 30833  df-cbn 30883
This theorem is referenced by:  minvecolem5  30901
  Copyright terms: Public domain W3C validator