MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  minvecolem4 Structured version   Unicode version

Theorem minvecolem4 26367
Description: Lemma for minveco 26371. 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.) (New usage is discouraged.)
Hypotheses
Ref Expression
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.  CPreHil OLD )
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  =  sup ( 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
Ref Expression
minvecolem4  |-  ( ph  ->  E. x  e.  Y  A. y  e.  Y  ( N `  ( A M x ) )  <_  ( N `  ( A M y ) ) )
Distinct variable groups:    x, n, y, F    n, J, x, y    x, M, y   
x, N, y    ph, n, x, y    x, R    S, n, x, y    A, n, x, y    D, n, x, y    x, U, y    x, W, y    T, n    n, X, x   
n, Y, x, y
Allowed substitution hints:    R( y, n)    T( x, y)    U( n)    M( n)    N( n)    W( n)    X( y)

Proof of Theorem minvecolem4
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 minveco.u . . . . . 6  |-  ( ph  ->  U  e.  CPreHil OLD )
2 phnv 26300 . . . . . 6  |-  ( U  e.  CPreHil OLD  ->  U  e.  NrmCVec )
3 minveco.x . . . . . . 7  |-  X  =  ( BaseSet `  U )
4 minveco.d . . . . . . 7  |-  D  =  ( IndMet `  U )
53, 4imsxmet 26169 . . . . . 6  |-  ( U  e.  NrmCVec  ->  D  e.  ( *Met `  X
) )
61, 2, 53syl 18 . . . . 5  |-  ( ph  ->  D  e.  ( *Met `  X ) )
7 minveco.j . . . . . 6  |-  J  =  ( MetOpen `  D )
87methaus 21466 . . . . 5  |-  ( D  e.  ( *Met `  X )  ->  J  e.  Haus )
9 lmfun 20328 . . . . 5  |-  ( J  e.  Haus  ->  Fun  ( ~~> t `  J )
)
106, 8, 93syl 18 . . . 4  |-  ( ph  ->  Fun  ( ~~> t `  J ) )
11 minveco.m . . . . . 6  |-  M  =  ( -v `  U
)
12 minveco.n . . . . . 6  |-  N  =  ( normCV `  U )
13 minveco.y . . . . . 6  |-  Y  =  ( BaseSet `  W )
14 minveco.w . . . . . 6  |-  ( ph  ->  W  e.  ( (
SubSp `  U )  i^i 
CBan ) )
15 minveco.a . . . . . 6  |-  ( ph  ->  A  e.  X )
16 minveco.r . . . . . 6  |-  R  =  ran  ( y  e.  Y  |->  ( N `  ( A M y ) ) )
17 minveco.s . . . . . 6  |-  S  =  sup ( R ,  RR ,  `'  <  )
18 minveco.f . . . . . 6  |-  ( ph  ->  F : NN --> Y )
19 minveco.1 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( A D ( F `
 n ) ) ^ 2 )  <_ 
( ( S ^
2 )  +  ( 1  /  n ) ) )
203, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4a 26364 . . . . 5  |-  ( ph  ->  F ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y
) ) ) ) ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y
) ) ) ) `
 F ) )
21 eqid 2429 . . . . . . 7  |-  ( Jt  Y )  =  ( Jt  Y )
22 nnuz 11194 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
23 fvex 5891 . . . . . . . . 9  |-  ( BaseSet `  W )  e.  _V
2413, 23eqeltri 2513 . . . . . . . 8  |-  Y  e. 
_V
2524a1i 11 . . . . . . 7  |-  ( ph  ->  Y  e.  _V )
261, 2syl 17 . . . . . . . 8  |-  ( ph  ->  U  e.  NrmCVec )
277mopntop 21386 . . . . . . . 8  |-  ( D  e.  ( *Met `  X )  ->  J  e.  Top )
2826, 5, 273syl 18 . . . . . . 7  |-  ( ph  ->  J  e.  Top )
29 elin 3655 . . . . . . . . . . . . 13  |-  ( W  e.  ( ( SubSp `  U )  i^i  CBan ) 
<->  ( W  e.  (
SubSp `  U )  /\  W  e.  CBan ) )
3014, 29sylib 199 . . . . . . . . . . . 12  |-  ( ph  ->  ( W  e.  (
SubSp `  U )  /\  W  e.  CBan ) )
3130simpld 460 . . . . . . . . . . 11  |-  ( ph  ->  W  e.  ( SubSp `  U ) )
32 eqid 2429 . . . . . . . . . . . 12  |-  ( SubSp `  U )  =  (
SubSp `  U )
333, 13, 32sspba 26211 . . . . . . . . . . 11  |-  ( ( U  e.  NrmCVec  /\  W  e.  ( SubSp `  U )
)  ->  Y  C_  X
)
3426, 31, 33syl2anc 665 . . . . . . . . . 10  |-  ( ph  ->  Y  C_  X )
35 xmetres2 21307 . . . . . . . . . 10  |-  ( ( D  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( D  |`  ( Y  X.  Y
) )  e.  ( *Met `  Y
) )
366, 34, 35syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( D  |`  ( Y  X.  Y ) )  e.  ( *Met `  Y ) )
37 eqid 2429 . . . . . . . . . 10  |-  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) )  =  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) )
3837mopntopon 21385 . . . . . . . . 9  |-  ( ( D  |`  ( Y  X.  Y ) )  e.  ( *Met `  Y )  ->  ( MetOpen
`  ( D  |`  ( Y  X.  Y
) ) )  e.  (TopOn `  Y )
)
3936, 38syl 17 . . . . . . . 8  |-  ( ph  ->  ( MetOpen `  ( D  |`  ( Y  X.  Y
) ) )  e.  (TopOn `  Y )
)
40 lmcl 20244 . . . . . . . 8  |-  ( ( ( 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 )
4139, 20, 40syl2anc 665 . . . . . . 7  |-  ( ph  ->  ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y
) ) ) ) `
 F )  e.  Y )
42 1zzd 10968 . . . . . . 7  |-  ( ph  ->  1  e.  ZZ )
4321, 22, 25, 28, 41, 42, 18lmss 20245 . . . . . 6  |-  ( ph  ->  ( F ( ~~> t `  J ) ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) ) ) `  F
)  <->  F ( ~~> t `  ( Jt  Y ) ) ( ( ~~> t `  ( MetOpen
`  ( D  |`  ( Y  X.  Y
) ) ) ) `
 F ) ) )
44 eqid 2429 . . . . . . . . . 10  |-  ( D  |`  ( Y  X.  Y
) )  =  ( D  |`  ( Y  X.  Y ) )
4544, 7, 37metrest 21470 . . . . . . . . 9  |-  ( ( D  e.  ( *Met `  X )  /\  Y  C_  X
)  ->  ( Jt  Y
)  =  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) ) )
466, 34, 45syl2anc 665 . . . . . . . 8  |-  ( ph  ->  ( Jt  Y )  =  (
MetOpen `  ( D  |`  ( Y  X.  Y
) ) ) )
4746fveq2d 5885 . . . . . . 7  |-  ( ph  ->  ( ~~> t `  ( Jt  Y ) )  =  ( ~~> t `  ( MetOpen
`  ( D  |`  ( Y  X.  Y
) ) ) ) )
4847breqd 4437 . . . . . 6  |-  ( ph  ->  ( F ( ~~> t `  ( Jt  Y ) ) ( ( ~~> t `  ( MetOpen
`  ( D  |`  ( Y  X.  Y
) ) ) ) `
 F )  <->  F ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) ) ) ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y
) ) ) ) `
 F ) ) )
