This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem minvecolem5

Description: Lemma for minveco . Discharge the assumption about the sequence F by applying countable choice ax-cc . (Contributed by Mario Carneiro, 9-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 , < )
Assertion minvecolem5 
|- ( ph -> E. x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )

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 nnrecgt0 
 |-  ( n e. NN -> 0 < ( 1 / n ) )
13 12 adantl 
 |-  ( ( ph /\ n e. NN ) -> 0 < ( 1 / n ) )
14 nnrecre 
 |-  ( n e. NN -> ( 1 / n ) e. RR )
15 14 adantl 
 |-  ( ( ph /\ n e. NN ) -> ( 1 / n ) e. RR )
16 1 2 3 4 5 6 7 8 9 10 minvecolem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
17 16 adantr 
 |-  ( ( ph /\ n e. NN ) -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
18 17 simp1d 
 |-  ( ( ph /\ n e. NN ) -> R C_ RR )
19 17 simp2d 
 |-  ( ( ph /\ n e. NN ) -> R =/= (/) )
20 0re 
 |-  0 e. RR
21 17 simp3d 
 |-  ( ( ph /\ n e. NN ) -> A. w e. R 0 <_ w )
22 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
23 22 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
24 23 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
25 20 21 24 sylancr 
 |-  ( ( ph /\ n e. NN ) -> E. x e. RR A. w e. R x <_ w )
26 infrecl 
 |-  ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) -> inf ( R , RR , < ) e. RR )
27 18 19 25 26 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> inf ( R , RR , < ) e. RR )
28 11 27 eqeltrid 
 |-  ( ( ph /\ n e. NN ) -> S e. RR )
29 28 resqcld 
 |-  ( ( ph /\ n e. NN ) -> ( S ^ 2 ) e. RR )
30 15 29 ltaddposd 
 |-  ( ( ph /\ n e. NN ) -> ( 0 < ( 1 / n ) <-> ( S ^ 2 ) < ( ( S ^ 2 ) + ( 1 / n ) ) ) )
31 13 30 mpbid 
 |-  ( ( ph /\ n e. NN ) -> ( S ^ 2 ) < ( ( S ^ 2 ) + ( 1 / n ) ) )
32 29 15 readdcld 
 |-  ( ( ph /\ n e. NN ) -> ( ( S ^ 2 ) + ( 1 / n ) ) e. RR )
33 28 sqge0d 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( S ^ 2 ) )
34 29 15 33 13 addgegt0d 
 |-  ( ( ph /\ n e. NN ) -> 0 < ( ( S ^ 2 ) + ( 1 / n ) ) )
35 32 34 elrpd 
 |-  ( ( ph /\ n e. NN ) -> ( ( S ^ 2 ) + ( 1 / n ) ) e. RR+ )
36 35 rpge0d 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
37 resqrtth 
 |-  ( ( ( ( S ^ 2 ) + ( 1 / n ) ) e. RR /\ 0 <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) ^ 2 ) = ( ( S ^ 2 ) + ( 1 / n ) ) )
38 32 36 37 syl2anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) ^ 2 ) = ( ( S ^ 2 ) + ( 1 / n ) ) )
39 31 38 breqtrrd 
 |-  ( ( ph /\ n e. NN ) -> ( S ^ 2 ) < ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) ^ 2 ) )
40 35 rpsqrtcld 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) e. RR+ )
41 40 rpred 
 |-  ( ( ph /\ n e. NN ) -> ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) e. RR )
42 0red 
 |-  ( ( ph /\ n e. NN ) -> 0 e. RR )
43 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ 0 e. RR ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
44 18 19 25 42 43 syl31anc 
 |-  ( ( ph /\ n e. NN ) -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
45 21 44 mpbird 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ inf ( R , RR , < ) )
46 45 11 breqtrrdi 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ S )
47 32 36 sqrtge0d 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) )
48 28 41 46 47 lt2sqd 
 |-  ( ( ph /\ n e. NN ) -> ( S < ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <-> ( S ^ 2 ) < ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) ^ 2 ) ) )
