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

Theorem stoweidlem60 27676
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 stoweidlem60.1 . . . . . . . 8  |-  F/_ t F
2 stoweidlem60.2 . . . . . . . 8  |-  F/ t
ph
3 stoweidlem60.3 . . . . . . . 8  |-  K  =  ( topGen `  ran  (,) )
4 stoweidlem60.8 . . . . . . . 8  |-  ( ph  ->  J  e.  Comp )
5 stoweidlem60.4 . . . . . . . 8  |-  T  = 
U. J
6 stoweidlem60.9 . . . . . . . 8  |-  ( ph  ->  T  =/=  (/) )
7 stoweidlem60.5 . . . . . . . 8  |-  C  =  ( J  Cn  K
)
8 stoweidlem60.15 . . . . . . . 8  |-  ( ph  ->  F  e.  C )
91, 2, 3, 4, 5, 6, 7, 8rfcnnnub 27574 . . . . . . 7  |-  ( ph  ->  E. m  e.  NN  A. t  e.  T  ( F `  t )  <  m )
10 nnre 9963 . . . . . . . . . . . . . . 15  |-  ( m  e.  NN  ->  m  e.  RR )
1110adantl 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  RR )
12 stoweidlem60.17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  e.  RR+ )
1312rpred 10604 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  e.  RR )
1413adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  E  e.  RR )
1512rpne0d 10609 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  =/=  0 )
1615adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  E  =/=  0 )
1711, 14, 16redivcld 9798 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  NN )  ->  ( m  /  E )  e.  RR )
18 1re 9046 . . . . . . . . . . . . . 14  |-  1  e.  RR
1918a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  NN )  ->  1  e.  RR )
2017, 19readdcld 9071 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( m  /  E )  +  1 )  e.  RR )
2120adantr 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  (
( m  /  E
)  +  1 )  e.  RR )
22 arch 10174 . . . . . . . . . . 11  |-  ( ( ( m  /  E
)  +  1 )  e.  RR  ->  E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n
)
2321, 22syl 16 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n
)
24 nfv 1626 . . . . . . . . . . . . . . . . 17  |-  F/ t  m  e.  NN
252, 24nfan 1842 . . . . . . . . . . . . . . . 16  |-  F/ t ( ph  /\  m  e.  NN )
26 nfra1 2716 . . . . . . . . . . . . . . . 16  |-  F/ t A. t  e.  T  ( F `  t )  <  m
2725, 26nfan 1842 . . . . . . . . . . . . . . 15  |-  F/ t ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )
28 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ t  n  e.  NN
2927, 28nfan 1842 . . . . . . . . . . . . . 14  |-  F/ t ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )
30 nfv 1626 . . . . . . . . . . . . . 14  |-  F/ t ( ( m  /  E )  +  1 )  <  n
3129, 30nfan 1842 . . . . . . . . . . . . 13  |-  F/ t ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )
32 simp-5l 745 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ph )
333, 5, 7, 8fcnre 27563 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  F : T --> RR )
3433fnvinran 27552 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR )
3532, 34sylancom 649 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 )
36 simp-5r 746 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  m  e.  NN )
3736nnred 9971 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  m  e.  RR )
38 simpllr 736 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  n  e.  NN )
3938nnred 9971 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  n  e.  RR )
4018a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  1  e.  RR )
4139, 40resubcld 9421 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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 )
4232, 13syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  E  e.  RR )
4341, 42remulcld 9072 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 )
44 simpllr 736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( 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 )
4544r19.21bi 2764 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( F `  t
)  <  m )
46 simplr 732 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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 )
47 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  +  1 )  <  n )
48 simpl1 960 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  ph )
49 simpl2 961 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  NN )
5048, 49, 17syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  /  E
)  e.  RR )
5118a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
1  e.  RR )
52 simpl3 962 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  NN )
5352nnred 9971 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  RR )
5450, 51, 53ltaddsubd 9582 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( ( m  /  E )  +  1 )  <  n  <->  ( m  /  E )  <  ( n  - 
1 ) ) )
5547, 54mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  /  E
)  <  ( n  -  1 ) )
56103ad2ant2 979 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  m  e.  RR )
5756adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  RR )
5853, 51resubcld 9421 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( n  -  1 )  e.  RR )
59133ad2ant1 978 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  E  e.  RR )
6059adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  E  e.  RR )
6112rpgt0d 10607 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <  E )
6248, 61syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
0  <  E )
63 ltdivmul2 9841 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  e.  RR  /\  ( n  -  1
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( (
m  /  E )  <  ( n  - 
1 )  <->  m  <  ( ( n  -  1 )  x.  E ) ) )
6457, 58, 60, 62, 63syl112anc 1188 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  <  (
n  -  1 )  <-> 
m  <  ( (
n  -  1 )  x.  E ) ) )
6555, 64mpbid 202 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  <  ( ( n  -  1 )  x.  E ) )
6632, 36, 38, 46, 65syl31anc 1187 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 ) )
6735, 37, 43, 45, 66lttrd 9187 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
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 ) )
6867ex 424 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 ) ) )
6931, 68ralrimi 2747 . . . . . . . . . . . 12  |-  ( ( ( ( ( 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 ) )
7069ex 424 . . . . . . . . . . 11  |-  ( ( ( ( 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 ) ) )
7170reximdva 2778 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
7223, 71mpd 15 . . . . . . . . 9  |-  ( ( ( 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 ) )
7372ex 424 . . . . . . . 8  |-  ( (
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 ) ) )
7473rexlimdva 2790 . . . . . . 7  |-  ( ph  ->  ( E. m  e.  NN  A. t  e.  T  ( F `  t )  <  m  ->  E. n  e.  NN  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) ) )
759, 74mpd 15 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
76 df-rex 2672 . . . . . 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
) ) )
7775, 76sylib 189 . . . . 5  |-  ( ph  ->  E. n ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) ) )
78 simpr 448 . . . . . . . . 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 ) ) )
792, 28nfan 1842 . . . . . . . . . . 11  |-  F/ t ( ph  /\  n  e.  NN )
80 stoweidlem60.6 . . . . . . . . . . 11  |-  D  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
81 stoweidlem60.7 . . . . . . . . . . 11  |-  B  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
82 eqid 2404 . . . . . . . . . . 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 ) }
83 eqid 2404 . . . . . . . . . . 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 ) ) } )
844adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  J  e. 
Comp )
85 stoweidlem60.10 . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  C )
8685adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  A  C_  C )
87 stoweidlem60.11 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
88873adant1r 1177 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  +  ( g `
 t ) ) )  e.  A )
89 stoweidlem60.12 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
90893adant1r 1177 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) )  e.  A )
91 stoweidlem60.13 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A )
9291adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  RR )  ->  (
t  e.  T  |->  y )  e.  A )
93 stoweidlem60.14 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
9493adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
958adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  F  e.  C )
9612adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  E  e.  RR+ )
97 stoweidlem60.18 . . . . . . . . . . . 12  |-  ( ph  ->  E  <  ( 1  /  3 ) )
9897adantr 452 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  E  < 
( 1  /  3
) )
99 simpr 448 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
1001, 79, 3, 5, 7, 80, 81, 82, 83, 84, 86, 88, 90, 92, 94, 95, 96, 98, 99stoweidlem59 27675 . . . . . . . . . 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 )
) ) )
101100adantrr 698 . . . . . . . . 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 )
) ) )
102 19.42v 1924 . . . . . . . . 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 ) ) ) ) )
10378, 101, 102sylanbrc 646 . . . . . . . 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 ) ) ) ) )
104 3anass 940 . . . . . . . . 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 ) ) ) ) )
105104exbii 1589 . . . . . . . 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 )
) ) ) )
106103, 105sylibr 204 . . . . . . 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 ) ) ) )
107106ex 424 . . . . . 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 ) ) ) ) )
108107eximdv 1629 . . . . 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 ) ) ) ) )
10977, 108mpd 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 ) ) ) )
110 simpl 444 . . . . . . . 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 )
111 simpr1l 1014 . . . . . . . 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 )
112 simpr2 964 . . . . . . . 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 )
113 nfv 1626 . . . . . . . . . 10  |-  F/ t  x : ( 0 ... n ) --> A
1142, 28, 113nf3an 1845 . . . . . . . . 9  |-  F/ t ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )
115 simp2 958 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  n  e.  NN )
116 simp3 959 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  x : ( 0 ... n ) --> A )
117 simp1 957 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  ph )
118117, 87syl3an1 1217 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A
)
119117, 89syl3an1 1217 . . . . . . . . 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
)
120913ad2antl1 1119 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A
)
121123ad2ant1 978 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR+ )
122121rpred 10604 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR )
12385sselda 3308 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  A )  ->  f  e.  C )
1243, 5, 7, 123fcnre 27563 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  A )  ->  f : T --> RR )
1251243ad2antl1 1119 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A )  ->  f : T --> RR )
126114, 115, 116, 118, 119, 120, 122, 125stoweidlem17 27633 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) )  e.  A )
127110, 111, 112, 126syl3anc 1184 . . . . . . 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 )
128 nfv 1626 . . . . . . . . 9  |-  F/ j
ph
129 nfv 1626 . . . . . . . . . 10  |-  F/ j ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
130 nfv 1626 . . . . . . . . . 10  |-  F/ j  x : ( 0 ... n ) --> A
131 nfra1 2716 . . . . . . . . . 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 ) )
132129, 130, 131nf3an 1845 . . . . . . . . 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 ) ) )
133128, 132nfan 1842 . . . . . . . 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 ) ) ) )
134 nfra1 2716 . . . . . . . . . . 11  |-  F/ t A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E )
13528, 134nfan 1842 . . . . . . . . . 10  |-  F/ t ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
136 nfcv 2540 . . . . . . . . . . 11  |-  F/_ t
( 0 ... n
)
137 nfra1 2716 . . . . . . . . . . . 12  |-  F/ t A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )
138 nfra1 2716 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( D `  j ) ( ( x `  j ) `  t
)  <  ( E  /  n )
139 nfra1 2716 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( B `  j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t )
140137, 138, 139nf3an 1845 . . . . . . . . . . 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 ) )
141136, 140nfral 2719 . . . . . . . . . 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 ) )
142135, 113, 141nf3an 1845 . . . . . . . . 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 ) ) )
1432, 142nfan 1842 . . . . . . . 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 ) ) ) )
144 eqid 2404 . . . . . . . 8  |-  ( t  e.  T  |->  { j  e.  ( 1 ... n )  |  t  e.  ( D `  j ) } )  =  ( t  e.  T  |->  { j  e.  ( 1 ... n
)  |  t  e.  ( D `  j
) } )
145 uniexg 4665 . . . . . . . . . . 11  |-  ( J  e.  Comp  ->  U. J  e.  _V )
1464, 145syl 16 . . . . . . . . . 10  |-  ( ph  ->  U. J  e.  _V )
1475, 146syl5eqel 2488 . . . . . . . . 9  |-  ( ph  ->  T  e.  _V )
148147adantr 452 . . . . . . . 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 )
14933adantr 452 . . . . . . . 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 )
150 stoweidlem60.16 . . . . . . . . . 10  |-  ( ph  ->  A. t  e.  T 
0  <_  ( F `  t ) )
151150r19.21bi 2764 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
152151adantlr 696 . . . . . . . 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
) )
153 simpr1r 1015 . . . . . . . . 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 ) )
154153r19.21bi 2764 . . . . . . . 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
) )
15512adantr 452 . . . . . . . 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+ )
15697adantr 452 . . . . . . . 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 ) )
157 simpll 731 . . . . . . . . 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 )
158 simplr2 1000 . . . . . . . . 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 )
159 simpr 448 . . . . . . . . 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
) )
160 simp1 957 . . . . . . . . . 10  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  ph )
161 ffvelrn 5827 . . . . . . . . . . 11  |-  ( ( x : ( 0 ... n ) --> A  /\  j  e.  ( 0 ... n ) )  ->  ( x `  j )  e.  A
)
1621613adant1 975 . . . . . . . . . 10  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j )  e.  A )
16385sselda 3308 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j )  e.  C
)
1643, 5, 7, 163fcnre 27563 . . . . . . . . . 10  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j ) : T --> RR )
165160, 162, 164syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j ) : T --> RR )
166157, 158, 159, 165syl3anc 1184 . . . . . . . 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 )
167 simp1r3 1055 . . . . . . . . . 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 )
) )
168 r19.26-3 2800 . . . . . . . . . . 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 )
) )
169168simp1bi 972 . . . . . . . . . 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 ) )
170 simpl 444 . . . . . . . . . . . 12  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  0  <_  ( ( x `  j ) `  t
) )
171170ralimi 2741 . . . . . . . . . . 11  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  0  <_  ( ( x `  j
) `  t )
)
172171ralimi 2741 . . . . . . . . . 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 )
)
173167, 169, 1723syl 19 . . . . . . . . 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 )
)
174 simp2 958 . . . . . . . . 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
) )
175 simp3 959 . . . . . . . . 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 )
176 rsp 2726 . . . . . . . . . . 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 )
) )
177176imp 419 . . . . . . . . . 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 )
)
178177r19.21bi 2764 . . . . . . . . 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 )
)
179173, 174, 175, 178syl21anc 1183 . . . . . . . 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
) )
180 simpr 448 . . . . . . . . . . . 12  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  (
( x `  j
) `  t )  <_  1 )
181180ralimi 2741 . . . . . . . . . . 11  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  ( (
x `  j ) `  t )  <_  1
)
182181ralimi 2741 . . . . . . . . . 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
)
183167, 169, 1823syl 19 . . . . . . . . 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
)
184 rsp 2726 . . . . . . . . . . 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
) )
185184imp 419 . . . . . . . . . 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 )
186185r19.21bi 2764 . . . . . . . . 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
)
187183, 174, 175, 186syl21anc 1183 . . . . . . . 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 )
188 simp1r3 1055 . . . . . . . . . 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 )
) )
189168simp2bi 973 . . . . . . . . . 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
) )
190188, 189syl 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 ) )
191 simp2 958 . . . . . . . . 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
) )
192 simp3 959 . . . . . . . . 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 ) )
193 rsp 2726 . . . . . . . . . . 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 ) ) )
194193imp 419 . . . . . . . . . 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 ) )
195194r19.21bi 2764 . . . . . . . . 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 ) )
196190, 191, 192, 195syl21anc 1183 . . . . . . . 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 ) )
197 simp1r3 1055 . . . . . . . . . 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 )
) )
198168simp3bi 974 . . . . . . . . . 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
) )
199197, 198syl 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 )
)
200 simp2 958 . . . . . . . . 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
) )
201 simp3 959 . . . . . . . . 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 ) )
202 rsp 2726 . . . . . . . . . . 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 )
) )
203202imp 419 . . . . . . . . . 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 )
)
204203r19.21bi 2764 . . . . . . . . 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
) )
205199, 200, 201, 204syl21anc 1183 . . . . . . . 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
) )
2061, 133, 143, 80, 81, 144, 111, 148, 149, 152, 154, 155, 156, 166, 179, 187, 196, 205stoweidlem34 27650 . . . . . . 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 ) ) ) )
207 nfmpt1 4258 . . . . . . . . . 10  |-  F/_ t
( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )
208207nfeq2 2551 . . . . . . . . 9  |-  F/ t  g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n
) ( E  x.  ( ( x `  i ) `  t
) ) )
209 fveq1 5686 . . . . . . . . . . . . 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 ) )
210209breq1d 4182 . . . . . . . . . . . 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 ) ) )
211209breq2d 4184 . . . . . . . . . . . 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
) ) )
212210, 211anbi12d 692 . . . . . . . . . . 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 ) ) ) )
213212anbi2d 685 . . . . . . . . . 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 ) ) ) ) )
214213rexbidv 2687 . . . . . . . . 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 ) ) ) ) )
215208, 214ralbid 2684 . . . . . . . 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 ) ) ) ) )
216215rspcev 3012 . . . . . . 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 ) ) ) )
217127, 206, 216syl2anc 643 . . . . . 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 ) ) ) )
218217ex 424 . . . . 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 ) ) ) ) )
2192182eximdv 1631 . . . 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 ) )