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

Theorem minvecolem4 27624
Description: Lemma for minveco 27628. 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 27557 . . . . . 6 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
3 minveco.x . . . . . . 7 𝑋 = (BaseSet‘𝑈)
4 minveco.d . . . . . . 7 𝐷 = (IndMet‘𝑈)
53, 4imsxmet 27435 . . . . . 6 (𝑈 ∈ NrmCVec → 𝐷 ∈ (∞Met‘𝑋))
61, 2, 53syl 18 . . . . 5 (𝜑𝐷 ∈ (∞Met‘𝑋))
7 minveco.j . . . . . 6 𝐽 = (MetOpen‘𝐷)
87methaus 22265 . . . . 5 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Haus)
9 lmfun 21125 . . . . 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 27621 . . . . 5 (𝜑𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
21 eqid 2621 . . . . . . 7 (𝐽t 𝑌) = (𝐽t 𝑌)
22 nnuz 11683 . . . . . . 7 ℕ = (ℤ‘1)
23 fvex 6168 . . . . . . . . 9 (BaseSet‘𝑊) ∈ V
2413, 23eqeltri 2694 . . . . . . . 8 𝑌 ∈ V
2524a1i 11 . . . . . . 7 (𝜑𝑌 ∈ V)
261, 2syl 17 . . . . . . . 8 (𝜑𝑈 ∈ NrmCVec)
277mopntop 22185 . . . . . . . 8 (𝐷 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top)
2826, 5, 273syl 18 . . . . . . 7 (𝜑𝐽 ∈ Top)
29 elin 3780 . . . . . . . . . . . . 13 (𝑊 ∈ ((SubSp‘𝑈) ∩ CBan) ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
3014, 29sylib 208 . . . . . . . . . . . 12 (𝜑 → (𝑊 ∈ (SubSp‘𝑈) ∧ 𝑊 ∈ CBan))
3130simpld 475 . . . . . . . . . . 11 (𝜑𝑊 ∈ (SubSp‘𝑈))
32 eqid 2621 . . . . . . . . . . . 12 (SubSp‘𝑈) = (SubSp‘𝑈)
333, 13, 32sspba 27470 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
3426, 31, 33syl2anc 692 . . . . . . . . . 10 (𝜑𝑌𝑋)
35 xmetres2 22106 . . . . . . . . . 10 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
366, 34, 35syl2anc 692 . . . . . . . . 9 (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌))
37 eqid 2621 . . . . . . . . . 10 (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))
3837mopntopon 22184 . . . . . . . . 9 ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (∞Met‘𝑌) → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
3936, 38syl 17 . . . . . . . 8 (𝜑 → (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌))
40 lmcl 21041 . . . . . . . 8 (((MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))) ∈ (TopOn‘𝑌) ∧ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
4139, 20, 40syl2anc 692 . . . . . . 7 (𝜑 → ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ∈ 𝑌)
42 1zzd 11368 . . . . . . 7 (𝜑 → 1 ∈ ℤ)
4321, 22, 25, 28, 41, 42, 18lmss 21042 . . . . . 6 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
44 eqid 2621 . . . . . . . . . 10 (𝐷 ↾ (𝑌 × 𝑌)) = (𝐷 ↾ (𝑌 × 𝑌))
4544, 7, 37metrest 22269 . . . . . . . . 9 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑌𝑋) → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
466, 34, 45syl2anc 692 . . . . . . . 8 (𝜑 → (𝐽t 𝑌) = (MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))
4746fveq2d 6162 . . . . . . 7 (𝜑 → (⇝𝑡‘(𝐽t 𝑌)) = (⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌)))))
4847breqd 4634 . . . . . 6 (𝜑 → (𝐹(⇝𝑡‘(𝐽t 𝑌))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
4943, 48bitrd 268 . . . . 5 (𝜑 → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) ↔ 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
5020, 49mpbird 247 . . . 4 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
51 funbrfv 6201 . . . 4 (Fun (⇝𝑡𝐽) → (𝐹(⇝𝑡𝐽)((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹) → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)))
5210, 50, 51sylc 65 . . 3 (𝜑 → ((⇝𝑡𝐽)‘𝐹) = ((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹))
5352, 41eqeltrd 2698 . 2 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑌)
543, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4b 27622 . . . . . 6 (𝜑 → ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋)
553, 11, 12, 4imsdval 27429 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5626, 15, 54, 55syl3anc 1323 . . . . 5 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
5756adantr 481 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
583, 4imsmet 27434 . . . . . . . 8 (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
591, 2, 583syl 18 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
60 metcl 22077 . . . . . . 7 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6159, 15, 54, 60syl3anc 1323 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
6261adantr 481 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ)
633, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4c 27623 . . . . . 6 (𝜑𝑆 ∈ ℝ)
6463adantr 481 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ∈ ℝ)
6526adantr 481 . . . . . 6 ((𝜑𝑦𝑌) → 𝑈 ∈ NrmCVec)
6615adantr 481 . . . . . . 7 ((𝜑𝑦𝑌) → 𝐴𝑋)
6734sselda 3588 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑦𝑋)
683, 11nvmcl 27389 . . . . . . 7 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝑦𝑋) → (𝐴𝑀𝑦) ∈ 𝑋)
6965, 66, 67, 68syl3anc 1323 . . . . . 6 ((𝜑𝑦𝑌) → (𝐴𝑀𝑦) ∈ 𝑋)
703, 12nvcl 27404 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀𝑦) ∈ 𝑋) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7165, 69, 70syl2anc 692 . . . . 5 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ℝ)
7263, 61ltnled 10144 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ ¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
73 eqid 2621 . . . . . . . . . . 11 (ℤ‘((⌊‘𝑇) + 1)) = (ℤ‘((⌊‘𝑇) + 1))
746adantr 481 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐷 ∈ (∞Met‘𝑋))
75 minveco.t . . . . . . . . . . . . . . 15 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
7661, 63readdcld 10029 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ)
7776rehalfcld 11239 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
7877resqcld 12991 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
7963resqcld 12991 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆↑2) ∈ ℝ)
8078, 79resubcld 10418 . . . . . . . . . . . . . . . . . 18 (𝜑 → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8180adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
8263, 61, 63ltadd1d 10580 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
8363recnd 10028 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑𝑆 ∈ ℂ)
84832timesd 11235 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 · 𝑆) = (𝑆 + 𝑆))
8584breq1d 4633 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝑆 + 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
86 2re 11050 . . . . . . . . . . . . . . . . . . . . . . 23 2 ∈ ℝ
87 2pos 11072 . . . . . . . . . . . . . . . . . . . . . . 23 0 < 2
8886, 87pm3.2i 471 . . . . . . . . . . . . . . . . . . . . . 22 (2 ∈ ℝ ∧ 0 < 2)
8988a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (2 ∈ ℝ ∧ 0 < 2))
90 ltmuldiv2 10857 . . . . . . . . . . . . . . . . . . . . 21 ((𝑆 ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9163, 76, 89, 90syl3anc 1323 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((2 · 𝑆) < ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
9282, 85, 913bitr2d 296 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
933, 11, 12, 13, 1, 14, 15, 4, 7, 16minvecolem1 27618 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
9493simp3d 1073 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → ∀𝑤𝑅 0 ≤ 𝑤)
9593simp1d 1071 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ⊆ ℝ)
9693simp2d 1072 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝑅 ≠ ∅)
97 0re 10000 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℝ
98 breq1 4626 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
9998ralbidv 2982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10099rspcev 3299 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10197, 94, 100sylancr 694 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
10297a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 0 ∈ ℝ)
103 infregelb 10967 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10495, 96, 101, 102, 103syl31anc 1326 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
10594, 104mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
106105, 17syl6breqr 4665 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ 𝑆)
107 metge0 22090 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ ((⇝𝑡𝐽)‘𝐹) ∈ 𝑋) → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10859, 15, 54, 107syl3anc 1323 . . . . . . . . . . . . . . . . . . . . . 22 (𝜑 → 0 ≤ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)))
10961, 63, 108, 106addge0d 10563 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆))
110 divge0 10852 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ 0 ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)) ∧ (2 ∈ ℝ ∧ 0 < 2)) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11176, 109, 89, 110syl21anc 1322 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
11263, 77, 106, 111lt2sqd 12999 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑆 < (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ (𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
11379, 78posdifd 10574 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝑆↑2) < ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
11492, 112, 1133bitrd 294 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ↔ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
115114biimpa 501 . . . . . . . . . . . . . . . . 17 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
11681, 115elrpd 11829 . . . . . . . . . . . . . . . 16 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ+)
117116rpreccld 11842 . . . . . . . . . . . . . . 15 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∈ ℝ+)
11875, 117syl5eqel 2702 . . . . . . . . . . . . . 14 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝑇 ∈ ℝ+)
119118rprege0d 11839 . . . . . . . . . . . . 13 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝑇 ∈ ℝ ∧ 0 ≤ 𝑇))
120 flge0nn0 12577 . . . . . . . . . . . . 13 ((𝑇 ∈ ℝ ∧ 0 ≤ 𝑇) → (⌊‘𝑇) ∈ ℕ0)
121 nn0p1nn 11292 . . . . . . . . . . . . 13 ((⌊‘𝑇) ∈ ℕ0 → ((⌊‘𝑇) + 1) ∈ ℕ)
122119, 120, 1213syl 18 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℕ)
123122nnzd 11441 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → ((⌊‘𝑇) + 1) ∈ ℤ)
12450, 52breqtrrd 4651 . . . . . . . . . . . 12 (𝜑𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
125124adantr 481 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐹(⇝𝑡𝐽)((⇝𝑡𝐽)‘𝐹))
12615adantr 481 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → 𝐴𝑋)
12777adantr 481 . . . . . . . . . . . 12 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
128127rexrd 10049 . . . . . . . . . . 11 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ*)
129 simpll 789 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝜑)
130 eluznn 11718 . . . . . . . . . . . . . . . 16 ((((⌊‘𝑇) + 1) ∈ ℕ ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
131122, 130sylan 488 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℕ)
13259adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐷 ∈ (Met‘𝑋))
13315adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → 𝐴𝑋)
13418, 34fssd 6024 . . . . . . . . . . . . . . . . 17 (𝜑𝐹:ℕ⟶𝑋)
135134ffvelrnda 6325 . . . . . . . . . . . . . . . 16 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑋)
136 metcl 22077 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
137132, 133, 135, 136syl3anc 1323 . . . . . . . . . . . . . . 15 ((𝜑𝑛 ∈ ℕ) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
138129, 131, 137syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ∈ ℝ)
139138resqcld 12991 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ∈ ℝ)
14063ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑆 ∈ ℝ)
141140resqcld 12991 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝑆↑2) ∈ ℝ)
142131nnrecred 11026 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ∈ ℝ)
143141, 142readdcld 10029 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ∈ ℝ)
14478ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ∈ ℝ)
145129, 131, 19syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛)))
146118adantr 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ+)
147146rpred 11832 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ∈ ℝ)
148 reflcl 12553 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → (⌊‘𝑇) ∈ ℝ)
149 peano2re 10169 . . . . . . . . . . . . . . . . . 18 ((⌊‘𝑇) ∈ ℝ → ((⌊‘𝑇) + 1) ∈ ℝ)
150147, 148, 1493syl 18 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ∈ ℝ)
151131nnred 10995 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑛 ∈ ℝ)
152 fllep1 12558 . . . . . . . . . . . . . . . . . 18 (𝑇 ∈ ℝ → 𝑇 ≤ ((⌊‘𝑇) + 1))
153147, 152syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇 ≤ ((⌊‘𝑇) + 1))
154 eluzle 11660 . . . . . . . . . . . . . . . . . 18 (𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1)) → ((⌊‘𝑇) + 1) ≤ 𝑛)
155154adantl 482 . . . . . . . . . . . . . . . . 17 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((⌊‘𝑇) + 1) ≤ 𝑛)
156147, 150, 151, 153, 155letrd 10154 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 𝑇𝑛)
15775, 156syl5eqbrr 4659 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛)
158 1red 10015 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 1 ∈ ℝ)
15980ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ)
160115adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
161131nngt0d 11024 . . . . . . . . . . . . . . . 16 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 < 𝑛)
162 lediv23 10875 . . . . . . . . . . . . . . . 16 ((1 ∈ ℝ ∧ ((((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)) ∈ ℝ ∧ 0 < (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ∧ (𝑛 ∈ ℝ ∧ 0 < 𝑛)) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
163158, 159, 160, 151, 161, 162syl122anc 1332 . . . . . . . . . . . . . . 15 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((1 / (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ≤ 𝑛 ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
164157, 163mpbid 222 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2)))
165141, 142, 144leaddsub2d 10589 . . . . . . . . . . . . . 14 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) ↔ (1 / 𝑛) ≤ (((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))))
166164, 165mpbird 247 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝑆↑2) + (1 / 𝑛)) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
167139, 143, 144, 145, 166letrd 10154 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2))
16877ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ∈ ℝ)
169 metge0 22090 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋 ∧ (𝐹𝑛) ∈ 𝑋) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
170132, 133, 135, 169syl3anc 1323 . . . . . . . . . . . . . 14 ((𝜑𝑛 ∈ ℕ) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
171129, 131, 170syl2anc 692 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (𝐴𝐷(𝐹𝑛)))
172111ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → 0 ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
173138, 168, 171, 172le2sqd 13000 . . . . . . . . . . . 12 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → ((𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2) ↔ ((𝐴𝐷(𝐹𝑛))↑2) ≤ ((((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)↑2)))
174167, 173mpbird 247 . . . . . . . . . . 11 (((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ∧ 𝑛 ∈ (ℤ‘((⌊‘𝑇) + 1))) → (𝐴𝐷(𝐹𝑛)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17573, 7, 74, 123, 125, 126, 128, 174lmle 23039 . . . . . . . . . 10 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2))
17661, 63, 61leadd2d 10582 . . . . . . . . . . . 12 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
17761recnd 10028 . . . . . . . . . . . . . 14 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℂ)
1781772timesd 11235 . . . . . . . . . . . . 13 (𝜑 → (2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) = ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))))
179178breq1d 4633 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆)))
180 lemuldiv2 10864 . . . . . . . . . . . . . 14 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18188, 180mp3an3 1410 . . . . . . . . . . . . 13 (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ∈ ℝ ∧ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ∈ ℝ) → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
18261, 76, 181syl2anc 692 . . . . . . . . . . . 12 (𝜑 → ((2 · (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) ≤ ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
183176, 179, 1823bitr2d 296 . . . . . . . . . . 11 (𝜑 → ((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 ↔ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)))
184183biimpar 502 . . . . . . . . . 10 ((𝜑 ∧ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (((𝐴𝐷((⇝𝑡𝐽)‘𝐹)) + 𝑆) / 2)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
185175, 184syldan 487 . . . . . . . . 9 ((𝜑𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹))) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
186185ex 450 . . . . . . . 8 (𝜑 → (𝑆 < (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
18772, 186sylbird 250 . . . . . . 7 (𝜑 → (¬ (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆))
188187pm2.18d 124 . . . . . 6 (𝜑 → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
189188adantr 481 . . . . 5 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ 𝑆)
19095adantr 481 . . . . . . 7 ((𝜑𝑦𝑌) → 𝑅 ⊆ ℝ)
191101adantr 481 . . . . . . 7 ((𝜑𝑦𝑌) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
192 simpr 477 . . . . . . . . 9 ((𝜑𝑦𝑌) → 𝑦𝑌)
193 fvex 6168 . . . . . . . . 9 (𝑁‘(𝐴𝑀𝑦)) ∈ V
194 eqid 2621 . . . . . . . . . 10 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
195194elrnmpt1 5344 . . . . . . . . 9 ((𝑦𝑌 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ V) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
196192, 193, 195sylancl 693 . . . . . . . 8 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
197196, 16syl6eleqr 2709 . . . . . . 7 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅)
198 infrelb 10968 . . . . . . 7 ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤 ∧ (𝑁‘(𝐴𝑀𝑦)) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
199190, 191, 197, 198syl3anc 1323 . . . . . 6 ((𝜑𝑦𝑌) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀𝑦)))
20017, 199syl5eqbr 4658 . . . . 5 ((𝜑𝑦𝑌) → 𝑆 ≤ (𝑁‘(𝐴𝑀𝑦)))
20162, 64, 71, 189, 200letrd 10154 . . . 4 ((𝜑𝑦𝑌) → (𝐴𝐷((⇝𝑡𝐽)‘𝐹)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20257, 201eqbrtrrd 4647 . . 3 ((𝜑𝑦𝑌) → (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
203202ralrimiva 2962 . 2 (𝜑 → ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦)))
204 oveq2 6623 . . . . . 6 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝐴𝑀𝑥) = (𝐴𝑀((⇝𝑡𝐽)‘𝐹)))
205204fveq2d 6162 . . . . 5 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (𝑁‘(𝐴𝑀𝑥)) = (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))))
206205breq1d 4633 . . . 4 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → ((𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
207206ralbidv 2982 . . 3 (𝑥 = ((⇝𝑡𝐽)‘𝐹) → (∀𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)) ↔ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))))
208207rspcev 3299 . 2 ((((⇝𝑡𝐽)‘𝐹) ∈ 𝑌 ∧ ∀𝑦𝑌 (𝑁‘(𝐴𝑀((⇝𝑡𝐽)‘𝐹))) ≤ (𝑁‘(𝐴𝑀𝑦))) → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
20953, 203, 208syl2anc 692 1 (𝜑 → ∃𝑥𝑌𝑦𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wne 2790  wral 2908  wrex 2909  Vcvv 3190  cin 3559  wss 3560  c0 3897   class class class wbr 4623  cmpt 4683   × cxp 5082  ran crn 5085  cres 5086  Fun wfun 5851  wf 5853  cfv 5857  (class class class)co 6615  infcinf 8307  cr 9895  0cc0 9896  1c1 9897   + caddc 9899   · cmul 9901   < clt 10034  cle 10035  cmin 10226   / cdiv 10644  cn 10980  2c2 11030  0cn0 11252  cuz 11647  +crp 11792  cfl 12547  cexp 12816  t crest 16021  ∞Metcxmt 19671  Metcme 19672  MetOpencmopn 19676  Topctop 20638  TopOnctopon 20655  𝑡clm 20970  Hauscha 21052  NrmCVeccnv 27327  BaseSetcba 27329  𝑣 cnsb 27332  normCVcnmcv 27333  IndMetcims 27334  SubSpcss 27464  CPreHilOLDccphlo 27555  CBanccbn 27606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974  ax-addf 9975  ax-mulf 9976
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-iin 4495  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-oadd 7524  df-er 7702  df-map 7819  df-pm 7820  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-fi 8277  df-sup 8308  df-inf 8309  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-4 11041  df-n0 11253  df-z 11338  df-uz 11648  df-q 11749  df-rp 11793  df-xneg 11906  df-xadd 11907  df-xmul 11908  df-ico 12139  df-icc 12140  df-fl 12549  df-seq 12758  df-exp 12817  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-rest 16023  df-topgen 16044  df-psmet 19678  df-xmet 19679  df-met 19680  df-bl 19681  df-mopn 19682  df-fbas 19683  df-fg 19684  df-top 20639  df-topon 20656  df-bases 20690  df-cld 20763  df-ntr 20764  df-cls 20765  df-nei 20842  df-lm 20973  df-haus 21059  df-fil 21590  df-fm 21682  df-flim 21683  df-flf 21684  df-cfil 22993  df-cau 22994  df-cmet 22995  df-grpo 27235  df-gid 27236  df-ginv 27237  df-gdiv 27238  df-ablo 27287  df-vc 27302  df-nv 27335  df-va 27338  df-ba 27339  df-sm 27340  df-0v 27341  df-vs 27342  df-nmcv 27343  df-ims 27344  df-ssp 27465  df-ph 27556  df-cbn 27607
This theorem is referenced by:  minvecolem5  27625
  Copyright terms: Public domain W3C validator