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

Theorem stoweidlem34 27750
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 6098 . . . . . . . . 9  |-  ( 1 ... N )  e. 
_V
43rabex 4346 . . . . . . . 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 5804 . . . . . . . 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 3420 . . . . . . 7  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  C_  ( 1 ... N
)
97, 8syl6eqss 3390 . . . . . 6  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  C_  ( 1 ... N
) )
10 elfznn 11072 . . . . . . 7  |-  ( x  e.  ( 1 ... N )  ->  x  e.  NN )
1110ssriv 3344 . . . . . 6  |-  ( 1 ... N )  C_  NN
129, 11syl6ss 3352 . . . . 5  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  C_  NN )
13 nnssre 9996 . . . . 5  |-  NN  C_  RR
1412, 13syl6ss 3352 . . . 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 10513 . . . . . . . . . . . . . . 15  |-  NN  =  ( ZZ>= `  1 )
1816, 17syl6eleq 2525 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( ZZ>= `  1 )
)
19 eluzfz2 11057 . . . . . . . . . . . . . 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 10063 . . . . . . . . . . . . . . . . . . . . 21  |-  3  e.  RR
23 3ne0 10077 . . . . . . . . . . . . . . . . . . . . 21  |-  3  =/=  0
2422, 23rereccli 9771 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  /  3 )  e.  RR
2524a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  e.  RR )
26 1re 9082 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  RR
2726a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  1  e.  RR )
2816nnred 10007 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  RR )
29 1lt3 10136 . . . . . . . . . . . . . . . . . . . . 21  |-  1  <  3
3022, 29pm3.2i 442 . . . . . . . . . . . . . . . . . . . 20  |-  ( 3  e.  RR  /\  1  <  3 )
31 recgt1i 9899 . . . . . . . . . . . . . . . . . . . . 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 9631 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  1 )  <  ( N  -  ( 1  /  3
) ) )
3528, 27resubcld 9457 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  1 )  e.  RR )
3628, 25resubcld 9457 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  ( 1  /  3 ) )  e.  RR )
37 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  E  e.  RR+ )
3837rpred 10640 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  E  e.  RR )
3938adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  E  e.  RR )
4037rpgt0d 10643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  0  <  E )
4140adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  0  <  E )
42 ltmul1 9852 . . . . . . . . . . . . . . . . . . 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 27652 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR )
4835, 39remulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  x.  E )  e.  RR )
4936, 39remulcld 9108 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  (
1  /  3 ) )  x.  E )  e.  RR )
50 lttr 9144 . . . . . . . . . . . . . . . . . 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 9155 . . . . . . . . . . . . . . . . . . 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 2876 . . . . . . . . . . . . . . 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 10220 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  ->  N  e.  NN0 )
59 nn0uz 10512 . . . . . . . . . . . . . . . . . 18  |-  NN0  =  ( ZZ>= `  0 )
6058, 59syl6eleq 2525 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  N  e.  ( ZZ>= `  0 )
)
61 eluzfz2 11057 . . . . . . . . . . . . . . . . 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 4345 . . . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  N  ->  (
j  -  ( 1  /  3 ) )  =  ( N  -  ( 1  /  3
) ) )
6766oveq1d 6088 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  N  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( N  -  ( 1  / 
3 ) )  x.  E ) )
6867breq2d 4216 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  N  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) ) )
6968rabbidv 2940 . . . . . . . . . . . . . . . . 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 5796 . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  ( D `  N
) )
75 nfcv 2571 . . . . . . . . . . . . . 14  |-  F/_ j N
76 nfcv 2571 . . . . . . . . . . . . . 14  |-  F/_ j
( 1 ... N
)
77 nfmpt1 4290 . . . . . . . . . . . . . . . . 17  |-  F/_ j
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
7870, 77nfcxfr 2568 . . . . . . . . . . . . . . . 16  |-  F/_ j D
7978, 75nffv 5727 . . . . . . . . . . . . . . 15  |-  F/_ j
( D `  N
)
8079nfcri 2565 . . . . . . . . . . . . . 14  |-  F/ j  t  e.  ( D `
 N )
81 fveq2 5720 . . . . . . . . . . . . . . 15  |-  ( j  =  N  ->  ( D `  j )  =  ( D `  N ) )
8281eleq2d 2502 . . . . . . . . . . . . . 14  |-  ( j  =  N  ->  (
t  e.  ( D `
 j )  <->  t  e.  ( D `  N ) ) )
8375, 76, 80, 82elrabf 3083 . . . . . . . . . . . . 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 2512 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( J `  t
) )
86 ne0i 3626 . . . . . . . . . . 11  |-  ( N  e.  ( J `  t )  ->  ( J `  t )  =/=  (/) )
8785, 86syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  =/=  (/) )
88 nnwo 10534 . . . . . . . . . . 11  |-  ( ( ( J `  t
)  C_  NN  /\  ( J `  t )  =/=  (/) )  ->  E. i  e.  ( J `  t
) A. k  e.  ( J `  t
) i  <_  k
)
89 nfcv 2571 . . . . . . . . . . . 12  |-  F/_ i
( J `  t
)
90 nfcv 2571 . . . . . . . . . . . . . . 15  |-  F/_ j T
91 nfrab1 2880 . . . . . . . . . . . . . . 15  |-  F/_ j { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }
9290, 91nfmpt 4289 . . . . . . . . . . . . . 14  |-  F/_ j
( t  e.  T  |->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
935, 92nfcxfr 2568 . . . . . . . . . . . . 13  |-  F/_ j J
94 nfcv 2571 . . . . . . . . . . . . 13  |-  F/_ j
t
9593, 94nffv 5727 . . . . . . . . . . . 12  |-  F/_ j
( J `  t
)
96 nfv 1629 . . . . . . . . . . . . 13  |-  F/ j  i  <_  k
9795, 96nfral 2751 . . . . . . . . . . . 12  |-  F/ j A. k  e.  ( J `  t ) i  <_  k
98 nfv 1629 . . . . . . . . . . . 12  |-  F/ i A. k  e.  ( J `  t ) j  <_  k
99 breq1 4207 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
i  <_  k  <->  j  <_  k ) )
10099ralbidv 2717 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( A. k  e.  ( J `  t )
i  <_  k  <->  A. k  e.  ( J `  t
) j  <_  k
) )
10189, 95, 97, 98, 100cbvrexf 2919 . . . . . . . . . . 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 1629 . . . . . . . . . . 11  |-  F/ j  t  e.  T
106104, 105nfan 1846 . . . . . . . . . 10  |-  F/ j ( ph  /\  t  e.  T )
1077eleq2d 2502 . . . . . . . . . . . . . . . 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 2876 . . . . . . . . . . . . . . 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 3624 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  -.  t  e.  (/)
116 oveq1 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  1  ->  (
j  -  1 )  =  ( 1  -  1 ) )
117 1m1e0 10060 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 1  -  1 )  =  0
118116, 117syl6eq 2483 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  1  ->  (
j  -  1 )  =  0 )
119118fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  e.  RR )
123122renegcld 9456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  t  e.  T )  ->  -u (
1  /  3 )  e.  RR )
124123, 39remulcld 9108 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  e.  RR )
125 0re 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  0  e.  RR
126125a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  T )  ->  0  e.  RR )
127 3pos 10076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  <  3
12822, 127recgt0ii 9908 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  <  ( 1  /  3
)
129 lt0neg2 9527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9852 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( E  e.  RR  ->  (
0  x.  E )  =  0 )
13639, 135syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  t  e.  T )  ->  (
0  x.  E )  =  0 )
137134, 136breqtrd 4228 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  <  ( F `  t ) )
140124, 47ltnled 9212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10266 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  N  e.  NN0 )
147 elnn0uz 10515 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  NN0  <->  N  e.  ( ZZ>=
`  0 ) )
148146, 147sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
149 eluzfz1 11056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... N
) )
150148, 149syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  0  e.  ( 0 ... N ) )
151 rabexg 4345 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  =  0  ->  (
j  -  ( 1  /  3 ) )  =  ( 0  -  ( 1  /  3
) ) )
154 df-neg 9286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  -u (
1  /  3 )  =  ( 0  -  ( 1  /  3
) )
155153, 154syl6eqr 2485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  =  0  ->  (
j  -  ( 1  /  3 ) )  =  -u ( 1  / 
3 ) )
156155oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  =  0  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( -u (
1  /  3 )  x.  E ) )
157156breq2d 4216 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( j  =  0  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) ) )
158157rabbidv 2940 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  -.  t  e.  ( D `  0 ) )
1621, 161alrimi 1781 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  A. t  -.  t  e.  ( D `  0
) )
163 eq0 3634 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( D `  0 )  =  (/)  <->  A. s  -.  s  e.  ( D `  0
) )
164 nfcv 2571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/_ t
( 0 ... N
)
165 nfrab1 2880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/_ t { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
166164, 165nfmpt 4289 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
16770, 166nfcxfr 2568 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/_ t D
168 nfcv 2571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/_ t
0
169167, 168nffv 5727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/_ t
( D `  0
)
170169nfcri 2565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/ t  s  e.  ( D `
 0 )
171170nfn 1811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ t  -.  s  e.  ( D `  0 )
172 nfv 1629 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ s  -.  t  e.  ( D `  0 )
173 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2489 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  = 
1 )  ->  ( D `  ( j  -  1 ) )  =  (/) )
179178eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . . . . . 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 2525 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
188187adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( J `  t ) )  ->  N  e.  ( ZZ>= `  1 )
)
189 elfzp12 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11087 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1 ... ( N  - 
1 ) )  C_  ( 1 ... (
( N  -  1 )  +  1 ) )
19515nncnd 10008 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  N  e.  CC )
196 ax-1cn 9040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  1  e.  CC
197196a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  1  e.  CC )
198195, 197npcand 9407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
199198oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( 1 ... (
( N  -  1 )  +  1 ) )  =  ( 1 ... N ) )
200194, 199syl5sseq 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  1  e.  ZZ
204 zaddcl 10309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10366 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  N  e.  ZZ )
208207adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  N  e.  ZZ )
209 elfzelz 11051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11080 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 9303 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 1  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  1 )  -  1 )  =  1 )
216196, 196, 215mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 1  +  1 )  -  1 )  =  1
217216oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 1  +  1 )  -  1 ) ... ( N  - 
1 ) )  =  ( 1 ... ( N  -  1 ) )
218214, 217syl6eleq 2525 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  -  1 )  e.  ( 1 ... ( N  -  1 ) ) )
219201, 218sseldd 3341 . . . . . . . . . . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  ( j  - 
1 )  ->  ( D `  i )  =  ( D `  ( j  -  1 ) ) )
225224eleq2d 2502 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( i  =  ( j  - 
1 )  ->  (
t  e.  ( D `
 i )  <->  t  e.  ( D `  ( j  -  1 ) ) ) )
226225elrab3 3085 . . . . . . . . . . . . . . . . . . . . 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 2571 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ i
( 1 ... N
)
230 nfv 1629 . . . . . . . . . . . . . . . . . . . 20  |-  F/ i  t  e.  ( D `
 j )
231 nfcv 2571 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ j
i
23278, 231nffv 5727 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ j
( D `  i
)
233232nfcri 2565 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j  t  e.  ( D `
 i )
234 fveq2 5720 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  i  ->  ( D `  j )  =  ( D `  i ) )
235234eleq2d 2502 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  i  ->  (
t  e.  ( D `
 j )  <->  t  e.  ( D `  i ) ) )
23676, 229, 230, 233, 235cbvrab 2946 . . . . . . . . . . . . . . . . . . 19  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  =  { i  e.  ( 1 ... N )  |  t  e.  ( D `  i ) }
237228, 236syl6eleqr 2526 . . . . . . . . . . . . . . . . . 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 2512 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e.  ( J `  t
) )
240 elfzelz 11051 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ZZ )
241 zre 10278 . . . . . . . . . . . . . . . . . . . . 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 9359 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  RR  ->  (
j  -  1 )  e.  RR )
245243, 244ex-natded5.3i 21709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  e.  RR  /\  ( j  -  1 )  e.  RR ) )
246 ltm1 9842 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  RR  ->  (
j  -  1 )  <  j )
247246adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( j  e.  RR  /\  ( j  -  1 )  e.  RR )  ->  ( j  - 
1 )  <  j
)
248 ltnle 9147 . . . . . . . . . . . . . . . . . . . 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 4208 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  ( j  - 
1 )  ->  (
j  <_  k  <->  j  <_  ( j  -  1 ) ) )
253252notbid 286 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( j  - 
1 )  ->  ( -.  j  <_  k  <->  -.  j  <_  ( j  -  1 ) ) )
254253rspcev 3044 . . . . . . . . . . . . . . . . 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 2708 . . . . . . . . . . . . . . . 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 3323 . . . . . . . . . . 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 2806 . . . . . . . . 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 2703 . . . . . . . 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 3462 . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  k  ->  (
j  -  ( 1  /  3 ) )  =  ( k  -  ( 1  /  3
) ) )
274273oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  k  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( k  -  ( 1  / 
3 ) )  x.  E ) )
275274breq2d 4216 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  k  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) ) )
276275rabbidv 2940 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  k  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) } )
277276cbvmptv 4292 . . . . . . . . . . . . . . . . . . . . . . 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 2455 . . . . . . . . . . . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( j  - 
1 )  ->  (
k  -  ( 1  /  3 ) )  =  ( ( j  -  1 )  -  ( 1  /  3
) ) )
281280oveq1d 6088 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( j  - 
1 )  ->  (
( k  -  (
1  /  3 ) )  x.  E )  =  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) )
282281breq2d 4216 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( j  - 
1 )  ->  (
( F `  t
)  <_  ( (
k  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )
283282rabbidv 2940 . . . . . . . . . . . . . . . . . . . . . 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 11087 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... (
( N  -  1 )  +  1 ) )
286198oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 0 ... (
( N  -  1 )  +  1 ) )  =  ( 0 ... N ) )
287285, 286syl5sseq 3388 . . . . . . . . . . . . . . . . . . . . . . 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 11080 . . . . . . . . . . . . . . . . . . . . . . . . 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 6088 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
( 1  -  1 ) ... ( N  -  1 ) )  =  ( 0 ... ( N  -  1 ) ) )
298295, 297eleqtrd 2511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
299288, 298sseldd 3341 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( 0 ... N ) )
30063adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  T  e.  _V )
301 rabexg 4345 . . . . . . . . . . . . . . . . . . . . . 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 5802 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( D `  ( j  -  1 ) )  =  { t  e.  T  |  ( F `
 t )  <_ 
( ( ( j  -  1 )  -  ( 1  /  3
) )  x.  E
) } )
304303eleq2d 2502 . . . . . . . . . . . . . . . . . . 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 2876 . . . . . . . . . . . . . . . . 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 9072 . . . . . . . . . . . . . . . . . . . . . . 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 9725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
1  /  3 )  e.  RR )
314 recn 9072 . . . . . . . . . . . . . . . . . . . . . . . . 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 9434 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  RR  ->  (
( j  -  1 )  -  ( 1  /  3 ) )  =  ( j  -  ( 1  +  ( 1  /  3 ) ) ) )
318 3cn 10064 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  3  e.  CC
319318, 196, 318, 23divdiri 9763 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 3  +  1 )  /  3 )  =  ( ( 3  / 
3 )  +  ( 1  /  3 ) )
320 3p1e4 10096 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 3  +  1 )  =  4
321320oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 3  +  1 )  /  3 )  =  ( 4  /  3
)
322318, 23dividi 9739 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 3  /  3 )  =  1
323322oveq1i 6083 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 3  /  3 )  +  ( 1  / 
3 ) )  =  ( 1  +  ( 1  /  3 ) )
324319, 321, 3233eqtr3i 2463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 4  /  3 )  =  ( 1  +  ( 1  /  3 ) )
325324a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
4  /  3 )  =  ( 1  +  ( 1  /  3
) ) )
326325oveq2d 6089 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  RR  ->  (
j  -  ( 4  /  3 ) )  =  ( j  -  ( 1  +  ( 1  /  3 ) ) ) )
327317, 326eqtr4d 2470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  RR  ->  (
( j  -  1 )  -  ( 1  /  3 ) )  =  ( j  -  ( 4  /  3
) ) )
328327oveq1d 6088 . . . . . . . . . . . . . . . . . . . 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 4216 . . . . . . . . . . . . . . . . . 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 10065 . . . . . . . . . . . . . . . . 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 9834 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( 4  /  3 )  e.  RR )
344338, 343resubcld 9457 . . . . . . . . . . . . . 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 9067 . . . . . . . . . . . . . . 15  |-  ( ( ( j  -  (
4  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( j  -  ( 4  /  3
) )  x.  E
)  e.  RR )
347346rexrd 9126 . . . . . . . . . . . . . 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 9126 . . . . . . . . . . . . . 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 9136 . . . . . . . . . . . . 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 3324 . . . . . . . . . . . 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 6080 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  j  ->  (
k  -  ( 1  /  3 ) )  =  ( j  -  ( 1  /  3
) ) )
361360oveq1d 6088 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  j  ->  (
( k  -  (
1  /  3 ) )  x.  E )  =  ( ( j  -  ( 1  / 
3 ) )  x.  E ) )
362361breq2d 4216 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  j  ->  (
( F `  t
)  <_  ( (
k  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) ) )
363362rabbidv 2940 . . . . . . . . . . . . . . . . . . 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 10085 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  +  1 )  =  1
366365oveq1i 6083 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  +  1 ) ... N )  =  ( 1 ... N
)
367 0z 10285 . . . . . . . . . . . . . . . . . . . . . 22  |-  0  e.  ZZ
368 fzp1ss 11090 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  e.  ZZ  ->  (
( 0  +  1 ) ... N ) 
C_  ( 0 ... N ) )
369367, 368ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 0  +  1 ) ... N )  C_  ( 0 ... N
)
370366, 369eqsstr3i 3371 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... N )  C_  ( 0 ... N
)
371370sseli 3336 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ( 0 ... N
) )
372371adantl 453 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  j  e.  ( 0 ... N
) )
373 rabexg 4345 . . . . . . . . . . . . . . . . . . 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 5802 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
376375eleq2d 2502 . . . . . . . . . . . . . . . 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 2876 . . . . . . . . . . . . . 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 1629 . . . . . . . . . . . . . . . 16  |-  F/ j  i  e.  ( 0 ... N )
389104, 388nfan 1846 . . . . . . . . . . . . . . 15  |-  F/ j ( ph  /\  i  e.  ( 0 ... N
) )
390 nfv 1629 . . . . . . . . . . . . . . 15  |-  F/ j ( X `  i
) : T --> RR
391389, 390nfim 1832 . . . . . . . . . . . . . 14  |-  F/ j ( ( ph  /\  i  e.  ( 0 ... N ) )  ->  ( X `  i ) : T --> RR )
392 eleq1 2495 . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  ( X `  j )  =  ( X `  i ) )
395394feq1d 5572 . . . . . . . . . . . . . . 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 1968 . . . . . . . . . . . . 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 1849 . . . . . . . . . . . . . . 15  |-  F/ j ( ph  /\  i  e.  ( 0 ... N
)  /\  t  e.  T )
403 nfv 1629 . . . . . . . . . . . . . . 15  |-  F/ j ( ( X `  i ) `  t
)  <_  1
404402, 403nfim 1832 . . . . . . . . . . . . . 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 5722 . . . . . . . . . . . . . . . 16  |-  ( j  =  i  ->  (
( X `  j
) `  t )  =  ( ( X `
 i ) `  t ) )
407406breq1d 4214 . . . . . . . . . . . . . . 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 1968 . . . . . . . . . . . . 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 11049 . . . . . . . . . . . . . . . . 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 11051 . . . . . . . . . . . . . . . . 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 11050 . . . . . . . . . . . . . . . . . . 19  |-  ( i  e.  ( j ... N )  ->  j  e.  ZZ )
421420zred 10367 . . . . . . . . . . . . . . . . . 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 10367 . . . . . . . . . . . . . . . . . 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 9543 . . . . . . . . . . . . . . . . . . . 20  |-  0  <_  1
428427a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  0  <_  1 )
429 elfzle1 11052 . . . . . . . . . . . . . . . . . . . 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 9219 . . . . . . . . . . . . . . . . . 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 11052 . . . . . . . . . . . . . . . . . 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 9219 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  i  e.  ( j ... N
) )  ->  0  <_  i )
436 elfzle2 11053 . . . . . . . . . . . . . . . . 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 11042 . . . . . . . . . . . . . . 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 3324 . . . . . . . . . . . . . 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 9457 . . . . . . . . . . . . . . . . . 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 9108 . . . . . . . . . . . . . . . . 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 9457 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
i  -  ( 1  /  3 ) )  e.  RR )
45938adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  E  e.  RR )
460458, 459remulcld 9108 . . . . . . . . . . . . . . . . . 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 2511 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )  /\  t  e.  ( D `  j )
)  /\  i  e.  ( j ... N
) )