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	syl5bb	|- ( ( 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	sseldi	|- ( 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 ) ) )