Metamath Proof Explorer

Theorem minvecolem4

Description: Lemma for minveco . The convergent point of the Cauchy sequence F attains the minimum distance, and so is closer to A than any other point in Y . (Contributed by Mario Carneiro, 7-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 ) ) )
minveco.t 
|- T = ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
Assertion minvecolem4 
|- ( 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 minveco.f 
 |-  ( ph -> F : NN --> Y )
13 minveco.1 
 |-  ( ( ph /\ n e. NN ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
14 minveco.t 
 |-  T = ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
15 phnv 
 |-  ( U e. CPreHilOLD -> U e. NrmCVec )
16 1 8 imsxmet 
 |-  ( U e. NrmCVec -> D e. ( *Met ` X ) )
17 5 15 16 3syl 
 |-  ( ph -> D e. ( *Met ` X ) )
18 9 methaus 
 |-  ( D e. ( *Met ` X ) -> J e. Haus )
19 lmfun 
 |-  ( J e. Haus -> Fun ( ~~>t ` J ) )
20 17 18 19 3syl 
 |-  ( ph -> Fun ( ~~>t ` J ) )
21 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4a 
 |-  ( ph -> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) )
22 eqid 
 |-  ( J |`t Y ) = ( J |`t Y )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 4 fvexi 
 |-  Y e. _V
25 24 a1i 
 |-  ( ph -> Y e. _V )
26 5 15 syl 
 |-  ( ph -> U e. NrmCVec )
27 9 mopntop 
 |-  ( D e. ( *Met ` X ) -> J e. Top )
28 26 16 27 3syl 
 |-  ( ph -> J e. Top )
29 elin 
 |-  ( W e. ( ( SubSp ` U ) i^i CBan ) <-> ( W e. ( SubSp ` U ) /\ W e. CBan ) )
30 6 29 sylib 
 |-  ( ph -> ( W e. ( SubSp ` U ) /\ W e. CBan ) )
31 30 simpld 
 |-  ( ph -> W e. ( SubSp ` U ) )
32 eqid 
 |-  ( SubSp ` U ) = ( SubSp ` U )
33 1 4 32 sspba 
 |-  ( ( U e. NrmCVec /\ W e. ( SubSp ` U ) ) -> Y C_ X )
34 26 31 33 syl2anc 
 |-  ( ph -> Y C_ X )
35 xmetres2 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
36 17 34 35 syl2anc 
 |-  ( ph -> ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) )
37 eqid 
 |-  ( MetOpen ` ( D |` ( Y X. Y ) ) ) = ( MetOpen ` ( D |` ( Y X. Y ) ) )
38 37 mopntopon 
 |-  ( ( D |` ( Y X. Y ) ) e. ( *Met ` Y ) -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. ( TopOn ` Y ) )
39 36 38 syl 
 |-  ( ph -> ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. ( TopOn ` Y ) )
40 lmcl 
 |-  ( ( ( MetOpen ` ( D |` ( Y X. Y ) ) ) e. ( TopOn ` Y ) /\ F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) -> ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) e. Y )
41 39 21 40 syl2anc 
 |-  ( ph -> ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) e. Y )
42 1zzd 
 |-  ( ph -> 1 e. ZZ )
43 22 23 25 28 41 42 12 lmss 
 |-  ( ph -> ( F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) <-> F ( ~~>t ` ( J |`t Y ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
44 eqid 
 |-  ( D |` ( Y X. Y ) ) = ( D |` ( Y X. Y ) )
45 44 9 37 metrest 
 |-  ( ( D e. ( *Met ` X ) /\ Y C_ X ) -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
46 17 34 45 syl2anc 
 |-  ( ph -> ( J |`t Y ) = ( MetOpen ` ( D |` ( Y X. Y ) ) ) )
47 46 fveq2d 
 |-  ( ph -> ( ~~>t ` ( J |`t Y ) ) = ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) )
48 47 breqd 
 |-  ( ph -> ( F ( ~~>t ` ( J |`t Y ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) <-> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
49 43 48 bitrd 
 |-  ( ph -> ( F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) <-> F ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
50 21 49 mpbird 
 |-  ( ph -> F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) )
51 funbrfv 
 |-  ( Fun ( ~~>t ` J ) -> ( F ( ~~>t ` J ) ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) -> ( ( ~~>t ` J ) ` F ) = ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) ) )
52 20 50 51 sylc 
 |-  ( ph -> ( ( ~~>t ` J ) ` F ) = ( ( ~~>t ` ( MetOpen ` ( D |` ( Y X. Y ) ) ) ) ` F ) )
53 52 41 eqeltrd 
 |-  ( ph -> ( ( ~~>t ` J ) ` F ) e. Y )
54 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4b 
 |-  ( ph -> ( ( ~~>t ` J ) ` F ) e. X )
55 1 2 3 8 imsdval 
 |-  ( ( U e. NrmCVec /\ A e. X /\ ( ( ~~>t ` J ) ` F ) e. X ) -> ( A D ( ( ~~>t ` J ) ` F ) ) = ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) )
56 26 7 54 55 syl3anc 
 |-  ( ph -> ( A D ( ( ~~>t ` J ) ` F ) ) = ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) )
57 56 adantr 
 |-  ( ( ph /\ y e. Y ) -> ( A D ( ( ~~>t ` J ) ` F ) ) = ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) )
58 1 8 imsmet 
 |-  ( U e. NrmCVec -> D e. ( Met ` X ) )
59 5 15 58 3syl 
 |-  ( ph -> D e. ( Met ` X ) )
60 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ ( ( ~~>t ` J ) ` F ) e. X ) -> ( A D ( ( ~~>t ` J ) ` F ) ) e. RR )
61 59 7 54 60 syl3anc 
 |-  ( ph -> ( A D ( ( ~~>t ` J ) ` F ) ) e. RR )
62 61 adantr 
 |-  ( ( ph /\ y e. Y ) -> ( A D ( ( ~~>t ` J ) ` F ) ) e. RR )
63 1 2 3 4 5 6 7 8 9 10 11 12 13 minvecolem4c 
 |-  ( ph -> S e. RR )
64 63 adantr 
 |-  ( ( ph /\ y e. Y ) -> S e. RR )
65 26 adantr 
 |-  ( ( ph /\ y e. Y ) -> U e. NrmCVec )
66 7 adantr 
 |-  ( ( ph /\ y e. Y ) -> A e. X )
67 34 sselda 
 |-  ( ( ph /\ y e. Y ) -> y e. X )
68 1 2 nvmcl 
 |-  ( ( U e. NrmCVec /\ A e. X /\ y e. X ) -> ( A M y ) e. X )
69 65 66 67 68 syl3anc 
 |-  ( ( ph /\ y e. Y ) -> ( A M y ) e. X )
70 1 3 nvcl 
 |-  ( ( U e. NrmCVec /\ ( A M y ) e. X ) -> ( N ` ( A M y ) ) e. RR )
71 65 69 70 syl2anc 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A M y ) ) e. RR )
72 63 61 ltnled 
 |-  ( ph -> ( S < ( A D ( ( ~~>t ` J ) ` F ) ) <-> -. ( A D ( ( ~~>t ` J ) ` F ) ) <_ S ) )
73 eqid 
 |-  ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) = ( ZZ>= ` ( ( |_ ` T ) + 1 ) )
74 17 adantr 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> D e. ( *Met ` X ) )
75 61 63 readdcld 
 |-  ( ph -> ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) e. RR )
76 75 rehalfcld 
 |-  ( ph -> ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) e. RR )
77 76 resqcld 
 |-  ( ph -> ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) e. RR )
78 63 resqcld 
 |-  ( ph -> ( S ^ 2 ) e. RR )
79 77 78 resubcld 
 |-  ( ph -> ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR )
80 79 adantr 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR )
81 63 61 63 ltadd1d 
 |-  ( ph -> ( S < ( A D ( ( ~~>t ` J ) ` F ) ) <-> ( S + S ) < ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) ) )
82 63 recnd 
 |-  ( ph -> S e. CC )
83 82 2timesd 
 |-  ( ph -> ( 2 x. S ) = ( S + S ) )
84 83 breq1d 
 |-  ( ph -> ( ( 2 x. S ) < ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) <-> ( S + S ) < ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) ) )
85 2re 
 |-  2 e. RR
86 2pos 
 |-  0 < 2
87 85 86 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
88 87 a1i 
 |-  ( ph -> ( 2 e. RR /\ 0 < 2 ) )
89 ltmuldiv2 
 |-  ( ( S e. RR /\ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. S ) < ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) <-> S < ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) )
90 63 75 88 89 syl3anc 
 |-  ( ph -> ( ( 2 x. S ) < ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) <-> S < ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) )
91 81 84 90 3bitr2d 
 |-  ( ph -> ( S < ( A D ( ( ~~>t ` J ) ` F ) ) <-> S < ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) )
92 1 2 3 4 5 6 7 8 9 10 minvecolem1 
 |-  ( ph -> ( R C_ RR /\ R =/= (/) /\ A. w e. R 0 <_ w ) )
93 92 simp3d 
 |-  ( ph -> A. w e. R 0 <_ w )
94 92 simp1d 
 |-  ( ph -> R C_ RR )
95 92 simp2d 
 |-  ( ph -> R =/= (/) )
96 0re 
 |-  0 e. RR
97 breq1 
 |-  ( x = 0 -> ( x <_ w <-> 0 <_ w ) )
98 97 ralbidv 
 |-  ( x = 0 -> ( A. w e. R x <_ w <-> A. w e. R 0 <_ w ) )
99 98 rspcev 
 |-  ( ( 0 e. RR /\ A. w e. R 0 <_ w ) -> E. x e. RR A. w e. R x <_ w )
100 96 93 99 sylancr 
 |-  ( ph -> E. x e. RR A. w e. R x <_ w )
101 96 a1i 
 |-  ( ph -> 0 e. RR )
102 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 ) )
103 94 95 100 101 102 syl31anc 
 |-  ( ph -> ( 0 <_ inf ( R , RR , < ) <-> A. w e. R 0 <_ w ) )
104 93 103 mpbird 
 |-  ( ph -> 0 <_ inf ( R , RR , < ) )
105 104 11 breqtrrdi 
 |-  ( ph -> 0 <_ S )
106 metge0 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ ( ( ~~>t ` J ) ` F ) e. X ) -> 0 <_ ( A D ( ( ~~>t ` J ) ` F ) ) )
107 59 7 54 106 syl3anc 
 |-  ( ph -> 0 <_ ( A D ( ( ~~>t ` J ) ` F ) ) )
108 61 63 107 105 addge0d 
 |-  ( ph -> 0 <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) )
109 divge0 
 |-  ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) e. RR /\ 0 <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) ) /\ ( 2 e. RR /\ 0 < 2 ) ) -> 0 <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) )
