Metamath Proof Explorer

Theorem minvecolem3

Description: Lemma for minveco . The sequence formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-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 / 𝑛 ) ) )
Assertion minvecolem3 ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )

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 4re ⊢ 4 ∈ ℝ
15 4pos ⊢ 0 < 4
16 14 15 elrpii ⊢ 4 ∈ ℝ+
17 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
18 2z ⊢ 2 ∈ ℤ
19 rpexpcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
20 17 18 19 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
21 rpdivcl ⊢ ( ( 4 ∈ ℝ+ ∧ ( 𝑥 ↑ 2 ) ∈ ℝ+ ) → ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ+ )
22 16 20 21 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ+ )
23 rprege0 ⊢ ( ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ+ → ( ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( 4 / ( 𝑥 ↑ 2 ) ) ) )
24 flge0nn0 ⊢ ( ( ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ ∧ 0 ≤ ( 4 / ( 𝑥 ↑ 2 ) ) ) → ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) ∈ ℕ0 )
25 nn0p1nn ⊢ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℕ )
26 22 23 24 25 4syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℕ )
27 phnv ⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
28 1 8 imsmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝑋 ) )
29 5 27 28 3syl ⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
30 29 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝐷 ∈ ( Met ‘ 𝑋 ) )
31 5 27 syl ⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
32 inss1 ⊢ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ⊆ ( SubSp ‘ 𝑈 )
33 32 6 sselid ⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
34 eqid ⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
35 1 4 34 sspba ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
36 31 33 35 syl2anc ⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
37 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝑌 ⊆ 𝑋 )
38 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝐹 : ℕ ⟶ 𝑌 )
39 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℕ )
40 38 39 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ 𝑌 )
41 37 40 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ 𝑋 )
42 eluznn ⊢ ( ( ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℕ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝑛 ∈ ℕ )
43 26 42 sylan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝑛 ∈ ℕ )
44 38 43 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑌 )
45 37 44 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
46 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) → ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
47 30 41 45 46 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
48 47 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ∈ ℝ )
49 39 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℝ+ )
50 49 rpreccld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ ℝ+ )
51 rpmulcl ⊢ ( ( 4 ∈ ℝ+ ∧ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ ℝ+ ) → ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ∈ ℝ+ )
52 16 50 51 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ∈ ℝ+ )
53 52 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ∈ ℝ )
54 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ+ )
55 54 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝑥 ↑ 2 ) ∈ ℝ )
56 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝑈 ∈ CPreHilOLD )
57 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
58 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 𝐴 ∈ 𝑋 )
59 26 nnrpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℝ+ )
60 59 rpreccld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ ℝ+ )
61 60 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ ℝ+ )
62 61 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ ℝ )
63 61 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 0 ≤ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) )
64 12 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐹 : ℕ ⟶ 𝑌 )
65 64 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑌 )
66 43 65 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑌 )
67 fveq2 ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) )
68 67 oveq2d ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) = ( 𝐴 𝐷 ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
69 68 oveq1d ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) = ( ( 𝐴 𝐷 ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ↑ 2 ) )
70 oveq2 ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( 1 / 𝑛 ) = ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) )
71 70 oveq2d ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) = ( ( 𝑆 ↑ 2 ) + ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
72 69 71 breq12d ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ↔ ( ( 𝐴 𝐷 ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ) )
73 13 ralrimiva ⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
74 73 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ∀ 𝑛 ∈ ℕ ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
75 72 74 39 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
76 37 66 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 )
77 metcl ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
78 30 58 76 77 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ )
79 78 resqcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ∈ ℝ )
80 1 2 3 4 5 6 7 8 9 10 minvecolem1 ⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
81 0re ⊢ 0 ∈ ℝ
82 breq1 ⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
83 82 ralbidv ⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
84 83 rspcev ⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
85 81 84 mpan ⊢ ( ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
86 85 3anim3i ⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) )
87 infrecl ⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
88 80 86 87 3syl ⊢ ( 𝜑 → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
89 11 88 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ℝ )
90 89 resqcld ⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℝ )
91 90 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝑆 ↑ 2 ) ∈ ℝ )
92 43 nnrecred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
93 91 92 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ∈ ℝ )
94 91 62 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝑆 ↑ 2 ) + ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) ∈ ℝ )
95 13 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
96 43 95 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) )
97 eluzle ⊢ ( 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) → ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ≤ 𝑛 )
98 97 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ≤ 𝑛 )
99 49 rpregt0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℝ ∧ 0 < ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) )
100 nnre ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ )
101 nngt0 ⊢ ( 𝑛 ∈ ℕ → 0 < 𝑛 )
102 100 101 jca ⊢ ( 𝑛 ∈ ℕ → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
103 43 102 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) )
104 lerec ⊢ ( ( ( ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℝ ∧ 0 < ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∧ ( 𝑛 ∈ ℝ ∧ 0 < 𝑛 ) ) → ( ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ≤ 𝑛 ↔ ( 1 / 𝑛 ) ≤ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
105 99 103 104 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ≤ 𝑛 ↔ ( 1 / 𝑛 ) ≤ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
106 98 105 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / 𝑛 ) ≤ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) )
107 92 62 91 106 leadd2dd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝑆 ↑ 2 ) + ( 1 / 𝑛 ) ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
108 79 93 94 96 107 letrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝐴 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
109 1 2 3 4 56 57 58 8 9 10 11 62 63 40 66 75 108 minvecolem2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) ≤ ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) )
110 rpdivcl ⊢ ( ( ( 𝑥 ↑ 2 ) ∈ ℝ+ ∧ 4 ∈ ℝ+ ) → ( ( 𝑥 ↑ 2 ) / 4 ) ∈ ℝ+ )
111 54 16 110 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝑥 ↑ 2 ) / 4 ) ∈ ℝ+ )
112 rpcnne0 ⊢ ( ( 𝑥 ↑ 2 ) ∈ ℝ+ → ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ≠ 0 ) )
113 54 112 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ≠ 0 ) )
114 rpcnne0 ⊢ ( 4 ∈ ℝ+ → ( 4 ∈ ℂ ∧ 4 ≠ 0 ) )
115 16 114 ax-mp ⊢ ( 4 ∈ ℂ ∧ 4 ≠ 0 )
116 recdiv ⊢ ( ( ( ( 𝑥 ↑ 2 ) ∈ ℂ ∧ ( 𝑥 ↑ 2 ) ≠ 0 ) ∧ ( 4 ∈ ℂ ∧ 4 ≠ 0 ) ) → ( 1 / ( ( 𝑥 ↑ 2 ) / 4 ) ) = ( 4 / ( 𝑥 ↑ 2 ) ) )
117 113 115 116 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / ( ( 𝑥 ↑ 2 ) / 4 ) ) = ( 4 / ( 𝑥 ↑ 2 ) ) )
118 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ+ )
119 118 rpred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ )
120 flltp1 ⊢ ( ( 4 / ( 𝑥 ↑ 2 ) ) ∈ ℝ → ( 4 / ( 𝑥 ↑ 2 ) ) < ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) )
121 119 120 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 4 / ( 𝑥 ↑ 2 ) ) < ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) )
122 117 121 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / ( ( 𝑥 ↑ 2 ) / 4 ) ) < ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) )
123 111 49 122 ltrec1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) < ( ( 𝑥 ↑ 2 ) / 4 ) )
124 14 15 pm3.2i ⊢ ( 4 ∈ ℝ ∧ 0 < 4 )
125 ltmuldiv2 ⊢ ( ( ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ ℝ ∧ ( 𝑥 ↑ 2 ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) < ( 𝑥 ↑ 2 ) ↔ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) < ( ( 𝑥 ↑ 2 ) / 4 ) ) )
126 124 125 mp3an3 ⊢ ( ( ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ ℝ ∧ ( 𝑥 ↑ 2 ) ∈ ℝ ) → ( ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) < ( 𝑥 ↑ 2 ) ↔ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) < ( ( 𝑥 ↑ 2 ) / 4 ) ) )
127 62 55 126 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) < ( 𝑥 ↑ 2 ) ↔ ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) < ( ( 𝑥 ↑ 2 ) / 4 ) ) )
128 123 127 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 4 · ( 1 / ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) < ( 𝑥 ↑ 2 ) )
129 48 53 55 109 128 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) < ( 𝑥 ↑ 2 ) )
130 metge0 ⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ∈ 𝑋 ∧ ( 𝐹 ‘ 𝑛 ) ∈ 𝑋 ) → 0 ≤ ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
131 30 41 45 130 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → 0 ≤ ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
132 rprege0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
133 132 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
134 lt2sq ⊢ ( ( ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ∈ ℝ ∧ 0 ≤ ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ) ∧ ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) ) → ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ↔ ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) < ( 𝑥 ↑ 2 ) ) )
135 47 131 133 134 syl21anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ↔ ( ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) ↑ 2 ) < ( 𝑥 ↑ 2 ) ) )
136 129 135 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ) → ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 )
137 136 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 )
138 fveq2 ⊢ ( 𝑗 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( ℤ≥ ‘ 𝑗 ) = ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) )
139 fveq2 ⊢ ( 𝑗 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) )
140 139 oveq1d ⊢ ( 𝑗 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) = ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) )
141 140 breq1d ⊢ ( 𝑗 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ↔ ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ) )
142 138 141 raleqbidv ⊢ ( 𝑗 = ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ↔ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ) )
143 142 rspcev ⊢ ( ( ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ∈ ℕ ∧ ∀ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) ( ( 𝐹 ‘ ( ( ⌊ ‘ ( 4 / ( 𝑥 ↑ 2 ) ) ) + 1 ) ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ) → ∃ 𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 )
144 26 137 143 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 )
145 144 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 )
146 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
147 1 8 imsxmet ⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
148 5 27 147 3syl ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
149 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
150 eqidd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑛 ) )
151 eqidd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑗 ) )
152 12 36 fssd ⊢ ( 𝜑 → 𝐹 : ℕ ⟶ 𝑋 )
153 146 148 149 150 151 152 iscauf ⊢ ( 𝜑 → ( 𝐹 ∈ ( Cau ‘ 𝐷 ) ↔ ∀ 𝑥 ∈ ℝ+ ∃ 𝑗 ∈ ℕ ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( ( 𝐹 ‘ 𝑗 ) 𝐷 ( 𝐹 ‘ 𝑛 ) ) < 𝑥 ) )
154 145 153 mpbird ⊢ ( 𝜑 → 𝐹 ∈ ( Cau ‘ 𝐷 ) )