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

Theorem stoweidlem34 27451
Description: This lemma proves that for all  t in  T there is a  j as in the proof of [BrosowskiDeutsh] p. 91 (at the bottom of page 91 and at the top of page 92): (j-4/3) * ε < f(t) <= (j-1/3) * ε , g(t) < (j+1/3) * ε, and g(t) > (j-4/3) * ε. Here  E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem34.1  |-  F/_ t F
stoweidlem34.2  |-  F/ j
ph
stoweidlem34.3  |-  F/ t
ph
stoweidlem34.4  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
stoweidlem34.5  |-  B  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
stoweidlem34.6  |-  J  =  ( t  e.  T  |->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
stoweidlem34.7  |-  ( ph  ->  N  e.  NN )
stoweidlem34.8  |-  ( ph  ->  T  e.  _V )
stoweidlem34.9  |-  ( ph  ->  F : T --> RR )
stoweidlem34.10  |-  ( (
ph  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
stoweidlem34.11  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  <  ( ( N  - 
1 )  x.  E
) )
stoweidlem34.12  |-  ( ph  ->  E  e.  RR+ )
stoweidlem34.13  |-  ( ph  ->  E  <  ( 1  /  3 ) )
stoweidlem34.14  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( X `  j ) : T --> RR )
stoweidlem34.15  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  t  e.  T )  ->  0  <_  ( ( X `  j ) `  t
) )
stoweidlem34.16  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  t  e.  T )  ->  (
( X `  j
) `  t )  <_  1 )
stoweidlem34.17  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  t  e.  ( D `  j ) )  ->  ( ( X `  j ) `  t )  <  ( E  /  N ) )
stoweidlem34.18  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  t  e.  ( B `  j ) )  ->  ( 1  -  ( E  /  N ) )  < 
( ( X `  j ) `  t
) )
Assertion
Ref Expression
stoweidlem34  |-  ( ph  ->  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 ) ) ) )
Distinct variable groups:    i, j,
t, E    D, i    i, J    i, N, j, t    T, i, j, t    ph, i    j, F    j, X, t
Allowed substitution hints:    ph( t, j)    B( t, i, j)    D( t, j)    F( t, i)    J( t, j)    X( i)

Proof of Theorem stoweidlem34
Dummy variables  k 
l  s  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem34.3 . 2  |-  F/ t
ph
2 simpr 448 . . . . . . . 8  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  T )
3 ovex 6045 . . . . . . . . 9  |-  ( 1 ... N )  e. 
_V
43rabex 4295 . . . . . . . 8  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  e.  _V
5 stoweidlem34.6 . . . . . . . . 9  |-  J  =  ( t  e.  T  |->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
65fvmpt2 5751 . . . . . . . 8  |-  ( ( t  e.  T  /\  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) }  e.  _V )  -> 
( J `  t
)  =  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
72, 4, 6sylancl 644 . . . . . . 7  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  =  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
8 ssrab2 3371 . . . . . . 7  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  C_  ( 1 ... N
)
97, 8syl6eqss 3341 . . . . . 6  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  C_  ( 1 ... N
) )
10 elfznn 11012 . . . . . . 7  |-  ( x  e.  ( 1 ... N )  ->  x  e.  NN )
1110ssriv 3295 . . . . . 6  |-  ( 1 ... N )  C_  NN
129, 11syl6ss 3303 . . . . 5  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  C_  NN )
13 nnssre 9936 . . . . 5  |-  NN  C_  RR
1412, 13syl6ss 3303 . . . 4  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  C_  RR )
15 stoweidlem34.7 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  NN )
1615adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  NN )
17 nnuz 10453 . . . . . . . . . . . . . . 15  |-  NN  =  ( ZZ>= `  1 )
1816, 17syl6eleq 2477 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( ZZ>= `  1 )
)
19 eluzfz2 10997 . . . . . . . . . . . . . 14  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
2018, 19syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( 1 ... N
) )
21 stoweidlem34.11 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  <  ( ( N  - 
1 )  x.  E
) )
22 3re 10003 . . . . . . . . . . . . . . . . . . . . 21  |-  3  e.  RR
23 3ne0 10017 . . . . . . . . . . . . . . . . . . . . 21  |-  3  =/=  0
2422, 23rereccli 9711 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  3 )  e.  RR
2524a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  e.  RR )
26 1re 9023 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR
2726a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  1  e.  RR )
2816nnred 9947 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  RR )
29 1lt3 10076 . . . . . . . . . . . . . . . . . . . . 21  |-  1  <  3
3022, 29pm3.2i 442 . . . . . . . . . . . . . . . . . . . 20  |-  ( 3  e.  RR  /\  1  <  3 )
31 recgt1i 9839 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 3  e.  RR  /\  1  <  3 )  -> 
( 0  <  (
1  /  3 )  /\  ( 1  / 
3 )  <  1
) )
3231simprd 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 3  e.  RR  /\  1  <  3 )  -> 
( 1  /  3
)  <  1 )
3330, 32mp1i 12 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  <  1 )
3425, 27, 28, 33ltsub2dd 9571 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  1 )  <  ( N  -  ( 1  /  3
) ) )
3528, 27resubcld 9397 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  1 )  e.  RR )
3628, 25resubcld 9397 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  ( 1  /  3 ) )  e.  RR )
37 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  E  e.  RR+ )
3837rpred 10580 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  E  e.  RR )
3938adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  E  e.  RR )
4037rpgt0d 10583 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <  E )
4140adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  0  <  E )
42 ltmul1 9792 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( N  -  1 )  e.  RR  /\  ( N  -  (
1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( ( N  -  1 )  <  ( N  -  ( 1  /  3
) )  <->  ( ( N  -  1 )  x.  E )  < 
( ( N  -  ( 1  /  3
) )  x.  E
) ) )
4335, 36, 39, 41, 42syl112anc 1188 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  <  ( N  -  ( 1  / 
3 ) )  <->  ( ( N  -  1 )  x.  E )  < 
( ( N  -  ( 1  /  3
) )  x.  E
) ) )
4434, 43mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  x.  E )  <  ( ( N  -  ( 1  / 
3 ) )  x.  E ) )
4521, 44jca 519 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  (
( F `  t
)  <  ( ( N  -  1 )  x.  E )  /\  ( ( N  - 
1 )  x.  E
)  <  ( ( N  -  ( 1  /  3 ) )  x.  E ) ) )
46 stoweidlem34.9 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  F : T --> RR )
4746fnvinran 27353 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR )
4835, 39remulcld 9049 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  x.  E )  e.  RR )
4936, 39remulcld 9049 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  (
1  /  3 ) )  x.  E )  e.  RR )
50 lttr 9085 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  t
)  e.  RR  /\  ( ( N  - 
1 )  x.  E
)  e.  RR  /\  ( ( N  -  ( 1  /  3
) )  x.  E
)  e.  RR )  ->  ( ( ( F `  t )  <  ( ( N  -  1 )  x.  E )  /\  (
( N  -  1 )  x.  E )  <  ( ( N  -  ( 1  / 
3 ) )  x.  E ) )  -> 
( F `  t
)  <  ( ( N  -  ( 1  /  3 ) )  x.  E ) ) )
51 ltle 9096 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( F `  t
)  e.  RR  /\  ( ( N  -  ( 1  /  3
) )  x.  E
)  e.  RR )  ->  ( ( F `
 t )  < 
( ( N  -  ( 1  /  3
) )  x.  E
)  ->  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) ) )
52513adant2 976 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( F `  t
)  e.  RR  /\  ( ( N  - 
1 )  x.  E
)  e.  RR  /\  ( ( N  -  ( 1  /  3
) )  x.  E
)  e.  RR )  ->  ( ( F `
 t )  < 
( ( N  -  ( 1  /  3
) )  x.  E
)  ->  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) ) )
5350, 52syld 42 . . . . . . . . . . . . . . . . 17  |-  ( ( ( F `  t
)  e.  RR  /\  ( ( N  - 
1 )  x.  E
)  e.  RR  /\  ( ( N  -  ( 1  /  3
) )  x.  E
)  e.  RR )  ->  ( ( ( F `  t )  <  ( ( N  -  1 )  x.  E )  /\  (
( N  -  1 )  x.  E )  <  ( ( N  -  ( 1  / 
3 ) )  x.  E ) )  -> 
( F `  t
)  <_  ( ( N  -  ( 1  /  3 ) )  x.  E ) ) )
5447, 48, 49, 53syl3anc 1184 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  (
( ( F `  t )  <  (
( N  -  1 )  x.  E )  /\  ( ( N  -  1 )  x.  E )  <  (
( N  -  (
1  /  3 ) )  x.  E ) )  ->  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) ) )
5545, 54mpd 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  <_  ( ( N  -  ( 1  /  3
) )  x.  E
) )
56 rabid 2827 . . . . . . . . . . . . . . 15  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( N  -  ( 1  /  3
) )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( ( N  -  ( 1  /  3
) )  x.  E
) ) )
572, 55, 56sylanbrc 646 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) } )
58 nnnn0 10160 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  N  e.  NN0 )
59 nn0uz 10452 . . . . . . . . . . . . . . . . . 18  |-  NN0  =  ( ZZ>= `  0 )
6058, 59syl6eleq 2477 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  N  e.  ( ZZ>= `  0 )
)
61 eluzfz2 10997 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  0
)  ->  N  e.  ( 0 ... N
) )
6215, 60, 613syl 19 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  ( 0 ... N ) )
63 stoweidlem34.8 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  _V )
64 rabexg 4294 . . . . . . . . . . . . . . . . 17  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( N  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
6563, 64syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) }  e.  _V )
66 oveq1 6027 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  N  ->  (
j  -  ( 1  /  3 ) )  =  ( N  -  ( 1  /  3
) ) )
6766oveq1d 6035 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  N  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( N  -  ( 1  / 
3 ) )  x.  E ) )
6867breq2d 4165 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  N  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) ) )
6968rabbidv 2891 . . . . . . . . . . . . . . . . 17  |-  ( j  =  N  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) } )
70 stoweidlem34.4 . . . . . . . . . . . . . . . . 17  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
7169, 70fvmptg 5743 . . . . . . . . . . . . . . . 16  |-  ( ( N  e.  ( 0 ... N )  /\  { t  e.  T  | 
( F `  t
)  <_  ( ( N  -  ( 1  /  3 ) )  x.  E ) }  e.  _V )  -> 
( D `  N
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( N  -  ( 1  / 
3 ) )  x.  E ) } )
7262, 65, 71syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( D `  N
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( N  -  ( 1  / 
3 ) )  x.  E ) } )
7372adantr 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  ( D `  N )  =  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) } )
7457, 73eleqtrrd 2464 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  ( D `  N
) )
75 nfcv 2523 . . . . . . . . . . . . . 14  |-  F/_ j N
76 nfcv 2523 . . . . . . . . . . . . . 14  |-  F/_ j
( 1 ... N
)
77 nfmpt1 4239 . . . . . . . . . . . . . . . . 17  |-  F/_ j
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
7870, 77nfcxfr 2520 . . . . . . . . . . . . . . . 16  |-  F/_ j D
7978, 75nffv 5675 . . . . . . . . . . . . . . 15  |-  F/_ j
( D `  N
)
8079nfcri 2517 . . . . . . . . . . . . . 14  |-  F/ j  t  e.  ( D `
 N )