110 75 108 88 109 syl21anc 
 |-  ( ph -> 0 <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) )
111 63 76 105 110 lt2sqd 
 |-  ( ph -> ( S < ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) <-> ( S ^ 2 ) < ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) ) )
112 78 77 posdifd 
 |-  ( ph -> ( ( S ^ 2 ) < ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) <-> 0 < ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) )
113 91 111 112 3bitrd 
 |-  ( ph -> ( S < ( A D ( ( ~~>t ` J ) ` F ) ) <-> 0 < ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) )
114 113 biimpa 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> 0 < ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
115 80 114 elrpd 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR+ )
116 115 rpreccld 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) e. RR+ )
117 14 116 eqeltrid 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> T e. RR+ )
118 117 rprege0d 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( T e. RR /\ 0 <_ T ) )
119 flge0nn0 
 |-  ( ( T e. RR /\ 0 <_ T ) -> ( |_ ` T ) e. NN0 )
120 nn0p1nn 
 |-  ( ( |_ ` T ) e. NN0 -> ( ( |_ ` T ) + 1 ) e. NN )
121 118 119 120 3syl 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( ( |_ ` T ) + 1 ) e. NN )
122 121 nnzd 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( ( |_ ` T ) + 1 ) e. ZZ )
123 50 52 breqtrrd 
 |-  ( ph -> F ( ~~>t ` J ) ( ( ~~>t ` J ) ` F ) )
124 123 adantr 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> F ( ~~>t ` J ) ( ( ~~>t ` J ) ` F ) )
125 7 adantr 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> A e. X )
126 76 adantr 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) e. RR )
127 126 rexrd 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) e. RR* )
128 simpll 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ph )
129 eluznn 
 |-  ( ( ( ( |_ ` T ) + 1 ) e. NN /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> n e. NN )
