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

Theorem stoweidlem34 27886
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 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  T )
3 ovex 5899 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... N )  e. 
_V
4 rabexg 4180 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1 ... N )  e.  _V  ->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  e.  _V )
53, 4ax-mp 8 . . . . . . . . . . . . . . . . 17  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  e.  _V
65a1i 10 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  e.  _V )
72, 6jca 518 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  T )  ->  (
t  e.  T  /\  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) }  e.  _V ) )
8 stoweidlem34.6 . . . . . . . . . . . . . . . 16  |-  J  =  ( t  e.  T  |->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
98fvmpt2 5624 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  T  /\  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) }  e.  _V )  -> 
( J `  t
)  =  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
107, 9syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  =  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
11 ssrab2 3271 . . . . . . . . . . . . . . 15  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  C_  ( 1 ... N
)
1211a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  C_  ( 1 ... N
) )
1310, 12jca 518 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  T )  ->  (
( J `  t
)  =  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  /\  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) } 
C_  ( 1 ... N ) ) )
14 sseq1 3212 . . . . . . . . . . . . . 14  |-  ( ( J `  t )  =  { j  e.  ( 1 ... N
)  |  t  e.  ( D `  j
) }  ->  (
( J `  t
)  C_  ( 1 ... N )  <->  { j  e.  ( 1 ... N
)  |  t  e.  ( D `  j
) }  C_  (
1 ... N ) ) )
1514biimpar 471 . . . . . . . . . . . . 13  |-  ( ( ( J `  t
)  =  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  /\  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) } 
C_  ( 1 ... N ) )  -> 
( J `  t
)  C_  ( 1 ... N ) )
1613, 15syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  C_  ( 1 ... N
) )
17 elfznn 10835 . . . . . . . . . . . . . 14  |-  ( x  e.  ( 1 ... N )  ->  x  e.  NN )
1817ssriv 3197 . . . . . . . . . . . . 13  |-  ( 1 ... N )  C_  NN
1918a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  T )  ->  (
1 ... N )  C_  NN )
2016, 19sstrd 3202 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  C_  NN )
21 stoweidlem34.7 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  NN )
2221adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  NN )
23 nnuz 10279 . . . . . . . . . . . . . . . . 17  |-  NN  =  ( ZZ>= `  1 )
2422, 23syl6eleq 2386 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( ZZ>= `  1 )
)
25 eluzfz2 10820 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  1
)  ->  N  e.  ( 1 ... N
) )
2624, 25syl 15 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( 1 ... N
) )
27 stoweidlem34.11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  <  ( ( N  - 
1 )  x.  E
) )
28 3re 9833 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  3  e.  RR
29 1lt3 9904 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  1  <  3
3028, 29pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 3  e.  RR  /\  1  <  3 )
3130a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  T )  ->  (
3  e.  RR  /\  1  <  3 ) )
32 recgt1i 9669 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 3  e.  RR  /\  1  <  3 )  -> 
( 0  <  (
1  /  3 )  /\  ( 1  / 
3 )  <  1
) )
3332simprd 449 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 3  e.  RR  /\  1  <  3 )  -> 
( 1  /  3
)  <  1 )
3431, 33syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  <  1 )
35 1re 8853 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  1  e.  RR
36 3ne0 9847 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  3  =/=  0
3735, 28, 363pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )
38 redivcl 9495 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
1  /  3 )  e.  RR )
3937, 38ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  /  3 )  e.  RR
4039a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  e.  RR )
4135a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  T )  ->  1  e.  RR )
42 nnre 9769 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN  ->  N  e.  RR )
4322, 42syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  RR )
4440, 41, 433jca 1132 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  T )  ->  (
( 1  /  3
)  e.  RR  /\  1  e.  RR  /\  N  e.  RR ) )
45 ltsub2 9287 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1  /  3
)  e.  RR  /\  1  e.  RR  /\  N  e.  RR )  ->  (
( 1  /  3
)  <  1  <->  ( N  -  1 )  < 
( N  -  (
1  /  3 ) ) ) )
4644, 45syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  T )  ->  (
( 1  /  3
)  <  1  <->  ( N  -  1 )  < 
( N  -  (
1  /  3 ) ) ) )
4734, 46mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  1 )  <  ( N  -  ( 1  /  3
) ) )
4843, 41jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  T )  ->  ( N  e.  RR  /\  1  e.  RR ) )
49 resubcl 9127 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  RR  /\  1  e.  RR )  ->  ( N  -  1 )  e.  RR )
5048, 49syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  1 )  e.  RR )
5143, 40jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  T )  ->  ( N  e.  RR  /\  (
1  /  3 )  e.  RR ) )
52 resubcl 9127 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( N  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( N  -  ( 1  /  3
) )  e.  RR )
5351, 52syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  T )  ->  ( N  -  ( 1  /  3 ) )  e.  RR )
54 stoweidlem34.12 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  E  e.  RR+ )
55 rpre 10376 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E  e.  RR+  ->  E  e.  RR )
5654, 55syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  E  e.  RR )
5756adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  T )  ->  E  e.  RR )
58 rpgt0 10381 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( E  e.  RR+  ->  0  < 
E )
5954, 58syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  0  <  E )
6059adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  T )  ->  0  <  E )
6157, 60jca 518 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  T )  ->  ( E  e.  RR  /\  0  <  E ) )
6250, 53, 613jca 1132 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  e.  RR  /\  ( N  -  (
1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
63 ltmul1 9622 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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
) ) )
6462, 63syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  <  ( N  -  ( 1  / 
3 ) )  <->  ( ( N  -  1 )  x.  E )  < 
( ( N  -  ( 1  /  3
) )  x.  E
) ) )
6547, 64mpbid 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  x.  E )  <  ( ( N  -  ( 1  / 
3 ) )  x.  E ) )
6627, 65jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  t  e.  T )  ->  (
( F `  t
)  <  ( ( N  -  1 )  x.  E )  /\  ( ( N  - 
1 )  x.  E
)  <  ( ( N  -  ( 1  /  3 ) )  x.  E ) ) )
67 stoweidlem34.9 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F : T --> RR )
6867adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  t  e.  T )  ->  F : T --> RR )
6968, 2jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  T )  ->  ( F : T --> RR  /\  t  e.  T )
)
70 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F : T --> RR  /\  t  e.  T )  ->  ( F `  t
)  e.  RR )
7169, 70syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR )
7250, 57jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  e.  RR  /\  E  e.  RR )
)
73 remulcl 8838 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  -  1 )  e.  RR  /\  E  e.  RR )  ->  ( ( N  - 
1 )  x.  E
)  e.  RR )
7472, 73syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  1 )  x.  E )  e.  RR )
7553, 57jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  (
1  /  3 ) )  e.  RR  /\  E  e.  RR )
)
76 remulcl 8838 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( N  -  (
1  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( N  -  ( 1  /  3
) )  x.  E
)  e.  RR )
7775, 76syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  t  e.  T )  ->  (
( N  -  (
1  /  3 ) )  x.  E )  e.  RR )
7871, 74, 773jca 1132 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  t  e.  T )  ->  (
( F `  t
)  e.  RR  /\  ( ( N  - 
1 )  x.  E
)  e.  RR  /\  ( ( N  -  ( 1  /  3
) )  x.  E
)  e.  RR ) )
79 lttr 8915 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) )
80 3simpb 953 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( F `  t
)  e.  RR  /\  ( ( N  - 
1 )  x.  E
)  e.  RR  /\  ( ( N  -  ( 1  /  3
) )  x.  E
)  e.  RR )  ->  ( ( F `
 t )  e.  RR  /\  ( ( N  -  ( 1  /  3 ) )  x.  E )  e.  RR ) )
81 ltle 8926 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) )
8280, 81syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 ) ) )
8379, 82syld 40 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 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 ) ) )
8478, 83syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) )
8566, 84mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  <_  ( ( N  -  ( 1  /  3
) )  x.  E
) )
862, 85jca 518 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  e.  T )  ->  (
t  e.  T  /\  ( F `  t )  <_  ( ( N  -  ( 1  / 
3 ) )  x.  E ) ) )
87 rabid 2729 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( N  -  ( 1  /  3
) )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( ( N  -  ( 1  /  3
) )  x.  E
) ) )
8886, 87sylibr 203 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) } )
89 nnnn0 9988 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( N  e.  NN  ->  N  e.  NN0 )
90 nn0uz 10278 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  0 )
9189, 90syl6eleq 2386 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN  ->  N  e.  ( ZZ>= `  0 )
)
9221, 91syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
93 eluzfz2 10820 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( ZZ>= `  0
)  ->  N  e.  ( 0 ... N
) )
9492, 93syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ( 0 ... N ) )
95 stoweidlem34.8 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  _V )
96 rabexg 4180 . . . . . . . . . . . . . . . . . . . 20  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( N  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
9795, 96syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) }  e.  _V )
9894, 97jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( N  e.  ( 0 ... N )  /\  { t  e.  T  |  ( F `
 t )  <_ 
( ( N  -  ( 1  /  3
) )  x.  E
) }  e.  _V ) )
99 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  N  ->  (
j  -  ( 1  /  3 ) )  =  ( N  -  ( 1  /  3
) ) )
10099oveq1d 5889 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  N  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( N  -  ( 1  / 
3 ) )  x.  E ) )
101100breq2d 4051 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  N  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) ) )
102101rabbidv 2793 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  N  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) } )
103 stoweidlem34.4 . . . . . . . . . . . . . . . . . . 19  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
104102, 103fvmptg 5616 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) } )
10598, 104syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( D `  N
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( N  -  ( 1  / 
3 ) )  x.  E ) } )
106105adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  T )  ->  ( D `  N )  =  { t  e.  T  |  ( F `  t )  <_  (
( N  -  (
1  /  3 ) )  x.  E ) } )
10788, 106eleqtrrd 2373 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  T )  ->  t  e.  ( D `  N
) )
10826, 107jca 518 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  T )  ->  ( N  e.  ( 1 ... N )  /\  t  e.  ( D `  N ) ) )
109 nfcv 2432 . . . . . . . . . . . . . . 15  |-  F/_ j N
110 nfcv 2432 . . . . . . . . . . . . . . 15  |-  F/_ j
( 1 ... N
)
111 nfcv 2432 . . . . . . . . . . . . . . . 16  |-  F/_ j
t
112 nfmpt1 4125 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
113103, 112nfcxfr 2429 . . . . . . . . . . . . . . . . 17  |-  F/_ j D
114113, 109nffv 5548 . . . . . . . . . . . . . . . 16  |-  F/_ j
( D `  N
)
115111, 114nfel 2440 . . . . . . . . . . . . . . 15  |-  F/ j  t  e.  ( D `
 N )
116 fveq2 5541 . . . . . . . . . . . . . . . 16  |-  ( j  =  N  ->  ( D `  j )  =  ( D `  N ) )
117116eleq2d 2363 . . . . . . . . . . . . . . 15  |-  ( j  =  N  ->  (
t  e.  ( D `
 j )  <->  t  e.  ( D `  N ) ) )
118109, 110, 115, 117elrabf 2935 . . . . . . . . . . . . . 14  |-  ( N  e.  { j  e.  ( 1 ... N
)  |  t  e.  ( D `  j
) }  <->  ( N  e.  ( 1 ... N
)  /\  t  e.  ( D `  N ) ) )
119108, 118sylibr 203 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
12010eleq2d 2363 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  T )  ->  ( N  e.  ( J `  t )  <->  N  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) } ) )
121119, 120mpbird 223 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  e.  T )  ->  N  e.  ( J `  t
) )
122 ne0i 3474 . . . . . . . . . . . 12  |-  ( N  e.  ( J `  t )  ->  ( J `  t )  =/=  (/) )
123121, 122syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  t  e.  T )  ->  ( J `  t )  =/=  (/) )
12420, 123jca 518 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T )  ->  (
( J `  t
)  C_  NN  /\  ( J `  t )  =/=  (/) ) )
125 nnwo 10300 . . . . . . . . . . 11  |-  ( ( ( J `  t
)  C_  NN  /\  ( J `  t )  =/=  (/) )  ->  E. i  e.  ( J `  t
) A. k  e.  ( J `  t
) i  <_  k
)
126 nfcv 2432 . . . . . . . . . . . 12  |-  F/_ i
( J `  t
)
127 nfcv 2432 . . . . . . . . . . . . . . . . 17  |-  F/_ j T
128 nfrab1 2733 . . . . . . . . . . . . . . . . 17  |-  F/_ j { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }
129127, 128nfmpt 4124 . . . . . . . . . . . . . . . 16  |-  F/_ j
( t  e.  T  |->  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
1308, 129nfcxfr 2429 . . . . . . . . . . . . . . 15  |-  F/_ j J
131130, 111nffv 5548 . . . . . . . . . . . . . 14  |-  F/_ j
( J `  t
)
132131idi 2 . . . . . . . . . . . . 13  |-  F/_ j
( J `  t
)
133132idi 2 . . . . . . . . . . . 12  |-  F/_ j
( J `  t
)
134 nfv 1609 . . . . . . . . . . . . 13  |-  F/ j  i  <_  k
135131, 134nfral 2609 . . . . . . . . . . . 12  |-  F/ j A. k  e.  ( J `  t ) i  <_  k
136 nfv 1609 . . . . . . . . . . . 12  |-  F/ i A. k  e.  ( J `  t ) j  <_  k
137 breq1 4042 . . . . . . . . . . . . 13  |-  ( i  =  j  ->  (
i  <_  k  <->  j  <_  k ) )
138137ralbidv 2576 . . . . . . . . . . . 12  |-  ( i  =  j  ->  ( A. k  e.  ( J `  t )
i  <_  k  <->  A. k  e.  ( J `  t
) j  <_  k
) )
139126, 133, 135, 136, 138cbvrexf 2772 . . . . . . . . . . 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 )
140125, 139sylib 188 . . . . . . . . . 10  |-  ( ( ( J `  t
)  C_  NN  /\  ( J `  t )  =/=  (/) )  ->  E. j  e.  ( J `  t
) A. k  e.  ( J `  t
) j  <_  k
)
141124, 140syl 15 . . . . . . . . 9  |-  ( (
ph  /\  t  e.  T )  ->  E. j  e.  ( J `  t
) A. k  e.  ( J `  t
) j  <_  k
)
142 stoweidlem34.2 . . . . . . . . . . 11  |-  F/ j
ph
143 nfv 1609 . . . . . . . . . . 11  |-  F/ j  t  e.  T
144142, 143nfan 1783 . . . . . . . . . 10  |-  F/ j ( ph  /\  t  e.  T )
14510eleq2d 2363 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  e.  T )  ->  (
j  e.  ( J `
 t )  <->  j  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) } ) )