81 fveq2 5668 . . . . . . . . . . . . . . 15  |-  ( j  =  N  ->  ( D `  j )  =  ( D `  N ) )
8281eleq2d 2454 . . . . . . . . . . . . . 14  |-  ( j  =  N  ->  (
t  e.  ( D `
 j )  <->  t  e.  ( D `  N ) ) )
8375, 76, 80, 82elrabf 3034 . . . . . . . . . . . . 13  |-  ( N  e.  { j  e.  ( 1 ... N
)  |  t  e.  ( D `  j
) }  <->  ( N  e.  ( 1 ... N
)  /\  t  e.  ( D `  N ) ) )
8420, 74, 83sylanbrc 646 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
8584, 7eleqtrrd 2464 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( J `  t
) )
86 ne0i 3577 . . . . . . . . . . 11  |-  ( N  e.  ( J `  t )  ->  ( J `  t )  =/=  (/) )
8785, 86syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  =/=  (/) )
88 nnwo 10474 . . . . . . . . . . 11  |-  ( ( ( J `  t
)  C_  NN  /\  ( J `  t )  =/=  (/) )  ->  E. i  e.  ( J `  t
) A. k  e.  ( J `  t
) i  <_  k
)
89 nfcv 2523 . . . . . . . . . . . 12  |-  F/_ i
( J `  t
)
90 nfcv 2523 . . . . . . . . . . . . . . 15  |-  F/_ j T
91 nfrab1 2831 . . . . . . . . . . . . . . 15  |-  F/_ j { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }
9290, 91nfmpt 4238 . . . . . . . . . . . . . 14  |-  F/_ j
( t  e.  T  |->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
935, 92nfcxfr 2520 . . . . . . . . . . . . 13  |-  F/_ j J
94 nfcv 2523 . . . . . . . . . . . . 13  |-  F/_ j
t
9593, 94nffv 5675 . . . . . . . . . . . 12  |-  F/_ j
( J `  t
)
96 nfv 1626 . . . . . . . . . . . . 13  |-  F/ j  i  <_  k
9795, 96nfral 2702 . . . . . . . . . . . 12  |-  F/ j A. k  e.  ( J `  t ) i  <_  k
98 nfv 1626 . . . . . . . . . . . 12  |-  F/ i A. k  e.  ( J `  t ) j  <_  k
99 breq1 4156 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
i  <_  k  <->  j  <_  k ) )
10099ralbidv 2669 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( A. k  e.  ( J `  t )
i  <_  k  <->  A. k  e.  ( J `  t
) j  <_  k
) )
10189, 95, 97, 98, 100cbvrexf 2870 . . . . . . . . . . 11  |-  ( E. i  e.  ( J `
 t ) A. k  e.  ( J `  t ) i  <_ 
k  <->  E. j  e.  ( J `  t ) A. k  e.  ( J `  t ) j  <_  k )
10288, 101sylib 189 . . . . . . . . . 10  |-  ( ( ( J `  t
)  C_  NN  /\  ( J `  t )  =/=  (/) )  ->  E. j  e.  ( J `  t
) A. k  e.  ( J `  t
) j  <_  k
)
10312, 87, 102syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  E. j  e.  ( J `  t
) A. k  e.  ( J `  t
) j  <_  k
)
104 stoweidlem34.2 . . . . . . . . . . 11  |-  F/ j
ph
105 nfv 1626 . . . . . . . . . . 11  |-  F/ j  t  e.  T
106104, 105nfan 1836 . . . . . . . . . 10  |-  F/ j ( ph  /\  t  e.  T )
1077eleq2d 2454 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  (
j  e.  ( J `
 t )  <->  j  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) } ) )