4943, 48bitrd 256 . . . . 5  |-  ( 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 ) ) )
5020, 49mpbird 235 . . . 4  |-  ( ph  ->  F ( ~~> t `  J ) ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) ) ) `  F
) )
51 funbrfv 5919 . . . 4  |-  ( Fun  ( ~~> t `  J
)  ->  ( F
( ~~> t `  J
) ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y
) ) ) ) `
 F )  -> 
( ( ~~> t `  J ) `  F
)  =  ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) ) ) `  F
) ) )
5210, 50, 51sylc 62 . . 3  |-  ( ph  ->  ( ( ~~> t `  J ) `  F
)  =  ( ( ~~> t `  ( MetOpen `  ( D  |`  ( Y  X.  Y ) ) ) ) `  F
) )
5352, 41eqeltrd 2517 . 2  |-  ( ph  ->  ( ( ~~> t `  J ) `  F
)  e.  Y )
543, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4b 26365 . . . . . 6  |-  ( ph  ->  ( ( ~~> t `  J ) `  F
)  e.  X )
553, 11, 12, 4imsdval 26163 . . . . . 6  |-  ( ( U  e.  NrmCVec  /\  A  e.  X  /\  (
( ~~> t `  J
) `  F )  e.  X )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  =  ( N `  ( A M ( ( ~~> t `  J ) `  F
) ) ) )
5626, 15, 54, 55syl3anc 1264 . . . . 5  |-  ( ph  ->  ( A D ( ( ~~> t `  J
) `  F )
)  =  ( N `
 ( A M ( ( ~~> t `  J ) `  F
) ) ) )
5756adantr 466 . . . 4  |-  ( (
ph  /\  y  e.  Y )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  =  ( N `  ( A M ( ( ~~> t `  J ) `  F
) ) ) )
583, 4imsmet 26168 . . . . . . . 8  |-  ( U  e.  NrmCVec  ->  D  e.  ( Met `  X ) )
591, 2, 583syl 18 . . . . . . 7  |-  ( ph  ->  D  e.  ( Met `  X ) )
60 metcl 21278 . . . . . . 7  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  (
( ~~> t `  J
) `  F )  e.  X )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  e.  RR )
6159, 15, 54, 60syl3anc 1264 . . . . . 6  |-  ( ph  ->  ( A D ( ( ~~> t `  J
) `  F )
)  e.  RR )
6261adantr 466 . . . . 5  |-  ( (
ph  /\  y  e.  Y )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  e.  RR )
633, 11, 12, 13, 1, 14, 15, 4, 7, 16, 17, 18, 19minvecolem4c 26366 . . . . . 6  |-  ( ph  ->  S  e.  RR )
6463adantr 466 . . . . 5  |-  ( (
ph  /\  y  e.  Y )  ->  S  e.  RR )
6526adantr 466 . . . . . 6  |-  ( (
ph  /\  y  e.  Y )  ->  U  e.  NrmCVec )
6615adantr 466 . . . . . . 7  |-  ( (
ph  /\  y  e.  Y )  ->  A  e.  X )
6734sselda 3470 . . . . . . 7  |-  ( (
ph  /\  y  e.  Y )  ->  y  e.  X )
683, 11nvmcl 26113 . . . . . . 7  |-  ( ( U  e.  NrmCVec  /\  A  e.  X  /\  y  e.  X )  ->  ( A M y )  e.  X )
6965, 66, 67, 68syl3anc 1264 . . . . . 6  |-  ( (
ph  /\  y  e.  Y )  ->  ( A M y )  e.  X )
703, 12nvcl 26133 . . . . . 6  |-  ( ( U  e.  NrmCVec  /\  ( A M y )  e.  X )  ->  ( N `  ( A M y ) )  e.  RR )
7165, 69, 70syl2anc 665 . . . . 5  |-  ( (
ph  /\  y  e.  Y )  ->  ( N `  ( A M y ) )  e.  RR )
7263, 61ltnled 9781 . . . . . . . 8  |-  ( ph  ->  ( S  <  ( A D ( ( ~~> t `  J ) `  F
) )  <->  -.  ( A D ( ( ~~> t `  J ) `  F
) )  <_  S
) )
73 eqid 2429 . . . . . . . . . . 11  |-  ( ZZ>= `  ( ( |_ `  T )  +  1 ) )  =  (
ZZ>= `  ( ( |_
`  T )  +  1 ) )
746adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  D  e.  ( *Met `  X
) )
75 minveco.t . . . . . . . . . . . . . . 15  |-  T  =  ( 1  /  (
( ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ^ 2 )  -  ( S ^ 2 ) ) )
7661, 63readdcld 9669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  e.  RR )
7776rehalfcld 10859 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 )  e.  RR )
7877resqcld 12439 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ^ 2 )  e.  RR )
7963resqcld 12439 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( S ^ 2 )  e.  RR )
8078, 79resubcld 10046 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( ( ( A D ( ( ~~> t `  J
) `  F )
)  +  S )  /  2 ) ^
2 )  -  ( S ^ 2 ) )  e.  RR )
8180adantr 466 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( (
( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ^ 2 )  -  ( S ^ 2 ) )  e.  RR )
8263, 61, 63ltadd1d 10205 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( S  <  ( A D ( ( ~~> t `  J ) `  F
) )  <->  ( S  +  S )  <  (
( A D ( ( ~~> t `  J
) `  F )
)  +  S ) ) )
8363recnd 9668 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  S  e.  CC )
84832timesd 10855 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 2  x.  S
)  =  ( S  +  S ) )
8584breq1d 4436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( 2  x.  S )  <  (
( A D ( ( ~~> t `  J
) `  F )
)  +  S )  <-> 
( S  +  S
)  <  ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
) ) )
86 2re 10679 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  RR
87 2pos 10701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <  2
8886, 87pm3.2i 456 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2  e.  RR  /\  0  <  2 )
8988a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 2  e.  RR  /\  0  <  2 ) )
90 ltmuldiv2 10478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) ) )
9163, 76, 89, 90syl3anc 1264 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( 2  x.  S )  <  (
( A D ( ( ~~> t `  J
) `  F )
)  +  S )  <-> 
S  <  ( (
( A D ( ( ~~> t `  J
) `  F )
)  +  S )  /  2 ) ) )
9282, 85, 913bitr2d 284 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( S  <  ( A D ( ( ~~> t `  J ) `  F
) )  <->  S  <  ( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ) )
933, 11, 12, 13, 1, 14, 15, 4, 7, 16minvecolem1 26361 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( R  C_  RR  /\  R  =/=  (/)  /\  A. w  e.  R  0  <_  w ) )
9493simp3d 1019 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  A. w  e.  R 
0  <_  w )
9593simp1d 1017 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  R  C_  RR )
9693simp2d 1018 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  R  =/=  (/) )
97 0re 9642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  RR
98 breq1 4429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  =  0  ->  (
x  <_  w  <->  0  <_  w ) )
9998ralbidv 2871 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  =  0  ->  ( A. w  e.  R  x  <_  w  <->  A. w  e.  R  0  <_  w ) )
10099rspcev 3188 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 0  e.  RR  /\  A. w  e.  R  0  <_  w )  ->  E. x  e.  RR  A. w  e.  R  x  <_  w )
10197, 94, 100sylancr 667 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  E. x  e.  RR  A. w  e.  R  x  <_  w )
10297a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  0  e.  RR )
103 infmrgelbOLD 10595 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( R  C_  RR  /\  R  =/=  (/)  /\  E. x  e.  RR  A. w  e.  R  x  <_  w )  /\  0  e.  RR )  ->  (
0  <_  sup ( R ,  RR ,  `'  <  )  <->  A. w  e.  R  0  <_  w ) )
10495, 96, 101, 102, 103syl31anc 1267 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 0  <_  sup ( R ,  RR ,  `'  <  )  <->  A. w  e.  R  0  <_  w ) )
10594, 104mpbird 235 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  0  <_  sup ( R ,  RR ,  `'  <  ) )
106105, 17syl6breqr 4466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <_  S )
107 metge0 21291 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  (
( ~~> t `  J
) `  F )  e.  X )  ->  0  <_  ( A D ( ( ~~> t `  J
) `  F )
) )
10859, 15, 54, 107syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  <_  ( A D ( ( ~~> t `  J ) `  F
) ) )
10961, 63, 108, 106addge0d 10188 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  0  <_  ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
) )
110 divge0 10473 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( 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 ) )
11176, 109, 89, 110syl21anc 1263 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <_  ( (
( A D ( ( ~~> t `  J
) `  F )
)  +  S )  /  2 ) )
11263, 77, 106, 111lt2sqd 12447 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( S  <  (
( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 )  <-> 
( S ^ 2 )  <  ( ( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ^ 2 ) ) )
11379, 78posdifd 10199 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( S ^
2 )  <  (
( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ^ 2 )  <->  0  <  ( ( ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ^ 2 )  -  ( S ^ 2 ) ) ) )
11492, 112, 1133bitrd 282 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( S  <  ( A D ( ( ~~> t `  J ) `  F
) )  <->  0  <  ( ( ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ^ 2 )  -  ( S ^ 2 ) ) ) )
115114biimpa 486 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  0  <  ( ( ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ^ 2 )  -  ( S ^ 2 ) ) )
11681, 115elrpd 11338 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( (
( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ^ 2 )  -  ( S ^ 2 ) )  e.  RR+ )
117116rpreccld 11351 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( 1  /  ( ( ( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ^ 2 )  -  ( S ^ 2 ) ) )  e.  RR+ )
11875, 117syl5eqel 2521 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  T  e.  RR+ )
119118rprege0d 11348 . . . . . . . . . . . . 13  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( T  e.  RR  /\  0  <_  T ) )
120 flge0nn0 12051 . . . . . . . . . . . . 13  |-  ( ( T  e.  RR  /\  0  <_  T )  -> 
( |_ `  T
)  e.  NN0 )
121 nn0p1nn 10909 . . . . . . . . . . . . 13  |-  ( ( |_ `  T )  e.  NN0  ->  ( ( |_ `  T )  +  1 )  e.  NN )
122119, 120, 1213syl 18 . . . . . . . . . . . 12  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( ( |_ `  T )  +  1 )  e.  NN )
123122nnzd 11039 . . . . . . . . . . 11  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( ( |_ `  T )  +  1 )  e.  ZZ )
12450, 52breqtrrd 4452 . . . . . . . . . . . 12  |-  ( ph  ->  F ( ~~> t `  J ) ( ( ~~> t `  J ) `
 F ) )
125124adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  F ( ~~> t `  J )
( ( ~~> t `  J ) `  F
) )
12615adantr 466 . . . . . . . . . . 11  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  A  e.  X )
12777adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( (
( A D ( ( ~~> t `  J
) `  F )
)  +  S )  /  2 )  e.  RR )
128127rexrd 9689 . . . . . . . . . . 11  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( (
( A D ( ( ~~> t `  J
) `  F )
)  +  S )  /  2 )  e. 
RR* )
129 simpll 758 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ph )
130 eluznn 11229 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( |_ `  T )  +  1 )  e.  NN  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  n  e.  NN )
131122, 130sylan 473 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  n  e.  NN )
13259adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  D  e.  ( Met `  X
) )
13315adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  A  e.  X )
13418, 34fssd 5755 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F : NN --> X )
135134ffvelrnda 6037 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( F `
 n )  e.  X )
136 metcl 21278 . . . . . . . . . . . . . . . 16  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  ( F `  n )  e.  X )  ->  ( A D ( F `  n ) )  e.  RR )
137132, 133, 135, 136syl3anc 1264 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( A D ( F `  n ) )  e.  RR )
138129, 131, 137syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( A D ( F `  n
) )  e.  RR )
139138resqcld 12439 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( A D ( F `  n ) ) ^
2 )  e.  RR )
14063ad2antrr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  S  e.  RR )
141140resqcld 12439 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( S ^
2 )  e.  RR )
142131nnrecred 10655 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( 1  /  n )  e.  RR )
143141, 142readdcld 9669 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( S ^ 2 )  +  ( 1  /  n
) )  e.  RR )
14478ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( ( ( A D ( ( ~~> t `  J
) `  F )
)  +  S )  /  2 ) ^
2 )  e.  RR )
145129, 131, 19syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( A D ( F `  n ) ) ^
2 )  <_  (
( S ^ 2 )  +  ( 1  /  n ) ) )
146118adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  T  e.  RR+ )
147146rpred 11341 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  T  e.  RR )
148 reflcl 12029 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  RR  ->  ( |_ `  T )  e.  RR )
149 peano2re 9805 . . . . . . . . . . . . . . . . . 18  |-  ( ( |_ `  T )  e.  RR  ->  (
( |_ `  T
)  +  1 )  e.  RR )
150147, 148, 1493syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( |_
`  T )  +  1 )  e.  RR )
151131nnred 10624 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  n  e.  RR )
152 fllep1 12034 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  RR  ->  T  <_  ( ( |_ `  T )  +  1 ) )
153147, 152syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  T  <_  (
( |_ `  T
)  +  1 ) )
154 eluzle 11171 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  ( ZZ>= `  (
( |_ `  T
)  +  1 ) )  ->  ( ( |_ `  T )  +  1 )  <_  n
)
155154adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( |_
`  T )  +  1 )  <_  n
)
156147, 150, 151, 153, 155letrd 9791 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  T  <_  n
)
15775, 156syl5eqbrr 4460 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( 1  / 
( ( ( ( ( A D ( ( ~~> t `  J
) `  F )
)  +  S )  /  2 ) ^
2 )  -  ( S ^ 2 ) ) )  <_  n )
158 1red 9657 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  1  e.  RR )
15980ad2antrr 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( ( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ^ 2 )  -  ( S ^ 2 ) )  e.  RR )
160115adantr 466 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  0  <  (
( ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ^ 2 )  -  ( S ^ 2 ) ) )
161131nngt0d 10653 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  0  <  n
)
162 lediv23 10498 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) )
163158, 159, 160, 151, 161, 162syl122anc 1273 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) ) )
164157, 163mpbid 213 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( 1  /  n )  <_  (
( ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ^ 2 )  -  ( S ^ 2 ) ) )
165141, 142, 144leaddsub2d 10214 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) ) )
166164, 165mpbird 235 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( S ^ 2 )  +  ( 1  /  n
) )  <_  (
( ( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) ^ 2 ) )
167139, 143, 144, 145, 166letrd 9791 . . . . . . . . . . . 12  |-  ( ( ( 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 ) )
16877ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 )  e.  RR )
169 metge0 21291 . . . . . . . . . . . . . . 15  |-  ( ( D  e.  ( Met `  X )  /\  A  e.  X  /\  ( F `  n )  e.  X )  ->  0  <_  ( A D ( F `  n ) ) )
170132, 133, 135, 169syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( A D ( F `  n ) ) )
171129, 131, 170syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  0  <_  ( A D ( F `  n ) ) )
172111ad2antrr 730 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  0  <_  (
( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) )
173138, 168, 171, 172le2sqd 12448 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
174167, 173mpbird 235 . . . . . . . . . . 11  |-  ( ( ( ph  /\  S  <  ( A D ( ( ~~> t `  J
) `  F )
) )  /\  n  e.  ( ZZ>= `  ( ( |_ `  T )  +  1 ) ) )  ->  ( A D ( F `  n
) )  <_  (
( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) )
17573, 7, 74, 123, 125, 126, 128, 174lmle 22164 . . . . . . . . . 10  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  <_  (
( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) )
17661, 63, 61leadd2d 10207 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( A D ( ( ~~> t `  J ) `  F
) )  <_  S  <->  ( ( A D ( ( ~~> t `  J
) `  F )
)  +  ( A D ( ( ~~> t `  J ) `  F
) ) )  <_ 
( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
) ) )
17761recnd 9668 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A D ( ( ~~> t `  J
) `  F )
)  e.  CC )
1781772timesd 10855 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  x.  ( A D ( ( ~~> t `  J ) `  F
) ) )  =  ( ( A D ( ( ~~> t `  J ) `  F
) )  +  ( A D ( ( ~~> t `  J ) `
 F ) ) ) )
179178breq1d 4436 . . . . . . . . . . . 12  |-  ( 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
) ) )
180 lemuldiv2 10486 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
18188, 180mp3an3 1349 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) )
18261, 76, 181syl2anc 665 . . . . . . . . . . . 12  |-  ( 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 ) ) )
183176, 179, 1823bitr2d 284 . . . . . . . . . . 11  |-  ( ph  ->  ( ( A D ( ( ~~> t `  J ) `  F
) )  <_  S  <->  ( A D ( ( ~~> t `  J ) `
 F ) )  <_  ( ( ( A D ( ( ~~> t `  J ) `
 F ) )  +  S )  / 
2 ) ) )
184183biimpar 487 . . . . . . . . . 10  |-  ( (
ph  /\  ( A D ( ( ~~> t `  J ) `  F
) )  <_  (
( ( A D ( ( ~~> t `  J ) `  F
) )  +  S
)  /  2 ) )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  <_  S
)
185175, 184syldan 472 . . . . . . . . 9  |-  ( (
ph  /\  S  <  ( A D ( ( ~~> t `  J ) `
 F ) ) )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  <_  S
)
186185ex 435 . . . . . . . 8  |-  ( ph  ->  ( S  <  ( A D ( ( ~~> t `  J ) `  F
) )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  <_  S
) )
18772, 186sylbird 238 . . . . . . 7  |-  ( ph  ->  ( -.  ( A D ( ( ~~> t `  J ) `  F
) )  <_  S  ->  ( A D ( ( ~~> t `  J
) `  F )
)  <_  S )
)
188187pm2.18d 114 . . . . . 6  |-  ( ph  ->  ( A D ( ( ~~> t `  J
) `  F )
)  <_  S )
189188adantr 466 . . . . 5  |-  ( (
ph  /\  y  e.  Y )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  <_  S
)
19095adantr 466 . . . . . . 7  |-  ( (
ph  /\  y  e.  Y )  ->  R  C_  RR )
191101adantr 466 . . . . . . 7  |-  ( (
ph  /\  y  e.  Y )  ->  E. x  e.  RR  A. w  e.  R  x  <_  w
)
192 simpr 462 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  Y )  ->  y  e.  Y )
193 fvex 5891 . . . . . . . . 9  |-  ( N `
 ( A M y ) )  e. 