49 39 48 mpbird 
 |-  ( ( ph /\ n e. NN ) -> S < ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) )
50 28 41 ltnled 
 |-  ( ( ph /\ n e. NN ) -> ( S < ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <-> -. ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ S ) )
51 49 50 mpbid 
 |-  ( ( ph /\ n e. NN ) -> -. ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ S )
52 11 breq2i 
 |-  ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ S <-> ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ inf ( R , RR , < ) )
53 infregelb 
 |-  ( ( ( R C_ RR /\ R =/= (/) /\ E. x e. RR A. w e. R x <_ w ) /\ ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) e. RR ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w ) )
54 18 19 25 41 53 syl31anc 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ inf ( R , RR , < ) <-> A. w e. R ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w ) )
55 52 54 bitrid 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ S <-> A. w e. R ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w ) )
56 10 raleqi 
 |-  ( A. w e. R ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w <-> A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w )
57 fvex 
 |-  ( N ` ( A M y ) ) e. _V
58 57 rgenw 
 |-  A. y e. Y ( N ` ( A M y ) ) e. _V
59 eqid 
 |-  ( y e. Y |-> ( N ` ( A M y ) ) ) = ( y e. Y |-> ( N ` ( A M y ) ) )
60 breq2 
 |-  ( w = ( N ` ( A M y ) ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w <-> ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) ) )
61 59 60 ralrnmptw 
 |-  ( A. y e. Y ( N ` ( A M y ) ) e. _V -> ( A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) ) )
62 58 61 ax-mp 
 |-  ( A. w e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) )
63 56 62 bitri 
 |-  ( A. w e. R ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ w <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) )
64 55 63 bitrdi 
 |-  ( ( ph /\ n e. NN ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ S <-> A. y e. Y ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) ) )
65 51 64 mtbid 
 |-  ( ( ph /\ n e. NN ) -> -. A. y e. Y ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) )
66 rexnal 
 |-  ( E. y e. Y -. ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) <-> -. A. y e. Y ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) )
67 65 66 sylibr 
 |-  ( ( ph /\ n e. NN ) -> E. y e. Y -. ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) )
68 32 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( S ^ 2 ) + ( 1 / n ) ) e. RR )
69 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
70 5 69 syl 
 |-  ( ph -> U e. NrmCVec )
