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

Theorem mertenslemi1 11259
Description: Lemma for mertensabs 11261. (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 111 . . . . . 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 121 . . . . 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 111 . . . 4  |-  ( ph  ->  s  e.  NN )
65nnnn0d 8988 . . 3  |-  ( ph  ->  s  e.  NN0 )
71simprd 113 . . . 4  |-  ( ph  ->  ( t  e.  NN0  /\ 
A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) ) ) )
87simpld 111 . . 3  |-  ( ph  ->  t  e.  NN0 )
96, 8nn0addcld 8992 . 2  |-  ( ph  ->  ( s  +  t )  e.  NN0 )
10 0zd 9024 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  e.  ZZ )
11 eluzelz 9291 . . . . . . . 8  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  m  e.  ZZ )
1211adantl 275 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ZZ )
1310, 12fzfigd 10159 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... m )  e. 
Fin )
14 simpl 108 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ph )
15 elfznn0 9849 . . . . . . . 8  |-  ( j  e.  ( 0 ... m )  ->  j  e.  NN0 )
16 mertens.3 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN0 )  ->  A  e.  CC )
1714, 15, 16syl2an 287 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  A  e.  CC )
18 eqid 2117 . . . . . . . 8  |-  ( ZZ>= `  ( ( m  -  j )  +  1 ) )  =  (
ZZ>= `  ( ( m  -  j )  +  1 ) )
19 fznn0sub 9792 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... m )  ->  (
m  -  j )  e.  NN0 )
2019adantl 275 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
m  -  j )  e.  NN0 )
21 peano2nn0 8975 . . . . . . . . . 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 9129 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
24 simplll 507 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
25 eluznn0 9349 . . . . . . . . . 10  |-  ( ( ( ( m  -  j )  +  1 )  e.  NN0  /\  k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) )  -> 
k  e.  NN0 )
2622, 25sylan 281 . . . . . . . . 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 408 . . . . . . . 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 408 . . . . . . . 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 479 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq 0 (  +  ,  G )  e.  dom  ~~>  )
33 nn0uz 9316 . . . . . . . . . 10  |-  NN0  =  ( ZZ>= `  0 )
34 simpll 503 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ph )
3527, 29eqeltrd 2194 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3634, 35sylan 281 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3733, 22, 36iserex 11063 . . . . . . . . 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 146 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
3918, 23, 28, 30, 38isumcl 11149 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
4017, 39mulcld 7754 . . . . . 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 11124 . . . . 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 10908 . . . 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 10908 . . . . 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 11125 . . . 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 9438 . . . . 5  |-  ( ph  ->  E  e.  RR )
4746adantr 274 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  E  e.  RR )
4813, 40fsumabs 11189 . . . 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 9130 . . . . . . . . . 10  |-  ( ph  ->  s  e.  ZZ )
5049adantr 274 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ZZ )
5112, 50zsubcld 9136 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ZZ )
5210, 51fzfigd 10159 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  e. 
Fin )
536adantr 274 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  NN0 )
5453nn0ge0d 8991 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  <_  s )
5512zred 9131 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  RR )
5653nn0red 8989 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  RR )
5755, 56subge02d 8266 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0  <_  s  <->  ( m  -  s )  <_  m ) )
5854, 57mpbid 146 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  <_  m )
5953, 33eleqtrdi 2210 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( ZZ>= `  0 )
)
60 uzid 9296 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  s  e.  ( ZZ>= `  s )
)
6149, 60syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  s  e.  ( ZZ>= `  s ) )
62 uzaddcl 9337 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( ZZ>= `  s )  /\  t  e.  NN0 )  ->  (
s  +  t )  e.  ( ZZ>= `  s
) )
6361, 8, 62syl2anc 408 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  +  t )  e.  ( ZZ>= `  s ) )
64 eqid 2117 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= `  s )  =  (
ZZ>= `  s )
6564uztrn2 9299 . . . . . . . . . . . . . . . 16  |-  ( ( ( s  +  t )  e.  ( ZZ>= `  s )  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
6663, 65sylan 281 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
67 elfzuzb 9755 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( 0 ... m )  <->  ( s  e.  ( ZZ>= `  0 )  /\  m  e.  ( ZZ>=
`  s ) ) )
6859, 66, 67sylanbrc 413 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( 0 ... m
) )
69 fznn0sub2 9860 . . . . . . . . . . . . . 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 9761 . . . . . . . . . . . . 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 9295 . . . . . . . . . . . 12  |-  ( ( ( m  -  s
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( m  e.  (
ZZ>= `  ( m  -  s ) )  <->  ( m  -  s )  <_  m ) )
7472, 12, 73syl2anc 408 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  e.  ( ZZ>= `  ( m  -  s ) )  <-> 
( m  -  s
)  <_  m )
)
7558, 74mpbird 166 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  ( m  -  s ) ) )
76 fzss2 9799 . . . . . . . . . 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 3067 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ( 0 ... m
) )
7916abscld 10908 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  RR )
8014, 15, 79syl2an 287 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  A )  e.  RR )
8139abscld 10908 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
8280, 81remulcld 7764 . . . . . . . 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 280 . . . . . . 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 11125 . . . . . 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 9134 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ZZ )
8685, 12fzfigd 10159 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( m  -  s
)  +  1 ) ... m )  e. 
Fin )
87 elfznn0 9849 . . . . . . . . . . . . 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 8975 . . . . . . . . . . . 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 2210 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  0 )
)
92 fzss1 9798 . . . . . . . . . 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 3067 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( 0 ... m
) )
9594, 82syldan 280 . . . . . . 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 11125 . . . . . 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 9451 . . . . . . . 8  |-  ( ph  ->  ( E  /  2
)  e.  RR+ )
9897rpred 9438 . . . . . . 7  |-  ( ph  ->  ( E  /  2
)  e.  RR )
9998adantr 274 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  RR )
100 elfznn0 9849 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  NN0 )
10114, 100, 79syl2an 287 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  RR )
10252, 101fsumrecl 11125 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  RR )
103102, 99remulcld 7764 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  e.  RR )
104 0zd 9024 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ZZ )
105 eqidd 2118 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( K `  j ) )
106 mertens.2 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( abs `  A ) )
107106, 79eqeltrd 2194 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  e.  RR )
108 mertens.7 . . . . . . . . . . 11  |-  ( ph  ->  seq 0 (  +  ,  K )  e. 
dom 
~~>  )
10933, 104, 105, 107, 108isumrecl 11153 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  e.  RR )
11016absge0d 10911 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( abs `  A ) )
111110, 106breqtrrd 3926 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( K `  j ) )
11233, 104, 105, 107, 108, 111isumge0 11154 . . . . . . . . . 10  |-  ( ph  ->  0  <_  sum_ j  e. 
NN0  ( K `  j ) )
113109, 112ge0p1rpd 9469 . . . . . . . . 9  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR+ )
114113adantr 274 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR+ )
115103, 114rerpdivcld 9470 . . . . . . 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 9456 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR+ )
117116rpred 9438 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR )
118117ad2antrr 479 . . . . . . . . . 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 7764 . . . . . . . . 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 280 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
121 simplll 507 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
12278, 22syldan 280 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
123122, 25sylan 281 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
124121, 123, 27syl2anc 408 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
125121, 123, 29syl2anc 408 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  B  e.  CC )
12678, 38syldan 280 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  seq ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
12718, 120, 124, 125, 126isumcl 11149 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
128127abscld 10908 . . . . . . . . . 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 304 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( ( abs `  A )  e.  RR  /\  0  <_ 
( abs `  A
) ) )
13014, 100, 129syl2an 287 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
131124sumeq2dv 11092 . . . . . . . . . . . . 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 5393 . . . . . . . . . . . 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 5765 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( m  -  j )  ->  ( ZZ>=
`  ( n  + 
1 ) )  =  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) )
134133sumeq1d 11090 . . . . . . . . . . . . . . 15  |-  ( n  =  ( m  -  j )  ->  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) )
135134fveq2d 5393 . . . . . . . . . . . . . 14  |-  ( n  =  ( m  -  j )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) ) )
136135breq1d 3909 . . . . . . . . . . . . 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 113 . . . . . . . . . . . . . 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 479 . . . . . . . . . . . . 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 9761 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  ZZ )
140139adantl 275 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ZZ )
141140zred 9131 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  RR )
14211ad2antlr 480 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  ZZ )
143142zred 9131 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  RR )
14449ad2antrr 479 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  ZZ )
145144zred 9131 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  RR )
146 elfzle2 9763 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  <_  ( m  -  s
) )
147146adantl 275 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  <_  ( m  -  s
) )
148141, 143, 145, 147lesubd 8278 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  <_  ( m  -  j
) )
149142, 140zsubcld 9136 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ZZ )
150 eluz 9295 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ZZ  /\  ( m  -  j
)  e.  ZZ )  ->  ( ( m  -  j )  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
151144, 149, 150syl2anc 408 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
152148, 151mpbird 166 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ( ZZ>= `  s
) )
153136, 138, 152rspcdva 2768 . . . . . . . . . . . 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 3922 . . . . . . . . . . 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 7849 . . . . . . . . . 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 8581 . . . . . . . . . 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 1204 . . . . . . . . 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 11187 . . . . . . . 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 7762 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  CC )
16097rpcnd 9440 . . . . . . . . . . 11  |-  ( ph  ->  ( E  /  2
)  e.  CC )
161160adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  CC )
162 peano2re 7866 . . . . . . . . . . . . 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 7762 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  CC )
165164adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  CC )
166114rpap0d 9444 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) #  0 )
167159, 161, 165, 166divassapd 8553 . . . . . . . . 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 5389 . . . . . . . . . . . . . . . . 17  |-  ( n  =  j  ->  ( K `  n )  =  ( K `  j ) )
169168cbvsumv 11085 . . . . . . . . . . . . . . . 16  |-  sum_ n  e.  NN0  ( K `  n )  =  sum_ j  e.  NN0  ( K `
 j )
170169oveq1i 5752 . . . . . . . . . . . . . . 15  |-  ( sum_ n  e.  NN0  ( K `  n )  +  1 )  =  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )
171170oveq2i 5753 . . . . . . . . . . . . . 14  |-  ( ( E  /  2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  =  ( ( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
172171, 116eqeltrid 2204 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  RR+ )
173172rpcnd 9440 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
174173adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  / 
( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
17579recnd 7762 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  CC )
17614, 100, 175syl2an 287 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  CC )
17752, 174, 176fsummulc1 11173 . . . . . . . . . 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 5753 . . . . . . . . . 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 5753 . . . . . . . . . . . 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 11088 . . . . . . . . . 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 2173 . . . . . . . . 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 2150 . . . . . . . 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 3926 . . . . . . 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 274 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  e.  RR )
186163adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR )
187 fz0ssnn0 9851 . . . . . . . . . . . . 13  |-  ( 0 ... ( m  -  s ) )  C_  NN0
188187a1i 9 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  C_  NN0 )
189106adantlr 468 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( K `  j )  =  ( abs `  A
) )
190 nn0z 9032 . . . . . . . . . . . . . . 15  |-  ( j  e.  NN0  ->  j  e.  ZZ )
191190adantl 275 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  j  e.  ZZ )
192 0zd 9024 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  0  e.  ZZ )
19351adantr 274 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  (
m  -  s )  e.  ZZ )
194 fzdcel 9775 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ZZ  /\  0  e.  ZZ  /\  (
m  -  s )  e.  ZZ )  -> DECID  j  e.  ( 0 ... (
m  -  s ) ) )
195191, 192, 193, 194syl3anc 1201 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  -> DECID  j  e.  (
0 ... ( m  -  s ) ) )
196195ralrimiva 2482 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  A. j  e.  NN0 DECID  j  e.  ( 0 ... ( m  -  s ) ) )
19779adantlr 468 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( abs `  A )  e.  RR )
198110adantlr 468 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  0  <_  ( abs `  A
) )
199108adantr 274 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  seq 0
(  +  ,  K
)  e.  dom  ~~>  )
20033, 10, 52, 188, 189, 196, 197, 198, 199isumlessdc 11220 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( abs `  A
) )
201106sumeq2dv 11092 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
202201adantr 274 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
203200, 202breqtrrd 3926 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( K `  j ) )
204109ltp1d 8652 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )
205204adantr 274 . . . . . . . . . 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 7855 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
20797rpregt0d 9445 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  e.  RR  /\  0  <  ( E  /  2 ) ) )
208207adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  e.  RR  /\  0  < 
( E  /  2
) ) )
209 ltmul1 8321 . . . . . . . . . 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 1201 . . . . . . . . 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 146 . . . . . . . 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 9445 . . . . . . . . . 10  |-  ( ph  ->  ( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
213212adantr 274 . . . . . . . . 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 8598 . . . . . . . . 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 1201 . . . . . . . 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 166 . . . . . . 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 7855 . . . . . 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 7764 . . . . . . . . 9  |-  ( ph  ->  ( ( E  / 
2 )  x.  P
)  e.  RR )
220 mertens.pge0 . . . . . . . . . 10  |-  ( ph  ->  0  <_  P )
221218, 220ge0p1rpd 9469 . . . . . . . . 9  |-  ( ph  ->  ( P  +  1 )  e.  RR+ )
222219, 221rerpdivcld 9470 . . . . . . . 8  |-  ( ph  ->  ( ( ( E  /  2 )  x.  P )  /  ( P  +  1 ) )  e.  RR )
223222adantr 274 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( E  /  2
)  x.  P )  /  ( P  + 
1 ) )  e.  RR )
2245nnrpd 9437 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  RR+ )
22597, 224rpdivcld 9456 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  RR+ )
226225, 221rpdivcld 9456 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  e.  RR+ )
227226rpred 9438 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  e.  RR )
228227, 218remulcld 7764 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) )  x.  P
)  e.  RR )
229228ad2antrr 479 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  x.  P )  e.  RR )
230 simpll 503 . . . . . . . . . . . 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 408 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  e.  RR )
233227ad2antrr 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) )  e.  RR )
234230, 231, 106syl2anc 408 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  =  ( abs `  A
) )
235 fveq2 5389 . . . . . . . . . . . . . 14  |-  ( m  =  j  ->  ( K `  m )  =  ( K `  j ) )
236235breq1d 3909 . . . . . . . . . . . . 13  |-  ( m  =  j  ->  (
( K `  m
)  <  ( (
( E  /  2
)  /  s )  /  ( P  + 
1 ) )  <->  ( K `  j )  <  (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) ) ) )
2377simprd 113 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) ) )
238237ad2antrr 479 . . . . . . . . . . . . 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 9757 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  j  e.  ( ZZ>= `  ( (
m  -  s )  +  1 ) ) )
240 eluzle 9294 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  ( s  +  t )  <_  m )
241240adantl 275 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  t )  <_  m )
2428nn0zd 9129 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  t  e.  ZZ )
243242adantr 274 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  ZZ )
244243zred 9131 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  RR )
24556, 244, 55leaddsub2d 8276 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
s  +  t )  <_  m  <->  t  <_  ( m  -  s ) ) )
246241, 245mpbid 146 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  <_  ( m  -  s ) )
247 eluz 9295 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  ZZ  /\  ( m  -  s
)  e.  ZZ )  ->  ( ( m  -  s )  e.  ( ZZ>= `  t )  <->  t  <_  ( m  -  s ) ) )
248243, 72, 247syl2anc 408 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  e.  ( ZZ>= `  t
)  <->  t  <_  (
m  -  s ) ) )
249246, 248mpbird 166 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ( ZZ>= `  t )
)
250 peano2uz 9334 . . . . . . . . . . . . . . 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 9298 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  ( ( m  -  s )  +  1 ) )  /\  (
( m  -  s
)  +  1 )  e.  ( ZZ>= `  t
) )  ->  j  e.  ( ZZ>= `  t )
)
253239, 251, 252syl2anr 288 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( ZZ>= `  t )
)
254236, 238, 253rspcdva 2768 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  <  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )
255234, 254eqbrtrrd 3922 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  < 
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )
256232, 233, 255ltled 7849 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  <_ 
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )
257 breq1 3902 . . . . . . . . . . 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 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  A. w  e.  T  w  <_  P )
26055adantr 274 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  m  e.  RR )
261 peano2zm 9050 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  (
s  -  1 )  e.  ZZ )
26249, 261syl 14 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( s  -  1 )  e.  ZZ )
263262zred 9131 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  -  1 )  e.  RR )
264263ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  RR )
265231nn0red 8989 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  RR )
26612zcnd 9132 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  CC )
26756recnd 7762 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  CC )
268 1cnd 7750 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  CC )
269266, 267, 268subsubd 8069 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  ( s  - 
1 ) )  =  ( ( m  -  s )  +  1 ) )
270269adantr 274 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  =  ( ( m  -  s )  +  1 ) )
271 elfzle1 9762 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  (
( m  -  s
)  +  1 )  <_  j )
272271adantl 275 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  s
)  +  1 )  <_  j )
273270, 272eqbrtrd 3920 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  <_  j )
274260, 264, 265, 273subled 8277 . . . . . . . . . . . . . 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 2210 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( ZZ>= `  0
) )
277262ad2antrr 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  ZZ )
278 elfz5 9753 . . . . . . . . . . . . . . 15  |-  ( ( ( m  -  j
)  e.  ( ZZ>= ` 
0 )  /\  (
s  -  1 )  e.  ZZ )  -> 
( ( m  -  j )  e.  ( 0 ... ( s  -  1 ) )  <-> 
( m  -  j
)  <_  ( s  -  1 ) ) )
279276, 277, 278syl2anc 408 . . . . . . . . . . . . . 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 166 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( 0 ... ( s  -  1 ) ) )
281 simplll 507 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
28294, 22syldan 280 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
283282, 25sylan 281 . . . . . . . . . . . . . . . . 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 408 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
285284sumeq2dv 11092 . . . . . . . . . . . . . . 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 2123 . . . . . . . . . . . . . 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 5393 . . . . . . . . . . . . 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 2781 . . . . . . . . . . . . 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 408 . . . . . . . . . . . 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 280 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
291290abscld 10908 . . . . . . . . . . . . 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 2124 . . . . . . . . . . . . . . 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 2415 . . . . . . . . . . . . . 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 2804 . . . . . . . . . . . . 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 166 . . . . . . . . . . 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 2768 . . . . . . . . . 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 408 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
30094, 81syldan 280 . . . . . . . . . . . 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 10911 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
30294, 301syldan 280 . . . . . . . . . . . 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 304 . . . . . . . . . . 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 479 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  P  e.  RR )
305 lemul12a 8584 . . . . . . . . . . 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 1202 . . . . . . . . . 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 429 . . . . . . . . 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 11187 . . . . . . . 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 7762 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) )  x.  P
)  e.  CC )
310309adantr 274 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) )  x.  P )  e.  CC )
311 fsumconst 11178 . . . . . . . . . 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 408 . . . . . . . . 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 9039 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  ZZ )
314 fzen 9778 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  (
m  -  s )  e.  ZZ )  -> 
( 1 ... s
)  ~~  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) ) )
315313, 50, 72, 314syl3anc 1201 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( 1  +  ( m  -  s
) ) ... (
s  +  ( m  -  s ) ) ) )
316 ax-1cn 7681 . . . . . . . . . . . . . . 15  |-  1  e.  CC
31772zcnd 9132 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  CC )
318 addcom 7867 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  ( m  -  s
)  e.  CC )  ->  ( 1  +  ( m  -  s
) )  =  ( ( m  -  s
)  +  1 ) )
319316, 317, 318sylancr 410 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1  +  ( m  -  s ) )  =  ( ( m  -  s )  +  1 ) )
320267, 266pncan3d 8044 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  ( m  -  s ) )  =  m )
321319, 320oveq12d 5760 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) )  =  ( ( ( m  -  s )  +  1 ) ... m
) )
322315, 321breqtrd 3924 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( ( m  -  s )  +  1 ) ... m
) )
323313, 50fzfigd 10159 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  e. 
Fin )
324 hashen 10485 . . . . . . . . . . . . 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 408 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( `  ( 1 ... s
) )  =  ( `  ( ( ( m  -  s )  +  1 ) ... m
) )  <->  ( 1 ... s )  ~~  ( ( ( m  -  s )  +  1 ) ... m
) ) )
326322, 325mpbird 166 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( `  (
1 ... s ) )  =  ( `  (
( ( m  -  s )  +  1 ) ... m ) ) )
327 hashfz1 10484 . . . . . . . . . . . 12  |-  ( s  e.  NN0  ->  ( `  (
1 ... s ) )  =  s )
32853, 327syl 14 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( `  (
1 ... s ) )  =  s )
329326, 328eqtr3d 2152 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( `  (
( ( m  -  s )  +  1 ) ... m ) )  =  s )
330329oveq1d 5757 . . . . . . . . 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 7762 . . . . . . . . . . . 12  |-  ( ph  ->  P  e.  CC )
332221rpcnd 9440 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  +  1 )  e.  CC )
333221rpap0d 9444 . . . . . . . . . . . 12  |-  ( ph  ->  ( P  +  1 ) #  0 )
334160, 331, 332, 333div23apd 8555 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  x.  P )  /  ( P  +  1 ) )  =  ( ( ( E  /  2
)  /  ( P  +  1 ) )  x.  P ) )
33549zcnd 9132 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  CC )
336225rpcnd 9440 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  CC )
337335, 336, 332, 333divassapd 8553 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( P  +  1 ) )  =  ( s  x.  ( ( ( E  /  2 )  /  s )  / 
( P  +  1 ) ) ) )
3385nnap0d 8730 . . . . . . . . . . . . . . 15  |-  ( ph  ->  s #  0 )
339160, 335, 338divcanap2d 8519 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  x.  (
( E  /  2
)  /  s ) )  =  ( E  /  2 ) )
340339oveq1d 5757 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( P  +  1 ) )  =  ( ( E  /  2 )  /  ( P  + 
1 ) ) )
341337, 340eqtr3d 2152 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  x.  (
( ( E  / 
2 )  /  s
)  /  ( P  +  1 ) ) )  =  ( ( E  /  2 )  /  ( P  + 
1 ) ) )
342341oveq1d 5757 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )  x.  P
)  =  ( ( ( E  /  2
)  /  ( P  +  1 ) )  x.  P ) )
343226rpcnd 9440 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  e.  CC )
344335, 343, 331mulassd 7757 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) ) )  x.  P
)  =  ( s  x.  ( ( ( ( E  /  2
)  /  s )  /  ( P  + 
1 ) )  x.  P ) ) )
345334, 342, 3443eqtr2rd 2157 . . . . . . . . . 10  |-  ( ph  ->  ( s  x.  (
( ( ( E  /  2 )  / 
s )  /  ( P  +  1 ) )  x.  P ) )  =  ( ( ( E  /  2
)  x.  P )  /  ( P  + 
1 ) ) )
346345adantr 274 . . . . . . . . 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 2154 . . . . . . . 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 3924 . . . . . . 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 7866 . . . . . . . . . . 11  |-  ( P  e.  RR  ->  ( P  +  1 )  e.  RR )
350218, 349syl 14 . . . . . . . . . 10  |-  ( ph  ->  ( P  +  1 )  e.  RR )
351218ltp1d 8652 . . . . . . . . . 10  |-  ( ph  ->  P  <  ( P  +  1 ) )
352218, 350, 97, 351ltmul2dd 9495 . . . . . . . . 9  |-  ( ph  ->  ( ( E  / 
2 )  x.  P
)  <  ( ( E  /  2 )  x.  ( P  +  1 ) ) )
353219, 98, 221ltdivmul2d 9491 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( E  /  2 )  x.  P )  / 
( P  +  1 ) )  <  ( E  /  2 )  <->  ( ( E  /  2 )  x.  P )  <  (
( E  /  2
)  x.  ( P  +  1 ) ) ) )
354352, 353mpbird 166 . . . . . . . 8  |-  ( ph  ->  ( ( ( E  /  2 )  x.  P )  /  ( P  +  1 ) )  <  ( E  /  2 ) )
355354adantr 274 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( E  /  2
)  x.  P )  /  ( P  + 
1 ) )  < 
( E  /  2
) )
35696, 223, 99, 348, 355lelttrd 7855 . . . . . 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 8296 . . . . 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 10921 . . . . . . 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 11092 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) )  = 
sum_ j  e.  ( 0 ... m ) ( ( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) ) )
36072zred 9131 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  RR )
361360ltp1d 8652 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  < 
( ( m  -  s )  +  1 ) )
362 fzdisj 9787 . . . . . . . 8  |-  ( ( m  -  s )  <  ( ( m  -  s )  +  1 )  ->  (
( 0 ... (
m  -  s ) )  i^i  ( ( ( m  -  s
)  +  1 ) ... m ) )  =  (/) )
363361, 362syl 14 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
0 ... ( m  -  s ) )  i^i  ( ( ( m  -  s )  +  1 ) ... m
) )  =  (/) )
364 fzsplit 9786 . . . . . . . 8  |-  ( ( m  -  s )  e.  ( 0 ... m )  ->  (
0 ... m )  =  ( ( 0 ... ( m  -  s
) )  u.  (
( ( m  -  s )  +  1 ) ... m ) ) )
36570, 364syl 14 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... m )  =  ( ( 0 ... ( m  -  s
) )  u.  (
( ( m  -  s )  +  1 ) ... m ) ) )
36682recnd 7762 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  CC )
367363, 365, 13, 366fsumsplit 11131 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  =  (
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 ) ) ) )
368359, 367eqtr2d 2151 . . . . 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 ) ) )  = 
sum_ j  e.  ( 0 ... m ) ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) ) )
36945rpcnd 9440 . . . . . . 7  |-  ( ph  ->  E  e.  CC )
370369adantr 274 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  E  e.  CC )
3713702halvesd 8923 . . . . 5  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  +  ( E  /  2
) )  =  E )
372357, 368, 3713brtr3d 3929 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) )  < 
E )
37342, 44, 47, 48, 372lelttrd 7855 . . 3  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( abs ` 
sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <  E )
374373ralrimiva 2482 . 2  |-  ( ph  ->  A. m  e.  (
ZZ>= `  ( s  +  t ) ) ( abs `  sum_ j  e.  ( 0 ... m
) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <  E )
375 fveq2 5389 . . . 4  |-  ( y  =  ( s  +  t )  ->  ( ZZ>=
`  y )  =  ( ZZ>= `  ( s  +  t ) ) )
376375raleqdv 2609 . . 3  |-  ( y  =  ( s  +  t )  ->  ( A. m  e.  ( ZZ>=
`  y ) ( abs `  sum_ j  e.  ( 0 ... m
) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <  E  <->  A. m  e.  ( ZZ>= `  ( s  +  t ) ) ( abs `  sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) )  < 
E ) )
377376rspcev 2763 . 2  |-  ( ( ( s  +  t )  e.  NN0  /\  A. m  e.  ( ZZ>= `  ( s  +  t ) ) ( abs `  sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <  E )  ->  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 )
3789, 374, 377syl2anc 408 1  |-  ( 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 )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104  DECID wdc 804    = wceq 1316    e. wcel 1465   {cab 2103   A.wral 2393   E.wrex 2394    u. cun 3039    i^i cin 3040    C_ wss 3041   (/)c0 3333   class class class wbr 3899   dom cdm 4509   ` cfv 5093  (class class class)co 5742    ~~ cen 6600   Fincfn 6602   CCcc 7586   RRcr 7587   0cc0 7588   1c1 7589    + caddc 7591    x. cmul 7593    < clt 7768    <_ cle 7769    - cmin 7901    / cdiv 8399   NNcn 8684   2c2 8735   NN0cn0 8935   ZZcz 9012   ZZ>=cuz 9282   RR+crp 9397   ...cfz 9745    seqcseq 10173  ♯chash 10476   abscabs 10724    ~~> cli 11002   sum_csu 11077
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-13 1476  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-coll 4013  ax-sep 4016  ax-nul 4024  ax-pow 4068  ax-pr 4101  ax-un 4325  ax-setind 4422  ax-iinf 4472  ax-cnex 7679  ax-resscn 7680  ax-1cn 7681  ax-1re 7682  ax-icn 7683  ax-addcl 7684  ax-addrcl 7685  ax-mulcl 7686  ax-mulrcl 7687  ax-addcom 7688  ax-mulcom 7689  ax-addass 7690  ax-mulass 7691  ax-distr 7692  ax-i2m1 7693  ax-0lt1 7694  ax-1rid 7695  ax-0id 7696  ax-rnegex 7697  ax-precex 7698  ax-cnre 7699  ax-pre-ltirr 7700  ax-pre-ltwlin 7701  ax-pre-lttrn 7702  ax-pre-apti 7703  ax-pre-ltadd 7704  ax-pre-mulgt0 7705  ax-pre-mulext 7706  ax-arch 7707  ax-caucvg 7708
This theorem depends on definitions:  df-bi 116  df-dc 805  df-3or 948  df-3an 949  df-tru 1319  df-fal 1322  df-nf 1422  df-sb 1721  df-eu 1980  df-mo 1981  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ne 2286  df-nel 2381  df-ral 2398  df-rex 2399  df-reu 2400  df-rmo 2401  df-rab 2402  df-v 2662  df-sbc 2883  df-csb 2976  df-dif 3043  df-un 3045  df-in 3047  df-ss 3054  df-nul 3334  df-if 3445  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-uni 3707  df-int 3742  df-iun 3785  df-br 3900  df-opab 3960  df-mpt 3961  df-tr 3997  df-id 4185  df-po 4188  df-iso 4189  df-iord 4258  df-on 4260  df-ilim 4261  df-suc 4263  df-iom 4475  df-xp 4515  df-rel 4516  df-cnv 4517  df-co 4518  df-dm 4519  df-rn 4520  df-res 4521  df-ima 4522  df-iota 5058  df-fun 5095  df-fn 5096  df-f 5097  df-f1 5098  df-fo 5099  df-f1o 5100  df-fv 5101  df-isom 5102  df-riota 5698  df-ov 5745  df-oprab 5746  df-mpo 5747  df-1st 6006  df-2nd 6007  df-recs 6170  df-irdg 6235  df-frec 6256  df-1o 6281  df-oadd 6285  df-er 6397  df-en 6603  df-dom 6604  df-fin 6605  df-sup 6839  df-pnf 7770  df-mnf 7771  df-xr 7772  df-ltxr 7773  df-le 7774  df-sub 7903  df-neg 7904  df-reap 8304  df-ap 8311  df-div 8400  df-inn 8685  df-2 8743  df-3 8744  df-4 8745  df-n0 8936  df-z 9013  df-uz 9283  df-q 9368  df-rp 9398  df-ico 9632  df-fz 9746  df-fzo 9875  df-seqfrec 10174  df-exp 10248  df-ihash 10477  df-cj 10569  df-re 10570  df-im 10571  df-rsqrt 10725  df-abs 10726  df-clim 11003  df-sumdc 11078
This theorem is referenced by:  mertenslem2  11260
  Copyright terms: Public domain W3C validator