108107biimpa 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  j  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
109 rabid 2827 . . . . . . . . . . . . . . 15  |-  ( j  e.  { j  e.  ( 1 ... N
)  |  t  e.  ( D `  j
) }  <->  ( j  e.  ( 1 ... N
)  /\  t  e.  ( D `  j ) ) )
110108, 109sylib 189 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
j  e.  ( 1 ... N )  /\  t  e.  ( D `  j ) ) )
111110simprd 450 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  t  e.  ( D `  j
) )
112111adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  t  e.  ( D `  j ) )
113 simp3 959 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  t  e.  ( D `  ( j  -  1 ) ) )
114 simp1l 981 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ph )
115 noel 3575 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -.  t  e.  (/)
116 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  1  ->  (
j  -  1 )  =  ( 1  -  1 ) )
117 1m1e0 10000 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 1  -  1 )  =  0
118116, 117syl6eq 2435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  1  ->  (
j  -  1 )  =  0 )
119118fveq2d 5672 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  1  ->  ( D `  ( j  -  1 ) )  =  ( D ` 
0 ) )
12022a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  t  e.  T )  ->  3  e.  RR )
12123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  t  e.  T )  ->  3  =/=  0 )
12227, 120, 121redivcld 9774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  e.  RR )
123122renegcld 9396 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  t  e.  T )  ->  -u (
1  /  3 )  e.  RR )
124123, 39remulcld 9049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  e.  RR )
125 0re 9024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  0  e.  RR
126125a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  T )  ->  0  e.  RR )
127 3pos 10016 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  <  3
12822, 127recgt0ii 9848 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  <  ( 1  /  3
)
129 lt0neg2 9467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 1  /  3 )  e.  RR  ->  (
0  <  ( 1  /  3 )  <->  -u ( 1  /  3 )  <  0 ) )
13024, 129ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 0  <  ( 1  / 
3 )  <->  -u ( 1  /  3 )  <  0 )
131128, 130mpbi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  -u (
1  /  3 )  <  0
132 ltmul1 9792 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
-u ( 1  / 
3 )  e.  RR  /\  0  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( -u (
1  /  3 )  <  0  <->  ( -u (
1  /  3 )  x.  E )  < 
( 0  x.  E
) ) )
133123, 126, 39, 41, 132syl112anc 1188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  <  0  <->  ( -u (
1  /  3 )  x.  E )  < 
( 0  x.  E
) ) )
134131, 133mpbii 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  <  ( 0  x.  E ) )
135 mul02lem2 9175 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( E  e.  RR  ->  (
0  x.  E )  =  0 )
13639, 135syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  t  e.  T )  ->  (
0  x.  E )  =  0 )
137134, 136breqtrd 4177 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  <  0 )
138 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
139124, 126, 47, 137, 138ltletrd 9162 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  <  ( F `  t ) )
140124, 47ltnled 9152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  t  e.  T )  ->  (
( -u ( 1  / 
3 )  x.  E
)  <  ( F `  t )  <->  -.  ( F `  t )  <_  ( -u ( 1  /  3 )  x.  E ) ) )
141139, 140mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  t  e.  T )  ->  -.  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) )
142 nan 564 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  ->  -.  ( t  e.  T  /\  ( F `  t )  <_  ( -u ( 1  /  3 )  x.  E ) ) )  <-> 
( ( ph  /\  t  e.  T )  ->  -.  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) ) )
143141, 142mpbir 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  -.  ( t  e.  T  /\  ( F `
 t )  <_ 
( -u ( 1  / 
3 )  x.  E
) ) )
144 rabid 2827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( -u ( 1  / 
3 )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( -u ( 1  /  3 )  x.  E ) ) )
145143, 144sylnibr 297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  -.  t  e.  {
t  e.  T  | 
( F `  t
)  <_  ( -u (
1  /  3 )  x.  E ) } )
14615nnnn0d 10206 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  N  e.  NN0 )
147 elnn0uz 10455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  NN0  <->  N  e.  ( ZZ>=
`  0 ) )
148146, 147sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
149 eluzfz1 10996 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... N
) )
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  0  e.  ( 0 ... N ) )
151 rabexg 4294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) }  e.  _V )
15263, 151syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) }  e.  _V )
153 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  =  0  ->  (
j  -  ( 1  /  3 ) )  =  ( 0  -  ( 1  /  3
) ) )
154 df-neg 9226 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  -u (
1  /  3 )  =  ( 0  -  ( 1  /  3
) )
155153, 154syl6eqr 2437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  =  0  ->  (
j  -  ( 1  /  3 ) )  =  -u ( 1  / 
3 ) )
156155oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  =  0  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( -u (
1  /  3 )  x.  E ) )
157156breq2d 4165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( j  =  0  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) ) )
158157rabbidv 2891 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( j  =  0  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) } )
159158, 70fvmptg 5743 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 0  e.  ( 0 ... N )  /\  { t  e.  T  | 
( F `  t
)  <_  ( -u (
1  /  3 )  x.  E ) }  e.  _V )  -> 
( D `  0
)  =  { t  e.  T  |  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) } )
160150, 152, 159syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( D `  0
)  =  { t  e.  T  |  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) } )
161145, 160neleqtrrd 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  -.  t  e.  ( D `  0 ) )
1621, 161alrimi 1773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A. t  -.  t  e.  ( D `  0
) )
163 eq0 3585 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( D `  0 )  =  (/)  <->  A. s  -.  s  e.  ( D `  0
) )
164 nfcv 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/_ t
( 0 ... N
)
165 nfrab1 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/_ t { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
166164, 165nfmpt 4238 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
16770, 166nfcxfr 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/_ t D
168 nfcv 2523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/_ t
0
169167, 168nffv 5675 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/_ t
( D `  0
)
170169nfcri 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/ t  s  e.  ( D `
 0 )
171170nfn 1801 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ t  -.  s  e.  ( D `  0 )
172 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ s  -.  t  e.  ( D `  0 )
173 eleq1 2447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( s  =  t  ->  (
s  e.  ( D `
 0 )  <->  t  e.  ( D `  0 ) ) )
174173notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( s  =  t  ->  ( -.  s  e.  ( D `  0 )  <->  -.  t  e.  ( D `
 0 ) ) )
175171, 172, 174cbval 2019 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. s  -.  s  e.  ( D `  0 )  <->  A. t  -.  t  e.  ( D `  0
) )
176163, 175bitri 241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( D `  0 )  =  (/)  <->  A. t  -.  t  e.  ( D `  0
) )
177162, 176sylibr 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( D `  0
)  =  (/) )
178119, 177sylan9eqr 2441 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  = 
1 )  ->  ( D `  ( j  -  1 ) )  =  (/) )
179178eleq2d 2454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  = 
1 )  ->  (
t  e.  ( D `
 ( j  - 
1 ) )  <->  t  e.  (/) ) )
180115, 179mtbiri 295 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  = 
1 )  ->  -.  t  e.  ( D `  ( j  -  1 ) ) )
181180ex 424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( j  =  1  ->  -.  t  e.  ( D `  ( j  -  1 ) ) ) )
182181con2d 109 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( t  e.  ( D `  ( j  -  1 ) )  ->  -.  j  = 
1 ) )
183114, 113, 182sylc 58 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  j  =  1 )
184 simplll 735 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  -.  j  =  1 )  ->  ph )
185107, 109syl6bb 253 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  t  e.  T )  ->  (
j  e.  ( J `
 t )  <->  ( j  e.  ( 1 ... N
)  /\  t  e.  ( D `  j ) ) ) )
186185simprbda 607 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  j  e.  ( 1 ... N
) )
18715, 17syl6eleq 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
188187adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( J `  t ) )  ->  N  e.  ( ZZ>= `  1 )
)
189 elfzp12 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  1
)  ->  ( j  e.  ( 1 ... N
)  <->  ( j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N
) ) ) )
190188, 189syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( J `  t ) )  ->  ( j  e.  ( 1 ... N
)  <->  ( j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N
) ) ) )
191190adantlr 696 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
j  e.  ( 1 ... N )  <->  ( j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N
) ) ) )
192186, 191mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N ) ) )
193192orcanai 880 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  -.  j  =  1 )  -> 
j  e.  ( ( 1  +  1 ) ... N ) )
194 fzssp1 11027 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1 ... ( N  - 
1 ) )  C_  ( 1 ... (
( N  -  1 )  +  1 ) )
19515nncnd 9948 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  N  e.  CC )
196 ax-1cn 8981 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  1  e.  CC
197196a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  1  e.  CC )
198195, 197npcand 9347 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
199198oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( 1 ... (
( N  -  1 )  +  1 ) )  =  ( 1 ... N ) )
200194, 199syl5sseq 3339 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 1 ... N ) )
201200adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
1 ... ( N  - 
1 ) )  C_  ( 1 ... N
) )
202 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  j  e.  ( ( 1  +  1 ) ... N
) )
203 1z 10243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  1  e.  ZZ
204 zaddcl 10249 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ )  ->  ( 1  +  1 )  e.  ZZ )
205203, 203, 204mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 1  +  1 )  e.  ZZ
206205a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
1  +  1 )  e.  ZZ )
20715nnzd 10306 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  N  e.  ZZ )
208207adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  N  e.  ZZ )
209 elfzelz 10991 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( ( 1  +  1 ) ... N )  ->  j  e.  ZZ )
210209adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  j  e.  ZZ )
211203a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  1  e.  ZZ )
212 fzsubel 11020 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 1  +  1 )  e.  ZZ  /\  N  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( j  e.  ( ( 1  +  1 ) ... N )  <-> 
( j  -  1 )  e.  ( ( ( 1  +  1 )  -  1 ) ... ( N  - 
1 ) ) ) )
213206, 208, 210, 211, 212syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  e.  ( ( 1  +  1 ) ... N )  <->  ( j  -  1 )  e.  ( ( ( 1  +  1 )  - 
1 ) ... ( N  -  1 ) ) ) )
214202, 213mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  -  1 )  e.  ( ( ( 1  +  1 )  -  1 ) ... ( N  -  1 ) ) )
215 pncan 9243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 1  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  1 )  -  1 )  =  1 )
216196, 196, 215mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  +  1 )  -  1 )  =  1
217216oveq1i 6030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 1  +  1 )  -  1 ) ... ( N  - 
1 ) )  =  ( 1 ... ( N  -  1 ) )
218214, 217syl6eleq 2477 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  -  1 )  e.  ( 1 ... ( N  -  1 ) ) )
219201, 218sseldd 3292 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  -  1 )  e.  ( 1 ... N ) )
220184, 193, 219syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  -.  j  =  1 )  -> 
( j  -  1 )  e.  ( 1 ... N ) )
221220ex 424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  ( -.  j  =  1  ->  ( j  -  1 )  e.  ( 1 ... N ) ) )
2222213adant3 977 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( -.  j  =  1  ->  ( j  -  1 )  e.  ( 1 ... N ) ) )
223183, 222mpd 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e.  ( 1 ... N
) )
224 fveq2 5668 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  ( j  - 
1 )  ->  ( D `  i )  =  ( D `  ( j  -  1 ) ) )
225224eleq2d 2454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  ( j  - 
1 )  ->  (
t  e.  ( D `
 i )  <->  t  e.  ( D `  ( j  -  1 ) ) ) )
226225elrab3 3036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( j  -  1 )  e.  ( 1 ... N )  ->  (
( j  -  1 )  e.  { i  e.  ( 1 ... N )  |  t  e.  ( D `  i ) }  <->  t  e.  ( D `  ( j  -  1 ) ) ) )
227223, 226syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( (
j  -  1 )  e.  { i  e.  ( 1 ... N
)  |  t  e.  ( D `  i
) }  <->  t  e.  ( D `  ( j  -  1 ) ) ) )
228113, 227mpbird 224 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e. 
{ i  e.  ( 1 ... N )  |  t  e.  ( D `  i ) } )
229 nfcv 2523 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ i
( 1 ... N
)
230 nfv 1626 . . . . . . . . . . . . . . . . . . . 20  |-  F/ i  t  e.  ( D `
 j )
231 nfcv 2523 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ j
i
23278, 231nffv 5675 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ j
( D `  i
)
233232nfcri 2517 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j  t  e.  ( D `
 i )
234 fveq2 5668 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  i  ->  ( D `  j )  =  ( D `  i ) )
235234eleq2d 2454 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
t  e.  ( D `
 j )  <->  t  e.  ( D `  i ) ) )
23676, 229, 230, 233, 235cbvrab 2897 . . . . . . . . . . . . . . . . . . 19  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  =  { i  e.  ( 1 ... N )  |  t  e.  ( D `  i ) }
237228, 236syl6eleqr 2478 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e. 
{ j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
23873ad2ant1 978 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( J `  t )  =  {
j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) } )
239237, 238eleqtrrd 2464 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e.  ( J `  t
) )
240 elfzelz 10991 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ZZ )
241 zre 10218 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ZZ  ->  j  e.  RR )
242186, 240, 2413syl 19 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  j  e.  RR )
2432423adant3 977 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  j  e.  RR )
244 peano2rem 9299 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  RR  ->  (
j  -  1 )  e.  RR )
245243, 244ex-natded5.3i 21565 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  e.  RR  /\  ( j  -  1 )  e.  RR ) )
246 ltm1 9782 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  RR  ->  (
j  -  1 )  <  j )
247246adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  RR  /\  ( j  -  1 )  e.  RR )  ->  ( j  - 
1 )  <  j
)
248 ltnle 9088 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( j  -  1 )  e.  RR  /\  j  e.  RR )  ->  ( ( j  - 
1 )  <  j  <->  -.  j  <_  ( j  -  1 ) ) )
249248ancoms 440 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  RR  /\  ( j  -  1 )  e.  RR )  ->  ( ( j  -  1 )  < 
j  <->  -.  j  <_  ( j  -  1 ) ) )
250247, 249mpbid 202 . . . . . . . . . . . . . . . . . 18  |-  ( ( j  e.  RR  /\  ( j  -  1 )  e.  RR )  ->  -.  j  <_  ( j  -  1 ) )
251245, 250syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  j  <_  ( j  -  1 ) )
252 breq2 4157 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  ( j  - 
1 )  ->  (
j  <_  k  <->  j  <_  ( j  -  1 ) ) )
253252notbid 286 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( j  - 
1 )  ->  ( -.  j  <_  k  <->  -.  j  <_  ( j  -  1 ) ) )
254253rspcev 2995 . . . . . . . . . . . . . . . . 17  |-  ( ( ( j  -  1 )  e.  ( J `
 t )  /\  -.  j  <_  ( j  -  1 ) )  ->  E. k  e.  ( J `  t )  -.  j  <_  k
)
255239, 251, 254syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  E. k  e.  ( J `  t
)  -.  j  <_ 
k )
256 rexnal 2660 . . . . . . . . . . . . . . . 16  |-  ( E. k  e.  ( J `
 t )  -.  j  <_  k  <->  -.  A. k  e.  ( J `  t
) j  <_  k
)
257255, 256sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  A. k  e.  ( J `  t
) j  <_  k
)
2582573expia 1155 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
t  e.  ( D `
 ( j  - 
1 ) )  ->  -.  A. k  e.  ( J `  t ) j  <_  k )
)
259258con2d 109 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  ( A. k  e.  ( J `  t )
j  <_  k  ->  -.  t  e.  ( D `
 ( j  - 
1 ) ) ) )
260259imp 419 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  -.  t  e.  ( D `  (
j  -  1 ) ) )
261112, 260eldifd 3274 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) )
262261exp31 588 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T )  ->  (
j  e.  ( J `
 t )  -> 
