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

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

Proof of Theorem mertenslem1
StepHypRef Expression
1 mertens.12 . . . . . . 7  |-  ( ph  ->  ( ps  /\  (
t  e.  NN0  /\  A. m  e.  ( ZZ>= `  t ) ( K `
 m )  < 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) ) )
21simpld 447 . . . . . 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 190 . . . . 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 447 . . . 4  |-  ( ph  ->  s  e.  NN )
65nnnn0d 9971 . . 3  |-  ( ph  ->  s  e.  NN0 )
71simprd 451 . . . 4  |-  ( ph  ->  ( t  e.  NN0  /\ 
A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
87simpld 447 . . 3  |-  ( ph  ->  t  e.  NN0 )
96, 8nn0addcld 9975 . 2  |-  ( ph  ->  ( s  +  t )  e.  NN0 )
10 fzfid 10987 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... m )  e. 
Fin )
11 simpl 445 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ph )
12 elfznn0 10774 . . . . . . . 8  |-  ( j  e.  ( 0 ... m )  ->  j  e.  NN0 )
13 mertens.3 . . . . . . . 8  |-  ( (
ph  /\  j  e.  NN0 )  ->  A  e.  CC )
1411, 12, 13syl2an 465 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  A  e.  CC )
15 eqid 2256 . . . . . . . 8  |-  ( ZZ>= `  ( ( m  -  j )  +  1 ) )  =  (
ZZ>= `  ( ( m  -  j )  +  1 ) )
16 fznn0sub 10776 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... m )  ->  (
m  -  j )  e.  NN0 )
1716adantl 454 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
m  -  j )  e.  NN0 )
18 peano2nn0 9957 . . . . . . . . . 10  |-  ( ( m  -  j )  e.  NN0  ->  ( ( m  -  j )  +  1 )  e. 
NN0 )
1917, 18syl 17 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
2019nn0zd 10068 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
21 simplll 737 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
22 eluznn0 10241 . . . . . . . . . 10  |-  ( ( ( ( m  -  j )  +  1 )  e.  NN0  /\  k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) )  -> 
k  e.  NN0 )
2319, 22sylan 459 . . . . . . . . 9  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
24 mertens.4 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  =  B )
2521, 23, 24syl2anc 645 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
26 mertens.5 . . . . . . . . 9  |-  ( (
ph  /\  k  e.  NN0 )  ->  B  e.  CC )
2721, 23, 26syl2anc 645 . . . . . . . 8  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  B  e.  CC )
28 mertens.8 . . . . . . . . . 10  |-  ( ph  ->  seq  0 (  +  ,  G )  e. 
dom 
~~>  )
2928ad2antrr 709 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq  0 (  +  ,  G )  e.  dom  ~~>  )
30 nn0uz 10215 . . . . . . . . . 10  |-  NN0  =  ( ZZ>= `  0 )
31 simpll 733 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ph )
3224, 26eqeltrd 2330 . . . . . . . . . . 11  |-  ( (
ph  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3331, 32sylan 459 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m ) )  /\  k  e.  NN0 )  ->  ( G `  k )  e.  CC )
3430, 19, 33iserex 12081 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (  seq  0 (  +  ,  G )  e.  dom  ~~>  <->  seq  ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  ) )
3529, 34mpbid 203 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  seq  ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
3615, 20, 25, 27, 35isumcl 12175 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
3714, 36mulcld 8809 . . . . . 6  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  CC )
3810, 37fsumcl 12157 . . . . 5  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  CC )
3938abscld 11869 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( abs ` 
sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
4037abscld 11869 . . . . 5  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
4110, 40fsumrecl 12158 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... m
) ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) )  e.  RR )
42 mertens.9 . . . . . 6  |-  ( ph  ->  E  e.  RR+ )
4342rpred 10343 . . . . 5  |-  ( ph  ->  E  e.  RR )
4443adantr 453 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  E  e.  RR )
4510, 37fsumabs 12210 . . . 4  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( abs ` 
sum_ j  e.  ( 0 ... m ) ( A  x.  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  sum_ j  e.  ( 0 ... m
) ( abs `  ( A  x.  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B ) ) )
46 fzfid 10987 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  e. 
Fin )
476adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  NN0 )
4847nn0ge0d 9974 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  <_  s )
49 eluzelz 10191 . . . . . . . . . . . . . . 15  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  m  e.  ZZ )
5049adantl 454 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ZZ )
5150zred 10070 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  RR )
5247nn0red 9972 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  RR )
5351, 52subge02d 9318 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0  <_  s  <->  ( m  -  s )  <_  m ) )
5448, 53mpbid 203 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  <_  m )
5547, 30syl6eleq 2346 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( ZZ>= `  0 )
)
565nnzd 10069 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  s  e.  ZZ )
57 uzid 10195 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  s  e.  ( ZZ>= `  s )
)
5856, 57syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  s  e.  ( ZZ>= `  s ) )
59 uzaddcl 10228 . . . . . . . . . . . . . . . . 17  |-  ( ( s  e.  ( ZZ>= `  s )  /\  t  e.  NN0 )  ->  (
s  +  t )  e.  ( ZZ>= `  s
) )
6058, 8, 59syl2anc 645 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  +  t )  e.  ( ZZ>= `  s ) )
61 eqid 2256 . . . . . . . . . . . . . . . . 17  |-  ( ZZ>= `  s )  =  (
ZZ>= `  s )
6261uztrn2 10198 . . . . . . . . . . . . . . . 16  |-  ( ( ( s  +  t )  e.  ( ZZ>= `  s )  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
6360, 62sylan 459 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  s )
)
64 elfzuzb 10744 . . . . . . . . . . . . . . 15  |-  ( s  e.  ( 0 ... m )  <->  ( s  e.  ( ZZ>= `  0 )  /\  m  e.  ( ZZ>=
`  s ) ) )
6555, 63, 64sylanbrc 648 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ( 0 ... m
) )
66 fznn0sub2 10777 . . . . . . . . . . . . . 14  |-  ( s  e.  ( 0 ... m )  ->  (
m  -  s )  e.  ( 0 ... m ) )
6765, 66syl 17 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ( 0 ... m
) )
68 elfzelz 10750 . . . . . . . . . . . . 13  |-  ( ( m  -  s )  e.  ( 0 ... m )  ->  (
m  -  s )  e.  ZZ )
6967, 68syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ZZ )
70 eluz 10194 . . . . . . . . . . . 12  |-  ( ( ( m  -  s
)  e.  ZZ  /\  m  e.  ZZ )  ->  ( m  e.  (
ZZ>= `  ( m  -  s ) )  <->  ( m  -  s )  <_  m ) )
7169, 50, 70syl2anc 645 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  e.  ( ZZ>= `  ( m  -  s ) )  <-> 
( m  -  s
)  <_  m )
)
7254, 71mpbird 225 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  ( ZZ>= `  ( m  -  s ) ) )
73 fzss2 10783 . . . . . . . . . 10  |-  ( m  e.  ( ZZ>= `  (
m  -  s ) )  ->  ( 0 ... ( m  -  s ) )  C_  ( 0 ... m
) )
7472, 73syl 17 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  C_  ( 0 ... m
) )
7574sselda 3141 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ( 0 ... m
) )
7613abscld 11869 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  RR )
7711, 12, 76syl2an 465 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  A )  e.  RR )
7836abscld 11869 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
7977, 78remulcld 8817 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
8075, 79syldan 458 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
8146, 80fsumrecl 12158 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
82 fzfid 10987 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( m  -  s
)  +  1 ) ... m )  e. 
Fin )
83 elfznn0 10774 . . . . . . . . . . . . 13  |-  ( ( m  -  s )  e.  ( 0 ... m )  ->  (
m  -  s )  e.  NN0 )
8467, 83syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e. 
NN0 )
85 peano2nn0 9957 . . . . . . . . . . . 12  |-  ( ( m  -  s )  e.  NN0  ->  ( ( m  -  s )  +  1 )  e. 
NN0 )
8684, 85syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e. 
NN0 )
8786, 30syl6eleq 2346 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  0 )
)
88 fzss1 10782 . . . . . . . . . 10  |-  ( ( ( m  -  s
)  +  1 )  e.  ( ZZ>= `  0
)  ->  ( (
( m  -  s
)  +  1 ) ... m )  C_  ( 0 ... m
) )
8987, 88syl 17 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( m  -  s
)  +  1 ) ... m )  C_  ( 0 ... m
) )
9089sselda 3141 . . . . . . . 8  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( 0 ... m
) )
9190, 79syldan 458 . . . . . . 7  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
9282, 91fsumrecl 12158 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  e.  RR )
9342rphalfcld 10355 . . . . . . . 8  |-  ( ph  ->  ( E  /  2
)  e.  RR+ )
9493rpred 10343 . . . . . . 7  |-  ( ph  ->  ( E  /  2
)  e.  RR )
9594adantr 453 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  RR )
96 elfznn0 10774 . . . . . . . . . . 11  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  NN0 )
9711, 96, 76syl2an 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  RR )
9846, 97fsumrecl 12158 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  RR )
9998, 95remulcld 8817 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  e.  RR )
100 0z 9988 . . . . . . . . . . . 12  |-  0  e.  ZZ
101100a1i 12 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ZZ )
102 eqidd 2257 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( K `  j ) )
103 mertens.2 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  =  ( abs `  A ) )
104103, 76eqeltrd 2330 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( K `  j )  e.  RR )
105 mertens.7 . . . . . . . . . . 11  |-  ( ph  ->  seq  0 (  +  ,  K )  e. 
dom 
~~>  )
10630, 101, 102, 104, 105isumrecl 12179 . . . . . . . . . 10  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  e.  RR )
10713absge0d 11877 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( abs `  A ) )
108107, 103breqtrrd 4009 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  0  <_  ( K `  j ) )
10930, 101, 102, 104, 105, 108isumge0 12180 . . . . . . . . . 10  |-  ( ph  ->  0  <_  sum_ j  e. 
NN0  ( K `  j ) )
110106, 109ge0p1rpd 10369 . . . . . . . . 9  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR+ )
111110adantr 453 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR+ )
11299, 111rerpdivcld 10370 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR )
11393, 110rpdivcld 10360 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR+ )
114113rpred 10343 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  e.  RR )
115114ad2antrr 709 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )  e.  RR )
11697, 115remulcld 8817 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )  e.  RR )
11775, 20syldan 458 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  ZZ )
118 simplll 737 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
11975, 19syldan 458 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
120119, 22sylan 459 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
121118, 120, 24syl2anc 645 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
122118, 120, 26syl2anc 645 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... ( m  -  s ) ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  B  e.  CC )
12375, 35syldan 458 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  seq  ( ( m  -  j )  +  1 ) (  +  ,  G )  e.  dom  ~~>  )
12415, 117, 121, 122, 123isumcl 12175 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  e.  CC )
125124abscld 11869 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
12676, 107jca 520 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( ( abs `  A )  e.  RR  /\  0  <_ 
( abs `  A
) ) )
12711, 96, 126syl2an 465 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
128121sumeq2dv 12127 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )
129128fveq2d 5448 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
130 elfzelz 10750 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  e.  ZZ )
131130adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  ZZ )
132131zred 10070 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  e.  RR )
13349ad2antlr 710 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  ZZ )
134133zred 10070 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  m  e.  RR )
13556ad2antrr 709 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  ZZ )
136135zred 10070 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  e.  RR )
137 elfzle2 10752 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... ( m  -  s
) )  ->  j  <_  ( m  -  s
) )
138137adantl 454 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  j  <_  ( m  -  s
) )
139132, 134, 136, 138lesubd 9330 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  s  <_  ( m  -  j
) )
140133, 131zsubcld 10075 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ZZ )
141 eluz 10194 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  ZZ  /\  ( m  -  j
)  e.  ZZ )  ->  ( ( m  -  j )  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
142135, 140, 141syl2anc 645 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( m  -  j
)  e.  ( ZZ>= `  s )  <->  s  <_  ( m  -  j ) ) )
143139, 142mpbird 225 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
m  -  j )  e.  ( ZZ>= `  s
) )
1444simprd 451 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. n  e.  (
ZZ>= `  s ) ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) )  <  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) )
145144ad2antrr 709 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  A. n  e.  ( ZZ>= `  s )
( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
146 oveq1 5785 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( m  -  j )  ->  (
n  +  1 )  =  ( ( m  -  j )  +  1 ) )
147146fveq2d 5448 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( m  -  j )  ->  ( ZZ>=
`  ( n  + 
1 ) )  =  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) )
148147sumeq1d 12125 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( m  -  j )  ->  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) )
149148fveq2d 5448 . . . . . . . . . . . . . . 15  |-  ( n  =  ( m  -  j )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) ) )
150149breq1d 3993 . . . . . . . . . . . . . 14  |-  ( n  =  ( m  -  j )  ->  (
( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <-> 
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `
 k ) )  <  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
151150rcla4v 2848 . . . . . . . . . . . . 13  |-  ( ( m  -  j )  e.  ( ZZ>= `  s
)  ->  ( A. n  e.  ( ZZ>= `  s ) ( abs `  sum_ k  e.  (
ZZ>= `  ( n  + 
1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
152143, 145, 151sylc 58 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
153129, 152eqbrtrrd 4005 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
154125, 115, 153ltled 8921 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  ( ( E  /  2 )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
155 lemul2a 9565 . . . . . . . . . 10  |-  ( ( ( ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR  /\  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )  e.  RR  /\  ( ( abs `  A )  e.  RR  /\  0  <_  ( abs `  A
) ) )  /\  ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  <_  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) )  ->  ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
156125, 115, 127, 154, 155syl31anc 1190 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
15746, 80, 116, 156fsumle 12208 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  (
( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) ) ) )
15898recnd 8815 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  e.  CC )
15993rpcnd 10345 . . . . . . . . . . 11  |-  ( ph  ->  ( E  /  2
)  e.  CC )
160159adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( E  /  2 )  e.  CC )
161 peano2re 8939 . . . . . . . . . . . . 13  |-  ( sum_ j  e.  NN0  ( K `
 j )  e.  RR  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR )
162106, 161syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR )
163162recnd 8815 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  CC )
164163adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  CC )
165110rpne0d 10348 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  =/=  0 )
166165adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  =/=  0
)
167158, 160, 164, 166divassd 9525 . . . . . . . . 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 5444 . . . . . . . . . . . . . . . . 17  |-  ( n  =  j  ->  ( K `  n )  =  ( K `  j ) )
169168cbvsumv 12120 . . . . . . . . . . . . . . . 16  |-  sum_ n  e.  NN0  ( K `  n )  =  sum_ j  e.  NN0  ( K `
 j )
