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

Theorem stoweidlem11 27862
Description: This lemma is used to prove that there is a function  g as in the proof of [BrosowskiDeutsh] p. 92, (at the top of page 92): this lemma proves that g(t) < ( j + 1 / 3 ) * ε. Here  E is used to represent ε in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem11.1  |-  ( ph  ->  N  e.  NN )
stoweidlem11.2  |-  ( ph  ->  t  e.  T )
stoweidlem11.3  |-  ( ph  ->  j  e.  ( 1 ... N ) )
stoweidlem11.4  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
stoweidlem11.5  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  t )  <_  1 )
stoweidlem11.6  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( X `  i
) `  t )  <  ( E  /  N
) )
stoweidlem11.7  |-  ( ph  ->  E  e.  RR+ )
stoweidlem11.8  |-  ( ph  ->  E  <  ( 1  /  3 ) )
Assertion
Ref Expression
stoweidlem11  |-  ( ph  ->  ( ( t  e.  T  |->  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
) ) `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E ) )
Distinct variable groups:    i, j    t, i, E    i, N, t    ph, i    t, T   
t, X
Allowed substitution hints:    ph( t, j)    T( i, j)    E( j)    N( j)    X( i, j)

Proof of Theorem stoweidlem11
StepHypRef Expression
1 stoweidlem11.2 . . . 4  |-  ( ph  ->  t  e.  T )
2 sumex 12176 . . . . 5  |-  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) )  e.  _V
32a1i 10 . . . 4  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  _V )
41, 3jca 518 . . 3  |-  ( ph  ->  ( t  e.  T  /\  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  _V )
)
5 eqid 2296 . . . 4  |-  ( t  e.  T  |->  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) ) )  =  ( t  e.  T  |-> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
) )
65fvmpt2 5624 . . 3  |-  ( ( t  e.  T  /\  sum_ i  e.  ( 0 ... N ) ( E  x.  ( ( X `  i ) `
 t ) )  e.  _V )  -> 
( ( t  e.  T  |->  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
) ) `  t
)  =  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) ) )
74, 6syl 15 . 2  |-  ( ph  ->  ( ( t  e.  T  |->  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
) ) `  t
)  =  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) ) )
8 stoweidlem11.3 . . . . . . . . . . . . . 14  |-  ( ph  ->  j  e.  ( 1 ... N ) )
9 elfzuz 10810 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ( ZZ>= `  1 )
)
108, 9syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  j  e.  ( ZZ>= ` 
1 ) )
11 eluz2 10252 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  1
)  <->  ( 1  e.  ZZ  /\  j  e.  ZZ  /\  1  <_ 
j ) )
1210, 11sylib 188 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  e.  ZZ  /\  j  e.  ZZ  /\  1  <_  j ) )
1312simp2d 968 . . . . . . . . . . 11  |-  ( ph  ->  j  e.  ZZ )
14 zre 10044 . . . . . . . . . . 11  |-  ( j  e.  ZZ  ->  j  e.  RR )
1513, 14syl 15 . . . . . . . . . 10  |-  ( ph  ->  j  e.  RR )
16 ltm1 9612 . . . . . . . . . 10  |-  ( j  e.  RR  ->  (
j  -  1 )  <  j )
1715, 16syl 15 . . . . . . . . 9  |-  ( ph  ->  ( j  -  1 )  <  j )
18 fzdisj 10833 . . . . . . . . 9  |-  ( ( j  -  1 )  <  j  ->  (
( 0 ... (
j  -  1 ) )  i^i  ( j ... N ) )  =  (/) )
1917, 18syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( 0 ... ( j  -  1 ) )  i^i  (
j ... N ) )  =  (/) )
20 fzssp1 10850 . . . . . . . . . . . 12  |-  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... (
( N  -  1 )  +  1 ) )
21 stoweidlem11.1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  NN )
22 nncn 9770 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  N  e.  CC )
2321, 22syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
24 ax-1cn 8811 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
2524a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
2623, 25jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  e.  CC  /\  1  e.  CC ) )
27 npcan 9076 . . . . . . . . . . . . . 14  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  - 
1 )  +  1 )  =  N )
2826, 27syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
2928oveq2d 5890 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... (
( N  -  1 )  +  1 ) )  =  ( 0 ... N ) )
3020, 29syl5sseq 3239 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
31 1z 10069 . . . . . . . . . . . . . . . . 17  |-  1  e.  ZZ
3231a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  1  e.  ZZ )
33 nnz 10061 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  N  e.  ZZ )
3421, 33syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  ZZ )
3532, 34jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  e.  ZZ  /\  N  e.  ZZ ) )
3613, 32jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  ZZ  /\  1  e.  ZZ ) )
3735, 36jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  e.  ZZ  /\  N  e.  ZZ )  /\  (
j  e.  ZZ  /\  1  e.  ZZ )
) )
38 fzsubel 10843 . . . . . . . . . . . . . 14  |-  ( ( ( 1  e.  ZZ  /\  N  e.  ZZ )  /\  ( j  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( j  e.  ( 1 ... N )  <-> 
( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  - 
1 ) ) ) )
3937, 38syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( j  e.  ( 1 ... N )  <-> 
( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  - 
1 ) ) ) )
408, 39mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( j  -  1 )  e.  ( ( 1  -  1 ) ... ( N  - 
1 ) ) )
4124subidi 9133 . . . . . . . . . . . . 13  |-  ( 1  -  1 )  =  0
4241oveq1i 5884 . . . . . . . . . . . 12  |-  ( ( 1  -  1 ) ... ( N  - 
1 ) )  =  ( 0 ... ( N  -  1 ) )
4340, 42syl6eleq 2386 . . . . . . . . . . 11  |-  ( ph  ->  ( j  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
4430, 43sseldd 3194 . . . . . . . . . 10  |-  ( ph  ->  ( j  -  1 )  e.  ( 0 ... N ) )
45 fzsplit 10832 . . . . . . . . . 10  |-  ( ( j  -  1 )  e.  ( 0 ... N )  ->  (
0 ... N )  =  ( ( 0 ... ( j  -  1 ) )  u.  (
( ( j  - 
1 )  +  1 ) ... N ) ) )
4644, 45syl 15 . . . . . . . . 9  |-  ( ph  ->  ( 0 ... N
)  =  ( ( 0 ... ( j  -  1 ) )  u.  ( ( ( j  -  1 )  +  1 ) ... N ) ) )
47 recn 8843 . . . . . . . . . . . . . 14  |-  ( j  e.  RR  ->  j  e.  CC )
4815, 47syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  j  e.  CC )
4948, 25jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( j  e.  CC  /\  1  e.  CC ) )
50 npcan 9076 . . . . . . . . . . . 12  |-  ( ( j  e.  CC  /\  1  e.  CC )  ->  ( ( j  - 
1 )  +  1 )  =  j )
5149, 50syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( j  - 
1 )  +  1 )  =  j )
5251oveq1d 5889 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( j  -  1 )  +  1 ) ... N
)  =  ( j ... N ) )
5352uneq2d 3342 . . . . . . . . 9  |-  ( ph  ->  ( ( 0 ... ( j  -  1 ) )  u.  (
( ( j  - 
1 )  +  1 ) ... N ) )  =  ( ( 0 ... ( j  -  1 ) )  u.  ( j ... N ) ) )
5446, 53eqtrd 2328 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  =  ( ( 0 ... ( j  -  1 ) )  u.  ( j ... N ) ) )
55 fzfi 11050 . . . . . . . . 9  |-  ( 0 ... N )  e. 
Fin
5655a1i 10 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
57 stoweidlem11.7 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
58 rpcn 10378 . . . . . . . . . . . 12  |-  ( E  e.  RR+  ->  E  e.  CC )
5957, 58syl 15 . . . . . . . . . . 11  |-  ( ph  ->  E  e.  CC )
6059adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  E  e.  CC )
61 stoweidlem11.4 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( X `  i ) : T --> RR )
621adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  t  e.  T )
6361, 62jca 518 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) : T --> RR  /\  t  e.  T )
)
64 ffvelrn 5679 . . . . . . . . . . . 12  |-  ( ( ( X `  i
) : T --> RR  /\  t  e.  T )  ->  ( ( X `  i ) `  t
)  e.  RR )
6563, 64syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  t )  e.  RR )
66 recn 8843 . . . . . . . . . . 11  |-  ( ( ( X `  i
) `  t )  e.  RR  ->  ( ( X `  i ) `  t )  e.  CC )
6765, 66syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  t )  e.  CC )
6860, 67jca 518 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  e.  CC  /\  (
( X `  i
) `  t )  e.  CC ) )
69 mulcl 8837 . . . . . . . . 9  |-  ( ( E  e.  CC  /\  ( ( X `  i ) `  t
)  e.  CC )  ->  ( E  x.  ( ( X `  i ) `  t
) )  e.  CC )
7068, 69syl 15 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  e.  CC )
7119, 54, 56, 70fsumsplit 12228 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  =  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
) ) )
72 fzfi 11050 . . . . . . . . . . 11  |-  ( j ... N )  e. 
Fin
7372a1i 10 . . . . . . . . . 10  |-  ( ph  ->  ( j ... N
)  e.  Fin )
74 elfzuz3 10811 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... N )  ->  N  e.  ( ZZ>= `  j )
)
75 eluzfz2 10820 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  j
)  ->  N  e.  ( j ... N
) )
768, 74, 753syl 18 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( j ... N ) )
77 ne0i 3474 . . . . . . . . . . 11  |-  ( N  e.  ( j ... N )  ->  (
j ... N )  =/=  (/) )
7876, 77syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( j ... N
)  =/=  (/) )
79 rpre 10376 . . . . . . . . . . . . . 14  |-  ( E  e.  RR+  ->  E  e.  RR )
8057, 79syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  E  e.  RR )
8180adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  E  e.  RR )
82 simpl 443 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ph )
83 0z 10051 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
8483a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  e.  ZZ )
85 0le1 9313 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  <_  1
8685a1i 10 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  0  <_  1 )
8712simp3d 969 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  1  <_  j )
8886, 87jca 518 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 0  <_  1  /\  1  <_  j ) )
89 0re 8854 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  e.  RR
9089a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  0  e.  RR )
91 1re 8853 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  1  e.  RR
9291a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  1  e.  RR )
9390, 92, 153jca 1132 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 0  e.  RR  /\  1  e.  RR  /\  j  e.  RR )
)
94 letr 8930 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 0  e.  RR  /\  1  e.  RR  /\  j  e.  RR )  ->  (
( 0  <_  1  /\  1  <_  j )  ->  0  <_  j
) )
9593, 94syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( 0  <_ 
1  /\  1  <_  j )  ->  0  <_  j ) )
9688, 95mpd 14 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  <_  j )
9784, 13, 963jca 1132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 0  e.  ZZ  /\  j  e.  ZZ  /\  0  <_  j ) )
98 eluz2 10252 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  j  e.  ZZ  /\  0  <_ 
j ) )
9997, 98sylibr 203 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  j  e.  ( ZZ>= ` 
0 ) )
100 fzss1 10846 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( ZZ>= `  0
)  ->  ( j ... N )  C_  (
0 ... N ) )
10199, 100syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( j ... N
)  C_  ( 0 ... N ) )
102101adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
j ... N )  C_  ( 0 ... N
) )
103 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  i  e.  ( j ... N
) )
104102, 103jca 518 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( j ... N
)  C_  ( 0 ... N )  /\  i  e.  ( j ... N ) ) )
105 ssel2 3188 . . . . . . . . . . . . . . . . 17  |-  ( ( ( j ... N
)  C_  ( 0 ... N )  /\  i  e.  ( j ... N ) )  -> 
i  e.  ( 0 ... N ) )
106104, 105syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  i  e.  ( 0 ... N
) )
10782, 106jca 518 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( ph  /\  i  e.  ( 0 ... N ) ) )
108107, 61syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( X `  i ) : T --> RR )
1091adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  t  e.  T )
110108, 109jca 518 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( X `  i
) : T --> RR  /\  t  e.  T )
)
111110, 64syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( X `  i
) `  t )  e.  RR )
11281, 111jca 518 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  e.  RR  /\  (
( X `  i
) `  t )  e.  RR ) )
113 remulcl 8838 . . . . . . . . . . 11  |-  ( ( E  e.  RR  /\  ( ( X `  i ) `  t
)  e.  RR )  ->  ( E  x.  ( ( X `  i ) `  t
) )  e.  RR )
114112, 113syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  e.  RR )
11521adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  N  e.  NN )
116 nnre 9769 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  N  e.  RR )
117115, 116syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  N  e.  RR )
118 nnne0 9794 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  N  =/=  0 )
119115, 118syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  N  =/=  0 )
12081, 117, 1193jca 1132 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  e.  RR  /\  N  e.  RR  /\  N  =/=  0 ) )
121 redivcl 9495 . . . . . . . . . . . . 13  |-  ( ( E  e.  RR  /\  N  e.  RR  /\  N  =/=  0 )  ->  ( E  /  N )  e.  RR )
122120, 121syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  /  N )  e.  RR )
12381, 122jca 518 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  e.  RR  /\  ( E  /  N )  e.  RR ) )
124 remulcl 8838 . . . . . . . . . . 11  |-  ( ( E  e.  RR  /\  ( E  /  N
)  e.  RR )  ->  ( E  x.  ( E  /  N
) )  e.  RR )
125123, 124syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  x.  ( E  /  N ) )  e.  RR )
126 stoweidlem11.6 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( X `  i
) `  t )  <  ( E  /  N
) )
127 rpgt0 10381 . . . . . . . . . . . . . . . 16  |-  ( E  e.  RR+  ->  0  < 
E )
12857, 127syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <  E )
129128adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  0  <  E )
13081, 129jca 518 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  e.  RR  /\  0  <  E ) )
131111, 122, 1303jca 1132 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( ( X `  i ) `  t
)  e.  RR  /\  ( E  /  N
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
132 ltmul2 9623 . . . . . . . . . . . 12  |-  ( ( ( ( X `  i ) `  t
)  e.  RR  /\  ( E  /  N
)  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( (
( X `  i
) `  t )  <  ( E  /  N
)  <->  ( E  x.  ( ( X `  i ) `  t
) )  <  ( E  x.  ( E  /  N ) ) ) )
133131, 132syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  (
( ( X `  i ) `  t
)  <  ( E  /  N )  <->  ( E  x.  ( ( X `  i ) `  t
) )  <  ( E  x.  ( E  /  N ) ) ) )
134126, 133mpbid 201 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  < 
( E  x.  ( E  /  N ) ) )
13573, 78, 114, 125, 134fsumlt 12274 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  sum_ i  e.  ( j ... N
) ( E  x.  ( E  /  N
) ) )
13621, 118syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  =/=  0 )
13759, 23, 1363jca 1132 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E  e.  CC  /\  N  e.  CC  /\  N  =/=  0 ) )
138 divcl 9446 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  CC  /\  N  e.  CC  /\  N  =/=  0 )  ->  ( E  /  N )  e.  CC )
139137, 138syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  /  N
)  e.  CC )
14059, 139jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  e.  CC  /\  ( E  /  N
)  e.  CC ) )
141 mulcl 8837 . . . . . . . . . . . . 13  |-  ( ( E  e.  CC  /\  ( E  /  N
)  e.  CC )  ->  ( E  x.  ( E  /  N
) )  e.  CC )
142140, 141syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  x.  ( E  /  N ) )  e.  CC )
14373, 142jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( ( j ... N )  e.  Fin  /\  ( E  x.  ( E  /  N ) )  e.  CC ) )
144 fsumconst 12268 . . . . . . . . . . 11  |-  ( ( ( j ... N
)  e.  Fin  /\  ( E  x.  ( E  /  N ) )  e.  CC )  ->  sum_ i  e.  ( j ... N ) ( E  x.  ( E  /  N ) )  =  ( ( # `  ( j ... N
) )  x.  ( E  x.  ( E  /  N ) ) ) )
145143, 144syl 15 . . . . . . . . . 10  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  ( E  /  N ) )  =  ( ( # `  ( j ... N
) )  x.  ( E  x.  ( E  /  N ) ) ) )
1468, 74syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ( ZZ>= `  j ) )
147 hashfz 11397 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  j
)  ->  ( # `  (
j ... N ) )  =  ( ( N  -  j )  +  1 ) )
148146, 147syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
j ... N ) )  =  ( ( N  -  j )  +  1 ) )
149148oveq1d 5889 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  (
j ... N ) )  x.  ( E  x.  ( E  /  N
) ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
150145, 149eqtrd 2328 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  ( E  /  N ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
151135, 150breqtrd 4063 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( (
( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )
15273, 114fsumrecl 12223 . . . . . . . . . 10  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR )
15321, 116syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  RR )
154153, 15jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  e.  RR  /\  j  e.  RR ) )
155 resubcl 9127 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  RR  /\  j  e.  RR )  ->  ( N  -  j
)  e.  RR )
156154, 155syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  -  j
)  e.  RR )
157156, 92jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  -  j )  e.  RR  /\  1  e.  RR ) )
158 readdcl 8836 . . . . . . . . . . . . 13  |-  ( ( ( N  -  j
)  e.  RR  /\  1  e.  RR )  ->  ( ( N  -  j )  +  1 )  e.  RR )
159157, 158syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  -  j )  +  1 )  e.  RR )
16080, 153, 1363jca 1132 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E  e.  RR  /\  N  e.  RR  /\  N  =/=  0 ) )
161160, 121syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  /  N
)  e.  RR )
16280, 161jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  e.  RR  /\  ( E  /  N
)  e.  RR ) )
163162, 124syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  x.  ( E  /  N ) )  e.  RR )
164159, 163jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  e.  RR  /\  ( E  x.  ( E  /  N ) )  e.  RR ) )
165 remulcl 8838 . . . . . . . . . . 11  |-  ( ( ( ( N  -  j )  +  1 )  e.  RR  /\  ( E  x.  ( E  /  N ) )  e.  RR )  -> 
( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR )
166164, 165syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR )
167 fzfid 11051 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... (
j  -  1 ) )  e.  Fin )
16880adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  E  e.  RR )
169 simpl 443 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ph )
170 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ZZ )
171 peano2zm 10078 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
1728, 170, 1713syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( j  -  1 )  e.  ZZ )
173 lem1 9613 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
j  -  1 )  <_  j )
17415, 173syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( j  -  1 )  <_  j )
175 eluzle 10256 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  ( ZZ>= `  j
)  ->  j  <_  N )
176146, 175syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  j  <_  N )
177174, 176jca 518 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( j  - 
1 )  <_  j  /\  j  <_  N ) )
17815, 92jca 518 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( j  e.  RR  /\  1  e.  RR ) )
179 resubcl 9127 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( j  e.  RR  /\  1  e.  RR )  ->  ( j  -  1 )  e.  RR )
180178, 179syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( j  -  1 )  e.  RR )
181180, 15, 1533jca 1132 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( j  - 
1 )  e.  RR  /\  j  e.  RR  /\  N  e.  RR )
)
182 letr 8930 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( j  -  1 )  e.  RR  /\  j  e.  RR  /\  N  e.  RR )  ->  (
( ( j  - 
1 )  <_  j  /\  j  <_  N )  ->  ( j  - 
1 )  <_  N
) )
183181, 182syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( j  -  1 )  <_ 
j  /\  j  <_  N )  ->  ( j  -  1 )  <_  N ) )
184177, 183mpd 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( j  -  1 )  <_  N )
185172, 34, 1843jca 1132 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( j  - 
1 )  e.  ZZ  /\  N  e.  ZZ  /\  ( j  -  1 )  <_  N )
)
186 eluz2 10252 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ( ZZ>= `  (
j  -  1 ) )  <->  ( ( j  -  1 )  e.  ZZ  /\  N  e.  ZZ  /\  ( j  -  1 )  <_  N ) )
187185, 186sylibr 203 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ( ZZ>= `  ( j  -  1 ) ) )
188 fzss2 10847 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( ZZ>= `  (
j  -  1 ) )  ->  ( 0 ... ( j  - 
1 ) )  C_  ( 0 ... N
) )
189187, 188syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 0 ... (
j  -  1 ) )  C_  ( 0 ... N ) )
190189adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  (
0 ... ( j  - 
1 ) )  C_  ( 0 ... N
) )
191 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  i  e.  ( 0 ... (
j  -  1 ) ) )
192190, 191sseldd 3194 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  i  e.  ( 0 ... N
) )
193169, 192jca 518 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( ph  /\  i  e.  ( 0 ... N ) ) )
194193, 65syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  (
( X `  i
) `  t )  e.  RR )
195168, 194jca 518 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( E  e.  RR  /\  (
( X `  i
) `  t )  e.  RR ) )
196195, 113syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  e.  RR )
197167, 196fsumrecl 12223 . . . . . . . . . 10  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR )
198152, 166, 1973jca 1132 . . . . . . . . 9  |-  ( ph  ->  ( sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR  /\  sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  e.  RR ) )
199 axltadd 8912 . . . . . . . . 9  |-  ( (
sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR  /\  sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  e.  RR )  -> 
( sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( (
( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) )  -> 
( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  sum_ i  e.  ( j ... N
) ( E  x.  ( ( X `  i ) `  t
) ) )  < 
( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) ) )
200198, 199syl 15 . . . . . . . 8  |-  ( ph  ->  ( sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( (
( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) )  -> 
( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  sum_ i  e.  ( j ... N
) ( E  x.  ( ( X `  i ) `  t
) ) )  < 
( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) ) )
201151, 200mpd 14 . . . . . . 7  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  sum_ i  e.  ( j ... N
) ( E  x.  ( ( X `  i ) `  t
) ) )  < 
( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) )
20271, 201eqbrtrd 4059 . . . . . 6  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) ) )
203 stoweidlem11.5 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  (
( X `  i
) `  t )  <_  1 )
204193, 203syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  (
( X `  i
) `  t )  <_  1 )
20591a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  1  e.  RR )
206128adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  0  <  E )
207168, 206jca 518 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( E  e.  RR  /\  0  <  E ) )
208194, 205, 2073jca 1132 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  (
( ( X `  i ) `  t
)  e.  RR  /\  1  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
209 lemul2 9625 . . . . . . . . . . . . 13  |-  ( ( ( ( X `  i ) `  t
)  e.  RR  /\  1  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  -> 
( ( ( X `
 i ) `  t )  <_  1  <->  ( E  x.  ( ( X `  i ) `
 t ) )  <_  ( E  x.  1 ) ) )
210208, 209syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  (
( ( X `  i ) `  t
)  <_  1  <->  ( E  x.  ( ( X `  i ) `  t
) )  <_  ( E  x.  1 ) ) )
211204, 210mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  <_ 
( E  x.  1 ) )
212 mulid1 8851 . . . . . . . . . . . . 13  |-  ( E  e.  CC  ->  ( E  x.  1 )  =  E )
21359, 212syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  x.  1 )  =  E )
214213adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( E  x.  1 )  =  E )
215211, 214breqtrd 4063 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  <_  E )
216215idi 2 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... (
j  -  1 ) ) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  <_  E )
217167, 196, 168, 216fsumle 12273 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  <_  sum_ i  e.  ( 0 ... (
j  -  1 ) ) E )
218167, 59jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( 0 ... ( j  -  1 ) )  e.  Fin  /\  E  e.  CC ) )
219 fsumconst 12268 . . . . . . . . . 10  |-  ( ( ( 0 ... (
j  -  1 ) )  e.  Fin  /\  E  e.  CC )  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) E  =  ( (
# `  ( 0 ... ( j  -  1 ) ) )  x.  E ) )
220218, 219syl 15 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) E  =  ( (
# `  ( 0 ... ( j  -  1 ) ) )  x.  E ) )
221 1e0p1 10168 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( 0  +  1 )
222221fveq2i 5544 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
223222a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ZZ>= `  1 )  =  ( ZZ>= `  (
0  +  1 ) ) )
224223eleq2d 2363 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  (
ZZ>= `  1 )  <->  j  e.  ( ZZ>= `  ( 0  +  1 ) ) ) )
22510, 224mpbid 201 . . . . . . . . . . . . . 14  |-  ( ph  ->  j  e.  ( ZZ>= `  ( 0  +  1 ) ) )
22684, 225jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 0  e.  ZZ  /\  j  e.  ( ZZ>= `  ( 0  +  1 ) ) ) )
227 eluzp1m1 10267 . . . . . . . . . . . . 13  |-  ( ( 0  e.  ZZ  /\  j  e.  ( ZZ>= `  ( 0  +  1 ) ) )  -> 
( j  -  1 )  e.  ( ZZ>= ` 
0 ) )
228226, 227syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( j  -  1 )  e.  ( ZZ>= ` 
0 ) )
229 hashfz 11397 . . . . . . . . . . . 12  |-  ( ( j  -  1 )  e.  ( ZZ>= `  0
)  ->  ( # `  (
0 ... ( j  - 
1 ) ) )  =  ( ( ( j  -  1 )  -  0 )  +  1 ) )
230228, 229syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
0 ... ( j  - 
1 ) ) )  =  ( ( ( j  -  1 )  -  0 )  +  1 ) )
231 subcl 9067 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  CC  /\  1  e.  CC )  ->  ( j  -  1 )  e.  CC )
23249, 231syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  -  1 )  e.  CC )
233 subid1 9084 . . . . . . . . . . . . . 14  |-  ( ( j  -  1 )  e.  CC  ->  (
( j  -  1 )  -  0 )  =  ( j  - 
1 ) )
234232, 233syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( j  - 
1 )  -  0 )  =  ( j  -  1 ) )
235234oveq1d 5889 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( j  -  1 )  - 
0 )  +  1 )  =  ( ( j  -  1 )  +  1 ) )
236235, 51eqtrd 2328 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( j  -  1 )  - 
0 )  +  1 )  =  j )
237230, 236eqtrd 2328 . . . . . . . . . 10  |-  ( ph  ->  ( # `  (
0 ... ( j  - 
1 ) ) )  =  j )
238237oveq1d 5889 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  (
0 ... ( j  - 
1 ) ) )  x.  E )  =  ( j  x.  E
) )
23948, 59jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( j  e.  CC  /\  E  e.  CC ) )
240 mulcom 8839 . . . . . . . . . 10  |-  ( ( j  e.  CC  /\  E  e.  CC )  ->  ( j  x.  E
)  =  ( E  x.  j ) )
241239, 240syl 15 . . . . . . . . 9  |-  ( ph  ->  ( j  x.  E
)  =  ( E  x.  j ) )
242220, 238, 2413eqtrd 2332 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) E  =  ( E  x.  j ) )
243217, 242breqtrd 4063 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  <_  ( E  x.  j ) )
24480, 15jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( E  e.  RR  /\  j  e.  RR ) )
245 remulcl 8838 . . . . . . . . . 10  |-  ( ( E  e.  RR  /\  j  e.  RR )  ->  ( E  x.  j
)  e.  RR )
246244, 245syl 15 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  j
)  e.  RR )
247197, 246, 1663jca 1132 . . . . . . . 8  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( E  x.  j
)  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR ) )
248 leadd1 9258 . . . . . . . 8  |-  ( (
sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( E  x.  j
)  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR )  -> 
( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  <_  ( E  x.  j )  <->  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) ) )
249247, 248syl 15 . . . . . . 7  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  <_  ( E  x.  j )  <->  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) ) )
250243, 249mpbid 201 . . . . . 6  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  <_  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) ) )
251202, 250jca 518 . . . . 5  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  /\  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) ) )
25280adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  E  e.  RR )
253252, 65jca 518 . . . . . . . . 9  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  e.  RR  /\  (
( X `  i
) `  t )  e.  RR ) )
254253, 113syl 15 . . . . . . . 8  |-  ( (
ph  /\  i  e.  ( 0 ... N
) )  ->  ( E  x.  ( ( X `  i ) `  t ) )  e.  RR )
25556, 254fsumrecl 12223 . . . . . . 7  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR )
256197, 166jca 518 . . . . . . . 8  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR ) )
257 readdcl 8836 . . . . . . . 8  |-  ( (
sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR )  -> 
( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  e.  RR )
258256, 257syl 15 . . . . . . 7  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  e.  RR )
259246, 166jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  j )  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR ) )
260 readdcl 8836 . . . . . . . 8  |-  ( ( ( E  x.  j
)  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) )  e.  RR )  -> 
( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  e.  RR )
261259, 260syl 15 . . . . . . 7  |-  ( ph  ->  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  e.  RR )
262255, 258, 2613jca 1132 . . . . . 6  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  e.  RR  /\  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  e.  RR ) )
263 ltletr 8929 . . . . . 6  |-  ( (
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( sum_ i  e.  ( 0 ... ( j  -  1 ) ) ( E  x.  (
( X `  i
) `  t )
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  e.  RR  /\  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  e.  RR )  -> 
( ( sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) )  <  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  /\  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) )  ->  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) )  <  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) ) )
264262, 263syl 15 . . . . 5  |-  ( ph  ->  ( ( sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) )  <  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  /\  ( sum_ i  e.  ( 0 ... ( j  - 
1 ) ) ( E  x.  ( ( X `  i ) `
 t ) )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) )  ->  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) )  <  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) ) ) )
