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

Theorem stoweidlem11 26908
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 12207 . . . . 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 2316 . . . 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 5646 . . 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 10841 . . . . . . . . . . . . . 14  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ( ZZ>= `  1 )
)
108, 9syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  j  e.  ( ZZ>= ` 
1 ) )
11 eluz2 10283 . . . . . . . . . . . . 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 10075 . . . . . . . . . . 11  |-  ( j  e.  ZZ  ->  j  e.  RR )
1513, 14syl 15 . . . . . . . . . 10  |-  ( ph  ->  j  e.  RR )
16 ltm1 9641 . . . . . . . . . 10  |-  ( j  e.  RR  ->  (
j  -  1 )  <  j )
1715, 16syl 15 . . . . . . . . 9  |-  ( ph  ->  ( j  -  1 )  <  j )
18 fzdisj 10864 . . . . . . . . 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 10881 . . . . . . . . . . . 12  |-  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... (
( N  -  1 )  +  1 ) )
21 stoweidlem11.1 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  NN )
22 nncn 9799 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  N  e.  CC )
2321, 22syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  CC )
24 ax-1cn 8840 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
2524a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
2623, 25jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  e.  CC  /\  1  e.  CC ) )
27 npcan 9105 . . . . . . . . . . . . . 14  |-  ( ( N  e.  CC  /\  1  e.  CC )  ->  ( ( N  - 
1 )  +  1 )  =  N )
2826, 27syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
2928oveq2d 5916 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0 ... (
( N  -  1 )  +  1 ) )  =  ( 0 ... N ) )
3020, 29syl5sseq 3260 . . . . . . . . . . 11  |-  ( ph  ->  ( 0 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
31 1z 10100 . . . . . . . . . . . . . . . . 17  |-  1  e.  ZZ
3231a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  1  e.  ZZ )
33 nnz 10092 . . . . . . . . . . . . . . . . 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 10874 . . . . . . . . . . . . . 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 9162 . . . . . . . . . . . . 13  |-  ( 1  -  1 )  =  0
4241oveq1i 5910 . . . . . . . . . . . 12  |-  ( ( 1  -  1 ) ... ( N  - 
1 ) )  =  ( 0 ... ( N  -  1 ) )
4340, 42syl6eleq 2406 . . . . . . . . . . 11  |-  ( ph  ->  ( j  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
4430, 43sseldd 3215 . . . . . . . . . 10  |-  ( ph  ->  ( j  -  1 )  e.  ( 0 ... N ) )
45 fzsplit 10863 . . . . . . . . . 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 8872 . . . . . . . . . . . . . 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 9105 . . . . . . . . . . . 12  |-  ( ( j  e.  CC  /\  1  e.  CC )  ->  ( ( j  - 
1 )  +  1 )  =  j )
5149, 50syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( ( j  - 
1 )  +  1 )  =  j )
5251oveq1d 5915 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( j  -  1 )  +  1 ) ... N
)  =  ( j ... N ) )
5352uneq2d 3363 . . . . . . . . 9  |-  ( ph  ->  ( ( 0 ... ( j  -  1 ) )  u.  (
( ( j  - 
1 )  +  1 ) ... N ) )  =  ( ( 0 ... ( j  -  1 ) )  u.  ( j ... N ) ) )
5446, 53eqtrd 2348 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  =  ( ( 0 ... ( j  -  1 ) )  u.  ( j ... N ) ) )
55 fzfi 11081 . . . . . . . . 9  |-  ( 0 ... N )  e. 
Fin
5655a1i 10 . . . . . . . 8  |-  ( ph  ->  ( 0 ... N
)  e.  Fin )
57 stoweidlem11.7 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
58 rpcn 10409 . . . . . . . . . . . 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 5701 . . . . . . . . . . . 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 8872 . . . . . . . . . . 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 8866 . . . . . . . . 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 12259 . . . . . . 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 11081 . . . . . . . . . . 11  |-  ( j ... N )  e. 
Fin
7372a1i 10 . . . . . . . . . 10  |-  ( ph  ->  ( j ... N
)  e.  Fin )
74 elfzuz3 10842 . . . . . . . . . . . 12  |-  ( j  e.  ( 1 ... N )  ->  N  e.  ( ZZ>= `  j )
)
75 eluzfz2 10851 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  j
)  ->  N  e.  ( j ... N
) )
768, 74, 753syl 18 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( j ... N ) )
77 ne0i 3495 . . . . . . . . . . 11  |-  ( N  e.  ( j ... N )  ->  (
j ... N )  =/=  (/) )
7876, 77syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( j ... N
)  =/=  (/) )
79 rpre 10407 . . . . . . . . . . . . . 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 10082 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  e.  ZZ
8483a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  0  e.  ZZ )
85 0le1 9342 . . . . . . . . . . . . . . . . . . . . . . . . 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 8883 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  0  e.  RR
9089a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  0  e.  RR )
91 1re 8882 . . . . . . . . . . . . . . . . . . . . . . . . . 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 8959 . . . . . . . . . . . . . . . . . . . . . . . 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 10283 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ZZ>= `  0
)  <->  ( 0  e.  ZZ  /\  j  e.  ZZ  /\  0  <_ 
j ) )
9997, 98sylibr 203 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  j  e.  ( ZZ>= ` 
0 ) )
100 fzss1 10877 . . . . . . . . . . . . . . . . . . . 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 3209 . . . . . . . . . . . . . . . . 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 8867 . . . . . . . . . . 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 9798 . . . . . . . . . . . . . . 15  |-  ( N  e.  NN  ->  N  e.  RR )
117115, 116syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  i  e.  ( j ... N
) )  ->  N  e.  RR )
118 nnne0 9823 . . . . . . . . . . . . . . 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 9524 . . . . . . . . . . . . 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 8867 . . . . . . . . . . 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 10412 . . . . . . . . . . . . . . . 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 9652 . . . . . . . . . . . 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 12305 . . . . . . . . 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 9475 . . . . . . . . . . . . . . 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 8866 . . . . . . . . . . . . 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 12299 . . . . . . . . . . 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 11428 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  j
)  ->  ( # `  (
j ... N ) )  =  ( ( N  -  j )  +  1 ) )
148146, 147syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( # `  (
j ... N ) )  =  ( ( N  -  j )  +  1 ) )
149148oveq1d 5915 . . . . . . . . . 10  |-  ( ph  ->  ( ( # `  (
j ... N ) )  x.  ( E  x.  ( E  /  N
) ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
150145, 149eqtrd 2348 . . . . . . . . 9  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  ( E  /  N ) )  =  ( ( ( N  -  j )  +  1 )  x.  ( E  x.  ( E  /  N ) ) ) )
151135, 150breqtrd 4084 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( j ... N ) ( E  x.  (
( X `  i
) `  t )
)  <  ( (
( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )
15273, 114fsumrecl 12254 . . . . . . . . . 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 9156 . . . . . . . . . . . . . . 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 8865 . . . . . . . . . . . . 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 8867 . . . . . . . . . . 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 11082 . . . . . . . . . . 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 10845 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 1 ... N )  ->  j  e.  ZZ )
171 peano2zm 10109 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ZZ  ->  (
j  -  1 )  e.  ZZ )
1728, 170, 1713syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( j  -  1 )  e.  ZZ )
173 lem1 9642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  RR  ->  (
j  -  1 )  <_  j )
17415, 173syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( j  -  1 )  <_  j )
175 eluzle 10287 . . . . . . . . . . . . . . . . . . . . . . 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 9156 . . . . . . . . . . . . . . . . . . . . . . . 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 8959 . . . . . . . . . . . . . . . . . . . . . 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 10283 . . . . . . . . . . . . . . . . . . 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 10878 . . . . . . . . . . . . . . . . . 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 3215 . . . . . . . . . . . . . . 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 12254 . . . . . . . . . 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 8941 . . . . . . . . 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 4080 . . . . . 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 9654 . . . . . . . . . . . . 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 8880 . . . . . . . . . . . . 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 4084 . . . . . . . . . 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 12304 . . . . . . . 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 12299 . . . . . . . . . 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 10199 . . . . . . . . . . . . . . . . . 18  |-  1  =  ( 0  +  1 )
222221fveq2i 5566 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= ` 
1 )  =  (
ZZ>= `  ( 0  +  1 ) )
223222a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ZZ>= `  1 )  =  ( ZZ>= `  (
0  +  1 ) ) )
224223eleq2d 2383 . . . . . . . . . . . . . . 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 10298 . . . . . . . . . . . . 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 11428 . . . . . . . . . . . 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 9096 . . . . . . . . . . . . . . 15  |-  ( ( j  e.  CC  /\  1  e.  CC )  ->  ( j  -  1 )  e.  CC )
23249, 231syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( j  -  1 )  e.  CC )
233 subid1 9113 . . . . . . . . . . . . . 14  |-  ( ( j  -  1 )  e.  CC  ->  (
( j  -  1 )  -  0 )  =  ( j  - 
1 ) )
234232, 233syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( j  - 
1 )  -  0 )  =  ( j  -  1 ) )
235234oveq1d 5915 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( j  -  1 )  - 
0 )  +  1 )  =  ( ( j  -  1 )  +  1 ) )
236235, 51eqtrd 2348 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( j  -  1 )  - 
0 )  +  1 )  =  j )
237230, 236eqtrd 2348 . . . . . . . . . 10  |-  ( ph  ->  ( # `  (
0 ... ( j  - 
1 ) ) )  =  j )
238237oveq1d 5915 . . . . . . . . 9  |-  ( ph  ->  ( ( # `  (
0 ... ( j  - 
1 ) ) )  x.  E )  =  ( j  x.  E
) )
23948, 59jca 518 . . . . . . . . . 10  |-  ( ph  ->  ( j  e.  CC  /\  E  e.  CC ) )
240 mulcom 8868 . . . . . . . . . 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 2352 . . . . . . . 8  |-  ( ph  -> 
sum_ i  e.  ( 0 ... ( j  -  1 ) ) E  =  ( E  x.  j ) )
243217, 242breqtrd 4084 . . . . . . 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 8867 . . . . . . . . . 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 9287 . . . . . . . 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 12254 . . . . . . 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 8865 . . . . . . . 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 8865 . . . . . . . 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 8958 . . . . . 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 9096 . . . . . . . . . . . . . . 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 8864 . . . . . . . . . . . . 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 8870 . . . . . . . . . . 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 2321 . . . . . . . . 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 8868 . . . . . . . . . . 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 5915 . . . . . . . . 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 8870 . . . . . . . . . 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 2352 . . . . . . . 8  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  x.  ( E  /  N ) ) )  =  ( ( ( N  -  j
)  +  1 )  x.  ( E  x.  ( E  /  N
) ) ) )
284283oveq2d 5916 . . . . . . 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 8961 . . . . . . . . . 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 9491 . . . . . . . . . . . 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 8961 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  RR  ->  N  <_  N )
292153, 291syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  <_  N )
293 elfzle1 10846 . . . . . . . . . . . . . . . . . . . 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 9333 . . . . . . . . . . . . . . . . . . . 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 9156 . . . . . . . . . . . . . . . . . . . . 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 9301 . . . . . . . . . . . . . . . . . 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 9109 . . . . . . . . . . . . . . . . . 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 9043 . . . . . . . . . . . . . . . . . 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 2348 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  ( 1  -  j ) )  =  ( ( N  -  j )  +  1 ) )
315 addid1 9037 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  ( N  +  0 )  =  N )
31623, 315syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  0 )  =  N )
317307, 314, 3163brtr3d 4089 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  -  j )  +  1 )  <_  N )
318 nngt0 9820 . . . . . . . . . . . . . . . . . . 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 9666 . . . . . . . . . . . . . . . 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 9496 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  CC  /\  N  =/=  0 )  -> 
( N  /  N
)  =  1 )
326287, 325syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  /  N
)  =  1 )
327324, 326breqtrd 4084 . . . . . . . . . . . . 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 9524 . . . . . . . . . . . . . . . 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 9654 . . . . . . . . . . . . . 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 4084 . . . . . . . . . . 11  |-  ( ph  ->  ( E  x.  (
( ( N  -  j )  +  1 )  /  N ) )  <_  E )
337290, 336eqbrtrd 4080 . . . . . . . . . 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 8867 . . . . . . . . . . . . 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 9654 . . . . . . . . . . 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 8867 . . . . . . . . . . . 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 8867 . . . . . . . . . . . 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 9301 . . . . . . . . 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 4082 . . . . . 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 8868 . . . . . . . . . 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 5915 . . . . . . . 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 8875 . . . . . . . . 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 2351 . . . . . . 7  |-  ( ph  ->  ( ( E  x.  j )  +  ( E  x.  E ) )  =  ( ( j  +  E )  x.  E ) )
367 stoweidlem11.8 . . . . . . . . 9  |-  ( ph  ->  E  <  ( 1  /  3 ) )
368 3re 9862 . . . . . . . . . . . . . 14  |-  3  e.  RR
369368a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  3  e.  RR )
370 3ne0 9876 . . . . . . . . . . . . . 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 9524 . . . . . . . . . . . 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 8969 . . . . . . . . . 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 8865 . . . . . . . . . . 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 8865 . . . . . . . . . . 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 9651 . . . . . . . . 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 4080 . . . . . 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 8865 . . . . . . . 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 8867 . . . . . . . 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 8957 . . . . . 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 8944 . . . 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 4080 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 1633    e. wcel 1701    =/= wne 2479   _Vcvv 2822    u. cun 3184    i^i cin 3185    C_ wss 3186   (/)c0 3489   class class class wbr 4060    e. cmpt 4114   -->wf 5288   ` cfv 5292  (class class class)co 5900   Fincfn 6906   CCcc 8780   RRcr 8781   0cc0 8782   1c1 8783    + caddc 8785    x. cmul 8787    < clt 8912    <_ cle 8913    - cmin 9082    / cdiv 9468   NNcn 9791   3c3 9841   ZZcz 10071   ZZ>=cuz 10277   RR+crp 10401   ...cfz 10829   #chash 11384   sum_csu 12205
This theorem is referenced by:  stoweidlem34  26931
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859  ax-pre-sup 8860
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 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-oadd 6525  df-er 6702  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-sup 7239  df-oi 7270  df-card 7617  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-div 9469  df-nn 9792  df-2 9849  df-3 9850  df-n0 10013  df-z 10072  df-uz 10278  df-rp 10402  df-ico 10709  df-fz 10830  df-fzo 10918  df-seq 11094  df-exp 11152  df-hash 11385  df-cj 11631  df-re 11632  df-im 11633  df-sqr 11767  df-abs 11768  df-clim 12009  df-sum 12206
  Copyright terms: Public domain W3C validator