170169oveq1i 5788 . . . . . . . . . . . . . . 15  |-  ( sum_ n  e.  NN0  ( K `  n )  +  1 )  =  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )
171170oveq2i 5789 . . . . . . . . . . . . . 14  |-  ( ( E  /  2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  =  ( ( E  /  2
)  /  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
172171, 113syl5eqel 2340 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  RR+ )
173172rpcnd 10345 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  / 
2 )  /  ( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
174173adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  / 
( sum_ n  e.  NN0  ( K `  n )  +  1 ) )  e.  CC )
17576recnd 8815 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  NN0 )  ->  ( abs `  A )  e.  CC )
17611, 96, 175syl2an 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... (
m  -  s ) ) )  ->  ( abs `  A )  e.  CC )
17746, 174, 176fsummulc1 12198 . . . . . . . . . 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 5789 . . . . . . . . . 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 5789 . . . . . . . . . . . 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 12 . . . . . . . . . . 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 12123 . . . . . . . . . 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 2311 . . . . . . . . 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 2288 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  =  sum_ j  e.  ( 0 ... ( m  -  s ) ) ( ( abs `  A
)  x.  ( ( E  /  2 )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) ) )
184157, 183breqtrrd 4009 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
185106adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  e.  RR )
186162adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  e.  RR )
187100a1i 12 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  0  e.  ZZ )
18896ssriv 3145 . . . . . . . . . . . . 13  |-  ( 0 ... ( m  -  s ) )  C_  NN0
189188a1i 12 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 0 ... ( m  -  s ) )  C_  NN0 )
190103adantlr 698 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( K `  j )  =  ( abs `  A
) )
19176adantlr 698 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  ( abs `  A )  e.  RR )
192107adantlr 698 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e. 
NN0 )  ->  0  <_  ( abs `  A
) )
193105adantr 453 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  seq  0
(  +  ,  K
)  e.  dom  ~~>  )
19430, 187, 46, 189, 190, 191, 192, 193isumless 12252 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( abs `  A
) )
195103sumeq2dv 12127 . . . . . . . . . . . 12  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
196195adantr 453 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  =  sum_ j  e.  NN0  ( abs `  A ) )
197194, 196breqtrrd 4009 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <_  sum_ j  e. 
NN0  ( K `  j ) )
198106ltp1d 9641 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ j  e.  NN0  ( K `  j )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )
199198adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e. 
NN0  ( K `  j )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )
20098, 185, 186, 197, 199lelttrd 8928 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  <  ( sum_ j  e.  NN0  ( K `
 j )  +  1 ) )
20193rpregt0d 10349 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  / 
2 )  e.  RR  /\  0  <  ( E  /  2 ) ) )
202201adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( E  /  2 )  e.  RR  /\  0  < 
( E  /  2
) ) )
203 ltmul1 9560 . . . . . . . . . 10  |-  ( (
sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  e.  RR  /\  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  ( ( E  /  2 )  e.  RR  /\  0  <  ( E  /  2
) ) )  -> 
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  <  ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  <->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) ) )
20498, 186, 202, 203syl3anc 1187 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 )  <->  ( sum_ j  e.  ( 0 ... (
m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  <  ( ( sum_ j  e.  NN0  ( K `
 j )  +  1 )  x.  ( E  /  2 ) ) ) )
205200, 204mpbid 203 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) )
206110rpregt0d 10349 . . . . . . . . . 10  |-  ( ph  ->  ( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  <  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
207206adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  < 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )
208 ltdivmul 9582 . . . . . . . . 9  |-  ( ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  e.  RR  /\  ( E  /  2 )  e.  RR  /\  ( (
sum_ j  e.  NN0  ( K `  j )  +  1 )  e.  RR  /\  0  < 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) ) )  ->  ( (
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <  ( E  /  2 )  <->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) ) )
20999, 95, 207, 208syl3anc 1187 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A
)  x.  ( E  /  2 ) )  /  ( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <  ( E  /  2 )  <->  ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  < 
( ( sum_ j  e.  NN0  ( K `  j )  +  1 )  x.  ( E  /  2 ) ) ) )
210205, 209mpbird 225 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( sum_ j  e.  ( 0 ... ( m  -  s ) ) ( abs `  A )  x.  ( E  / 
2 ) )  / 
( sum_ j  e.  NN0  ( K `  j )  +  1 ) )  <  ( E  / 
2 ) )
21181, 112, 95, 184, 210lelttrd 8928 . . . . . 6  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( 0 ... (
m  -  s ) ) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <  ( E  /  2 ) )
212 mertens.13 . . . . . . . . . . . 12  |-  ( ph  ->  ( 0  <_  sup ( T ,  RR ,  <  )  /\  ( T 
C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z
) ) )
213212simprd 451 . . . . . . . . . . 11  |-  ( ph  ->  ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z ) )
214 suprcl 9668 . . . . . . . . . . 11  |-  ( ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z
)  ->  sup ( T ,  RR ,  <  )  e.  RR )
215213, 214syl 17 . . . . . . . . . 10  |-  ( ph  ->  sup ( T ,  RR ,  <  )  e.  RR )
21694, 215remulcld 8817 . . . . . . . . 9  |-  ( ph  ->  ( ( E  / 
2 )  x.  sup ( T ,  RR ,  <  ) )  e.  RR )
217212simpld 447 . . . . . . . . . 10  |-  ( ph  ->  0  <_  sup ( T ,  RR ,  <  ) )
218215, 217ge0p1rpd 10369 . . . . . . . . 9  |-  ( ph  ->  ( sup ( T ,  RR ,  <  )  +  1 )  e.  RR+ )
219216, 218rerpdivcld 10370 . . . . . . . 8  |-  ( ph  ->  ( ( ( E  /  2 )  x. 
sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
220219adantr 453 . . . . . . 7  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( E  /  2
)  x.  sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
2215nnrpd 10342 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  RR+ )
22293, 221rpdivcld 10360 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  RR+ )
223222, 218rpdivcld 10360 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR+ )
224223rpred 10343 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
225224, 215remulcld 8817 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  RR )
226225ad2antrr 709 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  RR )
227 simpll 733 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ph )
22890, 12syl 17 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  NN0 )
229227, 228, 76syl2anc 645 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  e.  RR )
230224ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )
231227, 228, 103syl2anc 645 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  =  ( abs `  A
) )
232 elfzuz 10746 . . . . . . . . . . . . . 14  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  j  e.  ( ZZ>= `  ( (
m  -  s )  +  1 ) ) )
233 eluzle 10193 . . . . . . . . . . . . . . . . . 18  |-  ( m  e.  ( ZZ>= `  (
s  +  t ) )  ->  ( s  +  t )  <_  m )
234233adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  t )  <_  m )
2358nn0zd 10068 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  t  e.  ZZ )
236235adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  ZZ )
237236zred 10070 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  e.  RR )
23852, 237, 51leaddsub2d 9328 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
s  +  t )  <_  m  <->  t  <_  ( m  -  s ) ) )
239234, 238mpbid 203 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  t  <_  ( m  -  s ) )
240 eluz 10194 . . . . . . . . . . . . . . . . 17  |-  ( ( t  e.  ZZ  /\  ( m  -  s
)  e.  ZZ )  ->  ( ( m  -  s )  e.  ( ZZ>= `  t )  <->  t  <_  ( m  -  s ) ) )
241236, 69, 240syl2anc 645 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  e.  ( ZZ>= `  t
)  <->  t  <_  (
m  -  s ) ) )
242239, 241mpbird 225 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  ( ZZ>= `  t )
)
243 peano2uz 10225 . . . . . . . . . . . . . . 15  |-  ( ( m  -  s )  e.  ( ZZ>= `  t
)  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  t )
)
244242, 243syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
m  -  s )  +  1 )  e.  ( ZZ>= `  t )
)
245 uztrn 10197 . . . . . . . . . . . . . 14  |-  ( ( j  e.  ( ZZ>= `  ( ( m  -  s )  +  1 ) )  /\  (
( m  -  s
)  +  1 )  e.  ( ZZ>= `  t
) )  ->  j  e.  ( ZZ>= `  t )
)
246232, 244, 245syl2anr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  ( ZZ>= `  t )
)
2477simprd 451 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. m  e.  (
ZZ>= `  t ) ( K `  m )  <  ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) ) )
248247ad2antrr 709 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  A. m  e.  ( ZZ>= `  t )
( K `  m
)  <  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
249 fveq2 5444 . . . . . . . . . . . . . . 15  |-  ( m  =  j  ->  ( K `  m )  =  ( K `  j ) )
250249breq1d 3993 . . . . . . . . . . . . . 14  |-  ( m  =  j  ->  (
( K `  m
)  <  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  <->  ( K `  j )  <  (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
251250rcla4v 2848 . . . . . . . . . . . . 13  |-  ( j  e.  ( ZZ>= `  t
)  ->  ( A. m  e.  ( ZZ>= `  t ) ( K `
 m )  < 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  ->  ( K `  j )  <  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
252246, 248, 251sylc 58 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( K `  j )  <  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
253231, 252eqbrtrrd 4005 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  < 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
254229, 230, 253ltled 8921 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  A )  <_ 
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
255213ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z
) )
25651adantr 453 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  m  e.  RR )
257 peano2zm 10015 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  ZZ  ->  (
s  -  1 )  e.  ZZ )
25856, 257syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( s  -  1 )  e.  ZZ )
259258zred 10070 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( s  -  1 )  e.  RR )
260259ad2antrr 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  RR )
261228nn0red 9972 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  j  e.  RR )
26250zcnd 10071 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  m  e.  CC )
26352recnd 8815 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  CC )
264 ax-1cn 8749 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  CC
265264a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  CC )
266262, 263, 265subsubd 9139 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  ( s  - 
1 ) )  =  ( ( m  -  s )  +  1 ) )
267266adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  =  ( ( m  -  s )  +  1 ) )
268 elfzle1 10751 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( ( ( m  -  s )  +  1 ) ... m )  ->  (
( m  -  s
)  +  1 )  <_  j )
269268adantl 454 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  s
)  +  1 )  <_  j )
270267, 269eqbrtrd 4003 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  ( s  -  1 ) )  <_  j )
271256, 260, 261, 270subled 9329 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  <_  ( s  - 
1 ) )
27290, 16syl 17 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  NN0 )
273272, 30syl6eleq 2346 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( ZZ>= `  0
) )
274258ad2antrr 709 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
s  -  1 )  e.  ZZ )
275 elfz5 10742 . . . . . . . . . . . . . . 15  |-  ( ( ( m  -  j
)  e.  ( ZZ>= ` 
0 )  /\  (
s  -  1 )  e.  ZZ )  -> 
( ( m  -  j )  e.  ( 0 ... ( s  -  1 ) )  <-> 
( m  -  j
)  <_  ( s  -  1 ) ) )
276273, 274, 275syl2anc 645 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  j
)  e.  ( 0 ... ( s  - 
1 ) )  <->  ( m  -  j )  <_ 
( s  -  1 ) ) )
277271, 276mpbird 225 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
m  -  j )  e.  ( 0 ... ( s  -  1 ) ) )
278 simplll 737 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ph )
27990, 19syldan 458 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( m  -  j
)  +  1 )  e.  NN0 )
280279, 22sylan 459 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  k  e.  NN0 )
281278, 280, 24syl2anc 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( (
( m  -  s
)  +  1 ) ... m ) )  /\  k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) )  ->  ( G `  k )  =  B )
282281sumeq2dv 12127 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
)  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )
283282eqcomd 2261 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B  =  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) )
284283fveq2d 5448 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `  k ) ) )
285149eqeq2d 2267 . . . . . . . . . . . . . 14  |-  ( n  =  ( m  -  j )  ->  (
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <-> 
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) ( G `
 k ) ) ) )
