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 
|- X = ( BaseSet ` U )
minveco.m 
|- M = ( -v ` U )
minveco.n 
|- N = ( normCV ` U )
minveco.y 
|- Y = ( BaseSet ` W )
minveco.u 
|- ( ph -> U e. CPreHilOLD )
minveco.w 
|- ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
minveco.a 
|- ( ph -> A e. X )
minveco.d 
|- D = ( IndMet ` U )
minveco.j 
|- J = ( MetOpen ` D )
minveco.r 
|- R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
minveco.s 
|- S = inf ( R , RR , < )
minveco.f 
|- ( ph -> F : NN --> Y )
minveco.1 
|- ( ( ph /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
Assertion minvecolem3 
|- ( ph -> F e. ( Cau ` D ) )

Proof

Step Hyp Ref Expression
1 minveco.x 
 |-  X = ( BaseSet ` U )
2 minveco.m 
 |-  M = ( -v ` U )
3 minveco.n 
 |-  N = ( normCV ` U )
4 minveco.y 
 |-  Y = ( BaseSet ` W )
5 minveco.u 
 |-  ( ph -> U e. CPreHilOLD )
6 minveco.w 
 |-  ( ph -> W e. ( ( SubSp ` U ) i^i CBan ) )
7 minveco.a 
 |-  ( ph -> A e. X )
8 minveco.d 
 |-  D = ( IndMet ` U )
9 minveco.j 
 |-  J = ( MetOpen ` D )
10 minveco.r 
 |-  R = ran ( y e. Y |-> ( N ` ( A M y ) ) )
11 minveco.s 
 |-  S = inf ( R , RR , < )
12 minveco.f 
 |-  ( ph -> F : NN --> Y )
13 minveco.1 
 |-  ( ( ph /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
14 4re 
 |-  4 e. RR
15 4pos 
 |-  0 < 4
16 14 15 elrpii 
 |-  4 e. RR+
17 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
18 2z 
 |-  2 e. ZZ
19 rpexpcl 
 |-  ( ( x e. RR+ /\ 2 e. ZZ ) -> ( x ^ 2 ) e. RR+ )
20 17 18 19 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( x ^ 2 ) e. RR+ )
21 rpdivcl 
 |-  ( ( 4 e. RR+ /\ ( x ^ 2 ) e. RR+ ) -> ( 4 / ( x ^ 2 ) ) e. RR+ )
22 16 20 21 sylancr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 4 / ( x ^ 2 ) ) e. RR+ )
23 rprege0 
 |-  ( ( 4 / ( x ^ 2 ) ) e. RR+ -> ( ( 4 / ( x ^ 2 ) ) e. RR /\ 0 <_ ( 4 / ( x ^ 2 ) ) ) )
24 flge0nn0 
 |-  ( ( ( 4 / ( x ^ 2 ) ) e. RR /\ 0 <_ ( 4 / ( x ^ 2 ) ) ) -> ( |_ ` ( 4 / ( x ^ 2 ) ) ) e. NN0 )
25 nn0p1nn 
 |-  ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) e. NN0 -> ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. NN )
26 22 23 24 25 4syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. NN )
27 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
28 1 8 imsmet 
 |-  ( U e. NrmCVec -> D e. ( Met ` X ) )
29 5 27 28 3syl 
 |-  ( ph -> D e. ( Met ` X ) )
30 29 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> D e. ( Met ` X ) )
31 5 27 syl 
 |-  ( ph -> U e. NrmCVec )
32 inss1 
 |-  ( ( SubSp ` U ) i^i CBan ) C_ ( SubSp ` U )
33 32 6 sselid 
 |-  ( ph -> W e. ( SubSp ` U ) )
34 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
35 1 4 34 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
36 31 33 35 syl2anc 
 |-  ( ph -> Y C_ X )
