MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mertenslem1 Unicode version

Theorem mertenslem1 12342
Description: Lemma for mertens 12344. (Contributed by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
mertens.1  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( F `  j )  =  A )
mertens.2  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( abs `  A ) )
mertens.3  |-  ( (
ph  /\  j  e.  NN0 )  ->  A  e.  CC )
mertens.4  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  =  B )
mertens.5  |-  ( (
ph  /\  k  e.  NN0 )  ->  B  e.  CC )
mertens.6  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( H `  k )  =  sum_ j  e.  ( 0 ... k ) ( A  x.  ( G `
 ( k  -  j ) ) ) )
mertens.7  |-  ( ph  ->  seq  0 (  +  ,  K )  e. 
dom 
~~>  )
mertens.8  |-  ( ph  ->  seq  0 (  +  ,  G )  e. 
dom 
~~>  )
mertens.9  |-  ( ph  ->  E  e.  RR+ )
mertens.10  |-  T  =  { z  |  E. n  e.  ( 0 ... ( s  - 
1 ) ) z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) }
mertens.11  |-  ( ps  <->  ( s  e.  NN  /\  A. n  e.  ( ZZ>= `  s ) ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
mertens.12  |-  ( ph  ->  ( ps  /\  (
t  e.  NN0  /\  A. m  e.  ( ZZ>= `  t ) ( K `
 m )  < 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) ) )
mertens.13  |-  ( ph  ->  ( 0  <_  sup ( T ,  RR ,  <  )  /\  ( T 
C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z
) ) )
Assertion
Ref Expression
mertenslem1  |-  ( ph  ->  E. y  e.  NN0  A. m  e.  ( ZZ>= `  y ) ( abs `  sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <  E )
Distinct variable groups:    j, m, n, s, t, y, z, B    j, k, G, m, n, s, y, z    ph, j, k, m, y, z    t, k, A, m, n, s, y    j, E, k, m, n, s, t, y, z    j, K, k, m, n, s, t, y, z    j, F, m, n, y    ps, j, k, m, n, t, y, z    w, j, T, k, m, n, t, y, z    k, H, m, y
Allowed substitution hints:    ph( w, t, n, s)    ps( w, s)    A( z, w, j)    B( w, k)    T( s)    E( w)    F( z, w, t, k, s)    G( w, t)    H( z, w, t, j, n, s)    K( w)

Proof of Theorem mertenslem1
StepHypRef Expression
1 mertens.12 . . . . . . 7  |-  ( ph  ->  ( ps  /\  (
t  e.  NN0  /\  A. m  e.  ( ZZ>= `  t ) ( K `
 m )  < 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) ) )
21simpld 445 . . . . . 6  |-  ( ph  ->  ps )
3 mertens.11 . . . . . 6  |-  ( ps  <->  ( s  e.  NN  /\  A. n  e.  ( ZZ>= `  s ) ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
42, 3sylib 188 . . . . 5  |-  ( ph  ->  ( s  e.  NN  /\ 
A. n  e.  (
ZZ>= `  s ) ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) )  <  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) ) )
54simpld 445 . . . 4  |-  ( ph  ->  s  e.  NN )
65nnnn0d 10020 . . 3  |-  ( ph  ->  s  e.  NN0 )
71simprd 449 . . . 4  |-  ( ph  ->  ( t  e.  NN0  /\ 
A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
87simpld 445 . . 3  |-  ( ph  ->  t  e.  NN0 )
96, 8nn0addcld 10024 . 2  |-  ( ph  ->  ( s  +  t )  e.  NN0 )
10 fzfid 11037 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... m )  e. 
Fin )
11 simpl 443 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ph )
12 elfznn0 10824 . . . . . . . 8  |-  ( j  e.  ( 0 ... m )  ->  j  e.  NN0 )
13 mertens.3 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN0 )  ->  A  e.  CC )
1411, 12, 13syl2an 463 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  A  e.  CC )
15 eqid 2285 . . . . . . . 8  |-  ( ZZ>= `  ( ( m  -  j )  +  1 ) )  =  (
ZZ>= `  ( ( m  -  j )  +  1 ) )
16 fznn0sub 10826 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... m )  ->  (
m  -  j )  e.  NN0 )
1716adantl 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
m  -  j )  e.  NN0 )
18 peano2nn0 10006 . . . . . . . . . 10  |-  ( ( m  -  j )  e.  NN0  ->  ( ( m  -  j )  +  1 )  e. 
NN0 )
1917, 18syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
2019nn0zd 10117 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
21 simplll 734 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
22 eluznn0 10290 . . . . . . . . . 10  |-  ( ( ( ( m  -  j )  +  1 )  e.  NN0  /\  k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) )  -> 
k  e.  NN0 )
2319, 22sylan 457 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
24 mertens.4 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  =  B )
2521, 23, 24syl2anc 642 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
26 mertens.5 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  B  e.  CC )
2721, 23, 26syl2anc 642 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  B  e.  CC )
28 mertens.8 . . . . . . . . . 10  |-  ( ph  ->  seq  0 (  +  ,  G )  e. 
dom 
~~>  )
2928ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq  0 (  +  ,  G )  e.  dom  ~~>  )
30 nn0uz 10264 . . . . . . . . . 10  |-  NN0  =  ( ZZ>= `  0 )
31 simpll 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ph )
3224, 26eqeltrd 2359 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3331, 32sylan 457 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3430, 19, 33iserex 12132 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (  seq  0 (  +  ,  G )  e.  dom  ~~>  <->  seq  ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  ) )
3529, 34mpbid 201 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq  ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
3615, 20, 25, 27, 35isumcl 12226 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
3714, 36mulcld 8857 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  CC )
3810, 37fsumcl 12208 . . . . 5  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  CC )
3938abscld 11920 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( abs ` 
sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
4037abscld 11920 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
4110, 40fsumrecl 12209 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) )  e.  RR )
42 mertens.9 . . . . . 6  |-  ( ph  ->  E  e.  RR+ )
4342rpred 10392 . . . . 5  |-  ( ph  ->  E  e.  RR )
4443adantr 451 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  E  e.  RR )
4510, 37fsumabs 12261 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( abs ` 
sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  sum_ j  e.  ( 0 ... m
) ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) ) )
46 fzfid 11037 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  e. 
Fin )
476adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  NN0 )
4847nn0ge0d 10023 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  <_  s )
49 eluzelz 10240 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  m  e.  ZZ )
5049adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ZZ )
5150zred 10119 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  RR )
5247nn0red 10021 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  RR )
5351, 52subge02d 9366 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0  <_  s  <->  ( m  -  s )  <_  m ) )
5448, 53mpbid 201 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  <_  m )
5547, 30syl6eleq 2375 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( ZZ>= `  0 )
)
565nnzd 10118 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  s  e.  ZZ )
57 uzid 10244 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  s  e.  ( ZZ>= `  s )
)
5856, 57syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  s  e.  ( ZZ>= `  s ) )
59 uzaddcl 10277 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( ZZ>= `  s )  /\  t  e.  NN0 )  ->  (
s  +  t )  e.  ( ZZ>= `  s
) )
6058, 8, 59syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  +  t )  e.  ( ZZ>= `  s ) )
61 eqid 2285 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= `  s )  =  (
ZZ>= `  s )
6261uztrn2 10247 . . . . . . . . . . . . . . . 16  |-  ( ( ( s  +  t )  e.  ( ZZ>= `  s )  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
6360, 62sylan 457 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
64 elfzuzb 10794 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( 0 ... m )  <->  ( s  e.  ( ZZ>= `  0 )  /\  m  e.  ( ZZ>=
`  s ) ) )
6555, 63, 64sylanbrc 645 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( 0 ... m
) )
66 fznn0sub2 10827 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 0 ... m )  ->  (
m  -  s )  e.  ( 0 ... m ) )
6765, 66syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ( 0 ... m
) )
68 elfzelz 10800 . . . . . . . . . . . . 13  |-  ( ( m  -  s )  e.  ( 0 ... m )  ->  (
m  -  s )  e.  ZZ )
6967, 68syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ZZ )
70 eluz 10243 . . . . . . . . . . . 12  |-  ( ( ( m  -  s
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( m  e.  (
ZZ>= `  ( m  -  s ) )  <->  ( m  -  s )  <_  m ) )
7169, 50, 70syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  e.  ( ZZ>= `  ( m  -  s ) )  <-> 
( m  -  s
)  <_  m )
)
7254, 71mpbird 223 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  ( m  -  s ) ) )
73 fzss2 10833 . . . . . . . . . 10  |-  ( m  e.  ( ZZ>= `  (
m  -  s ) )  ->  ( 0 ... ( m  -  s ) )  C_  ( 0 ... m
) )
7472, 73syl 15 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  C_  ( 0 ... m
) )
7574sselda 3182 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ( 0 ... m
) )
7613abscld 11920 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  RR )
7711, 12, 76syl2an 463 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  A )  e.  RR )
7836abscld 11920 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
7977, 78remulcld 8865 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
8075, 79syldan 456 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
8146, 80fsumrecl 12209 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
82 fzfid 11037 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( m  -  s
)  +  1 ) ... m )  e. 
Fin )
83 elfznn0 10824 . . . . . . . . . . . . 13  |-  ( ( m  -  s )  e.  ( 0 ... m )  ->  (
m  -  s )  e.  NN0 )
8467, 83syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e. 
NN0 )
85 peano2nn0 10006 . . . . . . . . . . . 12  |-  ( ( m  -  s )  e.  NN0  ->  ( ( m  -  s )  +  1 )  e. 
NN0 )
8684, 85syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e. 
NN0 )
8786, 30syl6eleq 2375 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  0 )
)
88 fzss1 10832 . . . . . . . . . 10  |-  ( ( ( m  -  s
)  +  1 )  e.  ( ZZ>= `  0
)  ->  ( (
( m  -  s
)  +  1 ) ... m )  C_  ( 0 ... m
) )
8987, 88syl 15 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( m  -  s
)  +  1 ) ... m )  C_  ( 0 ... m
) )
9089sselda 3182 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( 0 ... m
) )
9190, 79syldan 456 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
9282, 91fsumrecl 12209 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
9342rphalfcld 10404 . . . . . . . 8  |-  ( ph  ->  ( E  /  2
)  e.  RR+ )
9493rpred 10392 . . . . . . 7  |-  ( ph  ->  ( E  /  2
)  e.  RR )
9594adantr 451 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  RR )
96 elfznn0 10824 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  NN0 )
9711, 96, 76syl2an 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  RR )
9846, 97fsumrecl 12209 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  RR )
9998, 95remulcld 8865 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  e.  RR )
100 0z 10037 . . . . . . . . . . . 12  |-  0  e.  ZZ
101100a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ZZ )
102 eqidd 2286 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( K `  j ) )
103 mertens.2 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( abs `  A ) )
104103, 76eqeltrd 2359 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  e.  RR )
105 mertens.7 . . . . . . . . . . 11  |-  ( ph  ->  seq  0 (  +  ,  K )  e. 
dom 
~~>  )
10630, 101, 102, 104, 105isumrecl 12230 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  e.  RR )
10713absge0d 11928 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( abs `  A ) )
108107, 103breqtrrd 4051 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( K `  j ) )
10930, 101, 102, 104, 105, 108isumge0 12231 . . . . . . . . . 10  |-  ( ph  ->  0  <_  sum_ j  e. 
NN0  ( K `  j ) )
110106, 109ge0p1rpd 10418 . . . . . . . . 9  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR+ )
111110adantr 451 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR+ )
11299, 111rerpdivcld 10419 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR )
11393, 110rpdivcld 10409 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR+ )
114113rpred 10392 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR )
115114ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )  e.  RR )
11697, 115remulcld 8865 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )  e.  RR )
11775, 20syldan 456 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
118 simplll 734 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
11975, 19syldan 456 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
120119, 22sylan 457 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
121118, 120, 24syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
122118, 120, 26syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  B  e.  CC )
12375, 35syldan 456 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  seq  ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
12415, 117, 121, 122, 123isumcl 12226 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
125124abscld 11920 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
12676, 107jca 518 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( ( abs `  A )  e.  RR  /\  0  <_ 
( abs `  A
) ) )
12711, 96, 126syl2an 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
128121sumeq2dv 12178 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )
129128fveq2d 5531 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
130 elfzelz 10800 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  ZZ )
131130adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ZZ )
132131zred 10119 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  RR )
13349ad2antlr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  ZZ )
134133zred 10119 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  RR )
13556ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  ZZ )
136135zred 10119 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  RR )
137 elfzle2 10802 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  <_  ( m  -  s
) )
138137adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  <_  ( m  -  s
) )
139132, 134, 136, 138lesubd 9378 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  <_  ( m  -  j
) )
140133, 131zsubcld 10124 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ZZ )
141 eluz 10243 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ZZ  /\  ( m  -  j
)  e.  ZZ )  ->  ( ( m  -  j )  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
142135, 140, 141syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
143139, 142mpbird 223 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ( ZZ>= `  s
) )
1444simprd 449 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. n  e.  (
ZZ>= `  s ) ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) )  <  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) )
145144ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  A. n  e.  ( ZZ>= `  s )
( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
146 oveq1 5867 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  -  j )  ->  (
n  +  1 )  =  ( ( m  -  j )  +  1 ) )
147146fveq2d 5531 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( m  -  j )  ->  ( ZZ>=
`  ( n  + 
1 ) )  =  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) )
148147sumeq1d 12176 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( m  -  j )  ->  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) )
149148fveq2d 5531 . . . . . . . . . . . . . . 15  |-  ( n  =  ( m  -  j )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) ) )
150149breq1d 4035 . . . . . . . . . . . . . 14  |-  ( n  =  ( m  -  j )  ->  (
( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <-> 
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `
 k ) )  <  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
151150rspcv 2882 . . . . . . . . . . . . 13  |-  ( ( m  -  j )  e.  ( ZZ>= `  s
)  ->  ( A. n  e.  ( ZZ>= `  s ) ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
152143, 145, 151sylc 56 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
153129, 152eqbrtrrd 4047 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
154125, 115, 153ltled 8969 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
155 lemul2a 9613 . . . . . . . . . 10  |-  ( ( ( ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR  /\  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )  e.  RR  /\  ( ( abs `  A )  e.  RR  /\  0  <_  ( abs `  A
) ) )  /\  ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  <_  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) )  ->  ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
156125, 115, 127, 154, 155syl31anc 1185 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
15746, 80, 116, 156fsumle 12259 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) ) )
15898recnd 8863 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  CC )
15993rpcnd 10394 . . . . . . . . . . 11  |-  ( ph  ->  ( E  /  2
)  e.  CC )
160159adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  CC )
161 peano2re 8987 . . . . . . . . . . . . 13  |-  ( sum_ j  e.  NN0  ( K `
 j )  e.  RR  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR )
162106, 161syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR )
163162recnd 8863 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  CC )
164163adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  CC )
165110rpne0d 10397 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  =/=  0 )
166165adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  =/=  0
)
167158, 160, 164, 166divassd 9573 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  =  ( sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
168 fveq2 5527 . . . . . . . . . . . . . . . . 17  |-  ( n  =  j  ->  ( K `  n )  =  ( K `  j ) )
169168cbvsumv 12171 . . . . . . . . . . . . . . . 16  |-  sum_ n  e.  NN0  ( K `  n )  =  sum_ j  e.  NN0  ( K `
 j )
170169oveq1i 5870 . . . . . . . . . . . . . . 15  |-  ( sum_ n  e.  NN0  ( K `  n )  +  1 )  =  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )
171170oveq2i 5871 . . . . . . . . . . . . . 14  |-  ( ( E  /  2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  =  ( ( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
172171, 113syl5eqel 2369 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  RR+ )
173172rpcnd 10394 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
174173adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  / 
( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
17576recnd 8863 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  CC )
17611, 96, 175syl2an 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  CC )
17746, 174, 176fsummulc1 12249 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( ( E  /  2 )  / 
( sum_ n  e.  NN0  ( K `  n )  +  1 ) ) )  =  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  (
( E  /  2
)  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) ) ) )
178171oveq2i 5871 . . . . . . . . . 10  |-  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( ( E  /  2 )  / 
( sum_ n  e.  NN0  ( K `  n )  +  1 ) ) )  =  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
179171oveq2i 5871 . . . . . . . . . . . 12  |-  ( ( abs `  A )  x.  ( ( E  /  2 )  / 
( sum_ n  e.  NN0  ( K `  n )  +  1 ) ) )  =  ( ( abs `  A )  x.  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
180179a1i 10 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  (
( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) ) )  =  ( ( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
181180sumeq2i 12174 . . . . . . . . . 10  |-  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  (
( E  /  2
)  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) ) )  = 
sum_ j  e.  ( 0 ... ( m  -  s ) ) ( ( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
182177, 178, 1813eqtr3g 2340 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )  =  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) ) )
183167, 182eqtrd 2317 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  =  sum_ j  e.  ( 0 ... ( m  -  s ) ) ( ( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
184157, 183breqtrrd 4051 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
185106adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  e.  RR )
186162adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR )
187100a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  e.  ZZ )
18896ssriv 3186 . . . . . . . . . . . . 13  |-  ( 0 ... ( m  -  s ) )  C_  NN0
189188a1i 10 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  C_  NN0 )
190103adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( K `  j )  =  ( abs `  A
) )
19176adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( abs `  A )  e.  RR )
192107adantlr 695 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  0  <_  ( abs `  A
) )
193105adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  seq  0
(  +  ,  K
)  e.  dom  ~~>  )
19430, 187, 46, 189, 190, 191, 192, 193isumless 12306 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( abs `  A
) )
195103sumeq2dv 12178 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
196195adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
197194, 196breqtrrd 4051 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( K `  j ) )
198106ltp1d 9689 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )
199198adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )
20098, 185, 186, 197, 199lelttrd 8976 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
20193rpregt0d 10398 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  e.  RR  /\  0  <  ( E  /  2 ) ) )
202201adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  e.  RR  /\  0  < 
( E  /  2
) ) )
203 ltmul1 9608 . . . . . . . . . 10  |-  ( (
sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  e.  RR  /\  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  ( ( E  /  2 )  e.  RR  /\  0  <  ( E  /  2
) ) )  -> 
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  <  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  <->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) ) )
20498, 186, 202, 203syl3anc 1182 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  <->  ( sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  <  ( ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  x.  ( E  /  2 ) ) ) )
205200, 204mpbid 201 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) )
206110rpregt0d 10398 . . . . . . . . . 10  |-  ( ph  ->  ( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
207206adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  < 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
208 ltdivmul 9630 . . . . . . . . 9  |-  ( ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  e.  RR  /\  ( E  /  2 )  e.  RR  /\  ( (
sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  < 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )  ->  ( (
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <  ( E  /  2 )  <->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) ) )
20999, 95, 207, 208syl3anc 1182 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <  ( E  /  2 )  <->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) ) )
210205, 209mpbird 223 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <  ( E  / 
2 ) )
21181, 112, 95, 184, 210lelttrd 8976 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <  ( E  /  2 ) )
212 mertens.13 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <_  sup ( T ,  RR ,  <  )  /\  ( T 
C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z
) ) )
213212simprd 449 . . . . . . . . . . 11  |-  ( ph  ->  ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z ) )
214 suprcl 9716 . . . . . . . . . . 11  |-  ( ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z
)  ->  sup ( T ,  RR ,  <  )  e.  RR )
215213, 214syl 15 . . . . . . . . . 10  |-  ( ph  ->  sup ( T ,  RR ,  <  )  e.  RR )
21694, 215remulcld 8865 . . . . . . . . 9  |-  ( ph  ->  ( ( E  / 
2 )  x.  sup ( T ,  RR ,  <  ) )  e.  RR )
217212simpld 445 . . . . . . . . . 10  |-  ( ph  ->  0  <_  sup ( T ,  RR ,  <  ) )
218215, 217ge0p1rpd 10418 . . . . . . . . 9  |-  ( ph  ->  ( sup ( T ,  RR ,  <  )  +  1 )  e.  RR+ )
219216, 218rerpdivcld 10419 . . . . . . . 8  |-  ( ph  ->  ( ( ( E  /  2 )  x. 
sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
220219adantr 451 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( E  /  2
)  x.  sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
2215nnrpd 10391 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  RR+ )
22293, 221rpdivcld 10409 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  RR+ )
223222, 218rpdivcld 10409 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR+ )
224223rpred 10392 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
225224, 215remulcld 8865 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  RR )
226225ad2antrr 706 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  RR )
227 simpll 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ph )
22890, 12syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  NN0 )
229227, 228, 76syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  e.  RR )
230224ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
231227, 228, 103syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  =  ( abs `  A
) )
232 elfzuz 10796 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  j  e.  ( ZZ>= `  ( (
m  -  s )  +  1 ) ) )
233 eluzle 10242 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  ( s  +  t )  <_  m )
234233adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  t )  <_  m )
2358nn0zd 10117 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  t  e.  ZZ )
236235adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  ZZ )
237236zred 10119 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  RR )
23852, 237, 51leaddsub2d 9376 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
s  +  t )  <_  m  <->  t  <_  ( m  -  s ) ) )
239234, 238mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  <_  ( m  -  s ) )
240 eluz 10243 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  ZZ  /\  ( m  -  s
)  e.  ZZ )  ->  ( ( m  -  s )  e.  ( ZZ>= `  t )  <->  t  <_  ( m  -  s ) ) )
241236, 69, 240syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  e.  ( ZZ>= `  t
)  <->  t  <_  (
m  -  s ) ) )
242239, 241mpbird 223 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ( ZZ>= `  t )
)
243 peano2uz 10274 . . . . . . . . . . . . . . 15  |-  ( ( m  -  s )  e.  ( ZZ>= `  t
)  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  t )
)
244242, 243syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  t )
)
245 uztrn 10246 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  ( ( m  -  s )  +  1 ) )  /\  (
( m  -  s
)  +  1 )  e.  ( ZZ>= `  t
) )  ->  j  e.  ( ZZ>= `  t )
)
246232, 244, 245syl2anr 464 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( ZZ>= `  t )
)
2477simprd 449 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) ) )
248247ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  A. m  e.  ( ZZ>= `  t )
( K `  m
)  <  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
249 fveq2 5527 . . . . . . . . . . . . . . 15  |-  ( m  =  j  ->  ( K `  m )  =  ( K `  j ) )
250249breq1d 4035 . . . . . . . . . . . . . 14  |-  ( m  =  j  ->  (
( K `  m
)  <  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  <->  ( K `  j )  <  (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
251250rspcv 2882 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  t
)  ->  ( A. m  e.  ( ZZ>= `  t ) ( K `
 m )  < 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  ->  ( K `  j )  <  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
252246, 248, 251sylc 56 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  <  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
253231, 252eqbrtrrd 4047 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  < 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
254229, 230, 253ltled 8969 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  <_ 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
255213ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z
) )
25651adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  m  e.  RR )
257 peano2zm 10064 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  (
s  -  1 )  e.  ZZ )
25856, 257syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( s  -  1 )  e.  ZZ )
259258zred 10119 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  -  1 )  e.  RR )
260259ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  RR )
261228nn0red 10021 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  RR )
26250zcnd 10120 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  CC )
26352recnd 8863 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  CC )
264 ax-1cn 8797 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
265264a1i 10 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  CC )
266262, 263, 265subsubd 9187 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  ( s  - 
1 ) )  =  ( ( m  -  s )  +  1 ) )
267266adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  =  ( ( m  -  s )  +  1 ) )
268 elfzle1 10801 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  (
( m  -  s
)  +  1 )  <_  j )
269268adantl 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  s
)  +  1 )  <_  j )
270267, 269eqbrtrd 4045 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  <_  j )
271256, 260, 261, 270subled 9377 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  <_  ( s  - 
1 ) )
27290, 16syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  NN0 )
273272, 30syl6eleq 2375 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( ZZ>= `  0
) )
274258ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  ZZ )
275 elfz5 10792 . . . . . . . . . . . . . . 15  |-  ( ( ( m  -  j
)  e.  ( ZZ>= ` 
0 )  /\  (
s  -  1 )  e.  ZZ )  -> 
( ( m  -  j )  e.  ( 0 ... ( s  -  1 ) )  <-> 
( m  -  j
)  <_  ( s  -  1 ) ) )
276273, 274, 275syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  j
)  e.  ( 0 ... ( s  - 
1 ) )  <->  ( m  -  j )  <_ 
( s  -  1 ) ) )
277271, 276mpbird 223 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( 0 ... ( s  -  1 ) ) )
278 simplll 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
27990, 19syldan 456 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
280279, 22sylan 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
281278, 280, 24syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
282281sumeq2dv 12178 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )
283282eqcomd 2290 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) )
284283fveq2d 5531 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) ) )
285149eqeq2d 2296 . . . . . . . . . . . . . 14  |-  ( n  =  ( m  -  j )  ->  (
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <-> 
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `
 k ) ) ) )
286285rspcev 2886 . . . . . . . . . . . . 13  |-  ( ( ( m  -  j
)  e.  ( 0 ... ( s  - 
1 ) )  /\  ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) ) )  ->  E. n  e.  (
0 ... ( s  - 
1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) ) )
287277, 284, 286syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  E. n  e.  ( 0 ... (
s  -  1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) )
288 fvex 5541 . . . . . . . . . . . . 13  |-  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  _V
289 eqeq1 2291 . . . . . . . . . . . . . 14  |-  ( z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  ->  ( z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <-> 
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) ) )
290289rexbidv 2566 . . . . . . . . . . . . 13  |-  ( z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  ->  ( E. n  e.  ( 0 ... (
s  -  1 ) ) z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) )  <->  E. n  e.  ( 0 ... (
s  -  1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) ) )
291 mertens.10 . . . . . . . . . . . . 13  |-  T  =  { z  |  E. n  e.  ( 0 ... ( s  - 
1 ) ) z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) }
292288, 290, 291elab2 2919 . . . . . . . . . . . 12  |-  ( ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  T  <->  E. n  e.  ( 0 ... ( s  - 
1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) ) )
293287, 292sylibr 203 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  T )
294 suprub 9717 . . . . . . . . . . 11  |-  ( ( ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z )  /\  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  T )  ->  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )
295255, 293, 294syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )
296227, 228, 126syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
29790, 78syldan 456 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
29836absge0d 11928 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
29990, 298syldan 456 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
300297, 299jca 518 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR  /\  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) ) )
301215ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sup ( T ,  RR ,  <  )  e.  RR )
302 lemul12a 9616 . . . . . . . . . . 11  |-  ( ( ( ( ( abs `  A )  e.  RR  /\  0  <_  ( abs `  A ) )  /\  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )  /\  ( ( ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  RR  /\  0  <_  ( abs ` 
sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  /\  sup ( T ,  RR ,  <  )  e.  RR ) )  ->  ( (
( abs `  A
)  <_  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  /\  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
303296, 230, 300, 301, 302syl22anc 1183 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( abs `  A
)  <_  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  /\  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
304254, 295, 303mp2and 660 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
30582, 91, 226, 304fsumle 12259 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
306225recnd 8863 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  CC )
307306adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  CC )
308 fsumconst 12254 . . . . . . . . . 10  |-  ( ( ( ( ( m  -  s )  +  1 ) ... m
)  e.  Fin  /\  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  CC )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m ) ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  =  ( (
# `  ( (
( m  -  s
)  +  1 ) ... m ) )  x.  ( ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
30982, 307, 308syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  =  ( ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  x.  ( ( ( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
310 1z 10055 . . . . . . . . . . . . . . 15  |-  1  e.  ZZ
311310a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  ZZ )
31256adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ZZ )
313 fzen 10813 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  (
m  -  s )  e.  ZZ )  -> 
( 1 ... s
)  ~~  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) ) )
314311, 312, 69, 313syl3anc 1182 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( 1  +  ( m  -  s
) ) ... (
s  +  ( m  -  s ) ) ) )
31569zcnd 10120 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  CC )
316 addcom 9000 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  ( m  -  s
)  e.  CC )  ->  ( 1  +  ( m  -  s
) )  =  ( ( m  -  s
)  +  1 ) )
317264, 315, 316sylancr 644 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1  +  ( m  -  s ) )  =  ( ( m  -  s )  +  1 ) )
318263, 262pncan3d 9162 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  ( m  -  s ) )  =  m )
319317, 318oveq12d 5878 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) )  =  ( ( ( m  -  s )  +  1 ) ... m
) )
320314, 319breqtrd 4049 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( ( m  -  s )  +  1 ) ... m
) )
321 fzfid 11037 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  e. 
Fin )
322 hashen 11348 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... s
)  e.  Fin  /\  ( ( ( m  -  s )  +  1 ) ... m
)  e.  Fin )  ->  ( ( # `  (
1 ... s ) )  =  ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  <->  ( 1 ... s )  ~~  (
( ( m  -  s )  +  1 ) ... m ) ) )
323321, 82, 322syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( # `
 ( 1 ... s ) )  =  ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  <->  ( 1 ... s )  ~~  (
( ( m  -  s )  +  1 ) ... m ) ) )
324320, 323mpbird 223 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( # `  (
1 ... s ) )  =  ( # `  (
( ( m  -  s )  +  1 ) ... m ) ) )
325 hashfz1 11347 . . . . . . . . . . . 12  |-  ( s  e.  NN0  ->  ( # `  ( 1 ... s
) )  =  s )
32647, 325syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( # `  (
1 ... s ) )  =  s )
327324, 326eqtr3d 2319 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  =  s )
328327oveq1d 5875 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( # `
 ( ( ( m  -  s )  +  1 ) ... m ) )  x.  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )  =  ( s  x.  ( ( ( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
329215recnd 8863 . . . . . . . . . . . 12  |-  ( ph  ->  sup ( T ,  RR ,  <  )  e.  CC )
330218rpcnne0d 10401 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( sup ( T ,  RR ,  <  )  +  1 )  e.  CC  /\  ( sup ( T ,  RR ,  <  )  +  1 )  =/=  0 ) )
331 div23 9445 . . . . . . . . . . . 12  |-  ( ( ( E  /  2
)  e.  CC  /\  sup ( T ,  RR ,  <  )  e.  CC  /\  ( ( sup ( T ,  RR ,  <  )  +  1 )  e.  CC  /\  ( sup ( T ,  RR ,  <  )  +  1 )  =/=  0 ) )  ->  ( (
( E  /  2
)  x.  sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( ( ( E  / 
2 )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
332159, 329, 330, 331syl3anc 1182 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  x. 
sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( ( ( E  /  2
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
33356zcnd 10120 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  CC )
334222rpcnd 10394 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  CC )
335 divass 9444 . . . . . . . . . . . . . 14  |-  ( ( s  e.  CC  /\  ( ( E  / 
2 )  /  s
)  e.  CC  /\  ( ( sup ( T ,  RR ,  <  )  +  1 )  e.  CC  /\  ( sup ( T ,  RR ,  <  )  +  1 )  =/=  0 ) )  ->  ( (
s  x.  ( ( E  /  2 )  /  s ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( s  x.  ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
336333, 334, 330, 335syl3anc 1182 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( s  x.  ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
3375nnne0d 9792 . . . . . . . . . . . . . . 15  |-  ( ph  ->  s  =/=  0 )
338159, 333, 337divcan2d 9540 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  x.  (
( E  /  2
)  /  s ) )  =  ( E  /  2 ) )
339338oveq1d 5875 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( ( E  /  2
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
340336, 339eqtr3d 2319 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  x.  (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )  =  ( ( E  / 
2 )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
341340oveq1d 5875 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )  x. 
sup ( T ,  RR ,  <  ) )  =  ( ( ( E  /  2 )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
342223rpcnd 10394 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  CC )
343333, 342, 329mulassd 8860 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )  x. 
sup ( T ,  RR ,  <  ) )  =  ( s  x.  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
344332, 341, 3433eqtr2rd 2324 . . . . . . . . . 10  |-  ( ph  ->  ( s  x.  (
( ( ( E  /  2 )  / 
s )  /