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

Theorem stoweidlem60 27911
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 27809 . . . . . . 7  |-  ( ph  ->  E. m  e.  NN  A. t  e.  T  ( F `  t )  <  m )
10 simpl 443 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  ( ph  /\  m  e.  NN ) )
11 nnre 9769 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  NN  ->  m  e.  RR )
1211adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  RR )
13 stoweidlem60.17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  E  e.  RR+ )
14 rpre 10376 . . . . . . . . . . . . . . . . . . 19  |-  ( E  e.  RR+  ->  E  e.  RR )
1513, 14syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  e.  RR )
1615adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  NN )  ->  E  e.  RR )
17 rpne0 10385 . . . . . . . . . . . . . . . . . . 19  |-  ( E  e.  RR+  ->  E  =/=  0 )
1813, 17syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  E  =/=  0 )
1918adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  NN )  ->  E  =/=  0 )
2012, 16, 193jca 1132 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  NN )  ->  ( m  e.  RR  /\  E  e.  RR  /\  E  =/=  0 ) )
21 redivcl 9495 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  RR  /\  E  e.  RR  /\  E  =/=  0 )  ->  (
m  /  E )  e.  RR )
2220, 21syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  NN )  ->  ( m  /  E )  e.  RR )
23 1re 8853 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
2423a1i 10 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  NN )  ->  1  e.  RR )
2522, 24jca 518 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( m  /  E )  e.  RR  /\  1  e.  RR ) )
26 readdcl 8836 . . . . . . . . . . . . . 14  |-  ( ( ( m  /  E
)  e.  RR  /\  1  e.  RR )  ->  ( ( m  /  E )  +  1 )  e.  RR )
2725, 26syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( m  /  E )  +  1 )  e.  RR )
2810, 27syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  (
( m  /  E
)  +  1 )  e.  RR )
29 arch 9978 . . . . . . . . . . . 12  |-  ( ( ( m  /  E
)  +  1 )  e.  RR  ->  E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n
)
3028, 29syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  ->  E. n  e.  NN  ( ( m  /  E )  +  1 )  <  n
)
31 nfv 1609 . . . . . . . . . . . . . . . . . 18  |-  F/ t  m  e.  NN
322, 31nfan 1783 . . . . . . . . . . . . . . . . 17  |-  F/ t ( ph  /\  m  e.  NN )
33 nfra1 2606 . . . . . . . . . . . . . . . . 17  |-  F/ t A. t  e.  T  ( F `  t )  <  m
3432, 33nfan 1783 . . . . . . . . . . . . . . . 16  |-  F/ t ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )
35 nfv 1609 . . . . . . . . . . . . . . . 16  |-  F/ t  n  e.  NN
3634, 35nfan 1783 . . . . . . . . . . . . . . 15  |-  F/ t ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )
37 nfv 1609 . . . . . . . . . . . . . . 15  |-  F/ t ( ( m  /  E )  +  1 )  <  n
3836, 37nfan 1783 . . . . . . . . . . . . . 14  |-  F/ t ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )
39 simplll 734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  /\  n  e.  NN )  ->  ph )
4039adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  ph )
4140adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ph )
42 simpr 447 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  t  e.  T )
4341, 42jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( ph  /\  t  e.  T ) )
443, 5, 7, 8fcnre 27798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  F : T --> RR )
4544adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  T )  ->  F : T --> RR )
46 simpr 447 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  T )
4745, 46jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  ( F : T --> RR  /\  t  e.  T )
)
48 ffvelrn 5679 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F : T --> RR  /\  t  e.  T )  ->  ( F `  t
)  e.  RR )
4947, 48syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR )
5043, 49syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
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 )
51 simpllr 735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m )  /\  n  e.  NN )  ->  m  e.  NN )
5251adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  NN )
5352adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  m  e.  NN )
5453, 11syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  m  e.  RR )
55 simpllr 735 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  n  e.  NN )
56 nnre 9769 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  n  e.  RR )
5755, 56syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  n  e.  RR )
5823a1i 10 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  1  e.  RR )
5957, 58jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( n  e.  RR  /\  1  e.  RR ) )
60 resubcl 9127 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  RR  /\  1  e.  RR )  ->  ( n  -  1 )  e.  RR )
6159, 60syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
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 )
6241, 15syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  E  e.  RR )
6361, 62jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
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  /\  E  e.  RR ) )
64 remulcl 8838 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( n  -  1 )  e.  RR  /\  E  e.  RR )  ->  ( ( n  - 
1 )  x.  E
)  e.  RR )
6563, 64syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
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 )
6650, 54, 653jca 1132 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
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  /\  m  e.  RR  /\  ( ( n  - 
1 )  x.  E
)  e.  RR ) )
67 simpllr 735 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 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 )
6867adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  A. t  e.  T  ( F `  t )  <  m )
6968, 42jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( A. t  e.  T  ( F `  t )  <  m  /\  t  e.  T
) )
70 rsp 2616 . . . . . . . . . . . . . . . . . . 19  |-  ( A. t  e.  T  ( F `  t )  <  m  ->  ( t  e.  T  ->  ( F `
 t )  < 
m ) )
7170imp 418 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. t  e.  T  ( F `  t )  <  m  /\  t  e.  T )  ->  ( F `  t )  <  m )
7269, 71syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( F `  t
)  <  m )
7341, 53, 553jca 1132 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( ph  /\  m  e.  NN  /\  n  e.  NN ) )
74 simplr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( (
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 )
7573, 74jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n ) )
76 simpr 447 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  +  1 )  <  n )
77 simpl1 958 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  ph )
78 simpl2 959 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  NN )
7977, 78jca 518 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ph  /\  m  e.  NN ) )
8079, 22syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  /  E
)  e.  RR )
8123a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
1  e.  RR )
82 simpl3 960 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  NN )
8382, 56syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  n  e.  RR )
8480, 81, 833jca 1132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  e.  RR  /\  1  e.  RR  /\  n  e.  RR )
)
85 ltaddsub 9264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( m  /  E
)  e.  RR  /\  1  e.  RR  /\  n  e.  RR )  ->  (
( ( m  /  E )  +  1 )  <  n  <->  ( m  /  E )  <  (
n  -  1 ) ) )
8684, 85syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( ( m  /  E )  +  1 )  <  n  <->  ( m  /  E )  <  ( n  - 
1 ) ) )
8776, 86mpbid 201 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  /  E
)  <  ( n  -  1 ) )
88113ad2ant2 977 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  m  e.  RR )
8988adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  e.  RR )
9083, 81jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( n  e.  RR  /\  1  e.  RR ) )
9190, 60syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( n  -  1 )  e.  RR )
92153ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  m  e.  NN  /\  n  e.  NN )  ->  E  e.  RR )
9392adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  E  e.  RR )
94 rpgt0 10381 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( E  e.  RR+  ->  0  < 
E )
9513, 94syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  0  <  E )
9677, 95syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
0  <  E )
9793, 96jca 518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( E  e.  RR  /\  0  <  E ) )
9889, 91, 973jca 1132 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( m  e.  RR  /\  ( n  -  1 )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
99 ltdivmul2 9647 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  e.  RR  /\  ( n  -  1
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( (
m  /  E )  <  ( n  - 
1 )  <->  m  <  ( ( n  -  1 )  x.  E ) ) )
10098, 99syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  -> 
( ( m  /  E )  <  (
n  -  1 )  <-> 
m  <  ( (
n  -  1 )  x.  E ) ) )
10187, 100mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  NN  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  ->  m  <  ( ( n  -  1 )  x.  E ) )
10275, 101syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( (
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 ) )
10372, 102jca 518 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  m  e.  NN )  /\  A. t  e.  T  ( F `  t )  <  m
)  /\  n  e.  NN )  /\  (
( m  /  E
)  +  1 )  <  n )  /\  t  e.  T )  ->  ( ( F `  t )  <  m  /\  m  <  ( ( n  -  1 )  x.  E ) ) )
104 lttr 8915 . . . . . . . . . . . . . . . 16  |-  ( ( ( F `  t
)  e.  RR  /\  m  e.  RR  /\  (
( n  -  1 )  x.  E )  e.  RR )  -> 
( ( ( F `
 t )  < 
m  /\  m  <  ( ( n  -  1 )  x.  E ) )  ->  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )
10566, 103, 104sylc 56 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
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 ) )
106105ex 423 . . . . . . . . . . . . . 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 ) ) )
10738, 106ralrimi 2637 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 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 ) )
108107ex 423 . . . . . . . . . . . 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 ) ) )
109108reximdva 2668 . . . . . . . . . . 11  |-  ( ( ( 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 ) ) )
11030, 109mpd 14 . . . . . . . . . 10  |-  ( ( ( 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 ) )
111110ex 423 . . . . . . . . 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 ) ) )
112111ex 423 . . . . . . . 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 ) ) ) )
113112rexlimdv 2679 . . . . . . 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 ) ) )
1149, 113mpd 14 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
115 df-rex 2562 . . . . . 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
) ) )
116114, 115sylib 188 . . . . 5  |-  ( ph  ->  E. n ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) ) )
117 simpr 447 . . . . . . . . . 10  |-  ( (
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 ) ) )
118 simpl 443 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )  ->  ph )
119 simprl 732 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )  ->  n  e.  NN )
120118, 119jca 518 . . . . . . . . . . 11  |-  ( (
ph  /\  ( n  e.  NN  /\  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) ) )  ->  ( ph  /\  n  e.  NN ) )
1212, 35nfan 1783 . . . . . . . . . . . 12  |-  F/ t ( ph  /\  n  e.  NN )
122 stoweidlem60.6 . . . . . . . . . . . 12  |-  D  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
123 stoweidlem60.7 . . . . . . . . . . . 12  |-  B  =  ( j  e.  ( 0 ... n ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
124 eqid 2296 . . . . . . . . . . . 12  |-  { 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 ) }
125 eqid 2296 . . . . . . . . . . . 12  |-  ( 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 ) ) } )
1264adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  J  e. 
Comp )
127 stoweidlem60.10 . . . . . . . . . . . . 13  |-  ( ph  ->  A  C_  C )
128127adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  A  C_  C )
129 simp1l 979 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  ph )
130 simp2 956 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  f  e.  A )
131 simp3 957 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  g  e.  A )
132129, 130, 1313jca 1132 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  ( ph  /\  f  e.  A  /\  g  e.  A
) )
133 stoweidlem60.11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
134132, 133syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  +  ( g `
 t ) ) )  e.  A )
135 stoweidlem60.12 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
136132, 135syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) )  e.  A )
137 simpll 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  RR )  ->  ph )
138 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  RR )  ->  y  e.  RR )
139137, 138jca 518 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  RR )  ->  ( ph  /\  y  e.  RR ) )
140 stoweidlem60.13 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A )
141139, 140syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  y  e.  RR )  ->  (
t  e.  T  |->  y )  e.  A )
142 simpll 730 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  ph )
143 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )
144142, 143jca 518 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  ( ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t
) ) )
145 stoweidlem60.14 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
146144, 145syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
1478adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  F  e.  C )
14813adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  E  e.  RR+ )
149 stoweidlem60.18 . . . . . . . . . . . . 13  |-  ( ph  ->  E  <  ( 1  /  3 ) )
150149adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  E  < 
( 1  /  3
) )
151 simpr 447 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
1521, 121, 3, 5, 7, 122, 123, 124, 125, 126, 128, 134, 136, 141, 146, 147, 148, 150, 151stoweidlem59 27910 . . . . . . . . . . 11  |-  ( (
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 )
) ) )
153120, 152syl 15 . . . . . . . . . 10  |-  ( (
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 )
) ) )
154117, 153jca 518 . . . . . . . . 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 ) )  /\  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 ) ) ) ) )
155 19.42v 1858 . . . . . . . . 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 ) ) ) ) )
156154, 155sylibr 203 . . . . . . . 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 ) ) ) ) )
157 3anass 938 . . . . . . . . 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 ) ) ) ) )
158157exbii 1572 . . . . . . . 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 )
) ) ) )
159156, 158sylibr 203 . . . . . . 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 ) ) ) )
160159ex 423 . . . . . 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 ) ) ) ) )
161160eximdv 1612 . . . . 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 ) ) ) ) )
162116, 161mpd 14 . . . 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 ) ) ) )
163 simpl 443 . . . . . . . . . . 11  |-  ( (
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 )
164 simpr1l 1012 . . . . . . . . . . 11  |-  ( (
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 )
165 simpr2 962 . . . . . . . . . . 11  |-  ( (
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 )
166163, 164, 1653jca 1132 . . . . . . . . . 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 ) ) ) )  ->  ( ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A ) )
167 nfv 1609 . . . . . . . . . . . 12  |-  F/ t  x : ( 0 ... n ) --> A
1682, 35, 167nf3an 1786 . . . . . . . . . . 11  |-  F/ t ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )
169 simp2 956 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  n  e.  NN )
170 simp3 957 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  x : ( 0 ... n ) --> A )
171 simp1 955 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  ph )
1721713anim1i 1138 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A  /\  g  e.  A )  ->  ( ph  /\  f  e.  A  /\  g  e.  A ) )
173172, 133syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A
)
174172, 135syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A  /\  g  e.  A )  ->  ( t  e.  T  |->  ( ( f `  t )  x.  (
g `  t )
) )  e.  A
)
175 simpl1 958 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  y  e.  RR )  ->  ph )
176 simpr 447 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  y  e.  RR )  ->  y  e.  RR )
177175, 176jca 518 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  y  e.  RR )  ->  ( ph  /\  y  e.  RR ) )
178177, 140syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A
)
179133ad2ant1 976 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR+ )
180179, 14syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  E  e.  RR )
181 simpl1 958 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A )  ->  ph )
182 simpr 447 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A )  ->  f  e.  A )
183181, 182jca 518 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A )  ->  ( ph  /\  f  e.  A ) )
184127adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  A )  ->  A  C_  C )
185 simpr 447 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  f  e.  A )  ->  f  e.  A )
186184, 185jca 518 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  f  e.  A )  ->  ( A  C_  C  /\  f  e.  A ) )
187 ssel2 3188 . . . . . . . . . . . . . 14  |-  ( ( A  C_  C  /\  f  e.  A )  ->  f  e.  C )
188186, 187syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  f  e.  A )  ->  f  e.  C )
1893, 5, 7, 188fcnre 27798 . . . . . . . . . . . 12  |-  ( (
ph  /\  f  e.  A )  ->  f : T --> RR )
190183, 189syl 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN  /\  x : ( 0 ... n
) --> A )  /\  f  e.  A )  ->  f : T --> RR )
191168, 169, 170, 173, 174, 178, 180, 190stoweidlem17 27868 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  x : ( 0 ... n ) --> A )  ->  (
t  e.  T  |->  sum_ i  e.  ( 0 ... n ) ( E  x.  ( ( x `  i ) `
 t ) ) )  e.  A )
192166, 191syl 15 . . . . . . . . 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 ) ) ) )  ->  ( t  e.  T  |->  sum_ i  e.  ( 0 ... n
) ( E  x.  ( ( x `  i ) `  t
) ) )  e.  A )
193 nfv 1609 . . . . . . . . . . 11  |-  F/ j
ph
194 nfv 1609 . . . . . . . . . . . 12  |-  F/ j ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
195 nfv 1609 . . . . . . . . . . . 12  |-  F/ j  x : ( 0 ... n ) --> A
196 nfra1 2606 . . . . . . . . . . . 12  |-  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 ) )
197194, 195, 196nf3an 1786 . . . . . . . . . . 11  |-  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 ) ) )
198193, 197nfan 1783 . . . . . . . . . 10  |-  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 ) ) ) )
199 nfra1 2606 . . . . . . . . . . . . 13  |-  F/ t A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E )
20035, 199nfan 1783 . . . . . . . . . . . 12  |-  F/ t ( n  e.  NN  /\ 
A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E ) )
201 nfcv 2432 . . . . . . . . . . . . 13  |-  F/_ t
( 0 ... n
)
202 nfra1 2606 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )
203 nfra1 2606 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  ( D `  j ) ( ( x `  j ) `  t
)  <  ( E  /  n )
204 nfra1 2606 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  ( B `  j ) ( 1  -  ( E  /  n ) )  <  ( ( x `
 j ) `  t )
205202, 203, 204nf3an 1786 . . . . . . . . . . . . 13  |-  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 ) )
206201, 205nfral 2609 . . . . . . . . . . . 12  |-  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 ) )
207200, 167, 206nf3an 1786 . . . . . . . . . . 11  |-  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 ) ) )
2082, 207nfan 1783 . . . . . . . . . 10  |-  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 ) ) ) )
209 eqid 2296 . . . . . . . . . 10  |-  ( t  e.  T  |->  { j  e.  ( 1 ... n )  |  t  e.  ( D `  j ) } )  =  ( t  e.  T  |->  { j  e.  ( 1 ... n
)  |  t  e.  ( D `  j
) } )
210 uniexg 4533 . . . . . . . . . . . . 13  |-  ( J  e.  Comp  ->  U. J  e.  _V )
2114, 210syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  U. J  e.  _V )
2125, 211syl5eqel 2380 . . . . . . . . . . 11  |-  ( ph  ->  T  e.  _V )
213212adantr 451 . . . . . . . . . 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 ) ) ) )  ->  T  e.  _V )
21444adantr 451 . . . . . . . . . 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 ) ) ) )  ->  F : T
--> RR )
215 simpll 730 . . . . . . . . . . . 12  |-  ( ( ( 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 )  ->  ph )
216 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( 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 )  ->  t  e.  T )
217215, 216jca 518 . . . . . . . . . . 11  |-  ( ( ( 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 )  ->  ( ph  /\  t  e.  T
) )
218 stoweidlem60.16 . . . . . . . . . . . 12  |-  ( ph  ->  A. t  e.  T 
0  <_  ( F `  t ) )
219218r19.21bi 2654 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
220217, 219syl 15 . . . . . . . . . 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 ) ) ) )  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
221 simpr1r 1013 . . . . . . . . . . . . 13  |-  ( (
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 ) )
222221adantr 451 . . . . . . . . . . . 12  |-  ( ( ( 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 )  ->  A. t  e.  T  ( F `  t )  <  (
( n  -  1 )  x.  E ) )
223222, 216jca 518 . . . . . . . . . . 11  |-  ( ( ( 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 )  ->  ( A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E )  /\  t  e.  T ) )
224 rsp 2616 . . . . . . . . . . . 12  |-  ( A. t  e.  T  ( F `  t )  <  ( ( n  - 
1 )  x.  E
)  ->  ( t  e.  T  ->  ( F `
 t )  < 
( ( n  - 
1 )  x.  E
) ) )
225224imp 418 . . . . . . . . . . 11  |-  ( ( A. t  e.  T  ( F `  t )  <  ( ( n  -  1 )  x.  E )  /\  t  e.  T )  ->  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )
226223, 225syl 15 . . . . . . . . . 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 ) ) ) )  /\  t  e.  T )  ->  ( F `  t )  <  ( ( n  - 
1 )  x.  E
) )
22713adantr 451 . . . . . . . . . 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 ) ) ) )  ->  E  e.  RR+ )
228149adantr 451 . . . . . . . . . 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 ) ) ) )  ->  E  <  ( 1  /  3 ) )
229 simpll 730 . . . . . . . . . . . 12  |-  ( ( ( 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 )
230 simplr2 998 . . . . . . . . . . . 12  |-  ( ( ( 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 )
231 simpr 447 . . . . . . . . . . . 12  |-  ( ( ( 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
) )
232229, 230, 2313jca 1132 . . . . . . . . . . 11  |-  ( ( ( 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  /\  x : ( 0 ... n ) --> A  /\  j  e.  ( 0 ... n
) ) )
233 simp1 955 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  ph )
234 ffvelrn 5679 . . . . . . . . . . . . . 14  |-  ( ( x : ( 0 ... n ) --> A  /\  j  e.  ( 0 ... n ) )  ->  ( x `  j )  e.  A
)
2352343adant1 973 . . . . . . . . . . . . 13  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j )  e.  A )
236233, 235jca 518 . . . . . . . . . . . 12  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  ( ph  /\  ( x `  j )  e.  A
) )
237127adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  A  C_  C
)
238 simpr 447 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j )  e.  A
)
239237, 238jca 518 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( A  C_  C  /\  ( x `
 j )  e.  A ) )