146145biimpa 470 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  j  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
147 rabid 2729 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  { j  e.  ( 1 ... N
)  |  t  e.  ( D `  j
) }  <->  ( j  e.  ( 1 ... N
)  /\  t  e.  ( D `  j ) ) )
148146, 147sylib 188 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
j  e.  ( 1 ... N )  /\  t  e.  ( D `  j ) ) )
149148simprd 449 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  t  e.  ( D `  j
) )
150149adantr 451 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  t  e.  ( D `  j ) )
151 simpll 730 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  ( ph  /\  t  e.  T ) )
152 simplr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  j  e.  ( J `  t ) )
153 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  A. k  e.  ( J `  t
) j  <_  k
)
154151, 152, 1533jca 1132 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  ( ( ph  /\  t  e.  T
)  /\  j  e.  ( J `  t )  /\  A. k  e.  ( J `  t
) j  <_  k
) )
155 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  t  e.  ( D `  ( j  -  1 ) ) )
156 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ph )
157156, 155jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( ph  /\  t  e.  ( D `
 ( j  - 
1 ) ) ) )
158 noel 3472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  -.  t  e.  (/)
159 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  =  1  ->  (
j  -  1 )  =  ( 1  -  1 ) )
160 ax-1cn 8811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  1  e.  CC
161 subid 9083 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 1  e.  CC  ->  (
1  -  1 )  =  0 )
162160, 161ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 1  -  1 )  =  0
163159, 162syl6eq 2344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  =  1  ->  (
j  -  1 )  =  0 )
164163fveq2d 5545 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( j  =  1  ->  ( D `  ( j  -  1 ) )  =  ( D ` 
0 ) )
165164adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  = 
1 )  ->  ( D `  ( j  -  1 ) )  =  ( D ` 
0 ) )
166 0lt1 9312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  0  <  1
16735, 166pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( 1  e.  RR  /\  0  <  1 )
168 3pos 9846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  0  <  3
16928, 168pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( 3  e.  RR  /\  0  <  3 )
170167, 169pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( 1  e.  RR  /\  0  <  1 )  /\  ( 3  e.  RR  /\  0  <  3 ) )
171 divgt0 9640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( ( 1  e.  RR  /\  0  <  1 )  /\  ( 3  e.  RR  /\  0  <  3 ) )  -> 
0  <  ( 1  /  3 ) )
172170, 171ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  0  <  ( 1  /  3
)
173 lt0neg2 9297 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( 1  /  3 )  e.  RR  ->  (
0  <  ( 1  /  3 )  <->  -u ( 1  /  3 )  <  0 ) )
17439, 173ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( 0  <  ( 1  / 
3 )  <->  -u ( 1  /  3 )  <  0 )
175172, 174mpbi 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  -u (
1  /  3 )  <  0
176175a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  t  e.  T )  ->  -u (
1  /  3 )  <  0 )
17728a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  t  e.  T )  ->  3  e.  RR )
17836a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( (
ph  /\  t  e.  T )  ->  3  =/=  0 )
17941, 177, 1783jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( (
ph  /\  t  e.  T )  ->  (
1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 ) )
180179, 38syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( (
ph  /\  t  e.  T )  ->  (
1  /  3 )  e.  RR )
181 renegcl 9126 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( ( 1  /  3 )  e.  RR  ->  -u (
1  /  3 )  e.  RR )
182180, 181syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  t  e.  T )  ->  -u (
1  /  3 )  e.  RR )
183 0re 8854 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  0  e.  RR
184183a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( (
ph  /\  t  e.  T )  ->  0  e.  RR )
185182, 184, 613jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  e.  RR  /\  0  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
186 ltmul1 9622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( (
-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
) ) )
187185, 186syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  <  0  <->  ( -u (
1  /  3 )  x.  E )  < 
( 0  x.  E
) ) )
188176, 187mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  <  ( 0  x.  E ) )
189 mul02lem2 9005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( E  e.  RR  ->  (
0  x.  E )  =  0 )
19057, 189syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  t  e.  T )  ->  (
0  x.  E )  =  0 )
191188, 190breqtrd 4063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  <  0 )
192 stoweidlem34.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  t  e.  T )  ->  0  <_  ( F `  t
) )
193191, 192jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  t  e.  T )  ->  (
( -u ( 1  / 
3 )  x.  E
)  <  0  /\  0  <_  ( F `  t ) ) )
194182, 57jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  e.  RR  /\  E  e.  RR )
)
195 remulcl 8838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
-u ( 1  / 
3 )  e.  RR  /\  E  e.  RR )  ->  ( -u (
1  /  3 )  x.  E )  e.  RR )
196194, 195syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  e.  RR )
197196, 184, 713jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  t  e.  T )  ->  (
( -u ( 1  / 
3 )  x.  E
)  e.  RR  /\  0  e.  RR  /\  ( F `  t )  e.  RR ) )
198 ltletr 8929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( -u ( 1  /  3 )  x.  E )  e.  RR  /\  0  e.  RR  /\  ( F `  t )  e.  RR )  -> 
( ( ( -u ( 1  /  3
)  x.  E )  <  0  /\  0  <_  ( F `  t
) )  ->  ( -u ( 1  /  3
)  x.  E )  <  ( F `  t ) ) )
199197, 198syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  t  e.  T )  ->  (
( ( -u (
1  /  3 )  x.  E )  <  0  /\  0  <_ 
( F `  t
) )  ->  ( -u ( 1  /  3
)  x.  E )  <  ( F `  t ) ) )
200193, 199mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  <  ( F `  t ) )
201 rexr 8893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( F `  t )  e.  RR  ->  ( F `  t )  e.  RR* )
20271, 201syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  t  e.  T )  ->  ( F `  t )  e.  RR* )
203 rexr 8893 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
-u ( 1  / 
3 )  x.  E
)  e.  RR  ->  (
-u ( 1  / 
3 )  x.  E
)  e.  RR* )
204196, 203syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  t  e.  T )  ->  ( -u ( 1  /  3
)  x.  E )  e.  RR* )
205202, 204jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  t  e.  T )  ->  (
( F `  t
)  e.  RR*  /\  ( -u ( 1  /  3
)  x.  E )  e.  RR* ) )
206 xrlenlt 8906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( F `  t
)  e.  RR*  /\  ( -u ( 1  /  3
)  x.  E )  e.  RR* )  ->  (
( F `  t
)  <_  ( -u (
1  /  3 )  x.  E )  <->  -.  ( -u ( 1  /  3
)  x.  E )  <  ( F `  t ) ) )
207206con2bid 319 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( F `  t
)  e.  RR*  /\  ( -u ( 1  /  3
)  x.  E )  e.  RR* )  ->  (
( -u ( 1  / 
3 )  x.  E
)  <  ( F `  t )  <->  -.  ( F `  t )  <_  ( -u ( 1  /  3 )  x.  E ) ) )
208205, 207syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  t  e.  T )  ->  (
( -u ( 1  / 
3 )  x.  E
)  <  ( F `  t )  <->  -.  ( F `  t )  <_  ( -u ( 1  /  3 )  x.  E ) ) )
209200, 208mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  t  e.  T )  ->  -.  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) )
210 nan 563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  ->  -.  ( t  e.  T  /\  ( F `  t )  <_  ( -u ( 1  /  3 )  x.  E ) ) )  <-> 
( ( ph  /\  t  e.  T )  ->  -.  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) ) )
211209, 210mpbir 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  -.  ( t  e.  T  /\  ( F `
 t )  <_ 
( -u ( 1  / 
3 )  x.  E
) ) )
212 rabid 2729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( -u ( 1  / 
3 )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( -u ( 1  /  3 )  x.  E ) ) )
213211, 212sylnibr 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  -.  t  e.  {
t  e.  T  | 
( F `  t
)  <_  ( -u (
1  /  3 )  x.  E ) } )
21421, 89syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  N  e.  NN0 )
21590eleq2i 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( N  e.  NN0  <->  N  e.  ( ZZ>=
`  0 ) )
216214, 215sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
217 eluzfz1 10819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( N  e.  ( ZZ>= `  0
)  ->  0  e.  ( 0 ... N
) )
218216, 217syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ph  ->  0  e.  ( 0 ... N ) )
219 rabexg 4180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) }  e.  _V )
22095, 219syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ph  ->  { t  e.  T  |  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) }  e.  _V )
221218, 220jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ph  ->  ( 0  e.  ( 0 ... N )  /\  { t  e.  T  |  ( F `
 t )  <_ 
( -u ( 1  / 
3 )  x.  E
) }  e.  _V ) )
222 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( j  =  0  ->  (
j  -  ( 1  /  3 ) )  =  ( 0  -  ( 1  /  3
) ) )
223 df-neg 9056 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  -u (
1  /  3 )  =  ( 0  -  ( 1  /  3
) )
224222, 223syl6eqr 2346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( j  =  0  ->  (
j  -  ( 1  /  3 ) )  =  -u ( 1  / 
3 ) )
225224oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( j  =  0  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( -u (
1  /  3 )  x.  E ) )
226225breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( j  =  0  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) ) )
227226rabbidv 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( j  =  0  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  ( -u ( 1  /  3
)  x.  E ) } )
228227, 103fvmptg 5616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 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 ) } )
229221, 228syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  ( D `  0
)  =  { t  e.  T  |  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) } )
230229eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( t  e.  ( D `  0 )  <-> 
t  e.  { t  e.  T  |  ( F `  t )  <_  ( -u (
1  /  3 )  x.  E ) } ) )
231213, 230mtbird 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  -.  t  e.  ( D `  0 ) )
2321, 231alrimi 1757 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  A. t  -.  t  e.  ( D `  0
) )
233 eq0 3482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( D `  0 )  =  (/)  <->  A. s  -.  s  e.  ( D `  0
) )
234 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  F/_ t
s
235 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  F/_ t
( 0 ... N
)
236 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  F/_ t { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
237235, 236nfmpt 4124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
238103, 237nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  F/_ t D
239 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  F/_ t
0
240238, 239nffv 5548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  F/_ t
( D `  0
)
241234, 240nfel 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  F/ t  s  e.  ( D `
 0 )
242241nfn 1777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  F/ t  -.  s  e.  ( D `  0 )
243 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  F/ s  -.  t  e.  ( D `  0 )
244 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( s  =  t  ->  (
s  e.  ( D `
 0 )  <->  t  e.  ( D `  0 ) ) )
245244notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( s  =  t  ->  ( -.  s  e.  ( D `  0 )  <->  -.  t  e.  ( D `
 0 ) ) )
246242, 243, 245cbval 1937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( A. s  -.  s  e.  ( D `  0 )  <->  A. t  -.  t  e.  ( D `  0
) )
247233, 246bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( D `  0 )  =  (/)  <->  A. t  -.  t  e.  ( D `  0
) )
248232, 247sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( D `  0
)  =  (/) )
249248adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  = 
1 )  ->  ( D `  0 )  =  (/) )
250165, 249eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  = 
1 )  ->  ( D `  ( j  -  1 ) )  =  (/) )
251250eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  = 
1 )  ->  (
t  e.  ( D `
 ( j  - 
1 ) )  <->  t  e.  (/) ) )
252158, 251mtbiri 294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  = 
1 )  ->  -.  t  e.  ( D `  ( j  -  1 ) ) )
253252ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( j  =  1  ->  -.  t  e.  ( D `  ( j  -  1 ) ) ) )
254 con2b 324 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( j  =  1  ->  -.  t  e.  ( D `  ( j  -  1 ) ) )  <->  ( t  e.  ( D `  (
j  -  1 ) )  ->  -.  j  =  1 ) )
255253, 254sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( t  e.  ( D `  ( j  -  1 ) )  ->  -.  j  = 
1 ) )
256255imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  j  =  1 )
257157, 256syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  j  =  1 )
258 simplll 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  -.  j  =  1 )  ->  ph )
259147a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  t  e.  T )  ->  (
j  e.  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  <->  ( j  e.  ( 1 ... N
)  /\  t  e.  ( D `  j ) ) ) )
260145, 259bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  t  e.  T )  ->  (
j  e.  ( J `
 t )  <->  ( j  e.  ( 1 ... N
)  /\  t  e.  ( D `  j ) ) ) )
261260simprbda 606 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  j  e.  ( 1 ... N
) )
262 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  ph )
263 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  j  e.  ( J `  t
) )
264262, 263jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  ( ph  /\  j  e.  ( J `  t ) ) )
26521, 23syl6eleq 2386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
266265adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  j  e.  ( J `  t ) )  ->  N  e.  ( ZZ>= `  1 )
)
267 elfzp12 10877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( N  e.  ( ZZ>= `  1
)  ->  ( j  e.  ( 1 ... N
)  <->  ( j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N
) ) ) )
268266, 267syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  j  e.  ( J `  t ) )  ->  ( j  e.  ( 1 ... N
)  <->  ( j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N
) ) ) )
269264, 268syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
j  e.  ( 1 ... N )  <->  ( j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N
) ) ) )
270261, 269mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
j  =  1  \/  j  e.  ( ( 1  +  1 ) ... N ) ) )
271270orcanai 879 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  -.  j  =  1 )  -> 
j  e.  ( ( 1  +  1 ) ... N ) )
272258, 271jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  -.  j  =  1 )  -> 
( ph  /\  j  e.  ( ( 1  +  1 ) ... N
) ) )
273 fzssp1 10850 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 1 ... ( N  - 
1 ) )  C_  ( 1 ... (
( N  -  1 )  +  1 ) )
274273a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 1 ... ( ( N  -  1 )  +  1 ) ) )
275 nncn 9770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( N  e.  NN  ->  N  e.  CC )
27621, 275syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  N  e.  CC )
277276idi 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  N  e.  CC )
278160a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  1  e.  CC )
279277, 278jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( N  e.  CC  /\  1  e.  CC ) )
280 npcan 9076 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  - 
1 )  +  1 )  =  N )
281279, 280syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
282281oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( 1 ... (
( N  -  1 )  +  1 ) )  =  ( 1 ... N ) )
283274, 282sseqtrd 3227 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 1 ... N ) )
284283adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
1 ... ( N  - 
1 ) )  C_  ( 1 ... N
) )
285 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  j  e.  ( ( 1  +  1 ) ... N
) )
286 1z 10069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  1  e.  ZZ
287286, 286pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 1  e.  ZZ  /\  1  e.  ZZ )
288 zaddcl 10075 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 1  e.  ZZ  /\  1  e.  ZZ )  ->  ( 1  +  1 )  e.  ZZ )
289287, 288ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 1  +  1 )  e.  ZZ
290289a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
1  +  1 )  e.  ZZ )
291 nnz 10061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( N  e.  NN  ->  N  e.  ZZ )
29221, 291syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  N  e.  ZZ )
293292adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  N  e.  ZZ )
294290, 293jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
( 1  +  1 )  e.  ZZ  /\  N  e.  ZZ )
)
295 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( j  e.  ( ( 1  +  1 ) ... N )  ->  j  e.  ZZ )
296295adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  j  e.  ZZ )
297286a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  1  e.  ZZ )
298296, 297jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  e.  ZZ  /\  1  e.  ZZ )
)
299294, 298jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
( ( 1  +  1 )  e.  ZZ  /\  N  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) ) )
300 fzsubel 10843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ( 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 ) ) ) )
301299, 300syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  e.  ( ( 1  +  1 ) ... N )  <->  ( j  -  1 )  e.  ( ( ( 1  +  1 )  - 
1 ) ... ( N  -  1 ) ) ) )
302285, 301mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  -  1 )  e.  ( ( ( 1  +  1 )  -  1 ) ... ( N  -  1 ) ) )
303160, 160pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 1  e.  CC  /\  1  e.  CC )
304 pncan 9073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 1  e.  CC  /\  1  e.  CC )  ->  ( ( 1  +  1 )  -  1 )  =  1 )
305303, 304ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 1  +  1 )  -  1 )  =  1
306305oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( 1  +  1 )  -  1 ) ... ( N  - 
1 ) )  =  ( 1 ... ( N  -  1 ) )
307306a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
( ( 1  +  1 )  -  1 ) ... ( N  -  1 ) )  =  ( 1 ... ( N  -  1 ) ) )
308302, 307eleqtrd 2372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  -  1 )  e.  ( 1 ... ( N  -  1 ) ) )
309284, 308sseldd 3194 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  ( ( 1  +  1 ) ... N
) )  ->  (
j  -  1 )  e.  ( 1 ... N ) )
310272, 309syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  -.  j  =  1 )  -> 
( j  -  1 )  e.  ( 1 ... N ) )
311310ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  ( -.  j  =  1  ->  ( j  -  1 )  e.  ( 1 ... N ) ) )
312311orrd 367 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
j  =  1  \/  ( j  -  1 )  e.  ( 1 ... N ) ) )
3133123adant3 975 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  =  1  \/  (
j  -  1 )  e.  ( 1 ... N ) ) )
314 df-or 359 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( j  =  1  \/  ( j  -  1 )  e.  ( 1 ... N ) )  <-> 
( -.  j  =  1  ->  ( j  -  1 )  e.  ( 1 ... N
) ) )
315313, 314sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( -.  j  =  1  ->  ( j  -  1 )  e.  ( 1 ... N ) ) )
316257, 315mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e.  ( 1 ... N
) )
317 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  =  ( j  - 
1 )  ->  ( D `  i )  =  ( D `  ( j  -  1 ) ) )
318317eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  ( j  - 
1 )  ->  (
t  e.  ( D `
 i )  <->  t  e.  ( D `  ( j  -  1 ) ) ) )
319318elrab3 2937 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( j  -  1 )  e.  ( 1 ... N )  ->  (
( j  -  1 )  e.  { i  e.  ( 1 ... N )  |  t  e.  ( D `  i ) }  <->  t  e.  ( D `  ( j  -  1 ) ) ) )
320316, 319syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 ) ) ) )
321155, 320mpbird 223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e. 
{ i  e.  ( 1 ... N )  |  t  e.  ( D `  i ) } )
322 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ i
( 1 ... N
)
323 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ i  t  e.  ( D `
 j )
324 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ j
i
325113, 324nffv 5548 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ j
( D `  i
)
326111, 325nfel 2440 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ j  t  e.  ( D `
 i )
327 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  i  ->  ( D `  j )  =  ( D `  i ) )
328327eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  i  ->  (
t  e.  ( D `
 j )  <->  t  e.  ( D `  i ) ) )
329110, 322, 323, 326, 328cbvrab 2799 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) }  =  { i  e.  ( 1 ... N )  |  t  e.  ( D `  i ) }
330321, 329syl6eleqr 2387 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e. 
{ j  e.  ( 1 ... N )  |  t  e.  ( D `  j ) } )
331 simp1 955 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( ph  /\  t  e.  T ) )
332331, 10syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( J `  t )  =  {
j  e.  ( 1 ... N )  |  t  e.  ( D `
 j ) } )
333330, 332eleqtrrd 2373 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e.  ( J `  t
) )
334 3simpa 952 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( ( ph  /\  t  e.  T
)  /\  j  e.  ( J `  t ) ) )
335 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ZZ )
336 zre 10044 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  e.  ZZ  ->  j  e.  RR )
337261, 335, 3363syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  j  e.  RR )
338334, 337syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  j  e.  RR )
339 peano2rem 9129 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  RR  ->  (
j  -  1 )  e.  RR )
340338, 339syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  -  1 )  e.  RR )
341338, 340jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( j  e.  RR  /\  ( j  -  1 )  e.  RR ) )
342 ltm1 9612 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  RR  ->  (
j  -  1 )  <  j )
343342adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  RR  /\  ( j  -  1 )  e.  RR )  ->  ( j  - 
1 )  <  j
)
344 ltnle 8918 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( j  -  1 )  e.  RR  /\  j  e.  RR )  ->  ( ( j  - 
1 )  <  j  <->  -.  j  <_  ( j  -  1 ) ) )
345344ancoms 439 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  RR  /\  ( j  -  1 )  e.  RR )  ->  ( ( j  -  1 )  < 
j  <->  -.  j  <_  ( j  -  1 ) ) )
346343, 345mpbid 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( j  e.  RR  /\  ( j  -  1 )  e.  RR )  ->  -.  j  <_  ( j  -  1 ) )
347341, 346syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  j  <_  ( j  -  1 ) )
348333, 347jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  ( (
j  -  1 )  e.  ( J `  t )  /\  -.  j  <_  ( j  - 
1 ) ) )
349 breq2 4043 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  ( j  - 
1 )  ->  (
j  <_  k  <->  j  <_  ( j  -  1 ) ) )
350349notbid 285 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  ( j  - 
1 )  ->  ( -.  j  <_  k  <->  -.  j  <_  ( j  -  1 ) ) )
351350rspcev 2897 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( j  -  1 )  e.  ( J `
 t )  /\  -.  j  <_  ( j  -  1 ) )  ->  E. k  e.  ( J `  t )  -.  j  <_  k
)
352348, 351syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  E. k  e.  ( J `  t
)  -.  j  <_ 
k )
353 rexnal 2567 . . . . . . . . . . . . . . . . . . 19  |-  ( E. k  e.  ( J `
 t )  -.  j  <_  k  <->  -.  A. k  e.  ( J `  t
) j  <_  k
)
354352, 353sylib 188 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  A. k  e.  ( J `  t
) j  <_  k
)
3553543expia 1153 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  (
t  e.  ( D `
 ( j  - 
1 ) )  ->  -.  A. k  e.  ( J `  t ) j  <_  k )
)
356355con2d 107 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  ( A. k  e.  ( J `  t )
j  <_  k  ->  -.  t  e.  ( D `
 ( j  - 
1 ) ) ) )
3573563impia 1148 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  -.  t  e.  ( D `  (
j  -  1 ) ) )
358154, 357syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  -.  t  e.  ( D `  (
j  -  1 ) ) )
359150, 358jca 518 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  ( t  e.  ( D `  j
)  /\  -.  t  e.  ( D `  (
j  -  1 ) ) ) )
360 eldif 3175 . . . . . . . . . . . . 13  |-  ( t  e.  ( ( D `
 j )  \ 
( D `  (
j  -  1 ) ) )  <->  ( t  e.  ( D `  j
)  /\  -.  t  e.  ( D `  (
j  -  1 ) ) ) )
361359, 360sylibr 203 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t )
)  /\  A. k  e.  ( J `  t
) j  <_  k
)  ->  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) )
362361ex 423 . . . . . . . . . . 11  |-  ( ( ( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) )  ->  ( A. k  e.  ( J `  t )
j  <_  k  ->  t  e.  ( ( D `
 j )  \ 
( D `  (
j  -  1 ) ) ) ) )
363362ex 423 . . . . . . . . . 10  |-  ( (
ph  /\  t  e.  T )  ->  (
j  e.  ( J `
 t )  -> 
( A. k  e.  ( J `  t
) j  <_  k  ->  t  e.  ( ( D `  j ) 
\  ( D `  ( j  -  1 ) ) ) ) ) )
364144, 363reximdai 2664 . . . . . . . . 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 ) ) ) ) )
365141, 364mpd 14 . . . . . . . 8  |-  ( (
ph  /\  t  e.  T )  ->  E. j  e.  ( J `  t
) t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) )
366 df-rex 2562 . . . . . . . 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 ) ) ) ) )
367365, 366sylib 188 . . . . . . 7  |-  ( (
ph  /\  t  e.  T )  ->  E. j
( j  e.  ( J `  t )  /\  t  e.  ( ( D `  j
)  \  ( D `  ( j  -  1 ) ) ) ) )
368 simprl 732 . . . . . . . . . 10  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  j  e.  ( J `  t ) )
369 simpl 443 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( ph  /\  t  e.  T ) )
370 eldifn 3312 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( ( D `
 j )  \ 