130 121 129 sylan 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> n e. NN )
131 59 adantr 
 |-  ( ( ph /\ n e. NN ) -> D e. ( Met ` X ) )
132 7 adantr 
 |-  ( ( ph /\ n e. NN ) -> A e. X )
133 12 34 fssd 
 |-  ( ph -> F : NN --> X )
134 133 ffvelcdmda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. X )
135 metcl 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ ( F ` n ) e. X ) -> ( A D ( F ` n ) ) e. RR )
136 131 132 134 135 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> ( A D ( F ` n ) ) e. RR )
137 128 130 136 syl2anc 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( A D ( F ` n ) ) e. RR )
138 137 resqcld 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( A D ( F ` n ) ) ^ 2 ) e. RR )
139 63 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> S e. RR )
140 139 resqcld 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( S ^ 2 ) e. RR )
141 130 nnrecred 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( 1 / n ) e. RR )
142 140 141 readdcld 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( S ^ 2 ) + ( 1 / n ) ) e. RR )
143 77 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) e. RR )
144 128 130 13 syl2anc 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( S ^ 2 ) + ( 1 / n ) ) )
145 117 adantr 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> T e. RR+ )
146 145 rpred 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> T e. RR )
147 reflcl 
 |-  ( T e. RR -> ( |_ ` T ) e. RR )
148 peano2re 
 |-  ( ( |_ ` T ) e. RR -> ( ( |_ ` T ) + 1 ) e. RR )
149 146 147 148 3syl 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( |_ ` T ) + 1 ) e. RR )
150 130 nnred 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> n e. RR )
151 fllep1 
 |-  ( T e. RR -> T <_ ( ( |_ ` T ) + 1 ) )
152 146 151 syl 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> T <_ ( ( |_ ` T ) + 1 ) )
153 eluzle 
 |-  ( n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) -> ( ( |_ ` T ) + 1 ) <_ n )
154 153 adantl 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( |_ ` T ) + 1 ) <_ n )
155 146 149 150 152 154 letrd 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> T <_ n )
156 14 155 eqbrtrrid 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) <_ n )
157 1red 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> 1 e. RR )
158 79 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR )
159 114 adantr 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> 0 < ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
160 130 nngt0d 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> 0 < n )
161 lediv23 
 |-  ( ( 1 e. RR /\ ( ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) e. RR /\ 0 < ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) /\ ( n e. RR /\ 0 < n ) ) -> ( ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) <_ n <-> ( 1 / n ) <_ ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) )
