Metamath Proof Explorer

Theorem minvecolem4

Description: Lemma for minveco . The convergent point of the Cauchy sequence F attains the minimum distance, and so is closer to A than any other point in Y . (Contributed by Mario Carneiro, 7-May-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

Ref Expression
Hypotheses 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 minvecolem4 ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 minveco.x ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 minveco.m ⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3 minveco.n ⊢ 𝑁 = ( normCV ‘ 𝑈 )
4 minveco.y ⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5 minveco.u ⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6 minveco.w ⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7 minveco.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8 minveco.d ⊢ 𝐷 = ( IndMet ‘ 𝑈 )
9 minveco.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
10 minveco.r ⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11 minveco.s ⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
12 minveco.f ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑌 )
13 minveco.1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
14 minveco.t ⊢ 𝑇 = ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) )
15 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
16 1 8 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
17 5 15 16 3syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
18 9 methaus ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Haus )
19 lmfun ⊢ ( 𝐽 ∈ Haus → Fun ( ⇝𝑡 ‘ 𝐽 ) )
20 17 18 19 3syl ⊢ ( 𝜑 → Fun ( ⇝𝑡 ‘ 𝐽 ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4a ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
22 eqid ⊢ ( 𝐽 ↾t 𝑌 ) = ( 𝐽 ↾t 𝑌 )
23 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
24 4 fvexi ⊢ 𝑌 ∈ V
25 24 a1i ⊢ ( 𝜑 → 𝑌 ∈ V )
26 5 15 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
27 9 mopntop ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐽 ∈ Top )
28 26 16 27 3syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
29 elin ⊢ ( 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ↔ ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
30 6 29 sylib ⊢ ( 𝜑 → ( 𝑊 ∈ ( SubSp ‘ 𝑈 ) ∧ 𝑊 ∈ CBan ) )
31 30 simpld ⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
32 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
33 1 4 32 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
34 26 31 33 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
35 xmetres2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
36 17 34 35 syl2anc ⊢ ( 𝜑 → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) )
37 eqid ⊢ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) )
38 37 mopntopon ⊢ ( ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ 𝑌 ) → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) )
39 36 38 syl ⊢ ( 𝜑 → ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) )
40 lmcl ⊢ ( ( ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) → ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ∈ 𝑌 )
41 39 21 40 syl2anc ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ∈ 𝑌 )
42 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
43 22 23 25 28 41 42 12 lmss ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
44 eqid ⊢ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) )
45 44 9 37 metrest ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
46 17 34 45 syl2anc ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑌 ) = ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) )
47 46 fveq2d ⊢ ( 𝜑 → ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) = ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) )
48 47 breqd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ ( 𝐽 ↾t 𝑌 ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
49 43 48 bitrd ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ↔ 𝐹 ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
50 21 49 mpbird ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
51 funbrfv ⊢ ( Fun ( ⇝𝑡 ‘ 𝐽 ) → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) ) )
52 20 50 51 sylc ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ) ) ‘ 𝐹 ) )
53 52 41 eqeltrd ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑌 )
54 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4b ⊢ ( 𝜑 → ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 )
55 1 2 3 8 imsdval ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) )
56 26 7 54 55 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) )
58 1 8 imsmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝑋 ) )
59 5 15 58 3syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
60 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ∈ ℝ )
61 59 7 54 60 syl3anc ⊢ ( 𝜑 → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ∈ ℝ )
62 61 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ∈ ℝ )
63 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4c ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑆 ∈ ℝ )
65 26 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑈 ∈ NrmCVec )
66 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝐴 ∈ 𝑋 )
67 34 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
68 1 2 nvmcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
69 65 66 67 68 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 )
70 1 3 nvcl ⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 𝑦 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
71 65 69 70 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ℝ )
72 63 61 ltnled ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ↔ ¬ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 ) )
73 eqid ⊢ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) = ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) )
74 17 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
75 61 63 readdcld ⊢ ( 𝜑 → ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ∈ ℝ )
76 75 rehalfcld ⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ )
77 76 resqcld ⊢ ( 𝜑 → ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ∈ ℝ )
78 63 resqcld ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℝ )
79 77 78 resubcld ⊢ ( 𝜑 → ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ )
80 79 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ )
81 63 61 63 ltadd1d ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ↔ ( 𝑆 + 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ) )
82 63 recnd ⊢ ( 𝜑 → 𝑆 ∈ ℂ )
83 82 2timesd ⊢ ( 𝜑 → ( 2 · 𝑆 ) = ( 𝑆 + 𝑆 ) )
84 83 breq1d ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ↔ ( 𝑆 + 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ) )
85 2re ⊢ 2 ∈ ℝ
86 2pos ⊢ 0 < 2
87 85 86 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
88 87 a1i ⊢ ( 𝜑 → ( 2 ∈ ℝ ∧ 0 < 2 ) )
89 ltmuldiv2 ⊢ ( ( 𝑆 ∈ ℝ ∧ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
90 63 75 88 89 syl3anc ⊢ ( 𝜑 → ( ( 2 · 𝑆 ) < ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
91 81 84 90 3bitr2d ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ↔ 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
92 1 2 3 4 5 6 7 8 9 10 minvecolem1 ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
93 92 simp3d ⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
94 92 simp1d ⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
95 92 simp2d ⊢ ( 𝜑 → 𝑅 ≠ ∅ )
96 0re ⊢ 0 ∈ ℝ
97 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
98 97 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
99 98 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
100 96 93 99 sylancr ⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
101 96 a1i ⊢ ( 𝜑 → 0 ∈ ℝ )
102 infregelb ⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
103 94 95 100 101 102 syl31anc ⊢ ( 𝜑 → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
104 93 103 mpbird ⊢ ( 𝜑 → 0 ≤ inf ( 𝑅 , ℝ , < ) )
105 104 11 breqtrrdi ⊢ ( 𝜑 → 0 ≤ 𝑆 )
106 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) )
107 59 7 54 106 syl3anc ⊢ ( 𝜑 → 0 ≤ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) )
108 61 63 107 105 addge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) )
109 divge0 ⊢ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ∈ ℝ ∧ 0 ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ) ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → 0 ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) )
110 75 108 88 109 syl21anc ⊢ ( 𝜑 → 0 ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) )
111 63 76 105 110 lt2sqd ⊢ ( 𝜑 → ( 𝑆 < ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↔ ( 𝑆 ↑ 2 ) < ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ) )
112 78 77 posdifd ⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) < ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ↔ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) )
113 91 111 112 3bitrd ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ↔ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) )
114 113 biimpa ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) )
115 80 114 elrpd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ+ )
116 115 rpreccld ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) ∈ ℝ+ )
117 14 116 eqeltrid ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → 𝑇 ∈ ℝ+ )
118 117 rprege0d ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ) )
119 flge0nn0 ⊢ ( ( 𝑇 ∈ ℝ ∧ 0 ≤ 𝑇 ) → ( ⌊ ‘ 𝑇 ) ∈ ℕ0 )
120 nn0p1nn ⊢ ( ( ⌊ ‘ 𝑇 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑇 ) + 1 ) ∈ ℕ )
121 118 119 120 3syl ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( ( ⌊ ‘ 𝑇 ) + 1 ) ∈ ℕ )
122 121 nnzd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( ( ⌊ ‘ 𝑇 ) + 1 ) ∈ ℤ )
123 50 52 breqtrrd ⊢ ( 𝜑 → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) )
124 123 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → 𝐹 ( ⇝𝑡 ‘ 𝐽 ) ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) )
125 7 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → 𝐴 ∈ 𝑋 )
126 76 adantr ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ )
127 126 rexrd ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ* )
128 simpll ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝜑 )
129 eluznn ⊢ ( ( ( ( ⌊ ‘ 𝑇 ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑛 ∈ ℕ )
130 121 129 sylan ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑛 ∈ ℕ )
131 59 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
132 7 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 𝐴 ∈ 𝑋 )
133 12 34 fssd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
134 133 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
135 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
136 131 132 134 135 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
137 128 130 136 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
138 137 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ∈ ℝ )
139 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑆 ∈ ℝ )
140 139 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( 𝑆 ↑ 2 ) ∈ ℝ )
141 130 nnrecred ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
142 140 141 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
143 77 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ∈ ℝ )
144 128 130 13 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
145 117 adantr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑇 ∈ ℝ+ )
146 145 rpred ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑇 ∈ ℝ )
147 reflcl ⊢ ( 𝑇 ∈ ℝ → ( ⌊ ‘ 𝑇 ) ∈ ℝ )
148 peano2re ⊢ ( ( ⌊ ‘ 𝑇 ) ∈ ℝ → ( ( ⌊ ‘ 𝑇 ) + 1 ) ∈ ℝ )
149 146 147 148 3syl ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( ⌊ ‘ 𝑇 ) + 1 ) ∈ ℝ )
150 130 nnred ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑛 ∈ ℝ )
151 fllep1 ⊢ ( 𝑇 ∈ ℝ → 𝑇 ≤ ( ( ⌊ ‘ 𝑇 ) + 1 ) )
152 146 151 syl ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑇 ≤ ( ( ⌊ ‘ 𝑇 ) + 1 ) )
153 eluzle ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) → ( ( ⌊ ‘ 𝑇 ) + 1 ) ≤ 𝑛 )
154 153 adantl ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( ⌊ ‘ 𝑇 ) + 1 ) ≤ 𝑛 )
155 146 149 150 152 154 letrd ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 𝑇 ≤ 𝑛 )
156 14 155 eqbrtrrid ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) ≤ 𝑛 )
157 1red ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 1 ∈ ℝ )
158 79 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ )
159 114 adantr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) )
160 130 nngt0d ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 0 < 𝑛 )
161 lediv23 ⊢ ( ( 1 ∈ ℝ ∧ ( ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ∈ ℝ ∧ 0 < ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) ≤ 𝑛 ↔ ( 1 / 𝑛 ) ≤ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) )
162 157 158 159 150 160 161 syl122anc ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( 1 / ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) ≤ 𝑛 ↔ ( 1 / 𝑛 ) ≤ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) )
163 156 162 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( 1 / 𝑛 ) ≤ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) )
164 140 141 143 leaddsub2d ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ↔ ( 1 / 𝑛 ) ≤ ( ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) − ( 𝑆 ↑ 2 ) ) ) )
165 163 164 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) )
166 138 142 143 144 165 letrd ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) )
167 76 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ∈ ℝ )
168 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) → 0 ≤ ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
169 131 132 134 168 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → 0 ≤ ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
170 128 130 169 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 0 ≤ ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
171 110 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → 0 ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) )
172 137 167 170 171 le2sqd ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↔ ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ↑ 2 ) ) )
173 166 172 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ 𝑇 ) + 1 ) ) ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) )
174 73 9 74 122 124 125 127 173 lmle ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) )
175 61 63 61 leadd2d ⊢ ( 𝜑 → ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 ↔ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ) )
176 61 recnd ⊢ ( 𝜑 → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ∈ ℂ )
177 176 2timesd ⊢ ( 𝜑 → ( 2 · ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) = ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) )
178 177 breq1d ⊢ ( 𝜑 → ( ( 2 · ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ↔ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ) )
179 lemuldiv2 ⊢ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ∈ ℝ ∧ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ↔ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
180 87 179 mp3an3 ⊢ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ∈ ℝ ∧ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ∈ ℝ ) → ( ( 2 · ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ↔ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
181 61 75 180 syl2anc ⊢ ( 𝜑 → ( ( 2 · ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) ↔ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
182 175 178 181 3bitr2d ⊢ ( 𝜑 → ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 ↔ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) )
183 182 biimpar ⊢ ( ( 𝜑 ∧ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ ( ( ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) + 𝑆 ) / 2 ) ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 )
184 174 183 syldan ⊢ ( ( 𝜑 ∧ 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 )
185 184 ex ⊢ ( 𝜑 → ( 𝑆 < ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 ) )
186 72 185 sylbird ⊢ ( 𝜑 → ( ¬ ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 ) )
187 186 pm2.18d ⊢ ( 𝜑 → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 )
188 187 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ 𝑆 )
189 94 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑅 ⊆ ℝ )
190 100 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
191 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑌 )
192 fvex ⊢ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
193 eqid ⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
194 193 elrnmpt1 ⊢ ( ( 𝑦 ∈ 𝑌 ∧ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
195 191 192 194 sylancl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
196 195 10 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ 𝑅 )
197 infrelb ⊢ ( ( 𝑅 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ 𝑅 ) → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
198 189 190 196 197 syl3anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
199 11 198 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → 𝑆 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
200 62 64 71 188 199 letrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝐴 𝐷 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
201 57 200 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
202 201 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
203 oveq2 ⊢ ( 𝑥 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) → ( 𝐴 𝑀 𝑥 ) = ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) )
204 203 fveq2d ⊢ ( 𝑥 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) )
205 204 breq1d ⊢ ( 𝑥 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) → ( ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
206 205 ralbidv ⊢ ( 𝑥 = ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) → ( ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
207 206 rspcev ⊢ ( ( ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ∈ 𝑌 ∧ ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 ( ( ⇝𝑡 ‘ 𝐽 ) ‘ 𝐹 ) ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
208 53 202 207 syl2anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑌 ∀ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 𝑥 ) ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )