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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 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	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ℤ≥ ‘ ( ( ⌊ ‘ ( 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	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ℕ ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝑌 )
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 ‘ 𝐷 ) )