240 ssel2 3188 . . . . . . . . . . . . . 14  |-  ( ( A  C_  C  /\  ( x `  j
)  e.  A )  ->  ( x `  j )  e.  C
)
241239, 240syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j )  e.  C
)
2423, 5, 7, 241fcnre 27798 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x `  j )  e.  A
)  ->  ( x `  j ) : T --> RR )
243236, 242syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  x :
( 0 ... n
) --> A  /\  j  e.  ( 0 ... n
) )  ->  (
x `  j ) : T --> RR )
244232, 243syl 15 . . . . . . . . . 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
) )  ->  (
x `  j ) : T --> RR )
245 simp1r3 1053 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
) )
246 r19.26-3 2690 . . . . . . . . . . . . . . . 16  |-  ( 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 )
) )
247246simp1bi 970 . . . . . . . . . . . . . . 15  |-  ( 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 ) )
248 simpl 443 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  0  <_  ( ( x `  j ) `  t
) )
249248ralimi 2631 . . . . . . . . . . . . . . . 16  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  0  <_  ( ( x `  j
) `  t )
)
250249ralimi 2631 . . . . . . . . . . . . . . 15  |-  ( 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 )
)
251247, 250syl 15 . . . . . . . . . . . . . 14  |-  ( 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
) )
252245, 251syl 15 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
)
253 simp2 956 . . . . . . . . . . . . 13  |-  ( ( ( 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
) )
254252, 253jca 518 . . . . . . . . . . . 12  |-  ( ( ( 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
)  /\  j  e.  ( 0 ... n
) ) )
255 simp3 957 . . . . . . . . . . . 12  |-  ( ( ( 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 )
256254, 255jca 518 . . . . . . . . . . 11  |-  ( ( ( 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 )  /\  j  e.  (
0 ... n ) )  /\  t  e.  T
) )
257 rsp 2616 . . . . . . . . . . . . . 14  |-  ( 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 )
) )
258257imp 418 . . . . . . . . . . . . 13  |-  ( ( 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 )
)
259 rsp 2616 . . . . . . . . . . . . 13  |-  ( A. t  e.  T  0  <_  ( ( x `  j ) `  t
)  ->  ( t  e.  T  ->  0  <_ 
( ( x `  j ) `  t
) ) )
260258, 259syl 15 . . . . . . . . . . . 12  |-  ( ( A. j  e.  ( 0 ... n ) A. t  e.  T 
0  <_  ( (
x `  j ) `  t )  /\  j  e.  ( 0 ... n
) )  ->  (
t  e.  T  -> 
0  <_  ( (
x `  j ) `  t ) ) )
261260imp 418 . . . . . . . . . . 11  |-  ( ( ( A. j  e.  ( 0 ... n
) A. t  e.  T  0  <_  (
( x `  j
) `  t )  /\  j  e.  (
0 ... n ) )  /\  t  e.  T
)  ->  0  <_  ( ( x `  j
) `  t )
)
262256, 261syl 15 . . . . . . . . . 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 )  ->  0  <_  ( ( x `  j ) `  t
) )
263 simpr 447 . . . . . . . . . . . . . . . . 17  |-  ( ( 0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  (
( x `  j
) `  t )  <_  1 )
264263ralimi 2631 . . . . . . . . . . . . . . . 16  |-  ( A. t  e.  T  (
0  <_  ( (
x `  j ) `  t )  /\  (
( x `  j
) `  t )  <_  1 )  ->  A. t  e.  T  ( (
x `  j ) `  t )  <_  1
)
265264ralimi 2631 . . . . . . . . . . . . . . 15  |-  ( 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
)
266247, 265syl 15 . . . . . . . . . . . . . 14  |-  ( 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  (
( x `  j
) `  t )  <_  1 )
267245, 266syl 15 . . . . . . . . . . . . 13  |-  ( ( ( 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
)
268267, 253jca 518 . . . . . . . . . . . 12  |-  ( ( ( 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  /\  j  e.  ( 0 ... n
) ) )
269268, 255jca 518 . . . . . . . . . . 11  |-  ( ( ( 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  /\  j  e.  (
0 ... n ) )  /\  t  e.  T
) )
270 rsp 2616 . . . . . . . . . . . . . . 15  |-  ( 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
) )
271270imp 418 . . . . . . . . . . . . . 14  |-  ( ( 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 )
272271adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( A. j  e.  ( 0 ... n
) A. t  e.  T  ( ( x `
 j ) `  t )  <_  1  /\  j  e.  (
0 ... n ) )  /\  t  e.  T
)  ->  A. t  e.  T  ( (
x `  j ) `  t )  <_  1
)
273 simpr 447 . . . . . . . . . . . . 13  |-  ( ( ( A. j  e.  ( 0 ... n
) A. t  e.  T  ( ( x `
 j ) `