_V
194 eqid 2429 . . . . . . . . . 10  |-  ( y  e.  Y  |->  ( N `
 ( A M y ) ) )  =  ( y  e.  Y  |->  ( N `  ( A M y ) ) )
195194elrnmpt1 5103 . . . . . . . . 9  |-  ( ( y  e.  Y  /\  ( N `  ( A M y ) )  e.  _V )  -> 
( N `  ( A M y ) )  e.  ran  ( y  e.  Y  |->  ( N `
 ( A M y ) ) ) )
196192, 193, 195sylancl 666 . . . . . . . 8  |-  ( (
ph  /\  y  e.  Y )  ->  ( N `  ( A M y ) )  e.  ran  ( y  e.  Y  |->  ( N `
 ( A M y ) ) ) )
197196, 16syl6eleqr 2528 . . . . . . 7  |-  ( (
ph  /\  y  e.  Y )  ->  ( N `  ( A M y ) )  e.  R )
198 infmrlbOLD 10597 . . . . . . 7  |-  ( ( R  C_  RR  /\  E. x  e.  RR  A. w  e.  R  x  <_  w  /\  ( N `  ( A M y ) )  e.  R )  ->  sup ( R ,  RR ,  `'  <  )  <_  ( N `  ( A M y ) ) )
199190, 191, 197, 198syl3anc 1264 . . . . . 6  |-  ( (
ph  /\  y  e.  Y )  ->  sup ( R ,  RR ,  `'  <  )  <_  ( N `  ( A M y ) ) )
20017, 199syl5eqbr 4459 . . . . 5  |-  ( (
ph  /\  y  e.  Y )  ->  S  <_  ( N `  ( A M y ) ) )
20162, 64, 71, 189, 200letrd 9791 . . . 4  |-  ( (
ph  /\  y  e.  Y )  ->  ( A D ( ( ~~> t `  J ) `  F
) )  <_  ( N `  ( A M y ) ) )
20257, 201eqbrtrrd 4448 . . 3  |-  ( (
ph  /\  y  e.  Y )  ->  ( N `  ( A M ( ( ~~> t `  J ) `  F
) ) )  <_ 
( N `  ( A M y ) ) )
203202ralrimiva 2846 . 2  |-  ( ph  ->  A. y  e.  Y  ( N `  ( A M ( ( ~~> t `  J ) `  F
) ) )  <_ 
( N `  ( A M y ) ) )
204 oveq2 6313 . . . . . 6  |-  ( x  =  ( ( ~~> t `  J ) `  F
)  ->  ( A M x )  =  ( A M ( ( ~~> t `  J
) `  F )
) )
205204fveq2d 5885 . . . . 5  |-  ( x  =  ( ( ~~> t `  J ) `  F
)  ->  ( N `  ( A M x ) )  =  ( N `  ( A M ( ( ~~> t `  J ) `  F
) ) ) )
206205breq1d 4436 . . . 4  |-  ( x  =  ( ( ~~> t `  J ) `  F
)  ->  ( ( N `  ( A M x ) )  <_  ( N `  ( A M y ) )  <->  ( N `  ( A M ( ( ~~> t `  J ) `
 F ) ) )  <_  ( N `  ( A M y ) ) ) )
207206ralbidv 2871 . . 3  |-  ( 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 ) ) ) )
208207rspcev 3188 . 2  |-  ( ( ( ( ~~> 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 ) ) )
20953, 203, 208syl2anc 665 1  |-  ( ph  ->  E. x  e.  Y  A. y  e.  Y  ( N `  ( A M x ) )  <_  ( N `  ( A M y ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1870    =/= wne 2625   A.wral 2782   E.wrex 2783   _Vcvv 3087    i^i cin 3441    C_ wss 3442   (/)c0 3767   class class class wbr 4426    |-> cmpt 4484    X. cxp 4852   `'ccnv 4853   ran crn 4855    |` cres 4856   Fun wfun 5595   -->wf 5597   ` cfv 5601  (class class class)co 6305   supcsup 7960   RRcr 9537   0cc0 9538   1c1 9539    + caddc 9541    x. cmul 9543    < clt 9674    <_ cle 9675    - cmin 9859    / cdiv 10268   NNcn 10609   2c2 10659   NN0cn0 10869   ZZ>=cuz 11159   RR+crp 11302   |_cfl 12023   ^cexp 12269   ↾t crest 15278   *Metcxmt 18890   Metcme 18891   MetOpencmopn 18895   Topctop 19848  TopOnctopon 19849   ~~> tclm 20173   Hauscha 20255   NrmCVeccnv 26048   BaseSetcba 26050   -vcnsb 26053   normCVcnmcv 26054   IndMetcims 26055   SubSpcss 26205   CPreHil OLDccphlo 26298   CBanccbn 26349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-cnex 9594  ax-resscn 9595  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-mulcom 9602  ax-addass 9603  ax-mulass 9604  ax-distr 9605  ax-i2m1 9606  ax-1ne0 9607  ax-1rid 9608  ax-rnegex 9609  ax-rrecex 9610  ax-cnre 9611  ax-pre-lttri 9612  ax-pre-lttrn 9613  ax-pre-ltadd 9614  ax-pre-mulgt0 9615  ax-pre-sup 9616  ax-addf 9617  ax-mulf 9618
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-nel 2628  df-ral 2787  df-rex 2788  df-reu 2789  df-rmo 2790  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-iin 4305  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6267  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-oadd 7194  df-er 7371  df-map 7482  df-pm 7483  df-en 7578  df-dom 7579  df-sdom 7580  df-fin 7581  df-fi 7931  df-sup 7962  df-pnf 9676  df-mnf 9677  df-xr 9678  df-ltxr 9679  df-le 9680  df-sub 9861  df-neg 9862  df-div 10269  df-nn 10610  df-2 10668  df-3 10669  df-4 10670  df-n0 10870  df-z 10938  df-uz 11160  df-q 11265  df-rp 11303  df-xneg 11409  df-xadd 11410  df-xmul 11411  df-ico 11641  df-icc 11642  df-fl 12025  df-seq 12211  df-exp 12270  df-cj 13141  df-re 13142  df-im 13143  df-sqrt 13277  df-abs 13278  df-rest 15280  df-topgen 15301  df-psmet 18897  df-xmet 18898  df-met 18899  df-bl 18900  df-mopn 18901  df-fbas 18902  df-fg 18903  df-top 19852  df-bases 19853  df-topon 19854  df-cld 19965  df-ntr 19966  df-cls 19967  df-nei 20045  df-lm 20176  df-haus 20262  df-fil 20792  df-fm 20884  df-flim 20885  df-flf 20886  df-cfil 22118  df-cau 22119  df-cmet 22120  df-grpo 25764  df-gid 25765  df-ginv 25766  df-gdiv 25767  df-ablo 25855  df-vc 26010  df-nv 26056  df-va 26059  df-ba 26060  df-sm 26061  df-0v 26062  df-vs 26063  df-nmcv 26064  df-ims 26065  df-ssp 26206  df-ph 26299  df-cbn 26350
This theorem is referenced by:  minvecolem5  26368
  Copyright terms: Public domain W3C validator