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

Theorem stoweidlem60 37191
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 10582 . . . . . . . . . . . . 13  |-  ( m  e.  NN  ->  m  e.  RR )
21adantl 464 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  RR )
3 stoweidlem60.17 . . . . . . . . . . . . . 14  |-  ( ph  ->  E  e.  RR+ )
43rpred 11303 . . . . . . . . . . . . 13  |-  ( ph  ->  E  e.  RR )
54adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  E  e.  RR )
63rpne0d 11308 . . . . . . . . . . . . 13  |-  ( ph  ->  E  =/=  0 )
76adantr 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  E  =/=  0 )
82, 5, 7redivcld 10412 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  ( m  /  E )  e.  RR )
9 1red 9640 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  1  e.  RR )
108, 9readdcld 9652 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( m  /  E )  +  1 )  e.  RR )
1110adantr 463 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  (
( m  /  E
)  +  1 )  e.  RR )
12 arch 10832 . . . . . . . . 9  |-  ( ( ( m  /  E
)  +  1 )  e.  RR  ->  E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n
)
1311, 12syl 17 . . . . . . . 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 1728 . . . . . . . . . . . . . . 15  |-  F/ t  m  e.  NN
1614, 15nfan 1956 . . . . . . . . . . . . . 14  |-  F/ t ( ph  /\  m  e.  NN )
17 nfra1 2784 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  T  ( F `  t )  <  m
1816, 17nfan 1956 . . . . . . . . . . . . 13  |-  F/ t ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )
19 nfv 1728 . . . . . . . . . . . . 13  |-  F/ t  n  e.  NN
2018, 19nfan 1956 . . . . . . . . . . . 12  |-  F/ t ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )
21 nfv 1728 . . . . . . . . . . . 12  |-  F/ t ( ( m  /  E )  +  1 )  <  n
2220, 21nfan 1956 . . . . . . . . . . 11  |-  F/ t ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )
23 simp-5l 770 . . . . . . . . . . . . . 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 36760 . . . . . . . . . . . . . . 15  |-  ( ph  ->  F : T --> RR )
2928fnvinran 36749 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR )
3023, 29sylancom 665 . . . . . . . . . . . . 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 771 . . . . . . . . . . . . . 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 10590 . . . . . . . . . . . . 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 761 . . . . . . . . . . . . . . . 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 10590 . . . . . . . . . . . . . . 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 9640 . . . . . . . . . . . . . . 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 10027 . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . 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 9653 . . . . . . . . . . . . 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 761 . . . . . . . . . . . . . 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 2772 . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  +  1 )  <  n )
43 simpl1 1000 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  ph )
44 simpl2 1001 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  NN )
4543, 44, 8syl2anc 659 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  /  E
)  e.  RR )
46 1red 9640 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
1  e.  RR )
47 simpl3 1002 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  NN )
4847nnred 10590 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  RR )
4945, 46, 48ltaddsubd 10191 . . . . . . . . . . . . . . . 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 1019 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  m  e.  RR )
5251adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  RR )
5348, 46resubcld 10027 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( n  -  1 )  e.  RR )
5443ad2ant1 1018 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  E  e.  RR )
5554adantr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  E  e.  RR )
563rpgt0d 11306 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  <  E )
5743, 56syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
0  <  E )
58 ltdivmul2 10459 . . . . . . . . . . . . . . . 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 1234 . . . . . . . . . . . . . . 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 1233 . . . . . . . . . . . . 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 9776 . . . . . . . . . . . 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 432 . . . . . . . . . . 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 2803 . . . . . . . . . 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 432 . . . . . . . . 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 2878 . . . . . . . 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 36771 . . . . . . 7  |-  ( ph  ->  E. m  e.  NN  A. t  e.  T  ( F `  t )  <  m )
7267, 71r19.29a 2948 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
73 df-rex 2759 . . . . . 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 459 . . . . . . . . 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 1956 . . . . . . . . . . 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 2402 . . . . . . . . . . 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 2402 . . . . . . . . . . 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 463 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  J  e. 
Comp )
82 stoweidlem60.10 . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  C )
8382adantr 463 . . . . . . . . . . 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 1223 . . . . . . . . . . 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 1223 . . . . . . . . . . 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 713 . . . . . . . . . . 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 713 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
9227adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  F  e.  C )
933adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  E  e.  RR+ )
94 stoweidlem60.18 . . . . . . . . . . . 12  |-  ( ph  ->  E  <  ( 1  /  3 ) )
9594adantr 463 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN )  ->  E  < 
( 1  /  3
) )
96 simpr 459 . . . . . . . . . . 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 37190 . . . . . . . . . 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 715 . . . . . . . . 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 1799 . . . . . . . . 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 662 . . . . . . . 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 978 . . . . . . . . 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 1688 . . . . . . . 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 432 . . . . . 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 1731 . . . . 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 455 . . . . . . . 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 1054 . . . . . . . 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 1004 . . . . . . . 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 1728 . . . . . . . . . 10  |-  F/ t  x : ( 0 ... n ) --> A
11114, 19, 110nf3an 1958 . . . . . . . . 9  |-  F/ t ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )
112 simp2 998 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  n  e.  NN )
113 simp3 999 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  x : ( 0 ... n ) --> A )
114 simp1 997 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  ph )
115114, 84syl3an1 1263 . . . . . . . . 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 1263 . . . . . . . . 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 1159 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A
)
11833ad2ant1 1018 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR+ )
119118rpred 11303 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR )
12082sselda 3441 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  A )  ->  f  e.  C )
12124, 25, 26, 120fcnre 36760 . . . . . . . . . 10  |-  ( (
ph  /\  f  e.  A )  ->  f : T --> RR )
1221213ad2antl1 1159 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A )  ->  f : T --> RR )
123111, 112, 113, 115, 116, 117, 119, 122stoweidlem17 37148 . . . . . . . 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 1230 . . . . . . 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 1728 . . . . . . . . 9  |-  F/ j
ph
126 nfv 1728 . . . . . . . . . 10  |-  F/ j ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
127 nfv 1728 . . . . . . . . . 10  |-  F/ j  x : ( 0 ... n ) --> A
128 nfra1 2784 . . . . . . . . . 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 1958 . . . . . . . . 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 1956 . . . . . . . 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 2784 . . . . . . . . . . 11  |-  F/ t A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E )
13219, 131nfan 1956 . . . . . . . . . 10  |-  F/ t ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
133 nfcv 2564 . . . . . . . . . . 11  |-  F/_ t
( 0 ... n
)
134 nfra1 2784 . . . . . . . . . . . 12  |-  F/ t A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )
135 nfra1 2784 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( D `  j ) ( ( x `  j ) `  t
)  <  ( E  /  n )
136 nfra1 2784 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( B `  j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t )
137134, 135, 136nf3an 1958 . . . . . . . . . . 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 2789 . . . . . . . . . 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 1958 . . . . . . . . 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 1956 . . . . . . . 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 2402 . . . . . . . 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 6578 . . . . . . . . . . 11  |-  ( J  e.  Comp  ->  U. J  e.  _V )
14369, 142syl 17 . . . . . . . . . 10  |-  ( ph  ->  U. J  e.  _V )
14425, 143syl5eqel 2494 . . . . . . . . 9  |-  ( ph  ->  T  e.  _V )
145144adantr 463 . . . . . . . 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 463 . . . . . . . 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 2772 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
149148adantlr 713 . . . . . . . 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 1055 . . . . . . . . 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 2772 . . . . . . . 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 463 . . . . . . . 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 463 . . . . . . . 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 752 . . . . . . . . 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 1040 . . . . . . . . 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 459 . . . . . . . . 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 997 . . . . . . . . . 10  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  ph )
158 ffvelrn 6006 . . . . . . . . . . 11  |-  ( ( x : ( 0 ... n ) --> A  /\  j  e.  ( 0 ... n ) )  ->  ( x `  j )  e.  A
)
1591583adant1 1015 . . . . . . . . . 10  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j )  e.  A )
16082sselda 3441 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j )  e.  C
)
16124, 25, 26, 160fcnre 36760 . . . . . . . . . 10  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j ) : T --> RR )
162157, 159, 161syl2anc 659 . . . . . . . . 9  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j ) : T --> RR )
163154, 155, 156, 162syl3anc 1230 . . . . . . . 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 1095 . . . . . . . . . 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 2935 . . . . . . . . . . 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 1012 . . . . . . . . . 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 455 . . . . . . . . . . . 12  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  0  <_  ( ( x `  j ) `  t
) )
168167ralimi 2796 . . . . . . . . . . 11  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  0  <_  ( ( x `  j
) `  t )
)
169168ralimi 2796 . . . . . . . . . 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 998 . . . . . . . . 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 999 . . . . . . . . 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 rspa 2770 . . . . . . . . . 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 )
)
174173r19.21bi 2772 . . . . . . . . 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 )
)
175170, 171, 172, 174syl21anc 1229 . . . . . . . 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
) )
176 simpr 459 . . . . . . . . . . . 12  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  (
( x `  j
) `  t )  <_  1 )
177176ralimi 2796 . . . . . . . . . . 11  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  ( (
x `  j ) `  t )  <_  1
)
178177ralimi 2796 . . . . . . . . . 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
)
179164, 166, 1783syl 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
)
180 rspa 2770 . . . . . . . . . 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 )
181180r19.21bi 2772 . . . . . . . . 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
)
182179, 171, 172, 181syl21anc 1229 . . . . . . . 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 )
183 simp1r3 1095 . . . . . . . . . 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 )
) )
184165simp2bi 1013 . . . . . . . . . 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
) )
185183, 184syl 17 . . . . . . . . 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 ) )
186 simp2 998 . . . . . . . . 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
) )
187 simp3 999 . . . . . . . . 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 ) )
188 rspa 2770 . . . . . . . . . 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 ) )
189188r19.21bi 2772 . . . . . . . . 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 ) )
190185, 186, 187, 189syl21anc 1229 . . . . . . . 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 ) )
191 simp1r3 1095 . . . . . . . . . 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 )
) )
192165simp3bi 1014 . . . . . . . . . 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
) )
193191, 192syl 17 . . . . . . . . 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 )
)
194 simp2 998 . . . . . . . . 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
) )
195 simp3 999 . . . . . . . . 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 ) )
196 rspa 2770 . . . . . . . . . 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 )
)
197196r19.21bi 2772 . . . . . . . . 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
) )
198193, 194, 195, 197syl21anc 1229 . . . . . . . 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
) )
19968, 130, 140, 77, 78, 141, 108, 145, 146, 149, 151, 152, 153, 163, 175, 182, 190, 198stoweidlem34 37165 . . . . . . 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 ) ) ) )
200 nfmpt1 4483 . . . . . . . . . 10  |-  F/_ t
( t  e.  T  |-> 
sum_ i  e.  ( 0 ... n ) ( E  x.  (
( x `  i
) `  t )
) )
201200nfeq2 2581 . . . . . . . . 9  |-  F/ t  g  =  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n
) ( E  x.  ( ( x `  i ) `  t
) ) )
202 fveq1 5847 . . . . . . . . . . . . 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 ) )
203202breq1d 4404 . . . . . . . . . . . 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 ) ) )
204202breq2d 4406 . . . . . . . . . . . 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
) ) )
205203, 204anbi12d 709 . . . . . . . . . . 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 ) ) ) )
206205anbi2d 702 . . . . . . . . . 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 ) ) ) ) )
207206rexbidv 2917 . . . . . . . . 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 ) ) ) ) )
208201, 207ralbid 2837 . . . . . . . 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 ) ) ) ) )
209208rspcev 3159 . . . . . . 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 ) ) ) )
210124, 199, 209syl2anc 659 . . . . . 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 ) ) ) )
211210ex 432 . . . . 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 ) ) ) ) )
2122112eximdv 1733 . . . 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 ) ) ) ) )
213106, 212mpd 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 )  /\  (
( j  -  (
4  /  3 ) )  x.  E )  <  ( g `  t ) ) ) )
214 idd 24 . . . 4  |-  ( ph  ->  ( 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
) ) )  ->  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 ) ) ) ) )
215214exlimdv 1745 . . 3  |-  ( ph  ->  ( E. n E. x E. g  e.  A  A. t  e.  T  E. j  e.  RR  ( ( ( ( j  -  ( 4  /