( A. k  e.  ( J `  t
) j  <_  k  ->  t  e.  ( ( D `  j ) 
\  ( D `  ( j  -  1 ) ) ) ) ) )
263106, 262reximdai 2757 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  ( E. j  e.  ( J `  t ) A. k  e.  ( J `  t )
j  <_  k  ->  E. j  e.  ( J `
 t ) t  e.  ( ( D `
 j )  \ 
( D `  (
j  -  1 ) ) ) ) )
264103, 263mpd 15 . . . . . . . 8  |-  ( (
ph  /\  t  e.  T )  ->  E. j  e.  ( J `  t
) t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) )
265 df-rex 2655 . . . . . . . 8  |-  ( E. j  e.  ( J `
 t ) t  e.  ( ( D `
 j )  \ 
( D `  (
j  -  1 ) ) )  <->  E. j
( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )
266264, 265sylib 189 . . . . . . 7  |-  ( (
ph  /\  t  e.  T )  ->  E. j
( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )
267 simprl 733 . . . . . . . . . 10  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  j  e.  ( J `  t ) )
268 eldifn 3413 . . . . . . . . . . . . 13  |-  ( t  e.  ( ( D `
 j )  \ 
( D `  (
j  -  1 ) ) )  ->  -.  t  e.  ( D `  ( j  -  1 ) ) )
269 simplr 732 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  t  e.  T )
270 simpll 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  ph )
271186adantrr 698 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  j  e.  ( 1 ... N
) )
272 simprr 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  -.  t  e.  ( D `  ( j  -  1 ) ) )
273 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  k  ->  (
j  -  ( 1  /  3 ) )  =  ( k  -  ( 1  /  3
) ) )
274273oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  k  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( k  -  ( 1  / 
3 ) )  x.  E ) )
275274breq2d 4165 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  k  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) ) )
276275rabbidv 2891 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  k  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) } )
277276cbvmptv 4241 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  ( 0 ... N )  |->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) } )  =  ( k  e.  ( 0 ... N
)  |->  { t  e.  T  |  ( F `
 t )  <_ 