71 70 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> U e. NrmCVec )
72 7 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> A e. X )
73 inss1 
 |-  ( ( SubSp ` U ) i^i CBan ) C_ ( SubSp ` U )
74 73 6 sselid 
 |-  ( ph -> W e. ( SubSp ` U ) )
75 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
76 1 4 75 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
77 70 74 76 syl2anc 
 |-  ( ph -> Y C_ X )
78 77 adantr 
 |-  ( ( ph /\ n e. NN ) -> Y C_ X )
79 78 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> y e. X )
80 1 2 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ y e. X ) -> ( A M y ) e. X )
81 71 72 79 80 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( A M y ) e. X )
82 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ ( A M y ) e. X ) -> ( N ` ( A M y ) ) e. RR )
83 71 81 82 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( N ` ( A M y ) ) e. RR )
84 83 resqcld 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( N ` ( A M y ) ) ^ 2 ) e. RR )
85 68 84 letrid 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( N ` ( A M y ) ) ^ 2 ) \/ ( ( N ` ( A M y ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
86 85 ord 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( -. ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( N ` ( A M y ) ) ^ 2 ) -> ( ( N ` ( A M y ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
87 41 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) e. RR )
88 47 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> 0 <_ ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) )
89 1 3 nvge0 
 |-  ( ( U e. NrmCVec /\ ( A M y ) e. X ) -> 0 <_ ( N ` ( A M y ) ) )
90 71 81 89 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> 0 <_ ( N ` ( A M y ) ) )
91 87 83 88 90 le2sqd 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) <-> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) ^ 2 ) <_ ( ( N ` ( A M y ) ) ^ 2 ) ) )
92 38 adantr 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) ^ 2 ) = ( ( S ^ 2 ) + ( 1 / n ) ) )
93 92 breq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) ^ 2 ) <_ ( ( N ` ( A M y ) ) ^ 2 ) <-> ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( N ` ( A M y ) ) ^ 2 ) ) )
94 91 93 bitrd 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) <-> ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( N ` ( A M y ) ) ^ 2 ) ) )
95 94 notbid 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( -. ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) <-> -. ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( N ` ( A M y ) ) ^ 2 ) ) )
96 1 2 3 8 imsdval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ y e. X ) -> ( A D y ) = ( N ` ( A M y ) ) )
97 71 72 79 96 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( A D y ) = ( N ` ( A M y ) ) )
98 97 oveq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( A D y ) ^ 2 ) = ( ( N ` ( A M y ) ) ^ 2 ) )
99 98 breq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) <-> ( ( N ` ( A M y ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
100 86 95 99 3imtr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ y e. Y ) -> ( -. ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) -> ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
101 100 reximdva 
 |-  ( ( ph /\ n e. NN ) -> ( E. y e. Y -. ( sqrt ` ( ( S ^ 2 ) + ( 1 / n ) ) ) <_ ( N ` ( A M y ) ) -> E. y e. Y ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
102 67 101 mpd 
 |-  ( ( ph /\ n e. NN ) -> E. y e. Y ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
103 102 ralrimiva 
 |-  ( ph -> A. n e. NN E. y e. Y ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
104 4 fvexi 
 |-  Y e. _V
105 nnenom 
 |-  NN ~~ _om
106 oveq2 
 |-  ( y = ( f ` n ) -> ( A D y ) = ( A D ( f ` n ) ) )
107 106 oveq1d 
 |-  ( y = ( f ` n ) -> ( ( A D y ) ^ 2 ) = ( ( A D ( f ` n ) ) ^ 2 ) )
108 107 breq1d 
 |-  ( y = ( f ` n ) -> ( ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) <-> ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
109 104 105 108 axcc4 
 |-  ( A. n e. NN E. y e. Y ( ( A D y ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) -> E. f ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
110 103 109 syl 
 |-  ( ph -> E. f ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) )
111 5 adantr 
 |-  ( ( ph /\ ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) ) -> U e. CPreHilOLD )
112 6 adantr 
 |-  ( ( ph /\ ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) ) -> W e. ( ( SubSp ` U ) i^i CBan ) )
113 7 adantr 
 |-  ( ( ph /\ ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) ) -> A e. X )
114 simprl 
 |-  ( ( ph /\ ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) ) -> f : NN --> Y )
115 simprr 
 |-  ( ( ph /\ ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) ) -> A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
116 fveq2 
 |-  ( n = k -> ( f ` n ) = ( f ` k ) )
117 116 oveq2d 
 |-  ( n = k -> ( A D ( f ` n ) ) = ( A D ( f ` k ) ) )
118 117 oveq1d 
 |-  ( n = k -> ( ( A D ( f ` n ) ) ^ 2 ) = ( ( A D ( f ` k ) ) ^ 2 ) )
119 oveq2 
 |-  ( n = k -> ( 1 / n ) = ( 1 / k ) )
120 119 oveq2d 
 |-  ( n = k -> ( ( S ^ 2 ) + ( 1 / n ) ) = ( ( S ^ 2 ) + ( 1 / k ) ) )
121 118 120 breq12d 
 |-  ( n = k -> ( ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) <-> ( ( A D ( f ` k ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / k ) ) ) )
122 121 rspccva 
 |-  ( ( A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) /\ k e. NN ) -> ( ( A D ( f ` k ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / k ) ) )
123 115 122 sylan 
 |-  ( ( ( ph /\ ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) ) /\ k e. NN ) -> ( ( A D ( f ` k ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / k ) ) )
124 eqid 
 |-  ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` f ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) = ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` f ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
125 1 2 3 4 111 112 113 8 9 10 11 114 123 124 minvecolem4 
 |-  ( ( ph /\ ( f : NN --> Y /\ A. n e. NN ( ( A D ( f ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) ) ) -> E. x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )
126 110 125 exlimddv 
 |-  ( ph -> E. x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )