Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  stoweidlem60 Structured version   Unicode version

Theorem stoweidlem60 29993
Description: This lemma proves that there exists a function g as in the proof in [BrosowskiDeutsh] p. 91 (this parte of the proof actually spans through pages 91-92): g is in the subalgebra, and for all  t in  T, there is a  j such that (j-4/3)*ε < f(t) <= (j-1/3)*ε and (j-4/3)*ε < g(t) < (j+1/3)*ε. Here  F is used to represent f in the paper, and  E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem60.1  |-  F/_ t F
stoweidlem60.2  |-  F/ t
ph
stoweidlem60.3  |-  K  =  ( topGen `  ran  (,) )
stoweidlem60.4  |-  T  = 
U. J
stoweidlem60.5  |-  C  =  ( J  Cn  K
)
stoweidlem60.6  |-  D  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
stoweidlem60.7  |-  B  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
stoweidlem60.8  |-  ( ph  ->  J  e.  Comp )
stoweidlem60.9  |-  ( ph  ->  T  =/=  (/) )
stoweidlem60.10  |-  ( ph  ->  A  C_  C )
stoweidlem60.11  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
stoweidlem60.12  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
stoweidlem60.13  |-  ( (
ph  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A )
stoweidlem60.14  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
stoweidlem60.15  |-  ( ph  ->  F  e.  C )
stoweidlem60.16  |-  ( ph  ->  A. t  e.  T 
0  <_  ( F `  t ) )
stoweidlem60.17  |-  ( ph  ->  E  e.  RR+ )
stoweidlem60.18  |-  ( ph  ->  E  <  ( 1  /  3 ) )
Assertion
Ref Expression
stoweidlem60  |-  ( ph  ->  E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) ) )
Distinct variable groups:    f, g,
j, n, t, A, q, r    y, f, j, n, q, r, t, A    B, f,
g    D, f, g    f, E, g, j, n, t   
f, J, g, r, t    T, f, g, j, n, t    ph, f,
g, j, n    g, F, j, n    B, q, r, y    D, q, r, y    T, q, r, y    ph, q,
r, y    E, r,
y    t, K
Allowed substitution hints:    ph( t)    B( t, j, n)    C( y,
t, f, g, j, n, r, q)    D( t, j, n)    E( q)    F( y, t, f, r, q)    J( y, j, n, q)    K( y, f, g, j, n, r, q)

Proof of Theorem stoweidlem60
Dummy variables  i  x  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnre 10430 . . . . . . . . . . . . 13  |-  ( m  e.  NN  ->  m  e.  RR )
21adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  RR )
3 stoweidlem60.17 . . . . . . . . . . . . . 14  |-  ( ph  ->  E  e.  RR+ )
43rpred 11128 . . . . . . . . . . . . 13  |-  ( ph  ->  E  e.  RR )
54adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  E  e.  RR )
63rpne0d 11133 . . . . . . . . . . . . 13  |-  ( ph  ->  E  =/=  0 )
76adantr 465 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  E  =/=  0 )
82, 5, 7redivcld 10260 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  ( m  /  E )  e.  RR )
9 1red 9502 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  1  e.  RR )
108, 9readdcld 9514 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( m  /  E )  +  1 )  e.  RR )
1110adantr 465 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  (
( m  /  E
)  +  1 )  e.  RR )
12 arch 10677 . . . . . . . . 9  |-  ( ( ( m  /  E
)  +  1 )  e.  RR  ->  E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n
)
1311, 12syl 16 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n
)
14 stoweidlem60.2 . . . . . . . . . . . . . . 15  |-  F/ t
ph
15 nfv 1674 . . . . . . . . . . . . . . 15  |-  F/ t  m  e.  NN
1614, 15nfan 1863 . . . . . . . . . . . . . 14  |-  F/ t ( ph  /\  m  e.  NN )
17 nfra1 2875 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  T  ( F `  t )  <  m
1816, 17nfan 1863 . . . . . . . . . . . . 13  |-  F/ t ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )
19 nfv 1674 . . . . . . . . . . . . 13  |-  F/ t  n  e.  NN
2018, 19nfan 1863 . . . . . . . . . . . 12  |-  F/ t ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )
21 nfv 1674 . . . . . . . . . . . 12  |-  F/ t ( ( m  /  E )  +  1 )  <  n
2220, 21nfan 1863 . . . . . . . . . . 11  |-  F/ t ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )
23 simp-5l 767 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ph )
24 stoweidlem60.3 . . . . . . . . . . . . . . . 16  |-  K  =  ( topGen `  ran  (,) )
25 stoweidlem60.4 . . . . . . . . . . . . . . . 16  |-  T  = 
U. J
26 stoweidlem60.5 . . . . . . . . . . . . . . . 16  |-  C  =  ( J  Cn  K
)
27 stoweidlem60.15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  F  e.  C )
2824, 25, 26, 27fcnre 29885 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : T --> RR )
2928fnvinran 29874 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR )
3023, 29sylancom 667 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( F `  t
)  e.  RR )
31 simp-5r 768 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  m  e.  NN )
3231nnred 10438 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  m  e.  RR )
33 simpllr 758 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  n  e.  NN )
3433nnred 10438 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  n  e.  RR )
35 1red 9502 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  1  e.  RR )
3634, 35resubcld 9877 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( n  -  1 )  e.  RR )
3723, 4syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  E  e.  RR )
3836, 37remulcld 9515 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( ( n  - 
1 )  x.  E
)  e.  RR )
39 simpllr 758 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  A. t  e.  T  ( F `  t )  <  m )
4039r19.21bi 2910 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( F `  t
)  <  m )
41 simplr 754 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( ( m  /  E )  +  1 )  <  n )
42 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  +  1 )  <  n )
43 simpl1 991 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  ph )
44 simpl2 992 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  NN )
4543, 44, 8syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  /  E
)  e.  RR )
46 1red 9502 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
1  e.  RR )
47 simpl3 993 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  NN )
4847nnred 10438 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  RR )
4945, 46, 48ltaddsubd 10040 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( ( m  /  E )  +  1 )  <  n  <->  ( m  /  E )  <  ( n  - 
1 ) ) )
5042, 49mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  /  E
)  <  ( n  -  1 ) )
5113ad2ant2 1010 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  m  e.  RR )
5251adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  RR )
5348, 46resubcld 9877 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( n  -  1 )  e.  RR )
5443ad2ant1 1009 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  E  e.  RR )
5554adantr 465 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  E  e.  RR )
563rpgt0d 11131 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <  E )
5743, 56syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
0  <  E )
58 ltdivmul2 10308 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  RR  /\  ( n  -  1
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( (
m  /  E )  <  ( n  - 
1 )  <->  m  <  ( ( n  -  1 )  x.  E ) ) )
5952, 53, 55, 57, 58syl112anc 1223 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  <  (
n  -  1 )  <-> 
m  <  ( (
n  -  1 )  x.  E ) ) )
6050, 59mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  <  ( ( n  -  1 )  x.  E ) )
6123, 31, 33, 41, 60syl31anc 1222 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  m  <  ( ( n  -  1 )  x.  E ) )
6230, 32, 38, 40, 61lttrd 9633 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( F `  t
)  <  ( (
n  -  1 )  x.  E ) )
6362ex 434 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( t  e.  T  ->  ( F `  t
)  <  ( (
n  -  1 )  x.  E ) ) )
6422, 63ralrimi 2815 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
6564ex 434 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  /\  n  e.  NN )  ->  ( ( ( m  /  E )  +  1 )  <  n  ->  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) ) )
6665reximdva 2924 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  ( E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n  ->  E. n  e.  NN  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) ) )
6713, 66mpd 15 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  E. n  e.  NN  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )
68 stoweidlem60.1 . . . . . . . 8  |-  F/_ t F
69 stoweidlem60.8 . . . . . . . 8  |-  ( ph  ->  J  e.  Comp )
70 stoweidlem60.9 . . . . . . . 8  |-  ( ph  ->  T  =/=  (/) )
7168, 14, 24, 69, 25, 70, 26, 27rfcnnnub 29896 . . . . . . 7  |-  ( ph  ->  E. m  e.  NN  A. t  e.  T  ( F `  t )  <  m )
7267, 71r19.29a 2958 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
73 df-rex 2801 . . . . . 6  |-  ( E. n  e.  NN  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
)  <->  E. n ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) ) )
7472, 73sylib 196 . . . . 5  |-  ( ph  ->  E. n ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) ) )
75 simpr 461 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )  ->  (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) ) )
7614, 19nfan 1863 . . . . . . . . . . 11  |-  F/ t ( ph  /\  n  e.  NN )
77 stoweidlem60.6 . . . . . . . . . . 11  |-  D  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
78 stoweidlem60.7 . . . . . . . . . . 11  |-  B  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
79 eqid 2451 . . . . . . . . . . 11  |-  { y  e.  A  |  A. t  e.  T  (
0  <_  ( y `  t )  /\  (
y `  t )  <_  1 ) }  =  { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
80 eqid 2451 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... n )  |->  { y  e.  { y  e.  A  |  A. t  e.  T  ( 0  <_  ( y `  t )  /\  (
y `  t )  <_  1 ) }  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( y `  t ) ) } )  =  ( j  e.  ( 0 ... n )  |->  { y  e.  { y  e.  A  |  A. t  e.  T  ( 0  <_  ( y `  t )  /\  (
y `  t )  <_  1 ) }  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( y `  t ) ) } )
8169adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  J  e. 
Comp )
82 stoweidlem60.10 . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  C )
8382adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  A  C_  C )
84 stoweidlem60.11 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
85843adant1r 1212 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  +  ( g `
 t ) ) )  e.  A )
86 stoweidlem60.12 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
87863adant1r 1212 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) )  e.  A )
88 stoweidlem60.13 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A )
8988adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  RR )  ->  (
t  e.  T  |->  y )  e.  A )
90 stoweidlem60.14 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
9190adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
9227adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  F  e.  C )
933adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  E  e.  RR+ )
94 stoweidlem60.18 . . . . . . . . . . . 12  |-  ( ph  ->  E  <  ( 1  /  3 ) )
9594adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  E  < 
( 1  /  3
) )
96 simpr 461 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
9768, 76, 24, 25, 26, 77, 78, 79, 80, 81, 83, 85, 87, 89, 91, 92, 93, 95, 96stoweidlem59 29992 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  E. x
( x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n
) ( A. t  e.  T  ( 0  <_  ( ( x `
 j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) ) )