( ( k  -  ( 1  /  3
) )  x.  E
) } )
27870, 277eqtri 2407 . . . . . . . . . . . . . . . . . . . . . 22  |-  D  =  ( k  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) } )
279278a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  D  =  ( k  e.  ( 0 ... N
)  |->  { t  e.  T  |  ( F `
 t )  <_ 
( ( k  -  ( 1  /  3
) )  x.  E
) } ) )
280 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( j  - 
1 )  ->  (
k  -  ( 1  /  3 ) )  =  ( ( j  -  1 )  -  ( 1  /  3
) ) )
281280oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( j  - 
1 )  ->  (
( k  -  (
1  /  3 ) )  x.  E )  =  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) )
282281breq2d 4165 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( j  - 
1 )  ->  (
( F `  t
)  <_  ( (
k  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )
283282rabbidv 2891 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( j  - 
1 )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( k  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E ) } )
284283adantl 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  j  e.  ( 1 ... N
) )  /\  k  =  ( j  - 
1 ) )  ->  { t  e.  T  |  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } )
285 fzssp1 11027 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... (
( N  -  1 )  +  1 ) )
286198oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 0 ... (
( N  -  1 )  +  1 ) )  =  ( 0 ... N ) )
287285, 286syl5sseq 3339 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
288287adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
0 ... ( N  - 
1 ) )  C_  ( 0 ... N
) )
289 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  j  e.  ( 1 ... N
) )
290203a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  1  e.  ZZ )
291207adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  N  e.  ZZ )
292240adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  j  e.  ZZ )
293 fzsubel 11020 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 1  e.  ZZ  /\  N  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( j  e.  ( 1 ... N )  <-> 
( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  - 
1 ) ) ) )
294290, 291, 292, 290, 293syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  e.  ( 1 ... N )  <->  ( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  -  1 ) ) ) )
295289, 294mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  -  1 ) ) )
296117a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
1  -  1 )  =  0 )
297296oveq1d 6035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
( 1  -  1 ) ... ( N  -  1 ) )  =  ( 0 ... ( N  -  1 ) ) )
298295, 297eleqtrd 2463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
299288, 298sseldd 3292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( 0 ... N ) )
30063adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  T  e.  _V )
301 rabexg 4294 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
302300, 301syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
303279, 284, 299, 302fvmptd 5749 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( D `  ( j  -  1 ) )  =  { t  e.  T  |  ( F `
 t )  <_ 