286285rcla4ev 2852 . . . . . . . . . . . . 13  |-  ( ( ( m  -  j
)  e.  ( 0 ... ( s  - 
1 ) )  /\  ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) ( G `  k
) ) )  ->  E. n  e.  (
0 ... ( s  - 
1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) ) )
287277, 284, 286syl2anc 645 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  E. n  e.  ( 0 ... (
s  -  1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) )
288 fvex 5458 . . . . . . . . . . . . 13  |-  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  _V
289 eqeq1 2262 . . . . . . . . . . . . . 14  |-  ( z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  ->  ( z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) )  <-> 
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) ) )
290289rexbidv 2537 . . . . . . . . . . . . 13  |-  ( z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  ->  ( E. n  e.  ( 0 ... (
s  -  1 ) ) z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) )  <->  E. n  e.  ( 0 ... (
s  -  1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) ) )
291 mertens.10 . . . . . . . . . . . . 13  |-  T  =  { z  |  E. n  e.  ( 0 ... ( s  - 
1 ) ) z  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1
) ) ( G `
 k ) ) }
292288, 290, 291elab2 2885 . . . . . . . . . . . 12  |-  ( ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  T  <->  E. n  e.  ( 0 ... ( s  - 
1 ) ) ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  =  ( abs `  sum_ k  e.  ( ZZ>= `  ( n  +  1 ) ) ( G `  k
) ) )
293287, 292sylibr 205 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  T )
294 suprub 9669 . . . . . . . . . . 11  |-  ( ( ( T  C_  RR  /\  T  =/=  (/)  /\  E. z  e.  RR  A. w  e.  T  w  <_  z )  /\  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  T )  ->  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )
295255, 293, 294syl2anc 645 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )
296227, 228, 126syl2anc 645 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  e.  RR  /\  0  <_  ( abs `  A
) ) )
29790, 78syldan 458 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR )
29836absge0d 11877 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( 0 ... m
) )  ->  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
29990, 298syldan 458 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )
300297, 299jca 520 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  e.  RR  /\  0  <_  ( abs `  sum_ k  e.  ( ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) ) )
301215ad2antrr 709 . . . . . . . . . . 11  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  sup ( T ,  RR ,  <  )  e.  RR )
302 lemul12a 9568 . . . . . . . . . . 11  |-  ( ( ( ( ( abs `  A )  e.  RR  /\  0  <_  ( abs `  A ) )  /\  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  RR )  /\  ( ( ( abs `  sum_ k  e.  ( ZZ>= `  ( (
m  -  j )  +  1 ) ) B )  e.  RR  /\  0  <_  ( abs ` 
sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  /\  sup ( T ,  RR ,  <  )  e.  RR ) )  ->  ( (
( abs `  A
)  <_  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  /\  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
303296, 230, 300, 301, 302syl22anc 1188 . . . . . . . . . 10  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( ( abs `  A
)  <_  ( (
( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  /\  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B )  <_  sup ( T ,  RR ,  <  ) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
304254, 295, 303mp2and 663 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  /\  j  e.  ( ( ( m  -  s )  +  1 ) ... m
) )  ->  (
( abs `  A
)  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
30582, 91, 226, 304fsumle 12208 . . . . . . . 8  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( abs `  A )  x.  ( abs `  sum_ k  e.  (
ZZ>= `  ( ( m  -  j )  +  1 ) ) B ) )  <_  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
306225recnd 8815 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  CC )
307306adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  CC )
308 fsumconst 12203 . . . . . . . . . 10  |-  ( ( ( ( ( m  -  s )  +  1 ) ... m
)  e.  Fin  /\  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  e.  CC )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m ) ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  =  ( (
# `  ( (
( m  -  s
)  +  1 ) ... m ) )  x.  ( ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
30982, 307, 308syl2anc 645 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  sum_ j  e.  ( ( ( m  -  s )  +  1 ) ... m
) ( ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) )  =  ( ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  x.  ( ( ( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
310 1z 10006 . . . . . . . . . . . . . . 15  |-  1  e.  ZZ
311310a1i 12 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  1  e.  ZZ )
31256adantr 453 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  s  e.  ZZ )
313 fzen 10763 . . . . . . . . . . . . . 14  |-  ( ( 1  e.  ZZ  /\  s  e.  ZZ  /\  (
m  -  s )  e.  ZZ )  -> 
( 1 ... s
)  ~~  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) ) )
314311, 312, 69, 313syl3anc 1187 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( 1  +  ( m  -  s
) ) ... (
s  +  ( m  -  s ) ) ) )
31569zcnd 10071 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( m  -  s )  e.  CC )
316 addcom 8952 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  CC  /\  ( m  -  s
)  e.  CC )  ->  ( 1  +  ( m  -  s
) )  =  ( ( m  -  s
)  +  1 ) )
317264, 315, 316sylancr 647 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1  +  ( m  -  s ) )  =  ( ( m  -  s )  +  1 ) )
318263, 262pncan3d 9114 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( s  +  ( m  -  s ) )  =  m )
319317, 318oveq12d 5796 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( (
1  +  ( m  -  s ) ) ... ( s  +  ( m  -  s
) ) )  =  ( ( ( m  -  s )  +  1 ) ... m
) )
320314, 319breqtrd 4007 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  ~~  ( ( ( m  -  s )  +  1 ) ... m
) )
321 fzfid 10987 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( 1 ... s )  e. 
Fin )
322 hashen 11298 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... s
)  e.  Fin  /\  ( ( ( m  -  s )  +  1 ) ... m
)  e.  Fin )  ->  ( ( # `  (
1 ... s ) )  =  ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  <->  ( 1 ... s )  ~~  (
( ( m  -  s )  +  1 ) ... m ) ) )
323321, 82, 322syl2anc 645 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( # `
 ( 1 ... s ) )  =  ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  <->  ( 1 ... s )  ~~  (
( ( m  -  s )  +  1 ) ... m ) ) )
324320, 323mpbird 225 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( # `  (
1 ... s ) )  =  ( # `  (
( ( m  -  s )  +  1 ) ... m ) ) )
325 hashfz1 11297 . . . . . . . . . . . 12  |-  ( s  e.  NN0  ->  ( # `  ( 1 ... s
) )  =  s )
32647, 325syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( # `  (
1 ... s ) )  =  s )
327324, 326eqtr3d 2290 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( # `  (
( ( m  -  s )  +  1 ) ... m ) )  =  s )
328327oveq1d 5793 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  ( ZZ>= `  ( s  +  t ) ) )  ->  ( ( # `
 ( ( ( m  -  s )  +  1 ) ... m ) )  x.  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )  =  ( s  x.  ( ( ( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
329215recnd 8815 . . . . . . . . . . . 12  |-  ( ph  ->  sup ( T ,  RR ,  <  )  e.  CC )
330218rpcnne0d 10352 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( sup ( T ,  RR ,  <  )  +  1 )  e.  CC  /\  ( sup ( T ,  RR ,  <  )  +  1 )  =/=  0 ) )
331 div23 9397 . . . . . . . . . . . 12  |-  ( ( ( E  /  2
)  e.  CC  /\  sup ( T ,  RR ,  <  )  e.  CC  /\  ( ( sup ( T ,  RR ,  <  )  +  1 )  e.  CC  /\  ( sup ( T ,  RR ,  <  )  +  1 )  =/=  0 ) )  ->  ( (
( E  /  2
)  x.  sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( ( ( E  / 
2 )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
332159, 329, 330, 331syl3anc 1187 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( E  /  2 )  x. 
sup ( T ,  RR ,  <  ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( ( ( E  /  2
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
33356zcnd 10071 . . . . . . . . . . . . . 14  |-  ( ph  ->  s  e.  CC )
334222rpcnd 10345 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( E  / 
2 )  /  s
)  e.  CC )
335 divass 9396 . . . . . . . . . . . . . 14  |-  ( ( s  e.  CC  /\  ( ( E  / 
2 )  /  s
)  e.  CC  /\  ( ( sup ( T ,  RR ,  <  )  +  1 )  e.  CC  /\  ( sup ( T ,  RR ,  <  )  +  1 )  =/=  0 ) )  ->  ( (
s  x.  ( ( E  /  2 )  /  s ) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( s  x.  ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
336333, 334, 330, 335syl3anc 1187 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( s  x.  ( ( ( E  /  2
)  /  s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) ) )
3375nnne0d 9744 . . . . . . . . . . . . . . 15  |-  ( ph  ->  s  =/=  0 )
338159, 333, 337divcan2d 9492 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( s  x.  (
( E  /  2
)  /  s ) )  =  ( E  /  2 ) )
339338oveq1d 5793 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( s  x.  ( ( E  / 
2 )  /  s
) )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  =  ( ( E  /  2
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
340336, 339eqtr3d 2290 . . . . . . . . . . . 12  |-  ( ph  ->  ( s  x.  (
( ( E  / 
2 )  /  s
)  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )  =  ( ( E  / 
2 )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )
341340oveq1d 5793 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )  x. 
sup ( T ,  RR ,  <  ) )  =  ( ( ( E  /  2 )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) )
342223rpcnd 10345 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) )  e.  CC )
343333, 342, 329mulassd 8812 . . . . . . . . . . 11  |-  ( ph  ->  ( ( s  x.  ( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <  )  +  1 ) ) )  x. 
sup ( T ,  RR ,  <  ) )  =  ( s  x.  ( ( ( ( E  /  2 )  /  s )  / 
( sup ( T ,  RR ,  <  )  +  1 ) )  x.  sup ( T ,  RR ,  <  ) ) ) )
344332, 341, 3433eqtr2rd 2295 . . . . . . . . . 10  |-  ( ph  ->  ( s  x.  (
( ( ( E  /  2 )  / 
s )  /  ( sup ( T ,  RR ,  <