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

Theorem minvecolem4 29822
Description: Lemma for minveco 29826. 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 29756 . . . . . 6 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
3 minveco.x . . . . . . 7 𝑋 = (BaseSet‘𝑈)
4 minveco.d . . . . . . 7 𝐷 = (IndMet‘𝑈)
53, 4imsxmet 29634 . . . . . 6 (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋))
61, 2, 53syl 18 . . . . 5 (𝜑𝐷 ∈ (∞Met‘𝑋))
7 minveco.j . . . . . 6 𝐽 = (MetOpen‘𝐷)
87methaus 23876 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
9 lmfun 22732 . . . . 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 29819 . . . . 5 (𝜑𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
21 eqid 2736 . . . . . . 7 (𝐽t 𝑌) = (𝐽t 𝑌)
22 nnuz 12806 . . . . . . 7 ℕ = (ℤ‘1)
2313fvexi 6856 . . . . . . . 8 𝑌 ∈ V
2423a1i 11 . . . . . . 7 (𝜑𝑌 ∈ V)
251, 2syl 17 . . . . . . . 8 (𝜑𝑈 ∈ NrmCVec)
267mopntop 23793 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2725, 5, 263syl 18 . . . . . . 7 (𝜑𝐽 ∈ Top)
28 elin 3926 . . . . . . . . . . . . 13 (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
2914, 28sylib 217 . . . . . . . . . . . 12 (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
3029simpld 495 . . . . . . . . . . 11 (𝜑𝑊 ∈ (SubSp‘𝑈))
31 eqid 2736 . . . . . . . . . . . 12 (SubSp‘𝑈) = (SubSp‘𝑈)
323, 13, 31sspba 29669 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
3325, 30, 32syl2anc 584 . . . . . . . . . 10 (𝜑𝑌𝑋)
34 xmetres2 23714 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
356, 33, 34syl2anc 584 . . . . . . . . 9 (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
36 eqid 2736 . . . . . . . . . 10 (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
3736mopntopon 23792 . . . . . . . . 9 ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
3835, 37syl 17 . . . . . . . 8 (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
39 lmcl 22648 . . . . . . . 8 (((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
4038, 20, 39syl2anc 584 . . . . . . 7 (𝜑 → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
41 1zzd 12534 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
4221, 22, 24, 27, 40, 41, 18lmss 22649 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
43 eqid 2736 . . . . . . . . . 10 (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
4443, 7, 36metrest 23880 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
456, 33, 44syl2anc 584 . . . . . . . 8 (𝜑 → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
4645fveq2d 6846 . . . . . . 7 (𝜑 → (⇝𝑡‘(𝐽t 𝑌)) = (⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))))
4746breqd 5116 . . . . . 6 (𝜑 → (𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4842, 47bitrd 278 . . . . 5 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4920, 48mpbird 256 . . . 4 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
50 funbrfv 6893 . . . 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 29820 . . . . . 6 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋)
543, 11, 12, 4imsdval 29628 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5525, 15, 53, 54syl3anc 1371 . . . . 5 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5655adantr 481 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
573, 4imsmet 29633 . . . . . . . 8 (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
581, 2, 573syl 18 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
59 metcl 23685 . . . . . . 7 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6058, 15, 53, 59syl3anc 1371 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6160adantr 481 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
623, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4c 29821 . . . . . 6 (𝜑𝑆 ∈ ℝ)
6362adantr 481 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ∈ ℝ)
6425adantr 481 . . . . . 6 ((𝜑𝑦𝑌) → 𝑈 ∈ NrmCVec)
6515adantr 481 . . . . . . 7 ((𝜑𝑦𝑌) → 𝐴𝑋)
6633sselda 3944 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑦𝑋)
673, 11nvmcl 29588 . . . . . . 7 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝑀𝑦) ∈ 𝑋)
6864, 65, 66, 67syl3anc 1371 . . . . . 6 ((𝜑𝑦𝑌) → (𝐴𝑀𝑦) ∈ 𝑋)
693, 12nvcl 29603 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7064, 68, 69syl2anc 584 . . . . 5 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7162, 60ltnled 11302 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
72 eqid 2736 . . . . . . . . . . 11 (ℤ‘((⌊‘𝑇) + 1)) = (ℤ‘((⌊‘𝑇) + 1))
736adantr 481 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋))
74 minveco.t . . . . . . . . . . . . . . 15 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
7560, 62readdcld 11184 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ)
7675rehalfcld 12400 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
7776resqcld 14030 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
7862resqcld 14030 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆↑2) ∈ ℝ)
7977, 78resubcld 11583 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8079adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8162, 60, 62ltadd1d 11748 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
8262recnd 11183 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆 ∈ ℂ)
83822timesd 12396 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
8483breq1d 5115 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
85 2re 12227 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
86 2pos 12256 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
8785, 86pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
8887a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
89 ltmuldiv2 12029 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9062, 75, 88, 89syl3anc 1371 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9181, 84, 903bitr2d 306 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
923, 11, 12, 13, 1, 14, 15, 4, 7, 16minvecolem1 29816 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
9392simp3d 1144 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝑅 0 ≤ 𝑤)
9492simp1d 1142 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ⊆ ℝ)
9592simp2d 1143 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ≠ ∅)
96 0re 11157 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℝ
97 breq1 5108 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
9897ralbidv 3174 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
9998rspcev 3581 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10096, 93, 99sylancr 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10196a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ∈ ℝ)
102 infregelb 12139 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10394, 95, 100, 101, 102syl31anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10493, 103mpbird 256 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
105104, 17breqtrrdi 5147 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ 𝑆)
106 metge0 23698 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10758, 15, 53, 106syl3anc 1371 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10860, 62, 107, 105addge0d 11731 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆))
109 divge0 12024 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11075, 108, 88, 109syl21anc 836 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11162, 76, 105, 110lt2sqd 14159 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
11278, 77posdifd 11742 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
11391, 111, 1123bitrd 304 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
114113biimpa 477 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
11580, 114elrpd 12954 . . . . . . . . . . . . . . . 16 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ+)
116115rpreccld 12967 . . . . . . . . . . . . . . 15 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈ ℝ+)
11774, 116eqeltrid 2842 . . . . . . . . . . . . . 14 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝑇 ∈ ℝ+)
118117rprege0d 12964 . . . . . . . . . . . . 13 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇))
119 flge0nn0 13725 . . . . . . . . . . . . 13 ((𝑇 ∈ ℝ ∧ 0 ≤ 𝑇) → (⌊‘𝑇) ∈ ℕ0)
120 nn0p1nn 12452 . . . . . . . . . . . . 13 ((⌊‘𝑇) ∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ)
121118, 119, 1203syl 18 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ)
122121nnzd 12526 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ)
12349, 51breqtrrd 5133 . . . . . . . . . . . 12 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
124123adantr 481 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
12515adantr 481 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐴𝑋)
12676adantr 481 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
127126rexrd 11205 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ*)
128 simpll 765 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝜑)
129 eluznn 12843 . . . . . . . . . . . . . . . 16 ((((⌊‘𝑇) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
130121, 129sylan 580 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
13158adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
13215adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐴𝑋)
13318, 33fssd 6686 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:ℕ⟶𝑋)
134133ffvelcdmda 7035 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑋)
135 metcl 23685 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
136131, 132, 134, 135syl3anc 1371 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
137128, 130, 136syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
138137resqcld 14030 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ∈ ℝ)
13962ad2antrr 724 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ)
140139resqcld 14030 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ)
141130nnrecred 12204 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ)
142140, 141readdcld 11184 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ)
14377ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
144128, 130, 19syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
145117adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ+)
146145rpred 12957 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ)
147 reflcl 13701 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → (⌊‘𝑇) ∈ ℝ)
148 peano2re 11328 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑇) ∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ)
149146, 147, 1483syl 18 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈ ℝ)
150130nnred 12168 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ)
151 fllep1 13706 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1))
152146, 151syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1))
153 eluzle 12776 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛)
154153adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛)
155146, 149, 150, 152, 154letrd 11312 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇𝑛)
15674, 155eqbrtrrid 5141 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛)
157 1red 11156 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 1 ∈ ℝ)
15879ad2antrr 724 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
159114adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
160130nngt0d 12202 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < 𝑛)
161 lediv23 12047 . . . . . . . . . . . . . . . 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 11757 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
165163, 164mpbird 256 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
166138, 142, 143, 144, 165letrd 11312 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
16776ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
168 metge0 23698 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
169131, 132, 134, 168syl3anc 1371 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
170128, 130, 169syl2anc 584 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
171110ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
172137, 167, 170, 171le2sqd 14160 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
173166, 172mpbird 256 . . . . . . . . . . 11 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17472, 7, 73, 122, 124, 125, 127, 173lmle 24665 . . . . . . . . . 10 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17560, 62, 60leadd2d 11750 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
17660recnd 11183 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℂ)
1771762timesd 12396 . . . . . . . . . . . . 13 (𝜑 → (2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))))
178177breq1d 5115 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
179 lemuldiv2 12036 . . . . . . . . . . . . . 14 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18087, 179mp3an3 1450 . . . . . . . . . . . . 13 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18160, 75, 180syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
182175, 178, 1813bitr2d 306 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
183182biimpar 478 . . . . . . . . . 10 ((𝜑 ∧ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
184174, 183syldan 591 . . . . . . . . 9 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
185184ex 413 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
18671, 185sylbird 259 . . . . . . 7 (𝜑 → (¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
187186pm2.18d 127 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
188187adantr 481 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
18994adantr 481 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑅 ⊆ ℝ)
190100adantr 481 . . . . . . 7 ((𝜑𝑦𝑌) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
191 simpr 485 . . . . . . . . 9 ((𝜑𝑦𝑌) → 𝑦𝑌)
192 fvex 6855 . . . . . . . . 9 (𝑁‘(𝐴𝑀𝑦)) ∈ V
193 eqid 2736 . . . . . . . . . 10 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
194193elrnmpt1 5913 . . . . . . . . 9 ((𝑦𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
195191, 192, 194sylancl 586 . . . . . . . 8 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
196195, 16eleqtrrdi 2849 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅)
197 infrelb 12140 . . . . . . 7 ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
198189, 190, 196, 197syl3anc 1371 . . . . . 6 ((𝜑𝑦𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
19917, 198eqbrtrid 5140 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦)))
20061, 63, 70, 188, 199letrd 11312 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20156, 200eqbrtrrd 5129 . . 3 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
202201ralrimiva 3143 . 2 (𝜑 → ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
203 oveq2 7365 . . . . . 6 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡𝐽)‘𝐹)))
204203fveq2d 6846 . . . . 5 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
205204breq1d 5115 . . . 4 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
206205ralbidv 3174 . . 3 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (∀𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
207206rspcev 3581 . 2 ((((⇝𝑡𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20852, 202, 207syl2anc 584 1 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396   = wceq 1541  wcel 2106  wne 2943  wral 3064  wrex 3073  Vcvv 3445  cin 3909  wss 3910  c0 4282   class class class wbr 5105  cmpt 5188   × cxp 5631  ran crn 5634  cres 5635  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  infcinf 9377  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  2c2 12208  0cn0 12413  cuz 12763  +crp 12915  cfl 13695  cexp 13967  t crest 17302  ∞Metcxmet 20781  Metcmet 20782  MetOpencmopn 20786  Topctop 22242  TopOnctopon 22259  𝑡clm 22577  Hauscha 22659  NrmCVeccnv 29526  BaseSetcba 29528  𝑣 cnsb 29531  normCVcnmcv 29532  IndMetcims 29533  SubSpcss 29663  CPreHilOLDccphlo 29754  CBanccbn 29804
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-n0 12414  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ico 13270  df-icc 13271  df-fl 13697  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-rest 17304  df-topgen 17325  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-top 22243  df-topon 22260  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lm 22580  df-haus 22666  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-cfil 24619  df-cau 24620  df-cmet 24621  df-grpo 29435  df-gid 29436  df-ginv 29437  df-gdiv 29438  df-ablo 29487  df-vc 29501  df-nv 29534  df-va 29537  df-ba 29538  df-sm 29539  df-0v 29540  df-vs 29541  df-nmcv 29542  df-ims 29543  df-ssp 29664  df-ph 29755  df-cbn 29805
This theorem is referenced by:  minvecolem5  29823
  Copyright terms: Public domain W3C validator