( D `  (
j  -  1 ) ) )  ->  -.  t  e.  ( D `  ( j  -  1 ) ) )
371370ad2antll 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  -.  t  e.  ( D `  (
j  -  1 ) ) )
372368, 371jca 518 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( j  e.  ( J `  t
)  /\  -.  t  e.  ( D `  (
j  -  1 ) ) ) )
373369, 372jca 518 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( ( ph  /\  t  e.  T
)  /\  ( j  e.  ( J `  t
)  /\  -.  t  e.  ( D `  (
j  -  1 ) ) ) ) )
374 simplr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  t  e.  T )
375 simpll 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  ph )
376 simpl 443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  ( ph  /\  t  e.  T
) )
377 simprl 732 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  j  e.  ( J `  t
) )
378376, 377jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
( ph  /\  t  e.  T )  /\  j  e.  ( J `  t
) ) )
379378, 261syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  j  e.  ( 1 ... N
) )
380375, 379jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  ( ph  /\  j  e.  ( 1 ... N ) ) )
381 simprr 733 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  -.  t  e.  ( D `  ( j  -  1 ) ) )
382380, 381jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
( ph  /\  j  e.  ( 1 ... N
) )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )
383 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  k  ->  (
j  -  ( 1  /  3 ) )  =  ( k  -  ( 1  /  3
) ) )
384383oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  k  ->  (
( j  -  (
1  /  3 ) )  x.  E )  =  ( ( k  -  ( 1  / 
3 ) )  x.  E ) )
385384breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  k  ->  (
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) ) )
386385rabbidv 2793 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  k  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) } )
387386cbvmptv 4127 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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
) } )
388103, 387eqtri 2316 . . . . . . . . . . . . . . . . . . . . . . 23  |-  D  =  ( k  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( k  -  (
1  /  3 ) )  x.  E ) } )
389388a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  D  =  ( k  e.  ( 0 ... N
)  |->  { t  e.  T  |  ( F `
 t )  <_ 
( ( k  -  ( 1  /  3
) )  x.  E
) } ) )
390 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( k  =  ( j  - 
1 )  ->  (
k  -  ( 1  /  3 ) )  =  ( ( j  -  1 )  -  ( 1  /  3
) ) )
391390oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( k  =  ( j  - 
1 )  ->  (
( k  -  (
1  /  3 ) )  x.  E )  =  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) )
392391breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( k  =  ( j  - 
1 )  ->  (
( F `  t
)  <_  ( (
k  -  ( 1  /  3 ) )  x.  E )  <->  ( F `  t )  <_  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E ) ) )
393392rabbidv 2793 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  ( j  - 
1 )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( k  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E ) } )
394393adantl 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) } )
395 fzssp1 10850 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... (
( N  -  1 )  +  1 ) )
396281oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 0 ... (
( N  -  1 )  +  1 ) )  =  ( 0 ... N ) )
397395, 396syl5sseq 3239 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
398397adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
0 ... ( N  - 
1 ) )  C_  ( 0 ... N
) )
399 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  j  e.  ( 1 ... N
) )
400286a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  1  e.  ZZ )
401292adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  N  e.  ZZ )
402400, 401jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
1  e.  ZZ  /\  N  e.  ZZ )
)
403335adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  j  e.  ZZ )
404403, 400jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  e.  ZZ  /\  1  e.  ZZ )
)
405402, 404jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
( 1  e.  ZZ  /\  N  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) ) )
406 fzsubel 10843 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 1  e.  ZZ  /\  N  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( j  e.  ( 1 ... N )  <-> 
( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  - 
1 ) ) ) )
407405, 406syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  e.  ( 1 ... N )  <->  ( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  -  1 ) ) ) )
408399, 407mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  -  1 ) ) )
409160subidi 9133 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 1  -  1 )  =  0
410409a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
1  -  1 )  =  0 )
411410oveq1d 5889 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
( 1  -  1 ) ... ( N  -  1 ) )  =  ( 0 ... ( N  -  1 ) ) )
412411eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  - 
1 ) )  <->  ( j  -  1 )  e.  ( 0 ... ( N  -  1 ) ) ) )
413408, 412mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( 0 ... ( N  -  1 ) ) )
414398, 413sseldd 3194 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
j  -  1 )  e.  ( 0 ... N ) )
41595adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  T  e.  _V )
416 rabexg 4180 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
417415, 416syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
418389, 394, 414, 417fvmptd 5622 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( D `  ( j  -  1 ) )  =  { t  e.  T  |  ( F `
 t )  <_ 
( ( ( j  -  1 )  -  ( 1  /  3
) )  x.  E
) } )
419418eleq2d 2363 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  (
t  e.  ( D `
 ( j  - 
1 ) )  <->  t  e.  { t  e.  T  | 
( F `  t
)  <_  ( (
( j  -  1 )  -  ( 1  /  3 ) )  x.  E ) } ) )
420419notbid 285 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( -.  t  e.  ( D `  ( j  -  1 ) )  <->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } ) )
421420biimpd 198 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 1 ... N
) )  ->  ( -.  t  e.  ( D `  ( j  -  1 ) )  ->  -.  t  e.  { t  e.  T  | 
( F `  t
)  <_  ( (
( j  -  1 )  -  ( 1  /  3 ) )  x.  E ) } ) )
422421imp 418 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  j  e.  ( 1 ... N
) )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) )  ->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( ( j  -  1 )  -  ( 1  / 
3 ) )  x.  E ) } )
423382, 422syl 15 . . . . . . . . . . . . . . . 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
) } )
424 rabid 2729 . . . . . . . . . . . . . . . . 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
) ) )
425378, 337syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  j  e.  RR )
426 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  RR  ->  j  e.  CC )
427160a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  RR  ->  1  e.  CC )
428 recn 8843 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1  /  3 )  e.  RR  ->  (
1  /  3 )  e.  CC )
42937, 38, 428mp2b 9 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1  /  3 )  e.  CC
430429a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  RR  ->  (
1  /  3 )  e.  CC )
431426, 427, 4303jca 1132 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
j  e.  CC  /\  1  e.  CC  /\  (
1  /  3 )  e.  CC ) )
432 subsub4 9096 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( j  e.  CC  /\  1  e.  CC  /\  (
1  /  3 )  e.  CC )  -> 
( ( j  - 
1 )  -  (
1  /  3 ) )  =  ( j  -  ( 1  +  ( 1  /  3
) ) ) )
433431, 432syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  RR  ->  (
( j  -  1 )  -  ( 1  /  3 ) )  =  ( j  -  ( 1  +  ( 1  /  3 ) ) ) )
434 df-4 9822 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  4  =  ( 3  +  1 )
435434eqcomi 2300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 3  +  1 )  =  4
436435oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 3  +  1 )  /  3 )  =  ( 4  /  3
)
437 3cn 9834 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  3  e.  CC
438437, 36pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 3  e.  CC  /\  3  =/=  0 )
439437, 160, 4383pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 3  e.  CC  /\  1  e.  CC  /\  ( 3  e.  CC  /\  3  =/=  0 ) )
440 divdir 9463 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 3  e.  CC  /\  1  e.  CC  /\  (
3  e.  CC  /\  3  =/=  0 ) )  ->  ( ( 3  +  1 )  / 
3 )  =  ( ( 3  /  3
)  +  ( 1  /  3 ) ) )
441439, 440ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 3  +  1 )  /  3 )  =  ( ( 3  / 
3 )  +  ( 1  /  3 ) )
442436, 441eqtr3i 2318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 4  /  3 )  =  ( ( 3  / 
3 )  +  ( 1  /  3 ) )
443 divid 9467 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 3  e.  CC  /\  3  =/=  0 )  -> 
( 3  /  3
)  =  1 )
444438, 443ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 3  /  3 )  =  1
445444oveq1i 5884 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 3  /  3 )  +  ( 1  / 
3 ) )  =  ( 1  +  ( 1  /  3 ) )
446442, 445eqtri 2316 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 4  /  3 )  =  ( 1  +  ( 1  /  3 ) )
447446a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
4  /  3 )  =  ( 1  +  ( 1  /  3
) ) )
448447oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  RR  ->  (
j  -  ( 4  /  3 ) )  =  ( j  -  ( 1  +  ( 1  /  3 ) ) ) )
449433, 448eqtr4d 2331 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  RR  ->  (
( j  -  1 )  -  ( 1  /  3 ) )  =  ( j  -  ( 4  /  3
) ) )
450449oveq1d 5889 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  RR  ->  (
( ( j  - 
1 )  -  (
1  /  3 ) )  x.  E )  =  ( ( j  -  ( 4  / 
3 ) )  x.  E ) )
451425, 450syl 15 . . . . . . . . . . . . . . . . . . 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 ) )
452451breq2d 4051 . . . . . . . . . . . . . . . . . 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 ) ) )
453452anbi2d 684 . . . . . . . . . . . . . . . . 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 ) ) ) )
454424, 453syl5bb 248 . . . . . . . . . . . . . . . 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
) ) ) )
455423, 454mtbid 291 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  -.  ( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) ) )
456 imnan 411 . . . . . . . . . . . . . . 15  |-  ( ( t  e.  T  ->  -.  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) )  <->  -.  ( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) ) )
457455, 456sylibr 203 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  (
t  e.  T  ->  -.  ( F `  t
)  <_  ( (
j  -  ( 4  /  3 ) )  x.  E ) ) )
458374, 457mpd 14 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  -.  t  e.  ( D `  ( j  -  1 ) ) ) )  ->  -.  ( F `  t )  <_  ( ( j  -  ( 4  / 
3 ) )  x.  E ) )
459373, 458syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  -.  ( F `  t )  <_  ( ( j  -  ( 4  /  3
) )  x.  E
) )
460369, 368jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( ( ph  /\  t  e.  T
)  /\  j  e.  ( J `  t ) ) )
461460, 337syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  j  e.  RR )
462461idi 2 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  j  e.  RR )
463 4re 9835 . . . . . . . . . . . . . . . . . . . . 21  |-  4  e.  RR
464463a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  4  e.  RR )
46528a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  3  e.  RR )
46636a1i 10 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  3  =/=  0 )
467464, 465, 4663jca 1132 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( 4  e.  RR  /\  3  e.  RR  /\  3  =/=  0 ) )
468 redivcl 9495 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 4  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
4  /  3 )  e.  RR )
469467, 468syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( 4  /  3 )  e.  RR )
470462, 469jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( j  e.  RR  /\  ( 4  /  3 )  e.  RR ) )
471 resubcl 9127 . . . . . . . . . . . . . . . . 17  |-  ( ( j  e.  RR  /\  ( 4  /  3
)  e.  RR )  ->  ( j  -  ( 4  /  3
) )  e.  RR )
472470, 471syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ( j  -  ( 4  / 
3 ) )  e.  RR )
473 simpll 730 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -  1 ) ) ) ) )  ->  ph )
474473, 56syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  t  e.  T )  /\  (
j  e.  ( J `
 t )  /\  t  e.  ( ( D `  j )  \  ( D `  ( j  -