162 157 158 159 150 160 161 syl122anc 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( 1 / ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) <_ n <-> ( 1 / n ) <_ ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) )
163 156 162 mpbid 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( 1 / n ) <_ ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) )
164 140 141 143 leaddsub2d 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) <-> ( 1 / n ) <_ ( ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) - ( S ^ 2 ) ) ) )
165 163 164 mpbird 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( S ^ 2 ) + ( 1 / n ) ) <_ ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) )
166 138 142 143 144 165 letrd 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) )
167 76 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) e. RR )
168 metge0 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ ( F ` n ) e. X ) -> 0 <_ ( A D ( F ` n ) ) )
169 131 132 134 168 syl3anc 
 |-  ( ( ph /\ n e. NN ) -> 0 <_ ( A D ( F ` n ) ) )
170 128 130 169 syl2anc 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> 0 <_ ( A D ( F ` n ) ) )
171 110 ad2antrr 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> 0 <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) )
172 137 167 170 171 le2sqd 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( ( A D ( F ` n ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) <-> ( ( A D ( F ` n ) ) ^ 2 ) <_ ( ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ^ 2 ) ) )
173 166 172 mpbird 
 |-  ( ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) /\ n e. ( ZZ>= ` ( ( |_ ` T ) + 1 ) ) ) -> ( A D ( F ` n ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) )
174 73 9 74 122 124 125 127 173 lmle 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) )
175 61 63 61 leadd2d 
 |-  ( ph -> ( ( A D ( ( ~~>t ` J ) ` F ) ) <_ S <-> ( ( A D ( ( ~~>t ` J ) ` F ) ) + ( A D ( ( ~~>t ` J ) ` F ) ) ) <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) ) )
176 61 recnd 
 |-  ( ph -> ( A D ( ( ~~>t ` J ) ` F ) ) e. CC )
177 176 2timesd 
 |-  ( ph -> ( 2 x. ( A D ( ( ~~>t ` J ) ` F ) ) ) = ( ( A D ( ( ~~>t ` J ) ` F ) ) + ( A D ( ( ~~>t ` J ) ` F ) ) ) )
178 177 breq1d 
 |-  ( ph -> ( ( 2 x. ( A D ( ( ~~>t ` J ) ` F ) ) ) <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) <-> ( ( A D ( ( ~~>t ` J ) ` F ) ) + ( A D ( ( ~~>t ` J ) ` F ) ) ) <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) ) )
179 lemuldiv2 
 |-  ( ( ( A D ( ( ~~>t ` J ) ` F ) ) e. RR /\ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. ( A D ( ( ~~>t ` J ) ` F ) ) ) <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) <-> ( A D ( ( ~~>t ` J ) ` F ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) )
180 87 179 mp3an3 
 |-  ( ( ( A D ( ( ~~>t ` J ) ` F ) ) e. RR /\ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) e. RR ) -> ( ( 2 x. ( A D ( ( ~~>t ` J ) ` F ) ) ) <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) <-> ( A D ( ( ~~>t ` J ) ` F ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) )
181 61 75 180 syl2anc 
 |-  ( ph -> ( ( 2 x. ( A D ( ( ~~>t ` J ) ` F ) ) ) <_ ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) <-> ( A D ( ( ~~>t ` J ) ` F ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) )
182 175 178 181 3bitr2d 
 |-  ( ph -> ( ( A D ( ( ~~>t ` J ) ` F ) ) <_ S <-> ( A D ( ( ~~>t ` J ) ` F ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) )
183 182 biimpar 
 |-  ( ( ph /\ ( A D ( ( ~~>t ` J ) ` F ) ) <_ ( ( ( A D ( ( ~~>t ` J ) ` F ) ) + S ) / 2 ) ) -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ S )
184 174 183 syldan 
 |-  ( ( ph /\ S < ( A D ( ( ~~>t ` J ) ` F ) ) ) -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ S )
185 184 ex 
 |-  ( ph -> ( S < ( A D ( ( ~~>t ` J ) ` F ) ) -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ S ) )
186 72 185 sylbird 
 |-  ( ph -> ( -. ( A D ( ( ~~>t ` J ) ` F ) ) <_ S -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ S ) )
187 186 pm2.18d 
 |-  ( ph -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ S )
188 187 adantr 
 |-  ( ( ph /\ y e. Y ) -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ S )
189 94 adantr 
 |-  ( ( ph /\ y e. Y ) -> R C_ RR )
190 100 adantr 
 |-  ( ( ph /\ y e. Y ) -> E. x e. RR A. w e. R x <_ w )
191 simpr 
 |-  ( ( ph /\ y e. Y ) -> y e. Y )
192 fvex 
 |-  ( N ` ( A M y ) ) e. _V