265251, 264mpd 14 . . . 4  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) ) )
26623, 48jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  e.  CC  /\  j  e.  CC ) )
267 subcl 9067 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  CC  /\  j  e.  CC )  ->  ( N  -  j
)  e.  CC )
268266, 267syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  -  j
)  e.  CC )
269268, 25jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  -  j )  e.  CC  /\  1  e.  CC ) )
270 addcl 8835 . . . . . . . . . . . . 13  |-  ( ( ( N  -  j
)  e.  CC  /\  1  e.  CC )  ->  ( ( N  -  j )  +  1 )  e.  CC )
271269, 270syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  -  j )  +  1 )  e.  CC )
27259, 271, 1393jca 1132 . . . . . . . . . . 11  |-  ( ph  ->  ( E  e.  CC  /\  ( ( N  -  j )  +  1 )  e.  CC  /\  ( E  /  N
)  e.  CC ) )
273 mulass 8841 . . . . . . . . . . 11  |-  ( ( E  e.  CC  /\  ( ( N  -  j )  +  1 )  e.  CC  /\  ( E  /  N
)  e.  CC )  ->  ( ( E  x.  ( ( N  -  j )  +  1 ) )  x.  ( E  /  N
) )  =  ( E  x.  ( ( ( N  -  j
)  +  1 )  x.  ( E  /  N ) ) ) )
274272, 273syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  ( ( N  -  j )  +  1 ) )  x.  ( E  /  N ) )  =  ( E  x.  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) ) )
275274eqcomd 2301 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  =  ( ( E  x.  ( ( N  -  j )  +  1 ) )  x.  ( E  /  N ) ) )
27659, 271jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( E  e.  CC  /\  ( ( N  -  j )  +  1 )  e.  CC ) )
277 mulcom 8839 . . . . . . . . . . 11  |-  ( ( E  e.  CC  /\  ( ( N  -  j )  +  1 )  e.  CC )  ->  ( E  x.  ( ( N  -  j )  +  1 ) )  =  ( ( ( N  -  j )  +  1 )  x.  E ) )
278276, 277syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( E  x.  (
( N  -  j
)  +  1 ) )  =  ( ( ( N  -  j
)  +  1 )  x.  E ) )
279278oveq1d 5889 . . . . . . . . 9  |-  ( ph  ->  ( ( E  x.  ( ( N  -  j )  +  1 ) )  x.  ( E  /  N ) )  =  ( ( ( ( N  -  j
)  +  1 )  x.  E )  x.  ( E  /  N
) ) )
280271, 59, 1393jca 1132 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  e.  CC  /\  E  e.  CC  /\  ( E  /  N
)  e.  CC ) )
281 mulass 8841 . . . . . . . . . 10  |-  ( ( ( ( N  -  j )  +  1 )  e.  CC  /\  E  e.  CC  /\  ( E  /  N )  e.  CC )  ->  (
( ( ( N  -  j )  +  1 )  x.  E
)  x.  ( E  /  N ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
282280, 281syl 15 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( N  -  j )  +  1 )  x.  E )  x.  ( E  /  N ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
283275, 279, 2823eqtrd 2332 . . . . . . . 8  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  =  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )
284283oveq2d 5890 . . . . . . 7  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  ( ( ( N  -  j
)  +  1 )  x.  ( E  /  N ) ) ) )  =  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) ) )
285 leid 8932 . . . . . . . . . 10  |-  ( ( E  x.  j )  e.  RR  ->  ( E  x.  j )  <_  ( E  x.  j
) )
286246, 285syl 15 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  j
)  <_  ( E  x.  j ) )
28723, 136jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  e.  CC  /\  N  =/=  0 ) )
288271, 59, 2873jca 1132 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  e.  CC  /\  E  e.  CC  /\  ( N  e.  CC  /\  N  =/=  0 ) ) )
289 div12 9462 . . . . . . . . . . . 12  |-  ( ( ( ( N  -  j )  +  1 )  e.  CC  /\  E  e.  CC  /\  ( N  e.  CC  /\  N  =/=  0 ) )  -> 
( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) )  =  ( E  x.  ( ( ( N  -  j )  +  1 )  /  N
) ) )
290288, 289syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) )  =  ( E  x.  ( ( ( N  -  j )  +  1 )  /  N
) ) )
291 leid 8932 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  RR  ->  N  <_  N )
292153, 291syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  <_  N )
293 elfzle1 10815 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 1 ... N )  ->  1  <_  j )
2948, 293syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  1  <_  j )
29592, 15jca 518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  e.  RR  /\  j  e.  RR ) )
296 suble0 9304 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1  e.  RR  /\  j  e.  RR )  ->  ( ( 1  -  j )  <_  0  <->  1  <_  j ) )
297295, 296syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1  -  j )  <_  0  <->  1  <_  j ) )
298294, 297mpbird 223 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1  -  j
)  <_  0 )
299292, 298jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  <_  N  /\  ( 1  -  j
)  <_  0 ) )
300 resubcl 9127 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  RR  /\  j  e.  RR )  ->  ( 1  -  j
)  e.  RR )
301295, 300syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1  -  j
)  e.  RR )
302153, 301jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  e.  RR  /\  ( 1  -  j
)  e.  RR ) )
303153, 90jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  e.  RR  /\  0  e.  RR ) )
304302, 303jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( N  e.  RR  /\  ( 1  -  j )  e.  RR )  /\  ( N  e.  RR  /\  0  e.  RR ) ) )
305 le2add 9272 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( N  e.  RR  /\  ( 1  -  j
)  e.  RR )  /\  ( N  e.  RR  /\  0  e.  RR ) )  -> 
( ( N  <_  N  /\  ( 1  -  j )  <_  0
)  ->  ( N  +  ( 1  -  j ) )  <_ 
( N  +  0 ) ) )
306304, 305syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( N  <_  N  /\  ( 1  -  j )  <_  0
)  ->  ( N  +  ( 1  -  j ) )  <_ 
( N  +  0 ) ) )
307299, 306mpd 14 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  ( 1  -  j ) )  <_  ( N  +  0 ) )
30823, 25, 483jca 1132 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( N  e.  CC  /\  1  e.  CC  /\  j  e.  CC )
)
309 addsub12 9080 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  CC  /\  1  e.  CC  /\  j  e.  CC )  ->  ( N  +  ( 1  -  j ) )  =  ( 1  +  ( N  -  j
) ) )
310308, 309syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  +  ( 1  -  j ) )  =  ( 1  +  ( N  -  j ) ) )
31125, 268jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1  e.  CC  /\  ( N  -  j
)  e.  CC ) )
312 addcom 9014 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1  e.  CC  /\  ( N  -  j
)  e.  CC )  ->  ( 1  +  ( N  -  j
) )  =  ( ( N  -  j
)  +  1 ) )
313311, 312syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1  +  ( N  -  j ) )  =  ( ( N  -  j )  +  1 ) )
314310, 313eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  ( 1  -  j ) )  =  ( ( N  -  j )  +  1 ) )
315 addid1 9008 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  ( N  +  0 )  =  N )
31623, 315syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  0 )  =  N )
317307, 314, 3163brtr3d 4068 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  -  j )  +  1 )  <_  N )
318 nngt0 9791 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN  ->  0  <  N )
31921, 318syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  0  <  N )
320153, 319jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  e.  RR  /\  0  <  N ) )
321159, 153, 3203jca 1132 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  e.  RR  /\  N  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) ) )
322 lediv1 9637 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  -  j )  +  1 )  e.  RR  /\  N  e.  RR  /\  ( N  e.  RR  /\  0  <  N ) )  -> 
( ( ( N  -  j )  +  1 )  <_  N  <->  ( ( ( N  -  j )  +  1 )  /  N )  <_  ( N  /  N ) ) )
323321, 322syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  <_  N  <->  ( ( ( N  -  j )  +  1 )  /  N )  <_  ( N  /  N ) ) )
324317, 323mpbid 201 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  /  N
)  <_  ( N  /  N ) )
325 divid 9467 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  CC  /\  N  =/=  0 )  -> 
( N  /  N
)  =  1 )
326287, 325syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  /  N
)  =  1 )
327324, 326breqtrd 4063 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  /  N
)  <_  1 )
328159, 153, 1363jca 1132 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  e.  RR  /\  N  e.  RR  /\  N  =/=  0 ) )
329 redivcl 9495 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( N  -  j )  +  1 )  e.  RR  /\  N  e.  RR  /\  N  =/=  0 )  ->  (
( ( N  -  j )  +  1 )  /  N )  e.  RR )
330328, 329syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  /  N
)  e.  RR )
33180, 128jca 518 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E  e.  RR  /\  0  <  E ) )
332330, 92, 3313jca 1132 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( N  -  j )  +  1 )  /  N )  e.  RR  /\  1  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
333 lemul2 9625 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( N  -  j )  +  1 )  /  N
)  e.  RR  /\  1  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  -> 
( ( ( ( N  -  j )  +  1 )  /  N )  <_  1  <->  ( E  x.  ( ( ( N  -  j
)  +  1 )  /  N ) )  <_  ( E  x.  1 ) ) )
334332, 333syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( N  -  j )  +  1 )  /  N )  <_  1  <->  ( E  x.  ( ( ( N  -  j
)  +  1 )  /  N ) )  <_  ( E  x.  1 ) ) )
335327, 334mpbid 201 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  /  N ) )  <_  ( E  x.  1 ) )
336335, 213breqtrd 4063 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  /  N ) )  <_  E )
337290, 336eqbrtrd 4059 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) )  <_  E )
338159, 161jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  e.  RR  /\  ( E  /  N
)  e.  RR ) )
339 remulcl 8838 . . . . . . . . . . . . 13  |-  ( ( ( ( N  -  j )  +  1 )  e.  RR  /\  ( E  /  N
)  e.  RR )  ->  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N
) )  e.  RR )
340338, 339syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) )  e.  RR )
341340, 80, 3313jca 1132 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( N  -  j )  +  1 )  x.  ( E  /  N
) )  e.  RR  /\  E  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
342 lemul2 9625 . . . . . . . . . . 11  |-  ( ( ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) )  e.  RR  /\  E  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  -> 
( ( ( ( N  -  j )  +  1 )  x.  ( E  /  N
) )  <_  E  <->  ( E  x.  ( ( ( N  -  j
)  +  1 )  x.  ( E  /  N ) ) )  <_  ( E  x.  E ) ) )
343341, 342syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( N  -  j )  +  1 )  x.  ( E  /  N
) )  <_  E  <->  ( E  x.  ( ( ( N  -  j
)  +  1 )  x.  ( E  /  N ) ) )  <_  ( E  x.  E ) ) )
344337, 343mpbid 201 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  <_  ( E  x.  E ) )
345286, 344jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  j )  <_  ( E  x.  j )  /\  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  <_  ( E  x.  E ) ) )
34680, 340jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) )  e.  RR ) )
347 remulcl 8838 . . . . . . . . . . . 12  |-  ( ( E  e.  RR  /\  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) )  e.  RR )  -> 
( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  e.  RR )
348346, 347syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  e.  RR )
349246, 348jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  j )  e.  RR  /\  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  e.  RR ) )
35080, 80jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  e.  RR  /\  E  e.  RR ) )
351 remulcl 8838 . . . . . . . . . . . 12  |-  ( ( E  e.  RR  /\  E  e.  RR )  ->  ( E  x.  E
)  e.  RR )
352350, 351syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  E
)  e.  RR )
353246, 352jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( ( E  x.  j )  e.  RR  /\  ( E  x.  E
)  e.  RR ) )
354349, 353jca 518 . . . . . . . . 9  |-  ( ph  ->  ( ( ( E  x.  j )  e.  RR  /\  ( E  x.  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N
) ) )  e.  RR )  /\  (
( E  x.  j
)  e.  RR  /\  ( E  x.  E
)  e.  RR ) ) )
355 le2add 9272 . . . . . . . . 9  |-  ( ( ( ( E  x.  j )  e.  RR  /\  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  e.  RR )  /\  ( ( E  x.  j )  e.  RR  /\  ( E  x.  E )  e.  RR ) )  -> 
( ( ( E  x.  j )  <_ 
( E  x.  j
)  /\  ( E  x.  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  <_  ( E  x.  E ) )  -> 
( ( E  x.  j )  +  ( E  x.  ( ( ( N  -  j
)  +  1 )  x.  ( E  /  N ) ) ) )  <_  ( ( E  x.  j )  +  ( E  x.  E ) ) ) )
356354, 355syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( ( E  x.  j )  <_ 
( E  x.  j
)  /\  ( E  x.  ( ( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  <_  ( E  x.  E ) )  -> 
( ( E  x.  j )  +  ( E  x.  ( ( ( N  -  j
)  +  1 )  x.  ( E  /  N ) ) ) )  <_  ( ( E  x.  j )  +  ( E  x.  E ) ) ) )
357345, 356mpd 14 . . . . . . 7  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  ( ( ( N  -  j
)  +  1 )  x.  ( E  /  N ) ) ) )  <_  ( ( E  x.  j )  +  ( E  x.  E ) ) )
358284, 357eqbrtrrd 4061 . . . . . 6  |-  ( ph  ->  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  ( ( E  x.  j )  +  ( E  x.  E ) ) )
35959, 48jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( E  e.  CC  /\  j  e.  CC ) )
360 mulcom 8839 . . . . . . . . . 10  |-  ( ( E  e.  CC  /\  j  e.  CC )  ->  ( E  x.  j
)  =  ( j  x.  E ) )
361359, 360syl 15 . . . . . . . . 9  |-  ( ph  ->  ( E  x.  j
)  =  ( j  x.  E ) )
362361oveq1d 5889 . . . . . . . 8  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  E ) )  =  ( ( j  x.  E )  +  ( E  x.  E ) ) )
36348, 59, 593jca 1132 . . . . . . . . 9  |-  ( ph  ->  ( j  e.  CC  /\  E  e.  CC  /\  E  e.  CC )
)
364 adddir 8846 . . . . . . . . 9  |-  ( ( j  e.  CC  /\  E  e.  CC  /\  E  e.  CC )  ->  (
( j  +  E
)  x.  E )  =  ( ( j  x.  E )  +  ( E  x.  E
) ) )
365363, 364syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( j  +  E )  x.  E
)  =  ( ( j  x.  E )  +  ( E  x.  E ) ) )
366362, 365eqtr4d 2331 . . . . . . 7  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  E ) )  =  ( ( j  +  E )  x.  E ) )
367 stoweidlem11.8 . . . . . . . . 9  |-  ( ph  ->  E  <  ( 1  /  3 ) )
368 3re 9833 . . . . . . . . . . . . . 14  |-  3  e.  RR
369368a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  3  e.  RR )
370 3ne0 9847 . . . . . . . . . . . . . 14  |-  3  =/=  0
371370a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  3  =/=  0 )
37292, 369, 3713jca 1132 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 ) )
373 redivcl 9495 . . . . . . . . . . . 12  |-  ( ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
1  /  3 )  e.  RR )
374372, 373syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
37580, 374, 153jca 1132 . . . . . . . . . 10  |-  ( ph  ->  ( E  e.  RR  /\  ( 1  /  3
)  e.  RR  /\  j  e.  RR )
)
376 ltadd2 8940 . . . . . . . . . 10  |-  ( ( E  e.  RR  /\  ( 1  /  3
)  e.  RR  /\  j  e.  RR )  ->  ( E  <  (
1  /  3 )  <-> 
( j  +  E
)  <  ( j  +  ( 1  / 
3 ) ) ) )
377375, 376syl 15 . . . . . . . . 9  |-  ( ph  ->  ( E  <  (
1  /  3 )  <-> 
( j  +  E
)  <  ( j  +  ( 1  / 
3 ) ) ) )
378367, 377mpbid 201 . . . . . . . 8  |-  ( ph  ->  ( j  +  E
)  <  ( j  +  ( 1  / 
3 ) ) )
37915, 80jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( j  e.  RR  /\  E  e.  RR ) )
380 readdcl 8836 . . . . . . . . . . 11  |-  ( ( j  e.  RR  /\  E  e.  RR )  ->  ( j  +  E
)  e.  RR )
381379, 380syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( j  +  E
)  e.  RR )
38215, 374jca 518 . . . . . . . . . . 11  |-  ( ph  ->  ( j  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
383 readdcl 8836 . . . . . . . . . . 11  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( j  +  ( 1  /  3
) )  e.  RR )
384382, 383syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( j  +  ( 1  /  3 ) )  e.  RR )
385381, 384, 3313jca 1132 . . . . . . . . 9  |-  ( ph  ->  ( ( j  +  E )  e.  RR  /\  ( j  +  ( 1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
386 ltmul1 9622 . . . . . . . . 9  |-  ( ( ( j  +  E
)  e.  RR  /\  ( j  +  ( 1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( (
j  +  E )  <  ( j  +  ( 1  /  3
) )  <->  ( (
j  +  E )  x.  E )  < 
( ( j  +  ( 1  /  3
) )  x.  E
) ) )
387385, 386syl 15 . . . . . . . 8  |-  ( ph  ->  ( ( j  +  E )  <  (
j  +  ( 1  /  3 ) )  <-> 
( ( j  +  E )  x.  E
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E ) ) )
388378, 387mpbid 201 . . . . . . 7  |-  ( ph  ->  ( ( j  +  E )  x.  E
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E ) )
389366, 388eqbrtrd 4059 . . . . . 6  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  E ) )  <  ( ( j  +  ( 1  /  3 ) )  x.  E ) )
390358, 389jca 518 . . . . 5  |-  ( ph  ->  ( ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  ( ( E  x.  j )  +  ( E  x.  E ) )  /\  ( ( E  x.  j )  +  ( E  x.  E ) )  <  ( ( j  +  ( 1  /  3 ) )  x.  E ) ) )
391 readdcl 8836 . . . . . . . 8  |-  ( ( ( E  x.  j
)  e.  RR  /\  ( E  x.  E
)  e.  RR )  ->  ( ( E  x.  j )  +  ( E  x.  E
) )  e.  RR )
392353, 391syl 15 . . . . . . 7  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  E ) )  e.  RR )
393384, 80jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( j  +  ( 1  /  3
) )  e.  RR  /\  E  e.  RR ) )
394 remulcl 8838 . . . . . . . 8  |-  ( ( ( j  +  ( 1  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR )
395393, 394syl 15 . . . . . . 7  |-  ( ph  ->  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR )
396261, 392, 3953jca 1132 . . . . . 6  |-  ( ph  ->  ( ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  e.  RR  /\  ( ( E  x.  j )  +  ( E  x.  E ) )  e.  RR  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR ) )
397 lelttr 8928 . . . . . 6  |-  ( ( ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  e.  RR  /\  ( ( E  x.  j )  +  ( E  x.  E ) )  e.  RR  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR )  ->  ( ( ( ( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  <_  ( ( E  x.  j )  +  ( E  x.  E
) )  /\  (
( E  x.  j
)  +  ( E  x.  E ) )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) )  -> 
( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <  ( ( j  +  ( 1  /  3 ) )  x.  E ) ) )
398396, 397syl 15 . . . . 5  |-  ( ph  ->  ( ( ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <_  (
( E  x.  j
)  +  ( E  x.  E ) )  /\  ( ( E  x.  j )  +  ( E  x.  E
) )  <  (
( j  +  ( 1  /  3 ) )  x.  E ) )  ->  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <  (
( j  +  ( 1  /  3 ) )  x.  E ) ) )
399390, 398mpd 14 . . . 4  |-  ( ph  ->  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <  ( ( j  +  ( 1  /  3 ) )  x.  E ) )
400265, 399jca 518 . . 3  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  /\  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) ) )
40191, 368, 3703pm3.2i 1130 . . . . . . . . . . 11  |-  ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )
402401a1i 10 . . . . . . . . . 10  |-  ( ph  ->  ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 ) )
403402, 373syl 15 . . . . . . . . 9  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
40415, 403jca 518 . . . . . . . 8  |-  ( ph  ->  ( j  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
405404, 383syl 15 . . . . . . 7  |-  ( ph  ->  ( j  +  ( 1  /  3 ) )  e.  RR )
406405, 80jca 518 . . . . . 6  |-  ( ph  ->  ( ( j  +  ( 1  /  3
) )  e.  RR  /\  E  e.  RR ) )
407406, 394syl 15 . . . . 5  |-  ( ph  ->  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR )
408255, 261, 4073jca 1132 . . . 4  |-  ( ph  ->  ( sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  e.  RR  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR ) )
409 lttr 8915 . . . 4  |-  ( (
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  e.  RR  /\  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  e.  RR  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR )  ->  ( ( sum_ i  e.  ( 0 ... N ) ( E  x.  ( ( X `  i ) `
 t ) )  <  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  /\  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <  (
( j  +  ( 1  /  3 ) )  x.  E ) )  ->  sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) )  <  (
( j  +  ( 1  /  3 ) )  x.  E ) ) )
410408, 409syl 15 . . 3  |-  ( ph  ->  ( ( sum_ i  e.  ( 0 ... N
) ( E  x.  ( ( X `  i ) `  t
) )  <  (
( E  x.  j
)  +  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )  /\  ( ( E  x.  j )  +  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )  <  ( ( j  +  ( 1  /  3 ) )  x.  E ) )  ->  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E ) ) )
411400, 410mpd 14 . 2  |-  ( ph  -> 
sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E ) )
4127, 411eqbrtrd 4059 1  |-  ( ph  ->  ( ( t  e.  T  |->  sum_ i  e.  ( 0 ... N ) ( E  x.  (
( X `  i
) `  t )
) ) `  t
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696    =/= wne 2459   _Vcvv 2801    u. cun 3163    i^i cin 3164    C_ wss 3165   (/)c0 3468   class class class wbr 4039    e. cmpt 4093   -->wf 5267   ` cfv 5271  (class class class)co 5874   Fincfn 6879   CCcc 8751   RRcr 8752   0cc0 8753   1c1 8754    + caddc 8756    x. cmul 8758    < clt 8883    <_ cle 8884    - cmin 9053    / cdiv 9439   NNcn 9762   3c3 9812   ZZcz 10040   ZZ>=cuz 10246   RR+crp 10370   ...cfz 10798   #chash 11353   sum_csu 12174
This theorem is referenced by:  stoweidlem34  27885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358  ax-cnex 8809  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-mulcom 8817  ax-addass 8818  ax-mulass 8819  ax-distr 8820  ax-i2m1 8821  ax-1ne0 8822  ax-1rid 8823  ax-rnegex 8824  ax-rrecex 8825  ax-cnre 8826  ax-pre-lttri 8827  ax-pre-lttrn 8828  ax-pre-ltadd 8829  ax-pre-mulgt0 8830  ax-pre-sup 8831
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-nel 2462  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-oprab 5878  df-mpt2 5879  df-1st 6138  df-2nd 6139  df-riota 6320  df-recs 6404  df-rdg 6439  df-1o 6495  df-oadd 6499  df-er 6676  df-en 6880  df-dom 6881  df-sdom 6882  df-fin 6883  df-sup 7210  df-oi 7241  df-card 7588  df-pnf 8885  df-mnf 8886  df-xr 8887  df-ltxr 8888  df-le 8889  df-sub 9055  df-neg 9056  df-div 9440  df-nn 9763  df-2 9820  df-3 9821  df-n0 9982  df-z 10041  df-uz 10247  df-rp 10371  df-ico 10678  df-fz 10799  df-fzo 10887  df-seq 11063  df-exp 11121  df-hash 11354  df-cj 11600  df-re 11601  df-im 11602  df-sqr 11736  df-abs 11737  df-clim 11978  df-sum 12175
  Copyright terms: Public domain W3C validator