37 36 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> Y C_ X )
38 12 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> F : NN --> Y )
39 26 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. NN )
40 38 39 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. Y )
41 37 40 sseldd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. X )
42 eluznn 
 |-  ( ( ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> n e. NN )
43 26 42 sylan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> n e. NN )
44 38 43 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( F ` n ) e. Y )
45 37 44 sseldd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( F ` n ) e. X )
46 metcl 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. X /\ ( F ` n ) e. X ) -> ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) e. RR )
47 30 41 45 46 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) e. RR )
48 47 resqcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) ^ 2 ) e. RR )
49 39 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. RR+ )
50 49 rpreccld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. RR+ )
51 rpmulcl 
 |-  ( ( 4 e. RR+ /\ ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. RR+ ) -> ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) e. RR+ )
52 16 50 51 sylancr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) e. RR+ )
53 52 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) e. RR )
54 20 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( x ^ 2 ) e. RR+ )
55 54 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( x ^ 2 ) e. RR )
56 5 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> U e. CPreHilOLD )
57 6 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> W e. ( ( SubSp ` U ) i^i CBan ) )
58 7 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> A e. X )
59 26 nnrpd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. RR+ )
60 59 rpreccld 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. RR+ )
61 60 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. RR+ )
62 61 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. RR )
63 61 rpge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> 0 <_ ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) )
64 12 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> F : NN --> Y )
65 64 ffvelrnda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. NN ) -> ( F ` n ) e. Y )
66 43 65 syldan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( F ` n ) e. Y )
67 fveq2 
 |-  ( n = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( F ` n ) = ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) )
68 67 oveq2d 
 |-  ( n = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( A D ( F ` n ) ) = ( A D ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
69 68 oveq1d 
 |-  ( n = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( ( A D ( F ` n ) ) ^ 2 ) = ( ( A D ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) ^ 2 ) )
70 oveq2 
 |-  ( n = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( 1 / n ) = ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) )
71 70 oveq2d 
 |-  ( n = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( ( S ^ 2 ) + ( 1 / n ) ) = ( ( S ^ 2 ) + ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
72 69 71 breq12d 
 |-  ( n = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) <-> ( ( A D ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) ) )
73 13 ralrimiva 
 |-  ( ph -> A. n e. NN ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
74 73 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> A. n e. NN ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
75 72 74 39 rspcdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( A D ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
76 37 66 sseldd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( F ` n ) e. X )
77 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ ( F ` n ) e. X ) -> ( A D ( F ` n ) ) e. RR )
78 30 58 76 77 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( A D ( F ` n ) ) e. RR )
79 78 resqcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( A D ( F ` n ) ) ^ 2 ) e. RR )
80 1 2 3 4 5 6 7 8 9 10 minvecolem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
81 0re 
 |-  0 e. RR
82 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
83 82 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
84 83 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
85 81 84 mpan 
 |-  ( A. w e. R 0 <_ w -> E. x e. RR A. w e. R x <_ w )
86 85 3anim3i 
 |-  ( ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) -> ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) )
87 infrecl 
 |-  ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) -> inf ( R , RR , < ) e. RR )
88 80 86 87 3syl 
 |-  ( ph -> inf ( R , RR , < ) e. RR )
89 11 88 eqeltrid 
 |-  ( ph -> S e. RR )
90 89 resqcld 
 |-  ( ph -> ( S ^ 2 ) e. RR )
91 90 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( S ^ 2 ) e. RR )
92 43 nnrecred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / n ) e. RR )
93 91 92 readdcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( S ^ 2 ) + ( 1 / n ) ) e. RR )
94 91 62 readdcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( S ^ 2 ) + ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) e. RR )
95 13 adantlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
96 43 95 syldan 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
97 eluzle 
 |-  ( n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) -> ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) <_ n )
98 97 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) <_ n )
99 49 rpregt0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. RR /\ 0 < ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) )
100 nnre 
 |-  ( n e. NN -> n e. RR )
101 nngt0 
 |-  ( n e. NN -> 0 < n )
102 100 101 jca 
 |-  ( n e. NN -> ( n e. RR /\ 0 < n ) )
103 43 102 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( n e. RR /\ 0 < n ) )
104 lerec 
 |-  ( ( ( ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. RR /\ 0 < ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) /\ ( n e. RR /\ 0 < n ) ) -> ( ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) <_ n <-> ( 1 / n ) <_ ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
105 99 103 104 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) <_ n <-> ( 1 / n ) <_ ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
106 98 105 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / n ) <_ ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) )
107 92 62 91 106 leadd2dd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( S ^ 2 ) + ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
108 79 93 94 96 107 letrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
109 1 2 3 4 56 57 58 8 9 10 11 62 63 40 66 75 108 minvecolem2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) ^ 2 ) <_ ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) )
110 rpdivcl 
 |-  ( ( ( x ^ 2 ) e. RR+ /\ 4 e. RR+ ) -> ( ( x ^ 2 ) / 4 ) e. RR+ )
111 54 16 110 sylancl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( x ^ 2 ) / 4 ) e. RR+ )
112 rpcnne0 
 |-  ( ( x ^ 2 ) e. RR+ -> ( ( x ^ 2 ) e. CC /\ ( x ^ 2 ) =/= 0 ) )
113 54 112 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( x ^ 2 ) e. CC /\ ( x ^ 2 ) =/= 0 ) )
114 rpcnne0 
 |-  ( 4 e. RR+ -> ( 4 e. CC /\ 4 =/= 0 ) )
115 16 114 ax-mp 
 |-  ( 4 e. CC /\ 4 =/= 0 )