( ( ( j  -  1 )  -  ( 1  /  3
) )  x.  E
) } )
304303eleq2d 2454 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
t  e.  ( D `
 ( j  - 
1 ) )  <->  t  e.  { t  e.  T  | 
( F `  t
)  <_  ( (
( j  -  1 )  -  ( 1  /  3 ) )  x.  E ) } ) )
305304notbid 286 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( -.  t  e.  ( D `  ( j  -  1 ) )  <->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } ) )
306305biimpa 471 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 1 ... N
) )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } )
307270, 271, 272, 306syl21anc 1183 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  /  3
) )  x.  E
) } )
308 rabid 2827 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( ( j  -  1 )  -  ( 1  /  3
) )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  /  3
) )  x.  E
) ) )
309242adantrr 698 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  j  e.  RR )
310 recn 9013 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  j  e.  CC )
311196a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  1  e.  CC )
31226, 22, 233pm3.2i 1132 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )
313 redivcl 9665 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
1  /  3 )  e.  RR )
314 recn 9013 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1  /  3 )  e.  RR  ->  (
1  /  3 )  e.  CC )
315312, 313, 314mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  /  3 )  e.  CC
316315a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
1  /  3 )  e.  CC )
317310, 311, 316subsub4d 9374 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  RR  ->  (
( j  -  1 )  -  ( 1  /  3 ) )  =  ( j  -  ( 1  +  ( 1  /  3 ) ) ) )
318 3cn 10004 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  3  e.  CC
319318, 196, 318, 23divdiri 9703 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 3  +  1 )  /  3 )  =  ( ( 3  / 
3 )  +  ( 1  /  3 ) )
320 3p1e4 10036 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 3  +  1 )  =  4
321320oveq1i 6030 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 3  +  1 )  /  3 )  =  ( 4  /  3
)
322318, 23dividi 9679 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 3  /  3 )  =  1
323322oveq1i 6030 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 3  /  3 )  +  ( 1  / 
3 ) )  =  ( 1  +  ( 1  /  3 ) )
324319, 321, 3233eqtr3i 2415 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 4  /  3 )  =  ( 1  +  ( 1  /  3 ) )
325324a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
4  /  3 )  =  ( 1  +  ( 1  /  3
) ) )
326325oveq2d 6036 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  RR  ->  (
j  -  ( 4  /  3 ) )  =  ( j  -  ( 1  +  ( 1  /  3 ) ) ) )
327317, 326eqtr4d 2422 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  RR  ->  (
( j  -  1 )  -  ( 1  /  3 ) )  =  ( j  -  ( 4  /  3
) ) )
328327oveq1d 6035 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  RR  ->  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E )  =  ( ( j  -  ( 4  / 
3 ) )  x.  E ) )
329309, 328syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E )  =  ( ( j  -  ( 4  / 
3 ) )  x.  E ) )
330329breq2d 4165 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
( F `  t
)  <_  ( (
( j  -  1 )  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( j  -  (
4  /  3 ) )  x.  E ) ) )
331330anbi2d 685 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
( t  e.  T  /\  ( F `  t
)  <_  ( (
( j  -  1 )  -  ( 1  /  3 ) )  x.  E ) )  <-> 
( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) ) ) )
332308, 331syl5bb 249 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( ( j  -  ( 4  /  3
) )  x.  E
) ) ) )
333307, 332mtbid 292 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  -.  ( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) ) )
334 imnan 412 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  T  ->  -.  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) )  <->  -.  ( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) ) )
335333, 334sylibr 204 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
t  e.  T  ->  -.  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) ) )
336269, 335mpd 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  -.  ( F `  t )  <_  ( ( j  -  ( 4  / 
3 ) )  x.  E ) )
337268, 336sylanr2 635 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  -.  ( F `  t )  <_  ( ( j  -  ( 4  /  3
) )  x.  E
) )
338242adantrr 698 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  j  e.  RR )
339 4re 10005 . . . . . . . . . . . . . . . . 17  |-  4  e.  RR
340339a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  4  e.  RR )
34122a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  3  e.  RR )
34223a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  3  =/=  0 )
343340, 341, 342redivcld 9774 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( 4  /  3 )  e.  RR )
344338, 343resubcld 9397 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( j  -  ( 4  / 
3 ) )  e.  RR )
34538ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  E  e.  RR )
346 remulcl 9008 . . . . . . . . . . . . . . 15  |-  ( ( ( j  -  (
4  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( j  -  ( 4  /  3
) )  x.  E
)  e.  RR )
347346rexrd 9067 . . . . . . . . . . . . . 14  |-  ( ( ( j  -  (
4  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( j  -  ( 4  /  3
) )  x.  E
)  e.  RR* )
348344, 345, 347syl2anc 643 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( (
j  -  ( 4  /  3 ) )  x.  E )  e. 
RR* )
34947rexrd 9067 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR* )
350349adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( F `  t )  e.  RR* )
351 xrltnle 9077 . . . . . . . . . . . . 13  |-  ( ( ( ( j  -  ( 4  /  3
) )  x.  E
)  e.  RR*  /\  ( F `  t )  e.  RR* )  ->  (
( ( j  -  ( 4  /  3
) )  x.  E
)  <  ( F `  t )  <->  -.  ( F `  t )  <_  ( ( j  -  ( 4  /  3
) )  x.  E
) ) )
352348, 350, 351syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( (
( j  -  (
4  /  3 ) )  x.  E )  <  ( F `  t )  <->  -.  ( F `  t )  <_  ( ( j  -  ( 4  /  3
) )  x.  E
) ) )
353337, 352mpbird 224 . . . . . . . . . . 11  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( (
j  -  ( 4  /  3 ) )  x.  E )  < 
( F `  t
) )
354 simpl 444 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( ph  /\  t  e.  T ) )
355 simprr 734 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) )
356355eldifad 3275 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  t  e.  ( D `  j ) )
357 simplll 735 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  t  e.  ( D `  j ) )  ->  ph )
358186adantr 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  t  e.  ( D `  j ) )  ->  j  e.  ( 1 ... N
) )
359 simpr 448 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  t  e.  ( D `  j ) )  ->  t  e.  ( D `  j ) )
360 oveq1 6027 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
k  -  ( 1  /  3 ) )  =  ( j  -  ( 1  /  3
) ) )
361360oveq1d 6035 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
( k  -  (
1  /  3 ) )  x.  E )  =  ( ( j  -  ( 1  / 
3 ) )  x.  E ) )
362361breq2d 4165 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( F `  t
)  <_  ( (
k  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) ) )
363362rabbidv 2891 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  j  ->  { t  e.  T  |  ( F `  t )  <_  ( ( k  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
364363adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  j  e.  ( 1 ... N
) )  /\  k  =  j )  ->  { t  e.  T  |  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) } )
365 0p1e1 10025 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  +  1 )  =  1
366365oveq1i 6030 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  +  1 ) ... N )  =  ( 1 ... N
)
367 0z 10225 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  ZZ
368 fzp1ss 11030 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  e.  ZZ  ->  (
( 0  +  1 ) ... N ) 
C_  ( 0 ... N ) )
369367, 368ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  +  1 ) ... N )  C_  ( 0 ... N
)
370366, 369eqsstr3i 3322 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... N )  C_  ( 0 ... N
)
371370sseli 3287 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ( 0 ... N
) )
372371adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  j  e.  ( 0 ... N
) )
373 rabexg 4294 . . . . . . . . . . . . . . . . . . 19  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
374300, 373syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
375279, 364, 372, 374fvmptd 5749 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
376375eleq2d 2454 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
t  e.  ( D `
 j )  <->  t  e.  { t  e.  T  | 
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) } ) )
377376biimpa 471 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 1 ... N
) )  /\  t  e.  ( D `  j
) )  ->  t  e.  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
378357, 358, 359, 377syl21anc 1183 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  t  e.  ( D `  j ) )  ->  t  e.  { t  e.  T  | 
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) } )
379 rabid 2827 . . . . . . . . . . . . . 14  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( j  -  ( 1  /  3
) )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) ) )
380378, 379sylib 189 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  t  e.  ( D `  j ) )  ->  ( t  e.  T  /\  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) ) )
381380simprd 450 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  t  e.  ( D `  j ) )  ->  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )
382354, 267, 356, 381syl21anc 1183 . . . . . . . . . . 11  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) )
383353, 382jca 519 . . . . . . . . . 10  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( (
( j  -  (
4  /  3 ) )  x.  E )  <  ( F `  t )  /\  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) ) )
38415ad2antrr 707 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  N  e.  NN )
385 simplr 732 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  t  e.  T )
386186adantrr 698 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  j  e.  ( 1 ... N
) )
387 simplll 735 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( 0 ... N
) )  ->  ph )
388 nfv 1626 . . . . . . . . . . . . . . . 16  |-  F/ j  i  e.  ( 0 ... N )
389104, 388nfan 1836 . . . . . . . . . . . . . . 15  |-  F/ j ( ph  /\  i  e.  ( 0 ... N
) )
390 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ j ( X `  i
) : T --> RR
391389, 390nfim 1822 . . . . . . . . . . . . . 14  |-  F/ j ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  ( X `  i ) : T --> RR )
392 eleq1 2447 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  (
j  e.  ( 0 ... N )  <->  i  e.  ( 0 ... N
) ) )
393392anbi2d 685 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( ph  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  i  e.  ( 0 ... N ) ) ) )
394 fveq2 5668 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  ( X `  j )  =  ( X `  i ) )
395394feq1d 5520 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( X `  j
) : T --> RR  <->  ( X `  i ) : T --> RR ) )
396393, 395imbi12d 312 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  ( X `  j ) : T --> RR )  <->  ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  ( X `  i ) : T --> RR ) ) )
397 stoweidlem34.14 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( X `  j ) : T --> RR )
398391, 396, 397chvar 2021 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
399387, 398sylancom 649 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
400 simpr 448 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( 0 ... N
) )  ->  i  e.  ( 0 ... N
) )
401 simpllr 736 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( 0 ... N
) )  ->  t  e.  T )
402104, 388, 105nf3an 1839 . . . . . . . . . . . . . . 15  |-  F/ j ( ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  T )
403 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ j ( ( X `  i ) `  t
)  <_  1
404402, 403nfim 1822 . . . . . . . . . . . . . 14  |-  F/ j ( ( ph  /\  i  e.  ( 0 ... N )  /\  t  e.  T )  ->  ( ( X `  i ) `  t
)  <_  1 )
4053923anbi2d 1259 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( ph  /\  j  e.  ( 0 ... N
)  /\  t  e.  T )  <->  ( ph  /\  i  e.  ( 0 ... N )  /\  t  e.  T )
) )
406394fveq1d 5670 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  (
( X `  j
) `  t )  =  ( ( X `
 i ) `  t ) )
407406breq1d 4163 . . . . . . . . . . . . . . 15  |-  ( j  =  i  ->  (
( ( X `  j ) `  t
)  <_  1  <->  ( ( X `  i ) `  t )  <_  1
) )
408405, 407imbi12d 312 . . . . . . . . . . . . . 14  |-  ( j  =  i  ->  (
( ( ph  /\  j  e.  ( 0 ... N )  /\  t  e.  T )  ->  ( ( X `  j ) `  t
)  <_  1 )  <-> 
( ( ph  /\  i  e.  ( 0 ... N )  /\  t  e.  T )  ->  ( ( X `  i ) `  t
)  <_  1 ) ) )
409 stoweidlem34.16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  t  e.  T )  ->  (
( X `  j
) `  t )  <_  1 )
410404, 408, 409chvar 2021 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  T )  ->  (
( X `  i
) `  t )  <_  1 )
411387, 400, 401, 410syl3anc 1184 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  t )  <_  1 )
412 simplll 735 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( j ... N
) )  ->  ph )
413367a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  0  e.  ZZ )
414 elfzel2 10989 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( j ... N )  ->  N  e.  ZZ )
415414adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  N  e.  ZZ )
416 elfzelz 10991 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( j ... N )  ->  i  e.  ZZ )
417416adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  i  e.  ZZ )
418413, 415, 4173jca 1134 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  (
0  e.  ZZ  /\  N  e.  ZZ  /\  i  e.  ZZ ) )
419125a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  0  e.  RR )
420 elfzel1 10990 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( j ... N )  ->  j  e.  ZZ )
421420zred 10307 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( j ... N )  ->  j  e.  RR )
422421adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  j  e.  RR )
423416zred 10307 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( j ... N )  ->  i  e.  RR )
424423adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  i  e.  RR )
425125a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  0  e.  RR )
42626a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  1  e.  RR )
427 0le1 9483 . . . . . . . . . . . . . . . . . . . 20  |-  0  <_  1
428427a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  0  <_  1 )
429 elfzle1 10992 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... N )  ->  1  <_  j )
430186, 429syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  1  <_  j )
431425, 426, 242, 428, 430letrd 9159 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  0  <_  j )
432431adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  0  <_  j )
433 elfzle1 10992 . . . . . . . . . . . . . . . . . 18  |-  ( i  e.  ( j ... N )  ->  j  <_  i )
434433adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  j  <_  i )
435419, 422, 424, 432, 434letrd 9159 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  0  <_  i )
436 elfzle2 10993 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( j ... N )  ->  i  <_  N )
437436adantl 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  i  <_  N )
438435, 437jca 519 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  (
0  <_  i  /\  i  <_  N ) )
439 elfz2 10982 . . . . . . . . . . . . . . 15  |-  ( i  e.  ( 0 ... N )  <->  ( (
0  e.  ZZ  /\  N  e.  ZZ  /\  i  e.  ZZ )  /\  (
0  <_  i  /\  i  <_  N ) ) )
440418, 438, 439sylanbrc 646 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  i  e.  ( 0 ... N
) )
441440adantlrr 702 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( j ... N
) )  ->  i  e.  ( 0 ... N
) )
442 simpll 731 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( j ... N
) )  ->  ( ph  /\  t  e.  T
) )
443 simplrl 737 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( j ... N
) )  ->  j  e.  ( J `  t
) )
444 simplrr 738 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( j ... N
) )  ->  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) )
445444eldifad 3275 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( j ... N
) )  ->  t  e.  ( D `  j
) )
446 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  ( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )  /\  i  e.  ( j ... N
) )  ->  i  e.  ( j ... N
) )
447 simpl1 960 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  ( ph  /\  t  e.  T
) )
448447simprd 450 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  t  e.  T )
449447, 47syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  ( F `  t )  e.  RR )
450421adantl 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  j  e.  RR )
45124a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  (
1  /  3 )  e.  RR )
452450, 451resubcld 9397 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
453 simpl1l 1008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  ph )
454453, 38syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  E  e.  RR )
455452, 454remulcld 9049 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  e.  RR )
456423adantl 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  i  e.  RR )
45724a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
1  /  3 )  e.  RR )
458456, 457resubcld 9397 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
i  -  ( 1  /  3 ) )  e.  RR )
45938adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  E  e.  RR )
460458, 459remulcld 9049 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( i  -  (
1  /  3 ) )  x.  E )  e.  RR )
461453, 460sylancom 649 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  (
( i  -  (
1  /  3 ) )  x.  E )  e.  RR )
462 simpl3 962 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  t  e.  ( D `  j
) )
463 simpl2 961 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  j  e.  ( J `  t
) )
464447, 463, 186syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  j  e.  ( 1 ... N
) )
465453, 464, 375syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
466462, 465eleqtrd 2463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )  ->  t