9897adantrr 716 . . . . . . . . 9  |-  ( (
ph  /\  ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )  ->  E. x
( x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n
) ( A. t  e.  T  ( 0  <_  ( ( x `
 j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) ) )
99 19.42v 1933 . . . . . . . . 9  |-  ( E. x ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )  /\  (
x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n
) ( A. t  e.  T  ( 0  <_  ( ( x `
 j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) ) )  <->  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  E. x ( x : ( 0 ... n
) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) ) )
10075, 98, 99sylanbrc 664 . . . . . . . 8  |-  ( (
ph  /\  ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )  ->  E. x
( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  /\  ( x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) ) )
101 3anass 969 . . . . . . . . 9  |-  ( ( ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) )  <-> 
( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  /\  ( x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) ) )
102101exbii 1635 . . . . . . . 8  |-  ( E. x ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) )  <->  E. x ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )  /\  (
x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n
) ( A. t  e.  T  ( 0  <_  ( ( x `
 j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) ) ) )
103100, 102sylibr 212 . . . . . . 7  |-  ( (
ph  /\  ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )  ->  E. x
( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n
) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )
104103ex 434 . . . . . 6  |-  ( ph  ->  ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  ->  E. x
( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n
) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) ) )
105104eximdv 1677 . . . . 5  |-  ( ph  ->  ( E. n ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  ->  E. n E. x ( ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) ) )
10674, 105mpd 15 . . . 4  |-  ( ph  ->  E. n E. x
( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n
) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )
107 simpl 457 . . . . . . . 8  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  ph )
108 simpr1l 1045 . . . . . . . 8  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  n  e.  NN )
109 simpr2 995 . . . . . . . 8  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  x :
( 0 ... n
) --> A )
110 nfv 1674 . . . . . . . . . 10  |-  F/ t  x : ( 0 ... n ) --> A
11114, 19, 110nf3an 1865 . . . . . . . . 9  |-  F/ t ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )
112 simp2 989 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  n  e.  NN )
113 simp3 990 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  x : ( 0 ... n ) --> A )
114 simp1 988 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  ph )
115114, 84syl3an1 1252 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A
)
116114, 86syl3an1 1252 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  x.  (
g `  t )
) )  e.  A
)
117883ad2antl1 1150 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A
)
11833ad2ant1 1009 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR+ )
119118rpred 11128 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR )
12082sselda 3454 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  A )  ->  f  e.  C )
12124, 25, 26, 120fcnre 29885 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  A )  ->  f : T --> RR )
1221213ad2antl1 1150 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A )  ->  f : T --> RR )
123111, 112, 113, 115, 116, 117, 119, 122stoweidlem17 29950 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) )  e.  A )
124107, 108, 109, 123syl3anc 1219 . . . . . . 7  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n
) ( E  x.  ( ( x `  i ) `  t
) ) )  e.  A )
125 nfv 1674 . . . . . . . . 9  |-  F/ j
ph
126 nfv 1674 . . . . . . . . . 10  |-  F/ j ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
127 nfv 1674 . . . . . . . . . 10  |-  F/ j  x : ( 0 ... n ) --> A
128 nfra1 2875 . . . . . . . . . 10  |-  F/ j A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_ 
( ( x `  j ) `  t
)  /\  ( (
x `  j ) `  t )  <_  1
)  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) )
129126, 127, 128nf3an 1865 . . . . . . . . 9  |-  F/ j ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n
) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) )
130125, 129nfan 1863 . . . . . . . 8  |-  F/ j ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )
131 nfra1 2875 . . . . . . . . . . 11  |-  F/ t A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E )
13219, 131nfan 1863 . . . . . . . . . 10  |-  F/ t ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
133 nfcv 2613 . . . . . . . . . . 11  |-  F/_ t
( 0 ... n
)
134 nfra1 2875 . . . . . . . . . . . 12  |-  F/ t A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )
135 nfra1 2875 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( D `  j ) ( ( x `  j ) `  t
)  <  ( E  /  n )
136 nfra1 2875 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( B `  j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t )
137134, 135, 136nf3an 1865 . . . . . . . . . . 11  |-  F/ t ( A. t  e.  T  ( 0  <_ 
( ( x `  j ) `  t
)  /\  ( (
x `  j ) `  t )  <_  1
)  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) )
138133, 137nfral 2878 . . . . . . . . . 10  |-  F/ t A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_ 
( ( x `  j ) `  t
)  /\  ( (
x `  j ) `  t )  <_  1
)  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) )
139132, 110, 138nf3an 1865 . . . . . . . . 9  |-  F/ t ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n
) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) )
14014, 139nfan 1863 . . . . . . . 8  |-  F/ t ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )
141 eqid 2451 . . . . . . . 8  |-  ( t  e.  T  |->  { j  e.  ( 1 ... n )  |  t  e.  ( D `  j ) } )  =  ( t  e.  T  |->  { j  e.  ( 1 ... n
)  |  t  e.  ( D `  j
) } )
142 uniexg 6477 . . . . . . . . . . 11  |-  ( J  e.  Comp  ->  U. J  e.  _V )
14369, 142syl 16 . . . . . . . . . 10  |-  ( ph  ->  U. J  e.  _V )
14425, 143syl5eqel 2543 . . . . . . . . 9  |-  ( ph  ->  T  e.  _V )
145144adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  T  e.  _V )
14628adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  F : T
--> RR )
147 stoweidlem60.16 . . . . . . . . . 10  |-  ( ph  ->  A. t  e.  T 
0  <_  ( F `  t ) )
148147r19.21bi 2910 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
149148adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
150 simpr1r 1046 . . . . . . . . 9  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )
151150r19.21bi 2910 . . . . . . . 8  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  t  e.  T )  ->  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )
1523adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  E  e.  RR+ )
15394adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  E  <  ( 1  /  3 ) )
154 simpll 753 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
) )  ->  ph )
155 simplr2 1031 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
) )  ->  x : ( 0 ... n ) --> A )
156 simpr 461 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
) )  ->  j  e.  ( 0 ... n
) )
157 simp1 988 . . . . . . . . . 10  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  ph )
158 ffvelrn 5940 . . . . . . . . . . 11  |-  ( ( x : ( 0 ... n ) --> A  /\  j  e.  ( 0 ... n ) )  ->  ( x `  j )  e.  A
)
1591583adant1 1006 . . . . . . . . . 10  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j )  e.  A )
16082sselda 3454 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j )  e.  C
)
16124, 25, 26, 160fcnre 29885 . . . . . . . . . 10  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j ) : T --> RR )
162157, 159, 161syl2anc 661 . . . . . . . . 9  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j ) : T --> RR )
163154, 155, 156, 162syl3anc 1219 . . . . . . . 8  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j ) : T --> RR )
164 simp1r3 1086 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  T )  ->  A. j  e.  ( 0 ... n
) ( A. t  e.  T  ( 0  <_  ( ( x `
 j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) )
165 r19.26-3 2947 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) )  <->  ( A. j  e.  ( 0 ... n ) A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. j  e.  ( 0 ... n ) A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. j  e.  ( 0 ... n
) A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) )
166165simp1bi 1003 . . . . . . . . . 10  |-  ( A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) )  ->  A. j  e.  (
0 ... n ) A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 ) )
167 simpl 457 . . . . . . . . . . . 12  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  0  <_  ( ( x `  j ) `  t
) )
168167ralimi 2811 . . . . . . . . . . 11  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  0  <_  ( ( x `  j
) `  t )
)
169168ralimi 2811 . . . . . . . . . 10  |-  ( A. j  e.  ( 0 ... n ) A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. j  e.  ( 0 ... n
) A. t  e.  T  0  <_  (
( x `  j
) `  t )
)
170164, 166, 1693syl 20 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  T )  ->  A. j  e.  ( 0 ... n
) A. t  e.  T  0  <_  (
( x `  j
) `  t )
)
171 simp2 989 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  T )  ->  j  e.  ( 0 ... n
) )
172 simp3 990 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  T )  ->  t  e.  T )
173 rsp 2884 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... n ) A. t  e.  T  0  <_  ( ( x `  j ) `  t
)  ->  ( j  e.  ( 0 ... n
)  ->  A. t  e.  T  0  <_  ( ( x `  j
) `  t )
) )
174173imp 429 . . . . . . . . . 10  |-  ( ( A. j  e.  ( 0 ... n ) A. t  e.  T 
0  <_  ( (
x `  j ) `  t )  /\  j  e.  ( 0 ... n
) )  ->  A. t  e.  T  0  <_  ( ( x `  j
) `  t )
)
175174r19.21bi 2910 . . . . . . . . 9  |-  ( ( ( A. j  e.  ( 0 ... n
) A. t  e.  T  0  <_  (
( x `  j
) `  t )  /\  j  e.  (
0 ... n ) )  /\  t  e.  T
)  ->  0  <_  ( ( x `  j
) `  t )
)
176170, 171, 172, 175syl21anc 1218 . . . . . . . 8  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  T )  ->  0  <_  ( ( x `  j ) `  t
) )
177 simpr 461 . . . . . . . . . . . 12  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  (
( x `  j
) `  t )  <_  1 )
178177ralimi 2811 . . . . . . . . . . 11  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  ( (
x `  j ) `  t )  <_  1
)
179178ralimi 2811 . . . . . . . . . 10  |-  ( A. j  e.  ( 0 ... n ) A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. j  e.  ( 0 ... n
) A. t  e.  T  ( ( x `
 j ) `  t )  <_  1
)
180164, 166, 1793syl 20 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  T )  ->  A. j  e.  ( 0 ... n
) A. t  e.  T  ( ( x `
 j ) `  t )  <_  1
)
181 rsp 2884 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... n ) A. t  e.  T  (
( x `  j
) `  t )  <_  1  ->  ( j  e.  ( 0 ... n
)  ->  A. t  e.  T  ( (
x `  j ) `  t )  <_  1
) )
182181imp 429 . . . . . . . . . 10  |-  ( ( A. j  e.  ( 0 ... n ) A. t  e.  T  ( ( x `  j ) `  t
)  <_  1  /\  j  e.  ( 0 ... n ) )  ->  A. t  e.  T  ( ( x `  j ) `  t
)  <_  1 )
183182r19.21bi 2910 . . . . . . . . 9  |-  ( ( ( A. j  e.  ( 0 ... n
) A. t  e.  T  ( ( x `
 j ) `  t )  <_  1  /\  j  e.  (
0 ... n ) )  /\  t  e.  T
)  ->  ( (
x `  j ) `  t )  <_  1
)
184180, 171, 172, 183syl21anc 1218 . . . . . . . 8  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  T )  ->  (
( x `  j
) `  t )  <_  1 )
185 simp1r3 1086 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( D `  j ) )  ->  A. j  e.  ( 0 ... n
) ( A. t  e.  T  ( 0  <_  ( ( x `
 j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) )
186165simp2bi 1004 . . . . . . . . . 10  |-  ( A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) )  ->  A. j  e.  (
0 ... n ) A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
) )
187185, 186syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( D `  j ) )  ->  A. j  e.  ( 0 ... n
) A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n ) )
188 simp2 989 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( D `  j ) )  ->  j  e.  ( 0 ... n
) )
189 simp3 990 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( D `  j ) )  ->  t  e.  ( D `  j ) )
190 rsp 2884 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... n ) A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  ->  ( j  e.  ( 0 ... n
)  ->  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n ) ) )
191190imp 429 . . . . . . . . . 10  |-  ( ( A. j  e.  ( 0 ... n ) A. t  e.  ( D `  j ) ( ( x `  j ) `  t
)  <  ( E  /  n )  /\  j  e.  ( 0 ... n
) )  ->  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n ) )
192191r19.21bi 2910 . . . . . . . . 9  |-  ( ( ( A. j  e.  ( 0 ... n
) A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  j  e.  ( 0 ... n ) )  /\  t  e.  ( D `  j ) )  ->  ( (
x `  j ) `  t )  <  ( E  /  n ) )
193187, 188, 189, 192syl21anc 1218 . . . . . . . 8  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( D `  j ) )  ->  ( (
x `  j ) `  t )  <  ( E  /  n ) )
194 simp1r3 1086 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( B `  j ) )  ->  A. j  e.  ( 0 ... n
) ( A. t  e.  T  ( 0  <_  ( ( x `
 j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( x `  j ) `
 t )  < 
( E  /  n
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) )
195165simp3bi 1005 . . . . . . . . . 10  |-  ( A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) )  ->  A. j  e.  (
0 ... n ) A. t  e.  ( B `  j ) ( 1  -  ( E  /  n ) )  < 
( ( x `  j ) `  t
) )
196194, 195syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( B `  j ) )  ->  A. j  e.  ( 0 ... n
) A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
)
197 simp2 989 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( B `  j ) )  ->  j  e.  ( 0 ... n
) )
198 simp3 990 . . . . . . . . 9  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( B `  j ) )  ->  t  e.  ( B `  j ) )
199 rsp 2884 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... n ) A. t  e.  ( B `  j ) ( 1  -  ( E  /  n ) )  < 
( ( x `  j ) `  t
)  ->  ( j  e.  ( 0 ... n
)  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
) )
200199imp 429 . . . . . . . . . 10  |-  ( ( A. j  e.  ( 0 ... n ) A. t  e.  ( B `  j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t )  /\  j  e.  ( 0 ... n
) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )
)
201200r19.21bi 2910 . . . . . . . . 9  |-  ( ( ( A. j  e.  ( 0 ... n
) A. t  e.  ( B `  j
) ( 1  -  ( E  /  n
) )  <  (
( x `  j
) `  t )  /\  j  e.  (
0 ... n ) )  /\  t  e.  ( B `  j ) )  ->  ( 1  -  ( E  /  n ) )  < 
( ( x `  j ) `  t
) )
202196, 197, 198, 201syl21anc 1218 . . . . . . . 8  |-  ( ( ( ph  /\  (
( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  /\  j  e.  ( 0 ... n
)  /\  t  e.  ( B `  j ) )  ->  ( 1  -  ( E  /  n ) )  < 
( ( x `  j ) `  t
) )
20368, 130, 140, 77, 78, 141, 108, 145, 146, 149, 151, 152, 153, 163, 176, 184, 193, 202stoweidlem34 29967 . . . . . . 7  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  (
4  /  3 ) )  x.  E )  <  ( F `  t )  /\  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) )  /\  (
( ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) ) `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) ) `  t ) ) ) )
204 nfmpt1 4479 . . . . . . . . . 10  |-  F/_ t
( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )
205204nfeq2 2629 . . . . . . . . 9  |-  F/ t  g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n
) ( E  x.  ( ( x `  i ) `  t
) ) )
206 fveq1 5788 . . . . . . . . . . . . 13  |-  ( g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  ->  (
g `  t )  =  ( ( t  e.  T  |->  sum_ i  e.  ( 0 ... n
) ( E  x.  ( ( x `  i ) `  t
) ) ) `  t ) )
207206breq1d 4400 . . . . . . . . . . . 12  |-  ( g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  ->  (
( g `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  <->  ( (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) ) `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) ) )
208206breq2d 4402 . . . . . . . . . . . 12  |-  ( g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  ->  (
( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( g `  t )  <->  ( (
j  -  ( 4  /  3 ) )  x.  E )  < 
( ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) ) `  t
) ) )
209207, 208anbi12d 710 . . . . . . . . . . 11  |-  ( g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  ->  (
( ( g `  t )  <  (
( j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  -  ( 4  / 
3 ) )  x.  E )  <  (
g `  t )
)  <->  ( ( ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) ) `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( ( t  e.  T  |->  sum_ i  e.  ( 0 ... n
) ( E  x.  ( ( x `  i ) `  t
) ) ) `  t ) ) ) )
210209anbi2d 703 . . . . . . . . . 10  |-  ( g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  ->  (
( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) )  <-> 
( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( ( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) ) `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) ) `  t ) ) ) ) )
211210rexbidv 2844 . . . . . . . . 9  |-  ( g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  ->  ( E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) )  <->  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( ( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) ) `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) ) `  t ) ) ) ) )
212205, 211ralbid 2836 . . . . . . . 8  |-  ( g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  ->  ( A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) )  <->  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( ( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) ) `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) ) `  t ) ) ) ) )
213212rspcev 3169 . . . . . . 7  |-  ( ( ( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )  e.  A  /\  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( ( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) ) `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) ) `  t ) ) ) )  ->  E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) ) )
214124, 203, 213syl2anc 661 . . . . . 6  |-  ( (
ph  /\  ( (
n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) ) )  ->  E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  (
4  /  3 ) )  x.  E )  <  ( F `  t )  /\  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) )  /\  (
( g `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( g `  t ) ) ) )
215214ex 434 . . . . 5  |-  ( ph  ->  ( ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) )  ->  E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) ) ) )
2162152eximdv 1679 . . . 4  |-  ( ph  ->  ( E. n E. x ( ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )  /\  x : ( 0 ... n ) --> A  /\  A. j  e.  ( 0 ... n ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  n )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t ) ) )  ->  E. n E. x E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) ) ) )
217106, 216mpd 15 . . 3  |-  ( ph  ->  E. n E. x E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
)  /\  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )  /\  ( ( g `  t )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E )