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

Theorem stoweidlem11 27760
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 12160 . . . . 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 2283 . . . 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 5608 . . 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 10794 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ( ZZ>= `  1 )
)
108, 9syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  j  e.  ( ZZ>= ` 
1 ) )
11 eluz2 10236 . . . . . . . . . . . . 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 10028 . . . . . . . . . . 11  |-  ( j  e.  ZZ  ->  j  e.  RR )
1513, 14syl 15 . . . . . . . . . 10  |-  ( ph  ->  j  e.  RR )
16 ltm1 9596 . . . . . . . . . 10  |-  ( j  e.  RR  ->  (
j  -  1 )  <  j )
1715, 16syl 15 . . . . . . . . 9  |-  ( ph  ->  ( j  -  1 )  <  j )
18 fzdisj 10817 . . . . . . . . 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 10834 . . . . . . . . . . . 12  |-  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... (
( N  -  1 )  +  1 ) )
21 stoweidlem11.1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  NN )
22 nncn 9754 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  N  e.  CC )
2321, 22syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
24 ax-1cn 8795 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
2524a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
2623, 25jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  e.  CC  /\  1  e.  CC ) )
27 npcan 9060 . . . . . . . . . . . . . 14  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  - 
1 )  +  1 )  =  N )
2826, 27syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
2928oveq2d 5874 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... (
( N  -  1 )  +  1 ) )  =  ( 0 ... N ) )
3020, 29syl5sseq 3226 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
31 1z 10053 . . . . . . . . . . . . . . . . 17  |-  1  e.  ZZ
3231a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  1  e.  ZZ )
33 nnz 10045 . . . . . . . . . . . . . . . . 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 10827 . . . . . . . . . . . . . 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 9117 . . . . . . . . . . . . 13  |-  ( 1  -  1 )  =  0
4241oveq1i 5868 . . . . . . . . . . . 12  |-  ( ( 1  -  1 ) ... ( N  - 
1 ) )  =  ( 0 ... ( N  -  1 ) )
4340, 42syl6eleq 2373 . . . . . . . . . . 11  |-  ( ph  ->  ( j  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
4430, 43sseldd 3181 . . . . . . . . . 10  |-  ( ph  ->  ( j  -  1 )  e.  ( 0 ... N ) )
45 fzsplit 10816 . . . . . . . . . 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 8827 . . . . . . . . . . . . . 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 9060 . . . . . . . . . . . 12  |-  ( ( j  e.  CC  /\  1  e.  CC )  ->  ( ( j  - 
1 )  +  1 )  =  j )
5149, 50syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( j  - 
1 )  +  1 )  =  j )
5251oveq1d 5873 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( j  -  1 )  +  1 ) ... N
)  =  ( j ... N ) )
5352uneq2d 3329 . . . . . . . . 9  |-  ( ph  ->  ( ( 0 ... ( j  -  1 ) )  u.  (
( ( j  - 
1 )  +  1 ) ... N ) )  =  ( ( 0 ... ( j  -  1 ) )  u.  ( j ... N ) ) )
5446, 53eqtrd 2315 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  =  ( ( 0 ... ( j  -  1 ) )  u.  ( j ... N ) ) )
55 fzfi 11034 . . . . . . . . 9  |-  ( 0 ... N )  e. 
Fin
5655a1i 10 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
57 stoweidlem11.7 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
58 rpcn 10362 . . . . . . . . . . . 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 5663 . . . . . . . . . . . 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 8827 . . . . . . . . . . 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 8821 . . . . . . . . 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 12212 . . . . . . 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 11034 . . . . . . . . . . 11  |-  ( j ... N )  e. 
Fin
7372a1i 10 . . . . . . . . . 10  |-  ( ph  ->  ( j ... N
)  e.  Fin )
74 elfzuz3 10795 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... N )  ->  N  e.  ( ZZ>= `  j )
)
75 eluzfz2 10804 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  j
)  ->  N  e.  ( j ... N
) )
768, 74, 753syl 18 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( j ... N ) )
77 ne0i 3461 . . . . . . . . . . 11  |-  ( N  e.  ( j ... N )  ->  (
j ... N )  =/=  (/) )
7876, 77syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( j ... N
)  =/=  (/) )
79 rpre 10360 . . . . . . . . . . . . . 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 10035 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
8483a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  e.  ZZ )
85 0le1 9297 . . . . . . . . . . . . . . . . . . . . . . . . 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 8838 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  e.  RR
9089a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  0  e.  RR )
91 1re 8837 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8914 . . . . . . . . . . . . . . . . . . . . . . . 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 10236 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  j  e.  ZZ  /\  0  <_ 
j ) )
9997, 98sylibr 203 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  j  e.  ( ZZ>= ` 
0 ) )
100 fzss1 10830 . . . . . . . . . . . . . . . . . . . 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 3175 . . . . . . . . . . . . . . . . 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 8822 . . . . . . . . . . 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 9753 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  N  e.  RR )
117115, 116syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  N  e.  RR )
118 nnne0 9778 . . . . . . . . . . . . . . 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 9479 . . . . . . . . . . . . 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 8822 . . . . . . . . . . 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 10365 . . . . . . . . . . . . . . . 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 9607 . . . . . . . . . . . 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 12258 . . . . . . . . 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 9430 . . . . . . . . . . . . . . 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 8821 . . . . . . . . . . . . 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 12252 . . . . . . . . . . 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 11381 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  j
)  ->  ( # `  (
j ... N ) )  =  ( ( N  -  j )  +  1 ) )
148146, 147syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
j ... N ) )  =  ( ( N  -  j )  +  1 ) )
149148oveq1d 5873 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  (
j ... N ) )  x.  ( E  x.  ( E  /  N
) ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
150145, 149eqtrd 2315 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  ( E  /  N ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
151135, 150breqtrd 4047 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( (
( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )
15273, 114fsumrecl 12207 . . . . . . . . . 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 9111 . . . . . . . . . . . . . . 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 8820 . . . . . . . . . . . . 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 8822 . . . . . . . . . . 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 11035 . . . . . . . . . . 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 10798 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ZZ )
171 peano2zm 10062 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
1728, 170, 1713syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( j  -  1 )  e.  ZZ )
173 lem1 9597 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
j  -  1 )  <_  j )
17415, 173syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( j  -  1 )  <_  j )
175 eluzle 10240 . . . . . . . . . . . . . . . . . . . . . . 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 9111 . . . . . . . . . . . . . . . . . . . . . . . 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 8914 . . . . . . . . . . . . . . . . . . . . . 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 10236 . . . . . . . . . . . . . . . . . . 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 10831 . . . . . . . . . . . . . . . . . 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 3181 . . . . . . . . . . . . . . 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 12207 . . . . . . . . . 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 8896 . . . . . . . . 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 4043 . . . . . 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 9609 . . . . . . . . . . . . 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 8835 . . . . . . . . . . . . 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 4047 . . . . . . . . . 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 12257 . . . . . . . 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 12252 . . . . . . . . . 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 10152 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( 0  +  1 )
222221fveq2i 5528 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
223222a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ZZ>= `  1 )  =  ( ZZ>= `  (
0  +  1 ) ) )
224223eleq2d 2350 . . . . . . . . . . . . . . 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 10251 . . . . . . . . . . . . 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 11381 . . . . . . . . . . . 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 9051 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  CC  /\  1  e.  CC )  ->  ( j  -  1 )  e.  CC )
23249, 231syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  -  1 )  e.  CC )
233 subid1 9068 . . . . . . . . . . . . . 14  |-  ( ( j  -  1 )  e.  CC  ->  (
( j  -  1 )  -  0 )  =  ( j  - 
1 ) )
234232, 233syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( j  - 
1 )  -  0 )  =  ( j  -  1 ) )
235234oveq1d 5873 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( j  -  1 )  - 
0 )  +  1 )  =  ( ( j  -  1 )  +  1 ) )
236235, 51eqtrd 2315 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( j  -  1 )  - 
0 )  +  1 )  =  j )
237230, 236eqtrd 2315 . . . . . . . . . 10  |-  ( ph  ->  ( # `  (
0 ... ( j  - 
1 ) ) )  =  j )
238237oveq1d 5873 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  (
0 ... ( j  - 
1 ) ) )  x.  E )  =  ( j  x.  E
) )
23948, 59jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( j  e.  CC  /\  E  e.  CC ) )
240 mulcom 8823 . . . . . . . . . 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 2319 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) E  =  ( E  x.  j ) )
243217, 242breqtrd 4047 . . . . . . 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 8822 . . . . . . . . . 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 9242 . . . . . . . 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 12207 . . . . . . 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 8820 . . . . . . . 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 8820 . . . . . . . 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 8913 . . . . . 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 9051 . . . . . . . . . . . . . . 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 8819 . . . . . . . . . . . . 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 8825 . . . . . . . . . . 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 2288 . . . . . . . . 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 8823 . . . . . . . . . . 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 5873 . . . . . . . . 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 8825 . . . . . . . . . 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 2319 . . . . . . . 8  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  =  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )
284283oveq2d 5874 . . . . . . 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 8916 . . . . . . . . . 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 9446 . . . . . . . . . . . 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 8916 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  RR  ->  N  <_  N )
292153, 291syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  <_  N )
293 elfzle1 10799 . . . . . . . . . . . . . . . . . . . 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 9288 . . . . . . . . . . . . . . . . . . . 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 9111 . . . . . . . . . . . . . . . . . . . . 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 9256 . . . . . . . . . . . . . . . . . 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 9064 . . . . . . . . . . . . . . . . . 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 8998 . . . . . . . . . . . . . . . . . 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 2315 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  ( 1  -  j ) )  =  ( ( N  -  j )  +  1 ) )
315 addid1 8992 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  ( N  +  0 )  =  N )
31623, 315syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  0 )  =  N )
317307, 314, 3163brtr3d 4052 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  -  j )  +  1 )  <_  N )
318 nngt0 9775 . . . . . . . . . . . . . . . . . . 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 9621 . . . . . . . . . . . . . . . 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 9451 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  CC  /\  N  =/=  0 )  -> 
( N  /  N
)  =  1 )
326287, 325syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  /  N
)  =  1 )
327324, 326breqtrd 4047 . . . . . . . . . . . . 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 9479 . . . . . . . . . . . . . . . 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 9609 . . . . . . . . . . . . . 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 4047 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  /  N ) )  <_  E )
337290, 336eqbrtrd 4043 . . . . . . . . . 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 8822 . . . . . . . . . . . . 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 9609 . . . . . . . . . . 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 8822 . . . . . . . . . . . 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 8822 . . . . . . . . . . . 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 9256 . . . . . . . . 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 4045 . . . . . 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 8823 . . . . . . . . . 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 5873 . . . . . . . 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 8830 . . . . . . . . 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 2318 . . . . . . 7  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  E ) )  =  ( ( j  +  E )  x.  E ) )
367 stoweidlem11.8 . . . . . . . . 9  |-  ( ph  ->  E  <  ( 1  /  3 ) )
368 3re 9817 . . . . . . . . . . . . . 14  |-  3  e.  RR
369368a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  3  e.  RR )
370 3ne0 9831 . . . . . . . . . . . . . 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 9479 . . . . . . . . . . . 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 8924 . . . . . . . . . 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 8820 . . . . . . . . . . 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 8820 . . . . . . . . . . 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 9606 . . . . . . . . 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 4043 . . . . . 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 8820 . . . . . . . 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 8822 . . . . . . . 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 8912 . . . . . 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 8899 . . . 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 4043 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 1623    e. wcel 1684    =/= wne 2446   _Vcvv 2788    u. cun 3150    i^i cin 3151    C_ wss 3152   (/)c0 3455   class class class wbr 4023    e. cmpt 4077   -->wf 5251   ` cfv 5255  (class class class)co 5858   Fincfn 6863   CCcc 8735   RRcr 8736   0cc0 8737   1c1 8738    + caddc 8740    x. cmul 8742    < clt 8867    <_ cle 8868    - cmin 9037    / cdiv 9423   NNcn 9746   3c3 9796   ZZcz 10024   ZZ>=cuz 10230   RR+crp 10354   ...cfz 10782   #chash 11337   sum_csu 12158
This theorem is referenced by:  stoweidlem34  27783
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815
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 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-sup 7194  df-oi 7225  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-ico 10662  df-fz 10783  df-fzo 10871  df-seq 11047  df-exp 11105  df-hash 11338  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-clim 11962  df-sum 12159
  Copyright terms: Public domain W3C validator