193 eqid 
 |-  ( y e. Y |-> ( N ` ( A M y ) ) ) = ( y e. Y |-> ( N ` ( A M y ) ) )
194 193 elrnmpt1 
 |-  ( ( y e. Y /\ ( N ` ( A M y ) ) e. _V ) -> ( N ` ( A M y ) ) e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) )
195 191 192 194 sylancl 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A M y ) ) e. ran ( y e. Y |-> ( N ` ( A M y ) ) ) )
196 195 10 eleqtrrdi 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A M y ) ) e. R )
197 infrelb 
 |-  ( ( R C_ RR /\ E. x e. RR A. w e. R x <_ w /\ ( N ` ( A M y ) ) e. R ) -> inf ( R , RR , < ) <_ ( N ` ( A M y ) ) )
198 189 190 196 197 syl3anc 
 |-  ( ( ph /\ y e. Y ) -> inf ( R , RR , < ) <_ ( N ` ( A M y ) ) )
199 11 198 eqbrtrid 
 |-  ( ( ph /\ y e. Y ) -> S <_ ( N ` ( A M y ) ) )
200 62 64 71 188 199 letrd 
 |-  ( ( ph /\ y e. Y ) -> ( A D ( ( ~~>t ` J ) ` F ) ) <_ ( N ` ( A M y ) ) )
201 57 200 eqbrtrrd 
 |-  ( ( ph /\ y e. Y ) -> ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) <_ ( N ` ( A M y ) ) )
202 201 ralrimiva 
 |-  ( ph -> A. y e. Y ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) <_ ( N ` ( A M y ) ) )
203 oveq2 
 |-  ( x = ( ( ~~>t ` J ) ` F ) -> ( A M x ) = ( A M ( ( ~~>t ` J ) ` F ) ) )
204 203 fveq2d 
 |-  ( x = ( ( ~~>t ` J ) ` F ) -> ( N ` ( A M x ) ) = ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) )
205 204 breq1d 
 |-  ( x = ( ( ~~>t ` J ) ` F ) -> ( ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) <-> ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) <_ ( N ` ( A M y ) ) ) )
206 205 ralbidv 
 |-  ( x = ( ( ~~>t ` J ) ` F ) -> ( A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) <-> A. y e. Y ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) <_ ( N ` ( A M y ) ) ) )
207 206 rspcev 
 |-  ( ( ( ( ~~>t ` J ) ` F ) e. Y /\ A. y e. Y ( N ` ( A M ( ( ~~>t ` J ) ` F ) ) ) <_ ( N ` ( A M y ) ) ) -> E. x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )
208 53 202 207 syl2anc 
 |-  ( ph -> E. x e. Y A. y e. Y ( N ` ( A M x ) ) <_ ( N ` ( A M y ) ) )