ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mertenslemi1 Unicode version

Theorem mertenslemi1 11514
Description: Lemma for mertensabs 11516. (Contributed by Mario Carneiro, 29-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
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.p  |-  ( ph  ->  P  e.  RR )
mertens.i12  |-  ( ph  ->  ( ps  /\  (
t  e.  NN0  /\  A. m  e.  ( ZZ>= `  t ) ( K `
 m )  < 
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) ) ) )
mertens.pge0  |-  ( ph  ->  0  <_  P )
mertens.pub  |-  ( ph  ->  A. w  e.  T  w  <_  P )
Assertion
Ref Expression
mertenslemi1  |-  ( 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    w, B    P, j, m, w
Allowed substitution hints:    ph( w, t, n, s)    ps( w, s)    A( z, w, j)    B( k)    P( y, z, t, k, n, s)    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 mertenslemi1
StepHypRef Expression
1 mertens.i12 . . . . . . 7  |-  ( ph  ->  ( ps  /\  (
t  e.  NN0  /\  A. m  e.  ( ZZ>= `  t ) ( K `
 m )  < 
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) ) ) )
21simpld 112 . . . . . 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 122 . . . . 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 112 . . . 4  |-  ( ph  ->  s  e.  NN )
65nnnn0d 9205 . . 3  |-  ( ph  ->  s  e.  NN0 )
71simprd 114 . . . 4  |-  ( ph  ->  ( t  e.  NN0  /\ 
A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) ) ) )
87simpld 112 . . 3  |-  ( ph  ->  t  e.  NN0 )
96, 8nn0addcld 9209 . 2  |-  ( ph  ->  ( s  +  t )  e.  NN0 )
10 0zd 9241 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  e.  ZZ )
11 eluzelz 9513 . . . . . . . 8  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  m  e.  ZZ )
1211adantl 277 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ZZ )
1310, 12fzfigd 10404 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... m )  e. 
Fin )
14 simpl 109 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ph )
15 elfznn0 10087 . . . . . . . 8  |-  ( j  e.  ( 0 ... m )  ->  j  e.  NN0 )
16 mertens.3 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN0 )  ->  A  e.  CC )
1714, 15, 16syl2an 289 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  A  e.  CC )
18 eqid 2177 . . . . . . . 8  |-  ( ZZ>= `  ( ( m  -  j )  +  1 ) )  =  (
ZZ>= `  ( ( m  -  j )  +  1 ) )
19 fznn0sub 10030 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... m )  ->  (
m  -  j )  e.  NN0 )
2019adantl 277 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
m  -  j )  e.  NN0 )
21 peano2nn0 9192 . . . . . . . . . 10  |-  ( ( m  -  j )  e.  NN0  ->  ( ( m  -  j )  +  1 )  e. 
NN0 )
2220, 21syl 14 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
2322nn0zd 9349 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
24 simplll 533 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
25 eluznn0 9575 . . . . . . . . . 10  |-  ( ( ( ( m  -  j )  +  1 )  e.  NN0  /\  k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) )  -> 
k  e.  NN0 )
2622, 25sylan 283 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
27 mertens.4 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  =  B )
2824, 26, 27syl2anc 411 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
29 mertens.5 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  B  e.  CC )
3024, 26, 29syl2anc 411 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  B  e.  CC )
31 mertens.8 . . . . . . . . . 10  |-  ( ph  ->  seq 0 (  +  ,  G )  e. 
dom 
~~>  )
3231ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq 0 (  +  ,  G )  e.  dom  ~~>  )
33 nn0uz 9538 . . . . . . . . . 10  |-  NN0  =  ( ZZ>= `  0 )
34 simpll 527 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ph )
3527, 29eqeltrd 2254 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3634, 35sylan 283 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3733, 22, 36iserex 11318 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (  seq 0 (  +  ,  G )  e.  dom  ~~>  <->  seq ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  ) )
3832, 37mpbid 147 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
3918, 23, 28, 30, 38isumcl 11404 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
4017, 39mulcld 7955 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  CC )
4113, 40fsumcl 11379 . . . . 5  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  CC )
4241abscld 11161 . . . 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 )
4340abscld 11161 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
4413, 43fsumrecl 11380 . . . 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 )
45 mertens.9 . . . . . 6  |-  ( ph  ->  E  e.  RR+ )
4645rpred 9670 . . . . 5  |-  ( ph  ->  E  e.  RR )
4746adantr 276 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  E  e.  RR )
4813, 40fsumabs 11444 . . . 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 ) ) )
495nnzd 9350 . . . . . . . . . 10  |-  ( ph  ->  s  e.  ZZ )
5049adantr 276 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ZZ )
5112, 50zsubcld 9356 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ZZ )
5210, 51fzfigd 10404 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  e. 
Fin )
536adantr 276 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  NN0 )
5453nn0ge0d 9208 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  <_  s )
5512zred 9351 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  RR )
5653nn0red 9206 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  RR )
5755, 56subge02d 8471 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0  <_  s  <->  ( m  -  s )  <_  m ) )
5854, 57mpbid 147 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  <_  m )
5953, 33eleqtrdi 2270 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( ZZ>= `  0 )
)
60 uzid 9518 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  s  e.  ( ZZ>= `  s )
)
6149, 60syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  s  e.  ( ZZ>= `  s ) )
62 uzaddcl 9562 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( ZZ>= `  s )  /\  t  e.  NN0 )  ->  (
s  +  t )  e.  ( ZZ>= `  s
) )
6361, 8, 62syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  +  t )  e.  ( ZZ>= `  s ) )
64 eqid 2177 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= `  s )  =  (
ZZ>= `  s )
6564uztrn2 9521 . . . . . . . . . . . . . . . 16  |-  ( ( ( s  +  t )  e.  ( ZZ>= `  s )  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
6663, 65sylan 283 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
67 elfzuzb 9992 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( 0 ... m )  <->  ( s  e.  ( ZZ>= `  0 )  /\  m  e.  ( ZZ>=
`  s ) ) )
6859, 66, 67sylanbrc 417 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( 0 ... m
) )
69 fznn0sub2 10101 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 0 ... m )  ->  (
m  -  s )  e.  ( 0 ... m ) )
7068, 69syl 14 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ( 0 ... m
) )
71 elfzelz 9998 . . . . . . . . . . . . 13  |-  ( ( m  -  s )  e.  ( 0 ... m )  ->  (
m  -  s )  e.  ZZ )
7270, 71syl 14 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ZZ )
73 eluz 9517 . . . . . . . . . . . 12  |-  ( ( ( m  -  s
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( m  e.  (
ZZ>= `  ( m  -  s ) )  <->  ( m  -  s )  <_  m ) )
7472, 12, 73syl2anc 411 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  e.  ( ZZ>= `  ( m  -  s ) )  <-> 
( m  -  s
)  <_  m )
)
7558, 74mpbird 167 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  ( m  -  s ) ) )
76 fzss2 10037 . . . . . . . . . 10  |-  ( m  e.  ( ZZ>= `  (
m  -  s ) )  ->  ( 0 ... ( m  -  s ) )  C_  ( 0 ... m
) )
7775, 76syl 14 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  C_  ( 0 ... m
) )
7877sselda 3155 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ( 0 ... m
) )
7916abscld 11161 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  RR )
8014, 15, 79syl2an 289 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  A )  e.  RR )
8139abscld 11161 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
8280, 81remulcld 7965 . . . . . . . 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 )
8378, 82syldan 282 . . . . . . 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 )
8452, 83fsumrecl 11380 . . . . . 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 )
8551peano2zd 9354 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ZZ )
8685, 12fzfigd 10404 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( m  -  s
)  +  1 ) ... m )  e. 
Fin )
87 elfznn0 10087 . . . . . . . . . . . . 13  |-  ( ( m  -  s )  e.  ( 0 ... m )  ->  (
m  -  s )  e.  NN0 )
8870, 87syl 14 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e. 
NN0 )
89 peano2nn0 9192 . . . . . . . . . . . 12  |-  ( ( m  -  s )  e.  NN0  ->  ( ( m  -  s )  +  1 )  e. 
NN0 )
9088, 89syl 14 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e. 
NN0 )
9190, 33eleqtrdi 2270 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  0 )
)
92 fzss1 10036 . . . . . . . . . 10  |-  ( ( ( m  -  s
)  +  1 )  e.  ( ZZ>= `  0
)  ->  ( (
( m  -  s
)  +  1 ) ... m )  C_  ( 0 ... m
) )
9391, 92syl 14 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( m  -  s
)  +  1 ) ... m )  C_  ( 0 ... m
) )
9493sselda 3155 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( 0 ... m
) )
9594, 82syldan 282 . . . . . . 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 )
9686, 95fsumrecl 11380 . . . . . 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 )
9745rphalfcld 9683 . . . . . . . 8  |-  ( ph  ->  ( E  /  2
)  e.  RR+ )
9897rpred 9670 . . . . . . 7  |-  ( ph  ->  ( E  /  2
)  e.  RR )
9998adantr 276 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  RR )
100 elfznn0 10087 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  NN0 )
10114, 100, 79syl2an 289 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  RR )
10252, 101fsumrecl 11380 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  RR )
103102, 99remulcld 7965 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  e.  RR )
104 0zd 9241 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ZZ )
105 eqidd 2178 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( K `  j ) )
106 mertens.2 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( abs `  A ) )
107106, 79eqeltrd 2254 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  e.  RR )
108 mertens.7 . . . . . . . . . . 11  |-  ( ph  ->  seq 0 (  +  ,  K )  e. 
dom 
~~>  )
10933, 104, 105, 107, 108isumrecl 11408 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  e.  RR )
11016absge0d 11164 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( abs `  A ) )
111110, 106breqtrrd 4028 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( K `  j ) )
11233, 104, 105, 107, 108, 111isumge0 11409 . . . . . . . . . 10  |-  ( ph  ->  0  <_  sum_ j  e. 
NN0  ( K `  j ) )
113109, 112ge0p1rpd 9701 . . . . . . . . 9  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR+ )
114113adantr 276 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR+ )
115103, 114rerpdivcld 9702 . . . . . . 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 )
11697, 113rpdivcld 9688 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR+ )
117116rpred 9670 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR )
118117ad2antrr 488 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )  e.  RR )
119101, 118remulcld 7965 . . . . . . . . 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 )
12078, 23syldan 282 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
121 simplll 533 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
12278, 22syldan 282 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
123122, 25sylan 283 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
124121, 123, 27syl2anc 411 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
125121, 123, 29syl2anc 411 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  B  e.  CC )
12678, 38syldan 282 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  seq ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
12718, 120, 124, 125, 126isumcl 11404 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
128127abscld 11161 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
12979, 110jca 306 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( ( abs `  A )  e.  RR  /\  0  <_ 
( abs `  A
) ) )
13014, 100, 129syl2an 289 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
131124sumeq2dv 11347 . . . . . . . . . . . . 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 )
132131fveq2d 5514 . . . . . . . . . . . 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 ) )
133 fvoveq1 5891 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( m  -  j )  ->  ( ZZ>=
`  ( n  + 
1 ) )  =  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) )
134133sumeq1d 11345 . . . . . . . . . . . . . . 15  |-  ( n  =  ( m  -  j )  ->  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) )
135134fveq2d 5514 . . . . . . . . . . . . . 14  |-  ( n  =  ( m  -  j )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) ) )
136135breq1d 4010 . . . . . . . . . . . . 13  |-  ( 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 ) ) ) )
1374simprd 114 . . . . . . . . . . . . . 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 ) ) )
138137ad2antrr 488 . . . . . . . . . . . . 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 ) ) )
139 elfzelz 9998 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  ZZ )
140139adantl 277 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ZZ )
141140zred 9351 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  RR )
14211ad2antlr 489 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  ZZ )
143142zred 9351 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  RR )
14449ad2antrr 488 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  ZZ )
145144zred 9351 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  RR )
146 elfzle2 10001 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  <_  ( m  -  s
) )
147146adantl 277 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  <_  ( m  -  s
) )
148141, 143, 145, 147lesubd 8483 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  <_  ( m  -  j
) )
149142, 140zsubcld 9356 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ZZ )
150 eluz 9517 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ZZ  /\  ( m  -  j
)  e.  ZZ )  ->  ( ( m  -  j )  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
151144, 149, 150syl2anc 411 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
152148, 151mpbird 167 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ( ZZ>= `  s
) )
153136, 138, 152rspcdva 2846 . . . . . . . . . . . 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 ) ) )
154132, 153eqbrtrrd 4024 . . . . . . . . . . 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 ) ) )
155128, 118, 154ltled 8053 . . . . . . . . . 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 ) ) )
156 lemul2a 8792 . . . . . . . . . 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 ) ) ) )
157128, 118, 130, 155, 156syl31anc 1241 . . . . . . . . 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 ) ) ) )
15852, 83, 119, 157fsumle 11442 . . . . . . . 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 ) ) ) )
159102recnd 7963 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  CC )
16097rpcnd 9672 . . . . . . . . . . 11  |-  ( ph  ->  ( E  /  2
)  e.  CC )
161160adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  CC )
162 peano2re 8070 . . . . . . . . . . . . 13  |-  ( sum_ j  e.  NN0  ( K `
 j )  e.  RR  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR )
163109, 162syl 14 . . . . . . . . . . . 12  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR )
164163recnd 7963 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  CC )
165164adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  CC )
166114rpap0d 9676 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) #  0 )
167159, 161, 165, 166divassapd 8759 . . . . . . . . 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 5510 . . . . . . . . . . . . . . . . 17  |-  ( n  =  j  ->  ( K `  n )  =  ( K `  j ) )
169168cbvsumv 11340 . . . . . . . . . . . . . . . 16  |-  sum_ n  e.  NN0  ( K `  n )  =  sum_ j  e.  NN0  ( K `
 j )
170169oveq1i 5878 . . . . . . . . . . . . . . 15  |-  ( sum_ n  e.  NN0  ( K `  n )  +  1 )  =  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )
171170oveq2i 5879 . . . . . . . . . . . . . 14  |-  ( ( E  /  2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  =  ( ( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
172171, 116eqeltrid 2264 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  RR+ )
173172rpcnd 9672 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
174173adantr 276 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  / 
( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
17579recnd 7963 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  CC )
17614, 100, 175syl2an 289 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  CC )
17752, 174, 176fsummulc1 11428 . . . . . . . . . 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 5879 . . . . . . . . . 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 5879 . . . . . . . . . . . 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 9 . . . . . . . . . . 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 11343 . . . . . . . . . 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 2233 . . . . . . . . 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 2210 . . . . . . . 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 ) ) ) )
184158, 183breqtrrd 4028 . . . . . . 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 ) ) )
185109adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  e.  RR )
186163adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR )
187 fz0ssnn0 10089 . . . . . . . . . . . . 13  |-  ( 0 ... ( m  -  s ) )  C_  NN0
188187a1i 9 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  C_  NN0 )
189106adantlr 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( K `  j )  =  ( abs `  A
) )
190 nn0z 9249 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN0  ->  j  e.  ZZ )
191190adantl 277 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  j  e.  ZZ )
192 0zd 9241 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  0  e.  ZZ )
19351adantr 276 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  (
m  -  s )  e.  ZZ )
194 fzdcel 10013 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ZZ  /\  0  e.  ZZ  /\  (
m  -  s )  e.  ZZ )  -> DECID  j  e.  ( 0 ... (
m  -  s ) ) )
195191, 192, 193, 194syl3anc 1238 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  -> DECID  j  e.  (
0 ... ( m  -  s ) ) )
196195ralrimiva 2550 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  A. j  e.  NN0 DECID  j  e.  ( 0 ... ( m  -  s ) ) )
19779adantlr 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( abs `  A )  e.  RR )
198110adantlr 477 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  0  <_  ( abs `  A
) )
199108adantr 276 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  seq 0
(  +  ,  K
)  e.  dom  ~~>  )
20033, 10, 52, 188, 189, 196, 197, 198, 199isumlessdc 11475 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( abs `  A
) )
201106sumeq2dv 11347 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
202201adantr 276 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
203200, 202breqtrrd 4028 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( K `  j ) )
204109ltp1d 8863 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )
205204adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )
206102, 185, 186, 203, 205lelttrd 8059 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
20797rpregt0d 9677 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  e.  RR  /\  0  <  ( E  /  2 ) ) )
208207adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  e.  RR  /\  0  < 
( E  /  2
) ) )
209 ltmul1 8526 . . . . . . . . . 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 ) ) ) )
210102, 186, 208, 209syl3anc 1238 . . . . . . . . 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 ) ) ) )
211206, 210mpbid 147 . . . . . . . 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 ) ) )
212113rpregt0d 9677 . . . . . . . . . 10  |-  ( ph  ->  ( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
213212adantr 276 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  < 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
214 ltdivmul 8809 . . . . . . . . 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 ) ) ) )
215103, 99, 213, 214syl3anc 1238 . . . . . . . 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 ) ) ) )
216211, 215mpbird 167 . . . . . . 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 ) )
21784, 115, 99, 184, 216lelttrd 8059 . . . . . 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 ) )
218 mertens.p . . . . . . . . . 10  |-  ( ph  ->  P  e.  RR )
21998, 218remulcld 7965 . . . . . . . . 9  |-  ( ph  ->  ( ( E  / 
2 )  x.  P
)  e.  RR )
220 mertens.pge0 . . . . . . . . . 10  |-  ( ph  ->  0  <_  P )
221218, 220ge0p1rpd 9701 . . . . . . . . 9  |-  ( ph  ->  ( P  +  1 )  e.  RR+ )
222219, 221rerpdivcld 9702 . . . . . . . 8  |-  ( ph  ->  ( ( ( E  /  2 )  x.  P )  /  ( P  +  1 ) )  e.  RR )
223222adantr 276 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( E  /  2
)  x.  P )  /  ( P  + 
1 ) )  e.  RR )
2245nnrpd 9668 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  RR+ )
22597, 224rpdivcld 9688 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  RR+ )
226225, 221rpdivcld 9688 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  e.  RR+ )
227226rpred 9670 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  e.  RR )
228227, 218remulcld 7965 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) )  x.  P
)  e.  RR )
229228ad2antrr 488 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  x.  P )  e.  RR )
230 simpll 527 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ph )
23194, 15syl 14 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  NN0 )
232230, 231, 79syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  e.  RR )
233227ad2antrr 488 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) )  e.  RR )
234230, 231, 106syl2anc 411 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  =  ( abs `  A
) )
235 fveq2 5510 . . . . . . . . . . . . . 14  |-  ( m  =  j  ->  ( K `  m )  =  ( K `  j ) )
236235breq1d 4010 . . . . . . . . . . . . 13  |-  ( m  =  j  ->  (
( K `  m
)  <  ( (
( E  /  2
)  /  s )  /  ( P  + 
1 ) )  <->  ( K `  j )  <  (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) ) ) )
2377simprd 114 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) ) )
238237ad2antrr 488 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  A. m  e.  ( ZZ>= `  t )
( K `  m
)  <  ( (
( E  /  2
)  /  s )  /  ( P  + 
1 ) ) )
239 elfzuz 9994 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  j  e.  ( ZZ>= `  ( (
m  -  s )  +  1 ) ) )
240 eluzle 9516 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  ( s  +  t )  <_  m )
241240adantl 277 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  t )  <_  m )
2428nn0zd 9349 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  t  e.  ZZ )
243242adantr 276 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  ZZ )
244243zred 9351 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  RR )
24556, 244, 55leaddsub2d 8481 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
s  +  t )  <_  m  <->  t  <_  ( m  -  s ) ) )
246241, 245mpbid 147 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  <_  ( m  -  s ) )
247 eluz 9517 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  ZZ  /\  ( m  -  s
)  e.  ZZ )  ->  ( ( m  -  s )  e.  ( ZZ>= `  t )  <->  t  <_  ( m  -  s ) ) )
248243, 72, 247syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  e.  ( ZZ>= `  t
)  <->  t  <_  (
m  -  s ) ) )
249246, 248mpbird 167 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ( ZZ>= `  t )
)
250 peano2uz 9559 . . . . . . . . . . . . . . 15  |-  ( ( m  -  s )  e.  ( ZZ>= `  t
)  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  t )
)
251249, 250syl 14 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  t )
)
252 uztrn 9520 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  ( ( m  -  s )  +  1 ) )  /\  (
( m  -  s
)  +  1 )  e.  ( ZZ>= `  t
) )  ->  j  e.  ( ZZ>= `  t )
)
253239, 251, 252syl2anr 290 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( ZZ>= `  t )
)
254236, 238, 253rspcdva 2846 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  <  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )
255234, 254eqbrtrrd 4024 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  < 
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )
256232, 233, 255ltled 8053 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  <_ 
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )
257 breq1 4003 . . . . . . . . . . 11  |-  ( w  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  ->  ( w  <_  P 
<->  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  P ) )
258 mertens.pub . . . . . . . . . . . 12  |-  ( ph  ->  A. w  e.  T  w  <_  P )
259258ad2antrr 488 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  A. w  e.  T  w  <_  P )
26055adantr 276 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  m  e.  RR )
261 peano2zm 9267 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  (
s  -  1 )  e.  ZZ )
26249, 261syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( s  -  1 )  e.  ZZ )
263262zred 9351 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  -  1 )  e.  RR )
264263ad2antrr 488 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  RR )
265231nn0red 9206 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  RR )
26612zcnd 9352 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  CC )
26756recnd 7963 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  CC )
268 1cnd 7951 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  CC )
269266, 267, 268subsubd 8273 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  ( s  - 
1 ) )  =  ( ( m  -  s )  +  1 ) )
270269adantr 276 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  =  ( ( m  -  s )  +  1 ) )
271 elfzle1 10000 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  (
( m  -  s
)  +  1 )  <_  j )
272271adantl 277 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  s
)  +  1 )  <_  j )
273270, 272eqbrtrd 4022 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  <_  j )
274260, 264, 265, 273subled 8482 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  <_  ( s  - 
1 ) )
27594, 19syl 14 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  NN0 )
276275, 33eleqtrdi 2270 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( ZZ>= `  0
) )
277262ad2antrr 488 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  ZZ )
278 elfz5 9990 . . . . . . . . . . . . . . 15  |-  ( ( ( m  -  j
)  e.  ( ZZ>= ` 
0 )  /\  (
s  -  1 )  e.  ZZ )  -> 
( ( m  -  j )  e.  ( 0 ... ( s  -  1 ) )  <-> 
( m  -  j
)  <_  ( s  -  1 ) ) )
279276, 277, 278syl2anc 411 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  j
)  e.  ( 0 ... ( s  - 
1 ) )  <->  ( m  -  j )  <_ 
( s  -  1 ) ) )
280274, 279mpbird 167 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( 0 ... ( s  -  1 ) ) )
281 simplll 533 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
28294, 22syldan 282 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
283282, 25sylan 283 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
284281, 283, 27syl2anc 411 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
285284sumeq2dv 11347 . . . . . . . . . . . . . . 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 )
286285eqcomd 2183 . . . . . . . . . . . . . 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
) )
287286fveq2d 5514 . . . . . . . . . . . . 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 ) ) )
288135rspceeqv 2859 . . . . . . . . . . . . 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
) ) )
289280, 287, 288syl2anc 411 . . . . . . . . . . . 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 ) ) )
29094, 39syldan 282 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
291290abscld 11161 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
292 eqeq1 2184 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
293292rexbidv 2478 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
294 mertens.10 . . . . . . . . . . . . . 14  |-  T  =  { z  |  E. n  e.  ( 0 ... ( s  - 
1 ) ) z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) }
295293, 294elab2g 2884 . . . . . . . . . . . . 13  |-  ( ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  RR  ->  ( ( 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 ) ) ) )
296291, 295syl 14 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( 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 ) ) ) )
297289, 296mpbird 167 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  T )
298257, 259, 297rspcdva 2846 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  P )
299230, 231, 129syl2anc 411 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
30094, 81syldan 282 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
30139absge0d 11164 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
30294, 301syldan 282 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
303300, 302jca 306 . . . . . . . . . . 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 ) ) )
304218ad2antrr 488 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  P  e.  RR )
305 lemul12a 8795 . . . . . . . . . . 11  |-  ( ( ( ( ( abs `  A )  e.  RR  /\  0  <_  ( abs `  A ) )  /\  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  e.  RR )  /\  ( ( ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  RR  /\  0  <_  ( abs ` 
sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  /\  P  e.  RR ) )  -> 
( ( ( abs `  A )  <_  (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) )  /\  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  P )  -> 
( ( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  x.  P ) ) )
306299, 233, 303, 304, 305syl22anc 1239 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( abs `  A
)  <_  ( (
( E  /  2
)  /  s )  /  ( P  + 
1 ) )  /\  ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  <_  P
)  ->  ( ( abs `  A )  x.  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  ( (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) )  x.  P ) ) )
307256, 298, 306mp2and 433 . . . . . . . . 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 )  /  ( P  +  1 ) )  x.  P ) )
30886, 95, 229, 307fsumle 11442 . . . . . . . 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 )  /  ( P  + 
1 ) )  x.  P ) )
309228recnd 7963 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) )  x.  P
)  e.  CC )
310309adantr 276 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) )  x.  P )  e.  CC )
311 fsumconst 11433 . . . . . . . . . 10  |-  ( ( ( ( ( m  -  s )  +  1 ) ... m
)  e.  Fin  /\  ( ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) )  x.  P
)  e.  CC )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m ) ( ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) )  x.  P
)  =  ( ( `  ( ( ( m  -  s )  +  1 ) ... m
) )  x.  (
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  x.  P ) ) )
31286, 310, 311syl2anc 411 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( ( ( E  /  2
)  /  s )  /  ( P  + 
1 ) )  x.  P )  =  ( ( `  ( (
( m  -  s
)  +  1 ) ... m ) )  x.  ( ( ( ( E  /  2
)  /  s )  /  ( P  + 
1 ) )  x.  P ) ) )
313 1zzd 9256 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  ZZ )
314 fzen 10016 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  (
m  -  s )  e.  ZZ )  -> 
( 1 ... s
)  ~~  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) ) )
315313, 50, 72, 314syl3anc 1238 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( 1  +  ( m  -  s
) ) ... (
s  +  ( m  -  s ) ) ) )
316 ax-1cn 7882 . . . . . . . . . . . . . . 15  |-  1  e.  CC
31772zcnd 9352 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  CC )
318 addcom 8071 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  ( m  -  s
)  e.  CC )  ->  ( 1  +  ( m  -  s
) )  =  ( ( m  -  s
)  +  1 ) )
319316, 317, 318sylancr 414 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1  +  ( m  -  s ) )  =  ( ( m  -  s )  +  1 ) )
320267, 266pncan3d 8248 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  ( m  -  s ) )  =  m )
321319, 320oveq12d 5886 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) )  =  ( ( ( m  -  s )  +  1 ) ... m
) )
322315, 321breqtrd 4026 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( ( m  -  s )  +  1 ) ... m
) )
323313, 50fzfigd 10404 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  e. 
Fin )
324 hashen 10735 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... s
)  e.  Fin  /\  ( ( ( m  -  s )  +  1 ) ... m
)  e.  Fin )  ->  ( ( `  (
1 ... s ) )  =  ( `  (
( ( m  -  s )  +  1 ) ... m ) )  <->  ( 1 ... s )  ~~  (
( ( m  -  s )  +  1 ) ... m ) ) )
325323, 86, 324syl2anc 411 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( `  ( 1 ... s
) )  =  ( `  ( ( ( m  -  s )  +  1 ) ... m
) )  <->  ( 1 ... s )  ~~  ( ( ( m  -  s )  +  1 ) ... m
) ) )
326322, 325mpbird 167 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( `  (
1 ... s ) )  =  ( `  (
( ( m  -  s )  +  1 ) ... m ) ) )
327 hashfz1 10734 . . . . . . . . . . . 12  |-  ( s  e.  NN0  ->  ( `  (
1 ... s ) )  =  s )
32853, 327syl 14 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( `  (
1 ... s ) )  =  s )
329326, 328eqtr3d 2212 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( `  (
( ( m  -  s )  +  1 ) ... m ) )  =  s )
330329oveq1d 5883 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( `  ( ( ( m  -  s )  +  1 ) ... m
) )  x.  (
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  x.  P ) )  =  ( s  x.  ( ( ( ( E  /  2
)  /  s )  /  ( P  + 
1 ) )  x.  P ) ) )
331218recnd 7963 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  CC )
332221rpcnd 9672 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  +  1 )  e.  CC )
333221rpap0d 9676 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  +  1 ) #  0 )
334160, 331, 332, 333div23apd 8761 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  x.  P )  /  ( P  +  1 ) )  =  ( ( ( E  /  2
)  /  ( P  +  1 ) )  x.  P ) )
33549zcnd 9352 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  CC )
336225rpcnd 9672 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  CC )
337335, 336, 332, 333divassapd 8759 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( P  +  1 ) )  =  ( s  x.  ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) ) ) )
3385nnap0d 8941 . . . . . . . . . . . . . . 15  |-  ( ph  ->  s #  0 )
339160, 335, 338divcanap2d 8725 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  x.  (
( E  /  2
)  /  s ) )  =  ( E  /  2 ) )
340339oveq1d 5883 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( P  +  1 ) )  =  ( ( E  /  2 )  /  ( P  + 
1 ) ) )
341337, 340eqtr3d 2212 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  x.  (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) ) )  =  ( ( E  /  2 )  /  ( P  + 
1 ) ) )
342341oveq1d 5883 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )  x.  P
)  =  ( ( ( E  /  2
)  /  ( P  +  1 ) )  x.  P ) )
343226rpcnd 9672 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  e.  CC )
344335, 343, 331mulassd 7958 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )  x.  P
)  =  ( s  x.  ( ( ( ( E  /  2
)  /  s )  /  ( P  + 
1 ) )  x.  P ) ) )
345334, 342, 3443eqtr2rd 2217 . . . . . . . . . 10  |-  ( ph  ->  ( s  x.  (
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  x.  P ) )  =  ( ( ( E  /  2
)  x.  P )  /  ( P  + 
1 ) ) )
346345adantr 276 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  x.  ( ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) )  x.  P
) )  =  ( ( ( E  / 
2 )  x.  P
)  /  ( P  +  1 ) ) )
347312, 330, 3463eqtrd 2214 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( ( ( E  /  2
)  /  s )  /  ( P  + 
1 ) )  x.  P )  =  ( ( ( E  / 
2 )  x.  P
)  /  ( P  +  1 ) ) )
348308, 347breqtrd 4026 . . . . . . 7  |-  ( (
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  / 
2 )  x.  P
)  /  ( P  +  1 ) ) )
349 peano2re 8070 . . . . . . . . . . 11  |-  ( P  e.  RR  ->  ( P  +  1 )  e.  RR )
350218, 349syl 14 . . . . . . . . . 10  |-  ( ph  ->  ( P  +  1 )  e.  RR )
351218ltp1d 8863 . . . . . . . . . 10  |-  ( ph  ->  P  <  ( P  +  1 ) )
352218, 350, 97, 351ltmul2dd 9727 . . . . . . . . 9  |-  ( ph  ->  ( ( E  / 
2 )  x.  P
)  <  ( ( E  /  2 )  x.  ( P  +  1 ) ) )
353219, 98, 221ltdivmul2d 9723 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( E  /  2 )  x.  P )  / 
( P  +  1 ) )  <  ( E  /  2 )  <->  ( ( E  /  2 )  x.  P )  <  (
( E  /  2
)  x.  ( P  +  1 ) ) ) )
354352, 353mpbird 167 . . . . . . . 8  |-  ( ph  ->  ( ( ( E  /  2 )  x.  P )  /  ( P  +  1 ) )  <  ( E  /  2 ) )
355354adantr 276 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( E  /  2
)  x.  P )  /  ( P  + 
1 ) )  < 
( E  /  2
) )
35696, 223, 99, 348, 355lelttrd 8059 . . . . . 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  /  2 ) )
35784, 96, 99, 99, 217, 356lt2addd 8501 . . . . 5  |-  ( (
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.  ( (
( m  -  s
)  +  1 ) ... m ) ( ( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) ) )  < 
( ( E  / 
2 )  +  ( E  /  2 ) ) )
35817, 39absmuld 11174 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  =  ( ( abs `  A )  x.  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) ) )
359358sumeq2dv 11347 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.