116 recdiv 
 |-  ( ( ( ( x ^ 2 ) e. CC /\ ( x ^ 2 ) =/= 0 ) /\ ( 4 e. CC /\ 4 =/= 0 ) ) -> ( 1 / ( ( x ^ 2 ) / 4 ) ) = ( 4 / ( x ^ 2 ) ) )
117 113 115 116 sylancl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / ( ( x ^ 2 ) / 4 ) ) = ( 4 / ( x ^ 2 ) ) )
118 22 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 4 / ( x ^ 2 ) ) e. RR+ )
119 118 rpred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 4 / ( x ^ 2 ) ) e. RR )
120 flltp1 
 |-  ( ( 4 / ( x ^ 2 ) ) e. RR -> ( 4 / ( x ^ 2 ) ) < ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) )
121 119 120 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 4 / ( x ^ 2 ) ) < ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) )
122 117 121 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / ( ( x ^ 2 ) / 4 ) ) < ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) )
123 111 49 122 ltrec1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) < ( ( x ^ 2 ) / 4 ) )
124 14 15 pm3.2i 
 |-  ( 4 e. RR /\ 0 < 4 )
125 ltmuldiv2 
 |-  ( ( ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. RR /\ ( x ^ 2 ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) < ( x ^ 2 ) <-> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) < ( ( x ^ 2 ) / 4 ) ) )
126 124 125 mp3an3 
 |-  ( ( ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. RR /\ ( x ^ 2 ) e. RR ) -> ( ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) < ( x ^ 2 ) <-> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) < ( ( x ^ 2 ) / 4 ) ) )
127 62 55 126 syl2anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) < ( x ^ 2 ) <-> ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) < ( ( x ^ 2 ) / 4 ) ) )
128 123 127 mpbird 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( 4 x. ( 1 / ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) < ( x ^ 2 ) )
129 48 53 55 109 128 lelttrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) ^ 2 ) < ( x ^ 2 ) )
130 metge0 
 |-  ( ( D e. ( Met ` X ) /\ ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) e. X /\ ( F ` n ) e. X ) -> 0 <_ ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) )
131 30 41 45 130 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> 0 <_ ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) )
132 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
133 132 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( x e. RR /\ 0 <_ x ) )
134 lt2sq 
 |-  ( ( ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) e. RR /\ 0 <_ ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) ) /\ ( x e. RR /\ 0 <_ x ) ) -> ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) < x <-> ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) ^ 2 ) < ( x ^ 2 ) ) )
135 47 131 133 134 syl21anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) < x <-> ( ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) ^ 2 ) < ( x ^ 2 ) ) )
136 129 135 mpbird 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ) -> ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) < x )
137 136 ralrimiva 
 |-  ( ( ph /\ x e. RR+ ) -> A. n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) < x )
138 fveq2 
 |-  ( j = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( ZZ>= ` j ) = ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) )
139 fveq2 
 |-  ( j = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( F ` j ) = ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) )
140 139 oveq1d 
 |-  ( j = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( ( F ` j ) D ( F ` n ) ) = ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) )
141 140 breq1d 
 |-  ( j = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( ( ( F ` j ) D ( F ` n ) ) < x <-> ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) < x ) )
142 138 141 raleqbidv 
 |-  ( j = ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) -> ( A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x <-> A. n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) < x ) )
143 142 rspcev 
 |-  ( ( ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) e. NN /\ A. n e. ( ZZ>= ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) ( ( F ` ( ( |_ ` ( 4 / ( x ^ 2 ) ) ) + 1 ) ) D ( F ` n ) ) < x ) -> E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x )
144 26 137 143 syl2anc 
 |-  ( ( ph /\ x e. RR+ ) -> E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x )
145 144 ralrimiva 
 |-  ( ph -> A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x )
146 nnuz 
 |-  NN = ( ZZ>= ` 1 )
147 1 8 imsxmet 
 |-  ( U e. NrmCVec -> D e. ( *Met ` X ) )
148 5 27 147 3syl 
 |-  ( ph -> D e. ( *Met ` X ) )
149 1zzd 
 |-  ( ph -> 1 e. ZZ )
150 eqidd 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) = ( F ` n ) )
151 eqidd 
 |-  ( ( ph /\ j e. NN ) -> ( F ` j ) = ( F ` j ) )
152 12 36 fssd 
 |-  ( ph -> F : NN --> X )
153 146 148 149 150 151 152 iscauf 
 |-  ( ph -> ( F e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. n e. ( ZZ>= ` j ) ( ( F ` j ) D ( F ` n ) ) < x ) )
154 145 153 mpbird 
 |-  ( ph -> F e. ( Cau ` D ) )