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

Theorem pntlemf 22986
Description: Lemma for pnt 22995. Add up the pieces in pntlemi 22985 to get an estimate slightly better than the naive lower bound  0. (Contributed by Mario Carneiro, 13-Apr-2016.)
Hypotheses
Ref Expression
pntlem1.r  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
pntlem1.a  |-  ( ph  ->  A  e.  RR+ )
pntlem1.b  |-  ( ph  ->  B  e.  RR+ )
pntlem1.l  |-  ( ph  ->  L  e.  ( 0 (,) 1 ) )
pntlem1.d  |-  D  =  ( A  +  1 )
pntlem1.f  |-  F  =  ( ( 1  -  ( 1  /  D
) )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )
pntlem1.u  |-  ( ph  ->  U  e.  RR+ )
pntlem1.u2  |-  ( ph  ->  U  <_  A )
pntlem1.e  |-  E  =  ( U  /  D
)
pntlem1.k  |-  K  =  ( exp `  ( B  /  E ) )
pntlem1.y  |-  ( ph  ->  ( Y  e.  RR+  /\  1  <_  Y )
)
pntlem1.x  |-  ( ph  ->  ( X  e.  RR+  /\  Y  <  X ) )
pntlem1.c  |-  ( ph  ->  C  e.  RR+ )
pntlem1.w  |-  W  =  ( ( ( Y  +  ( 4  / 
( L  x.  E
) ) ) ^
2 )  +  ( ( ( X  x.  ( K ^ 2 ) ) ^ 4 )  +  ( exp `  (
( (; 3 2  x.  B
)  /  ( ( U  -  E )  x.  ( L  x.  ( E ^ 2 ) ) ) )  x.  ( ( U  x.  3 )  +  C
) ) ) ) )
pntlem1.z  |-  ( ph  ->  Z  e.  ( W [,) +oo ) )
pntlem1.m  |-  M  =  ( ( |_ `  ( ( log `  X
)  /  ( log `  K ) ) )  +  1 )
pntlem1.n  |-  N  =  ( |_ `  (
( ( log `  Z
)  /  ( log `  K ) )  / 
2 ) )
pntlem1.U  |-  ( ph  ->  A. z  e.  ( Y [,) +oo )
( abs `  (
( R `  z
)  /  z ) )  <_  U )
pntlem1.K  |-  ( ph  ->  A. y  e.  ( X (,) +oo ) E. z  e.  RR+  (
( y  <  z  /\  ( ( 1  +  ( L  x.  E
) )  x.  z
)  <  ( K  x.  y ) )  /\  A. u  e.  ( z [,] ( ( 1  +  ( L  x.  E ) )  x.  z ) ) ( abs `  ( ( R `  u )  /  u ) )  <_  E ) )
Assertion
Ref Expression
pntlemf  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  <_  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )
Distinct variable groups:    z, C    y, n, z, u, L   
n, K, y, z   
n, M, z    ph, n    n, N, z    R, n, u, y, z    U, n, z    n, W, z   
n, X, y, z   
n, Y, z    n, a, u, y, z, E   
n, Z, u, z
Allowed substitution hints:    ph( y, z, u, a)    A( y, z, u, n, a)    B( y, z, u, n, a)    C( y, u, n, a)    D( y, z, u, n, a)    R( a)    U( y, u, a)    F( y, z, u, n, a)    K( u, a)    L( a)    M( y, u, a)    N( y, u, a)    W( y, u, a)    X( u, a)    Y( y, u, a)    Z( y, a)

Proof of Theorem pntlemf
Dummy variables  j  m are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pntlem1.r . . . . . . 7  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
2 pntlem1.a . . . . . . 7  |-  ( ph  ->  A  e.  RR+ )
3 pntlem1.b . . . . . . 7  |-  ( ph  ->  B  e.  RR+ )
4 pntlem1.l . . . . . . 7  |-  ( ph  ->  L  e.  ( 0 (,) 1 ) )
5 pntlem1.d . . . . . . 7  |-  D  =  ( A  +  1 )
6 pntlem1.f . . . . . . 7  |-  F  =  ( ( 1  -  ( 1  /  D
) )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )
7 pntlem1.u . . . . . . 7  |-  ( ph  ->  U  e.  RR+ )
8 pntlem1.u2 . . . . . . 7  |-  ( ph  ->  U  <_  A )
9 pntlem1.e . . . . . . 7  |-  E  =  ( U  /  D
)
10 pntlem1.k . . . . . . 7  |-  K  =  ( exp `  ( B  /  E ) )
111, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 22976 . . . . . 6  |-  ( ph  ->  ( E  e.  RR+  /\  K  e.  RR+  /\  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E )  e.  RR+ ) ) )
1211simp3d 1002 . . . . 5  |-  ( ph  ->  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E
)  e.  RR+ )
)
1312simp3d 1002 . . . 4  |-  ( ph  ->  ( U  -  E
)  e.  RR+ )
141, 2, 3, 4, 5, 6pntlemd 22975 . . . . . . . 8  |-  ( ph  ->  ( L  e.  RR+  /\  D  e.  RR+  /\  F  e.  RR+ ) )
1514simp1d 1000 . . . . . . 7  |-  ( ph  ->  L  e.  RR+ )
1611simp1d 1000 . . . . . . . 8  |-  ( ph  ->  E  e.  RR+ )
17 2z 10788 . . . . . . . 8  |-  2  e.  ZZ
18 rpexpcl 12000 . . . . . . . 8  |-  ( ( E  e.  RR+  /\  2  e.  ZZ )  ->  ( E ^ 2 )  e.  RR+ )
1916, 17, 18sylancl 662 . . . . . . 7  |-  ( ph  ->  ( E ^ 2 )  e.  RR+ )
2015, 19rpmulcld 11153 . . . . . 6  |-  ( ph  ->  ( L  x.  ( E ^ 2 ) )  e.  RR+ )
21 3nn0 10707 . . . . . . . . 9  |-  3  e.  NN0
22 2nn 10589 . . . . . . . . 9  |-  2  e.  NN
2321, 22decnncl 10878 . . . . . . . 8  |- ; 3 2  e.  NN
24 nnrp 11110 . . . . . . . 8  |-  (; 3 2  e.  NN  -> ; 3
2  e.  RR+ )
2523, 24ax-mp 5 . . . . . . 7  |- ; 3 2  e.  RR+
26 rpmulcl 11122 . . . . . . 7  |-  ( (; 3
2  e.  RR+  /\  B  e.  RR+ )  ->  (; 3 2  x.  B )  e.  RR+ )
2725, 3, 26sylancr 663 . . . . . 6  |-  ( ph  ->  (; 3 2  x.  B
)  e.  RR+ )
2820, 27rpdivcld 11154 . . . . 5  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  RR+ )
29 pntlem1.y . . . . . . . . . 10  |-  ( ph  ->  ( Y  e.  RR+  /\  1  <_  Y )
)
30 pntlem1.x . . . . . . . . . 10  |-  ( ph  ->  ( X  e.  RR+  /\  Y  <  X ) )
31 pntlem1.c . . . . . . . . . 10  |-  ( ph  ->  C  e.  RR+ )
32 pntlem1.w . . . . . . . . . 10  |-  W  =  ( ( ( Y  +  ( 4  / 
( L  x.  E
) ) ) ^
2 )  +  ( ( ( X  x.  ( K ^ 2 ) ) ^ 4 )  +  ( exp `  (
( (; 3 2  x.  B
)  /  ( ( U  -  E )  x.  ( L  x.  ( E ^ 2 ) ) ) )  x.  ( ( U  x.  3 )  +  C
) ) ) ) )
33 pntlem1.z . . . . . . . . . 10  |-  ( ph  ->  Z  e.  ( W [,) +oo ) )
341, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33pntlemb 22978 . . . . . . . . 9  |-  ( ph  ->  ( Z  e.  RR+  /\  ( 1  <  Z  /\  _e  <_  ( sqr `  Z )  /\  ( sqr `  Z )  <_ 
( Z  /  Y
) )  /\  (
( 4  /  ( L  x.  E )
)  <_  ( sqr `  Z )  /\  (
( ( log `  X
)  /  ( log `  K ) )  +  2 )  <_  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 )  /\  (
( U  x.  3 )  +  C )  <_  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) ) )
3534simp1d 1000 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR+ )
3635rpred 11137 . . . . . . 7  |-  ( ph  ->  Z  e.  RR )
3734simp2d 1001 . . . . . . . 8  |-  ( ph  ->  ( 1  <  Z  /\  _e  <_  ( sqr `  Z )  /\  ( sqr `  Z )  <_ 
( Z  /  Y
) ) )
3837simp1d 1000 . . . . . . 7  |-  ( ph  ->  1  <  Z )
3936, 38rplogcld 22210 . . . . . 6  |-  ( ph  ->  ( log `  Z
)  e.  RR+ )
40 rpexpcl 12000 . . . . . 6  |-  ( ( ( log `  Z
)  e.  RR+  /\  2  e.  ZZ )  ->  (
( log `  Z
) ^ 2 )  e.  RR+ )
4139, 17, 40sylancl 662 . . . . 5  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  RR+ )
4228, 41rpmulcld 11153 . . . 4  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  e.  RR+ )
4313, 42rpmulcld 11153 . . 3  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR+ )
4443rpred 11137 . 2  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR )
4515, 16rpmulcld 11153 . . . . . . 7  |-  ( ph  ->  ( L  x.  E
)  e.  RR+ )
46 8re 10516 . . . . . . . 8  |-  8  e.  RR
47 8pos 10532 . . . . . . . 8  |-  0  <  8
4846, 47elrpii 11104 . . . . . . 7  |-  8  e.  RR+
49 rpdivcl 11123 . . . . . . 7  |-  ( ( ( L  x.  E
)  e.  RR+  /\  8  e.  RR+ )  ->  (
( L  x.  E
)  /  8 )  e.  RR+ )
5045, 48, 49sylancl 662 . . . . . 6  |-  ( ph  ->  ( ( L  x.  E )  /  8
)  e.  RR+ )
5150, 39rpmulcld 11153 . . . . 5  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) )  e.  RR+ )
5213, 51rpmulcld 11153 . . . 4  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  e.  RR+ )
5352rpred 11137 . . 3  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  e.  RR )
54 pntlem1.m . . . . . . . 8  |-  M  =  ( ( |_ `  ( ( log `  X
)  /  ( log `  K ) ) )  +  1 )
55 pntlem1.n . . . . . . . 8  |-  N  =  ( |_ `  (
( ( log `  Z
)  /  ( log `  K ) )  / 
2 ) )
561, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemg 22979 . . . . . . 7  |-  ( ph  ->  ( M  e.  NN  /\  N  e.  ( ZZ>= `  M )  /\  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 )  <_  ( N  -  M )
) )
5756simp1d 1000 . . . . . 6  |-  ( ph  ->  M  e.  NN )
5856simp2d 1001 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
59 eluznn 11035 . . . . . 6  |-  ( ( M  e.  NN  /\  N  e.  ( ZZ>= `  M ) )  ->  N  e.  NN )
6057, 58, 59syl2anc 661 . . . . 5  |-  ( ph  ->  N  e.  NN )
6160nnred 10447 . . . 4  |-  ( ph  ->  N  e.  RR )
6257nnred 10447 . . . 4  |-  ( ph  ->  M  e.  RR )
6361, 62resubcld 9886 . . 3  |-  ( ph  ->  ( N  -  M
)  e.  RR )
6453, 63remulcld 9524 . 2  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( N  -  M ) )  e.  RR )
65 fzfid 11911 . . 3  |-  ( ph  ->  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
667rpred 11137 . . . . . 6  |-  ( ph  ->  U  e.  RR )
67 elfznn 11594 . . . . . 6  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  NN )
68 nndivre 10467 . . . . . 6  |-  ( ( U  e.  RR  /\  n  e.  NN )  ->  ( U  /  n
)  e.  RR )
6966, 67, 68syl2an 477 . . . . 5  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  RR )
7035adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  RR+ )
7167adantl 466 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  NN )
7271nnrpd 11136 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  RR+ )
7370, 72rpdivcld 11154 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  /  n )  e.  RR+ )
741pntrf 22944 . . . . . . . . . 10  |-  R : RR+
--> RR
7574ffvelrni 5950 . . . . . . . . 9  |-  ( ( Z  /  n )  e.  RR+  ->  ( R `
 ( Z  /  n ) )  e.  RR )
7673, 75syl 16 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( R `  ( Z  /  n
) )  e.  RR )
7776, 70rerpdivcld 11164 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  RR )
7877recnd 9522 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  CC )
7978abscld 13039 . . . . 5  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  RR )
8069, 79resubcld 9886 . . . 4  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  e.  RR )
8172relogcld 22204 . . . 4  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  RR )
8280, 81remulcld 9524 . . 3  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
8365, 82fsumrecl 13328 . 2  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR )
8445rpcnd 11139 . . . . . . . . 9  |-  ( ph  ->  ( L  x.  E
)  e.  CC )
8511simp2d 1001 . . . . . . . . . . . . 13  |-  ( ph  ->  K  e.  RR+ )
8685rpred 11137 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  RR )
8712simp2d 1001 . . . . . . . . . . . 12  |-  ( ph  ->  1  <  K )
8886, 87rplogcld 22210 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  K
)  e.  RR+ )
8939, 88rpdivcld 11154 . . . . . . . . . 10  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  e.  RR+ )
9089rpcnd 11139 . . . . . . . . 9  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  e.  CC )
91 rpcnne0 11118 . . . . . . . . . 10  |-  ( 8  e.  RR+  ->  ( 8  e.  CC  /\  8  =/=  0 ) )
9248, 91mp1i 12 . . . . . . . . 9  |-  ( ph  ->  ( 8  e.  CC  /\  8  =/=  0 ) )
93 4re 10508 . . . . . . . . . . 11  |-  4  e.  RR
94 4pos 10527 . . . . . . . . . . 11  |-  0  <  4
9593, 94elrpii 11104 . . . . . . . . . 10  |-  4  e.  RR+
96 rpcnne0 11118 . . . . . . . . . 10  |-  ( 4  e.  RR+  ->  ( 4  e.  CC  /\  4  =/=  0 ) )
9795, 96mp1i 12 . . . . . . . . 9  |-  ( ph  ->  ( 4  e.  CC  /\  4  =/=  0 ) )
98 divmuldiv 10141 . . . . . . . . 9  |-  ( ( ( ( L  x.  E )  e.  CC  /\  ( ( log `  Z
)  /  ( log `  K ) )  e.  CC )  /\  (
( 8  e.  CC  /\  8  =/=  0 )  /\  ( 4  e.  CC  /\  4  =/=  0 ) ) )  ->  ( ( ( L  x.  E )  /  8 )  x.  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 ) )  =  ( ( ( L  x.  E )  x.  ( ( log `  Z )  /  ( log `  K ) ) )  /  ( 8  x.  4 ) ) )
9984, 90, 92, 97, 98syl22anc 1220 . . . . . . . 8  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 ) )  =  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  /  ( log `  K ) ) )  /  ( 8  x.  4 ) ) )
10010fveq2i 5801 . . . . . . . . . . . . . 14  |-  ( log `  K )  =  ( log `  ( exp `  ( B  /  E
) ) )
1013, 16rpdivcld 11154 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  /  E
)  e.  RR+ )
102101rpred 11137 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B  /  E
)  e.  RR )
103102relogefd 22209 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( log `  ( exp `  ( B  /  E ) ) )  =  ( B  /  E ) )
104100, 103syl5eq 2507 . . . . . . . . . . . . 13  |-  ( ph  ->  ( log `  K
)  =  ( B  /  E ) )
105104oveq2d 6215 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  =  ( ( log `  Z
)  /  ( B  /  E ) ) )
10639rpcnd 11139 . . . . . . . . . . . . 13  |-  ( ph  ->  ( log `  Z
)  e.  CC )
1073rpcnne0d 11146 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  e.  CC  /\  B  =/=  0 ) )
10816rpcnne0d 11146 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  e.  CC  /\  E  =/=  0 ) )
109 divdiv2 10153 . . . . . . . . . . . . 13  |-  ( ( ( log `  Z
)  e.  CC  /\  ( B  e.  CC  /\  B  =/=  0 )  /\  ( E  e.  CC  /\  E  =/=  0 ) )  -> 
( ( log `  Z
)  /  ( B  /  E ) )  =  ( ( ( log `  Z )  x.  E )  /  B ) )
110106, 107, 108, 109syl3anc 1219 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  Z
)  /  ( B  /  E ) )  =  ( ( ( log `  Z )  x.  E )  /  B ) )
111105, 110eqtrd 2495 . . . . . . . . . . 11  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  =  ( ( ( log `  Z )  x.  E
)  /  B ) )
112111oveq2d 6215 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  /  ( log `  K ) ) )  =  ( ( L  x.  E )  x.  ( ( ( log `  Z )  x.  E
)  /  B ) ) )
11316rpcnd 11139 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  CC )
114106, 113mulcld 9516 . . . . . . . . . . 11  |-  ( ph  ->  ( ( log `  Z
)  x.  E )  e.  CC )
115 divass 10122 . . . . . . . . . . 11  |-  ( ( ( L  x.  E
)  e.  CC  /\  ( ( log `  Z
)  x.  E )  e.  CC  /\  ( B  e.  CC  /\  B  =/=  0 ) )  -> 
( ( ( L  x.  E )  x.  ( ( log `  Z
)  x.  E ) )  /  B )  =  ( ( L  x.  E )  x.  ( ( ( log `  Z )  x.  E
)  /  B ) ) )
11684, 114, 107, 115syl3anc 1219 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  x.  E ) )  /  B )  =  ( ( L  x.  E )  x.  ( ( ( log `  Z )  x.  E
)  /  B ) ) )
11715rpcnd 11139 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  CC )
118117, 113, 106, 113mul4d 9691 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  x.  E ) )  =  ( ( L  x.  ( log `  Z ) )  x.  ( E  x.  E
) ) )
119113sqvald 12121 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E ^ 2 )  =  ( E  x.  E ) )
120119oveq2d 6215 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  x.  ( log `  Z ) )  x.  ( E ^ 2 ) )  =  ( ( L  x.  ( log `  Z
) )  x.  ( E  x.  E )
) )
121113sqcld 12122 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
122117, 106, 121mul32d 9689 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  x.  ( log `  Z ) )  x.  ( E ^ 2 ) )  =  ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) ) )
123118, 120, 1223eqtr2d 2501 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  x.  E ) )  =  ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) ) )
124123oveq1d 6214 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  x.  E ) )  /  B )  =  ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
) )
125112, 116, 1243eqtr2d 2501 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  /  ( log `  K ) ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
) )
126 8t4e32 10955 . . . . . . . . . 10  |-  ( 8  x.  4 )  = ; 3
2
127126a1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 8  x.  4 )  = ; 3 2 )
128125, 127oveq12d 6217 . . . . . . . 8  |-  ( ph  ->  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  /  ( log `  K ) ) )  /  ( 8  x.  4 ) )  =  ( ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
)  / ; 3 2 ) )
12920rpcnd 11139 . . . . . . . . . . 11  |-  ( ph  ->  ( L  x.  ( E ^ 2 ) )  e.  CC )
130129, 106mulcld 9516 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z ) )  e.  CC )
131 rpcnne0 11118 . . . . . . . . . . 11  |-  (; 3 2  e.  RR+  ->  (; 3 2  e.  CC  /\ ; 3
2  =/=  0 ) )
13225, 131mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  (; 3 2  e.  CC  /\ ; 3
2  =/=  0 ) )
133 divdiv1 10152 . . . . . . . . . 10  |-  ( ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z ) )  e.  CC  /\  ( B  e.  CC  /\  B  =/=  0 )  /\  (; 3 2  e.  CC  /\ ; 3 2  =/=  0
) )  ->  (
( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  B
)  / ; 3 2 )  =  ( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  ( B  x. ; 3 2 ) ) )
134130, 107, 132, 133syl3anc 1219 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
)  / ; 3 2 )  =  ( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  ( B  x. ; 3 2 ) ) )
13523nncni 10442 . . . . . . . . . . 11  |- ; 3 2  e.  CC
1363rpcnd 11139 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  CC )
137 mulcom 9478 . . . . . . . . . . 11  |-  ( (; 3
2  e.  CC  /\  B  e.  CC )  ->  (; 3 2  x.  B
)  =  ( B  x. ; 3 2 ) )
138135, 136, 137sylancr 663 . . . . . . . . . 10  |-  ( ph  ->  (; 3 2  x.  B
)  =  ( B  x. ; 3 2 ) )
139138oveq2d 6215 . . . . . . . . 9  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  (; 3 2  x.  B ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  ( B  x. ; 3 2 ) ) )
14027rpcnne0d 11146 . . . . . . . . . 10  |-  ( ph  ->  ( (; 3 2  x.  B
)  e.  CC  /\  (; 3 2  x.  B )  =/=  0 ) )
141 div23 10123 . . . . . . . . . 10  |-  ( ( ( L  x.  ( E ^ 2 ) )  e.  CC  /\  ( log `  Z )  e.  CC  /\  ( (; 3
2  x.  B )  e.  CC  /\  (; 3 2  x.  B )  =/=  0 ) )  -> 
( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  (; 3 2  x.  B ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  ( log `  Z ) ) )
142129, 106, 140, 141syl3anc 1219 . . . . . . . . 9  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  (; 3 2  x.  B ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  ( log `  Z ) ) )
143134, 139, 1423eqtr2d 2501 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
)  / ; 3 2 )  =  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  ( log `  Z ) ) )
14499, 128, 1433eqtrd 2499 . . . . . . 7  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 ) )  =  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  ( log `  Z ) ) )
145144oveq1d 6214 . . . . . 6  |-  ( ph  ->  ( ( ( ( L  x.  E )  /  8 )  x.  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 ) )  x.  ( log `  Z
) )  =  ( ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  ( log `  Z ) )  x.  ( log `  Z
) ) )
14650rpcnd 11139 . . . . . . 7  |-  ( ph  ->  ( ( L  x.  E )  /  8
)  e.  CC )
14789rpred 11137 . . . . . . . . 9  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  e.  RR )
148 4nn 10591 . . . . . . . . 9  |-  4  e.  NN
149 nndivre 10467 . . . . . . . . 9  |-  ( ( ( ( log `  Z
)  /  ( log `  K ) )  e.  RR  /\  4  e.  NN )  ->  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 )  e.  RR )
150147, 148, 149sylancl 662 . . . . . . . 8  |-  ( ph  ->  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 )  e.  RR )
151150recnd 9522 . . . . . . 7  |-  ( ph  ->  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 )  e.  CC )
152146, 106, 151mul32d 9689 . . . . . 6  |-  ( ph  ->  ( ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) )  x.  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 ) )  =  ( ( ( ( L  x.  E )  /  8 )  x.  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 ) )  x.  ( log `  Z
) ) )
153106sqvald 12121 . . . . . . . 8  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  =  ( ( log `  Z )  x.  ( log `  Z ) ) )
154153oveq2d 6215 . . . . . . 7  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
)  x.  ( log `  Z ) ) ) )
15528rpcnd 11139 . . . . . . . 8  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  CC )
156155, 106, 106mulassd 9519 . . . . . . 7  |-  ( ph  ->  ( ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  ( log `  Z ) )  x.  ( log `  Z
) )  =  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
)  x.  ( log `  Z ) ) ) )
157154, 156eqtr4d 2498 . . . . . 6  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  =  ( ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  ( log `  Z ) )  x.  ( log `  Z
) ) )
158145, 152, 1573eqtr4d 2505 . . . . 5  |-  ( ph  ->  ( ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) )  x.  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 ) )  =  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )
15956simp3d 1002 . . . . . 6  |-  ( ph  ->  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 )  <_ 
( N  -  M
) )
160150, 63, 51lemul2d 11177 . . . . . 6  |-  ( ph  ->  ( ( ( ( log `  Z )  /  ( log `  K
) )  /  4
)  <_  ( N  -  M )  <->  ( (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) )  x.  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 ) )  <_  ( ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) )  x.  ( N  -  M )
) ) )
161159, 160mpbid 210 . . . . 5  |-  ( ph  ->  ( ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) )  x.  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 ) )  <_ 
( ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) )  x.  ( N  -  M )
) )
162158, 161eqbrtrrd 4421 . . . 4  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  <_  ( (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) )  x.  ( N  -  M
) ) )
16342rpred 11137 . . . . 5  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  e.  RR )
16451rpred 11137 . . . . . 6  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) )  e.  RR )
165164, 63remulcld 9524 . . . . 5  |-  ( ph  ->  ( ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) )  x.  ( N  -  M )
)  e.  RR )
166163, 165, 13lemul2d 11177 . . . 4  |-  ( ph  ->  ( ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  <_  ( (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) )  x.  ( N  -  M
) )  <->  ( ( U  -  E )  x.  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  <_  (
( U  -  E
)  x.  ( ( ( ( L  x.  E )  /  8
)  x.  ( log `  Z ) )  x.  ( N  -  M
) ) ) ) )
167162, 166mpbid 210 . . 3  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  <_  (
( U  -  E
)  x.  ( ( ( ( L  x.  E )  /  8
)  x.  ( log `  Z ) )  x.  ( N  -  M
) ) ) )
16813rpcnd 11139 . . . 4  |-  ( ph  ->  ( U  -  E
)  e.  CC )
16951rpcnd 11139 . . . 4  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) )  e.  CC )
17063recnd 9522 . . . 4  |-  ( ph  ->  ( N  -  M
)  e.  CC )
171168, 169, 170mulassd 9519 . . 3  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( N  -  M ) )  =  ( ( U  -  E )  x.  ( ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) )  x.  ( N  -  M )
) ) )
172167, 171breqtrrd 4425 . 2  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  <_  (
( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  x.  ( N  -  M ) ) )
173 fzfid 11911 . . . 4  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
17460nnzd 10856 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
17585, 174rpexpcld 12147 . . . . . . . . . . 11  |-  ( ph  ->  ( K ^ N
)  e.  RR+ )
17635, 175rpdivcld 11154 . . . . . . . . . 10  |-  ( ph  ->  ( Z  /  ( K ^ N ) )  e.  RR+ )
177176rprege0d 11144 . . . . . . . . 9  |-  ( ph  ->  ( ( Z  / 
( K ^ N
) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ N ) ) ) )
178 flge0nn0 11782 . . . . . . . . 9  |-  ( ( ( Z  /  ( K ^ N ) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ N ) ) )  ->  ( |_ `  ( Z  /  ( K ^ N ) ) )  e.  NN0 )
179 nn0p1nn 10729 . . . . . . . . 9  |-  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  e.  NN0  ->  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  NN )
180177, 178, 1793syl 20 . . . . . . . 8  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  NN )
181 nnuz 11006 . . . . . . . 8  |-  NN  =  ( ZZ>= `  1 )
182180, 181syl6eleq 2552 . . . . . . 7  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  ( ZZ>= `  1
) )
183 fzss1 11613 . . . . . . 7  |-  ( ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  ( ZZ>= `  1 )  ->  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
184182, 183syl 16 . . . . . 6  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
185184sselda 3463 . . . . 5  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
186185, 82syldan 470 . . . 4  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
187173, 186fsumrecl 13328 . . 3  |-  ( ph  -> 
sum_ n  e.  (
( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR )
188 eluzfz2 11575 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ( M ... N ) )
18958, 188syl 16 . . . 4  |-  ( ph  ->  N  e.  ( M ... N ) )
190 oveq1 6206 . . . . . . . 8  |-  ( m  =  M  ->  (
m  -  M )  =  ( M  -  M ) )
191190oveq2d 6215 . . . . . . 7  |-  ( m  =  M  ->  (
( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  =  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( M  -  M ) ) )
192 oveq2 6207 . . . . . . . . . . . 12  |-  ( m  =  M  ->  ( K ^ m )  =  ( K ^ M
) )
193192oveq2d 6215 . . . . . . . . . . 11  |-  ( m  =  M  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ M ) ) )
194193fveq2d 5802 . . . . . . . . . 10  |-  ( m  =  M  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^ M ) ) ) )
195194oveq1d 6214 . . . . . . . . 9  |-  ( m  =  M  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 ) )
196195oveq1d 6214 . . . . . . . 8  |-  ( m  =  M  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
197196sumeq1d 13295 . . . . . . 7  |-  ( m  =  M  ->  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) )  = 
sum_ n  e.  (
( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
198191, 197breq12d 4412 . . . . . 6  |-  ( m  =  M  ->  (
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  <->  ( (
( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( M  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) )
199198imbi2d 316 . . . . 5  |-  ( m  =  M  ->  (
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( m  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  <-> 
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( M  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
200 oveq1 6206 . . . . . . . 8  |-  ( m  =  j  ->  (
m  -  M )  =  ( j  -  M ) )
201200oveq2d 6215 . . . . . . 7  |-  ( m  =  j  ->  (
( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  =  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( j  -  M ) ) )
202 oveq2 6207 . . . . . . . . . . . 12  |-  ( m  =  j  ->  ( K ^ m )  =  ( K ^ j
) )
203202oveq2d 6215 . . . . . . . . . . 11  |-  ( m  =  j  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ j ) ) )
204203fveq2d 5802 . . . . . . . . . 10  |-  ( m  =  j  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^
j ) ) ) )
205204oveq1d 6214 . . . . . . . . 9  |-  ( m  =  j  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) )
206205oveq1d 6214 . . . . . . . 8  |-  ( m  =  j  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
207206sumeq1d 13295 . . . . . . 7  |-  ( m  =  j  ->  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) )  = 
sum_ n  e.  (
( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
208201, 207breq12d 4412 . . . . . 6  |-  ( m  =  j  ->  (
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  <->  ( (
( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) )
209208imbi2d 316 . . . . 5  |-  ( m  =  j  ->  (
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( m  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  <-> 
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
210 oveq1 6206 . . . . . . . 8  |-  ( m  =  ( j  +  1 )  ->  (
m  -  M )  =  ( ( j  +  1 )  -  M ) )
211210oveq2d 6215 . . . . . . 7  |-  ( m  =  ( j  +  1 )  ->  (
( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  =  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( ( j  +  1 )  -  M ) ) )
212 oveq2 6207 . . . . . . . . . . . 12  |-  ( m  =  ( j  +  1 )  ->  ( K ^ m )  =  ( K ^ (
j  +  1 ) ) )
213212oveq2d 6215 . . . . . . . . . . 11  |-  ( m  =  ( j  +  1 )  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ ( j  +  1 ) ) ) )
214213fveq2d 5802 . . . . . . . . . 10  |-  ( m  =  ( j  +  1 )  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) ) )
215214oveq1d 6214 . . . . . . . . 9  |-  ( m  =  ( j  +  1 )  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) )
216215oveq1d 6214 . . . . . . . 8  |-  ( m  =  ( j  +  1 )  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
217216sumeq1d 13295 . . . . . . 7  |-  ( m  =  ( j  +  1 )  ->  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) )  = 
sum_ n  e.  (
( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
218211, 217breq12d 4412 . . . . . 6  |-  ( m  =  ( j  +  1 )  ->  (
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  <->  ( (
( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( ( j  +  1 )  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) )
219218imbi2d 316 . . . . 5  |-  ( m  =  ( j  +  1 )  ->  (
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( m  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  <-> 
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( ( j  +  1 )  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
220 oveq1 6206 . . . . . . . 8  |-  ( m  =  N  ->  (
m  -  M )  =  ( N  -  M ) )
221220oveq2d 6215 . . . . . . 7  |-  ( m  =  N  ->  (
( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  =  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( N  -  M ) ) )
222 oveq2 6207 . . . . . . . . . . . 12  |-  ( m  =  N  ->  ( K ^ m )  =  ( K ^ N
) )
223222oveq2d 6215 . . . . . . . . . . 11  |-  ( m  =  N  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ N ) ) )
224223fveq2d 5802 . . . . . . . . . 10  |-  ( m  =  N  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^ N ) ) ) )
225224oveq1d 6214 . . . . . . . . 9  |-  ( m  =  N  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 ) )
226225oveq1d 6214 . . . . . . . 8  |-  ( m  =  N  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
227226sumeq1d 13295 . . . . . . 7  |-  ( m  =  N  ->  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) )  = 
sum_ n  e.  (
( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
228221, 227breq12d 4412 . . . . . 6  |-  ( m  =  N  ->  (
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( m  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  <->  ( (
( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( N  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) )
229228imbi2d 316 . . . . 5  |-  ( m  =  N  ->  (
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( m  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ m
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  <-> 
( ph  ->  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( N  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
23057nncnd 10448 . . . . . . . . . 10  |-  ( ph  ->  M  e.  CC )
231230subidd 9817 . . . . . . . . 9  |-  ( ph  ->  ( M  -  M
)  =  0 )
232231oveq2d 6215 . . . . . . . 8  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( M  -  M ) )  =  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) ) )  x.  0 ) )
23352rpcnd 11139 . . . . . . . . 9  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  e.  CC )
234233mul01d 9678 . . . . . . . 8  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  0 )  =  0 )
235232, 234eqtrd 2495 . . . . . . 7  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( M  -  M ) )  =  0 )
236 fzfid 11911 . . . . . . . 8  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
23757nnzd 10856 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ZZ )
23885, 237rpexpcld 12147 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( K ^ M
)  e.  RR+ )
23935, 238rpdivcld 11154 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Z  /  ( K ^ M ) )  e.  RR+ )
240239rprege0d 11144 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Z  / 
( K ^ M
) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ M ) ) ) )
241 flge0nn0 11782 . . . . . . . . . . . . 13  |-  ( ( ( Z  /  ( K ^ M ) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ M ) ) )  ->  ( |_ `  ( Z  /  ( K ^ M ) ) )  e.  NN0 )
242 nn0p1nn 10729 . . . . . . . . . . . . 13  |-  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  e.  NN0  ->  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  NN )
243240, 241, 2423syl 20 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  NN )
244243, 181syl6eleq 2552 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  ( ZZ>= `  1
) )
245 fzss1 11613 . . . . . . . . . . 11  |-  ( ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  ( ZZ>= `  1 )  ->  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
246244, 245syl 16 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
247246sselda 3463 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
248247, 82syldan 470 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
249 elfzle2 11571 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  <_  ( |_ `  ( Z  /  Y ) ) )
250249adantl 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  <_  ( |_ `  ( Z  /  Y ) ) )
25129simpld 459 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  e.  RR+ )
25235, 251rpdivcld 11154 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Z  /  Y
)  e.  RR+ )
253252rpred 11137 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Z  /  Y
)  e.  RR )
254 elfzelz 11569 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  ZZ )
255 flge 11771 . . . . . . . . . . . . 13  |-  ( ( ( Z  /  Y
)  e.  RR  /\  n  e.  ZZ )  ->  ( n  <_  ( Z  /  Y )  <->  n  <_  ( |_ `  ( Z  /  Y ) ) ) )
256253, 254, 255syl2an 477 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( n  <_  ( Z  /  Y
)  <->  n  <_  ( |_
`  ( Z  /  Y ) ) ) )
257250, 256mpbird 232 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  <_  ( Z  /  Y ) )
25871, 257jca 532 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( n  e.  NN  /\  n  <_ 
( Z  /  Y
) ) )
259 pntlem1.U . . . . . . . . . . 11  |-  ( ph  ->  A. z  e.  ( Y [,) +oo )
( abs `  (
( R `  z
)  /  z ) )  <_  U )
2601, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55, 259pntlemn 22981 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  NN  /\  n  <_ 
( Z  /  Y
) ) )  -> 
0  <_  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) ) )
261258, 260syldan 470 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  0  <_  ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
262247, 261syldan 470 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  0  <_  ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
263236, 248, 262fsumge0 13375 . . . . . . 7  |-  ( ph  ->  0  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )
264235, 263eqbrtrd 4419 . . . . . 6  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( M  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
265264a1i 11 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( M  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) ) )
266 pntlem1.K . . . . . . . . . 10  |-  ( ph  ->  A. y  e.  ( X (,) +oo ) E. z  e.  RR+  (
( y  <  z  /\  ( ( 1  +  ( L  x.  E
) )  x.  z
)  <  ( K  x.  y ) )  /\  A. u  e.  ( z [,] ( ( 1  +  ( L  x.  E ) )  x.  z ) ) ( abs `  ( ( R `  u )  /  u ) )  <_  E ) )
267 eqid 2454 . . . . . . . . . 10  |-  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  =  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )
2681, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55, 259, 266, 267pntlemi 22985 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  / 
( K ^ j
) ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )
26952adantr 465 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  e.  RR+ )
270269rpred 11137 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  e.  RR )
271 elfzoelz 11669 . . . . . . . . . . . . . 14  |-  ( j  e.  ( M..^ N
)  ->  j  e.  ZZ )
272271adantl 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  j  e.  ZZ )
273272zred 10857 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  j  e.  RR )
27457adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  M  e.  NN )
275274nnred 10447 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  M  e.  RR )
276273, 275resubcld 9886 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( j  -  M )  e.  RR )
277270, 276remulcld 9524 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) )  e.  RR )
278 fzfid 11911 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  e.  Fin )
279 ssun1 3626 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  C_  ( (
( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^ j ) ) ) )  u.  (
( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) )
28036adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Z  e.  RR )
28185adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  K  e.  RR+ )
282272peano2zd 10860 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( j  +  1 )  e.  ZZ )
283281, 282rpexpcld 12147 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
( j  +  1 ) )  e.  RR+ )
284280, 283rerpdivcld 11164 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ (
j  +  1 ) ) )  e.  RR )
285281, 272rpexpcld 12147 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
j )  e.  RR+ )
286280, 285rerpdivcld 11164 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ j
) )  e.  RR )
28786adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  K  e.  RR )
288 1re 9495 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR
289 ltle 9573 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR  /\  K  e.  RR )  ->  ( 1  <  K  ->  1  <_  K )
)
290288, 86, 289sylancr 663 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 1  <  K  ->  1  <_  K )
)
29187, 290mpd 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  <_  K )
292291adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  1  <_  K
)
293 uzid 10985 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ZZ  ->  j  e.  ( ZZ>= `  j )
)
294 peano2uz 11018 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ZZ>= `  j
)  ->  ( j  +  1 )  e.  ( ZZ>= `  j )
)
295272, 293, 2943syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( j  +  1 )  e.  (
ZZ>= `  j ) )
296287, 292, 295leexp2ad 12156 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
j )  <_  ( K ^ ( j  +  1 ) ) )
29735adantr 465 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Z  e.  RR+ )
298285, 283, 297lediv2d 11161 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( K ^ j )  <_ 
( K ^ (
j  +  1 ) )  <->  ( Z  / 
( K ^ (
j  +  1 ) ) )  <_  ( Z  /  ( K ^
j ) ) ) )
299296, 298mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ (
j  +  1 ) ) )  <_  ( Z  /  ( K ^
j ) ) )
300 flword2 11777 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Z  /  ( K ^ ( j  +  1 ) ) )  e.  RR  /\  ( Z  /  ( K ^
j ) )  e.  RR  /\  ( Z  /  ( K ^
( j  +  1 ) ) )  <_ 
( Z  /  ( K ^ j ) ) )  ->  ( |_ `  ( Z  /  ( K ^ j ) ) )  e.  ( ZZ>= `  ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) ) ) )
301284, 286, 299, 300syl3anc 1219 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  ( K ^ j ) ) )  e.  ( ZZ>= `  ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) ) ) )
302 eluzp1p1 10996 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  ( Z  /  ( K ^
j ) ) )  e.  ( ZZ>= `  ( |_ `  ( Z  / 
( K ^ (
j  +  1 ) ) ) ) )  ->  ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 )  e.  (
ZZ>= `  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ) )
303301, 302syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 )  e.  (
ZZ>= `  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ) )
304286flcld 11764 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  ( K ^ j ) ) )  e.  ZZ )
305252adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  /  Y )  e.  RR+ )
306305rpred 11137 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  /  Y )  e.  RR )
307306flcld 11764 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  Y
) )  e.  ZZ )
308251adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  e.  RR+ )
309308rpred 11137 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  e.  RR )
310285rpred 11137 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
j )  e.  RR )
31130simpld 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  X  e.  RR+ )
312311rpred 11137 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  X  e.  RR )
313312adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  X  e.  RR )
31430simprd 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Y  <  X )
315314adantr 465 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  <  X
)
316 elfzofz 11683 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  ( M..^ N
)  ->  j  e.  ( M ... N ) )
3171, 2, 3, 4, 5, 6, 7, 8, 9, 10, 29, 30, 31, 32, 33, 54, 55pntlemh 22980 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( M ... N ) )  ->  ( X  <  ( K ^ j
)  /\  ( K ^ j )  <_ 
( sqr `  Z
) ) )
318316, 317sylan2 474 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( X  < 
( K ^ j
)  /\  ( K ^ j )  <_ 
( sqr `  Z
) ) )
319318simpld 459 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  X  <  ( K ^ j ) )
320309, 313, 310, 315, 319lttrd 9642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  <  ( K ^ j ) )
321309, 310, 320ltled 9632 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  <_  ( K ^ j ) )
322308, 285, 297lediv2d 11161 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Y  <_ 
( K ^ j
)  <->  ( Z  / 
( K ^ j
) )  <_  ( Z  /  Y ) ) )
323321, 322mpbid 210 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ j
) )  <_  ( Z  /  Y ) )
324 flwordi 11776 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Z  /  ( K ^ j ) )  e.  RR  /\  ( Z  /  Y )  e.  RR  /\  ( Z  /  ( K ^
j ) )  <_ 
( Z  /  Y
) )  ->  ( |_ `  ( Z  / 
( K ^ j
) ) )  <_ 
( |_ `  ( Z  /  Y ) ) )
325286, 306, 323, 324syl3anc 1219 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  ( K ^ j ) ) )  <_  ( |_ `  ( Z  /  Y
) ) )
326 eluz2 10977 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  ( Z  /  Y ) )  e.  ( ZZ>= `  ( |_ `  ( Z  / 
( K ^ j
) ) ) )  <-> 
( ( |_ `  ( Z  /  ( K ^ j ) ) )  e.  ZZ  /\  ( |_ `  ( Z  /  Y ) )  e.  ZZ  /\  ( |_ `  ( Z  / 
( K ^ j
) ) )  <_ 
( |_ `  ( Z  /  Y ) ) ) )
327304, 307, 325, 326syl3anbrc 1172 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  Y
) )  e.  (
ZZ>= `  ( |_ `  ( Z  /  ( K ^ j ) ) ) ) )
328 fzsplit2 11590 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 )  e.  ( ZZ>= `  (
( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) )  /\  ( |_ `  ( Z  /  Y
) )  e.  (
ZZ>= `  ( |_ `  ( Z  /  ( K ^ j ) ) ) ) )  -> 
( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  =  ( ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  u.  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ) )
329303, 327, 328syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  =  ( ( ( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^ j ) ) ) )  u.  (
( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ) )
330279, 329syl5sseqr 3512 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  C_  ( (
( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
331297, 283rpdivcld 11154 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ (
j  +  1 ) ) )  e.  RR+ )
332331rprege0d 11144 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( Z  /  ( K ^
( j  +  1 ) ) )  e.  RR  /\  0  <_ 
( Z  /  ( K ^ ( j  +  1 ) ) ) ) )
333 flge0nn0 11782 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Z  /  ( K ^ ( j  +  1 ) ) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  ->  ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  e.  NN0 )
334 nn0p1nn 10729 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  e.  NN0  ->  ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 )  e.  NN )
335332, 333, 3343syl 20 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 )  e.  NN )
336335, 181syl6eleq 2552 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 )  e.  (
ZZ>= `  1 ) )
337 fzss1 11613 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 )  e.  ( ZZ>= `  1 )  ->  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
338336, 337syl 16 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  C_  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )
339330, 338sstrd 3473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  C_  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )
340339sselda 3463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( M..^ N ) )  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  / 
( K ^ j
) ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
34182adantlr 714 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( M..^ N ) )  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
342340, 341syldan 470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( M..^ N ) )  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  / 
( K ^ j
) ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
343278, 342fsumrecl 13328 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^ j ) ) ) ) ( ( ( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
344 fzfid 11911 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
345 ssun2 3627 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  C_  ( (
( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^ j ) ) ) )  u.  (
( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) )
346345, 329syl5sseqr 3512 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  C_  ( (
( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
347346, 338sstrd 3473 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  C_  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )
348347sselda 3463 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( M..^ N ) )  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
349348, 341syldan 470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( M..^ N ) )  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
350344, 349fsumrecl 13328 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR )
351 le2add 9931 . . . . . . . . . 10  |-  ( ( ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  e.  RR  /\  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( j  -  M ) )  e.  RR )  /\  ( sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^ j ) ) ) ) ( ( ( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR  /\ 
sum_ n  e.  (
( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR ) )  ->  (
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  / 
( K ^ j
) ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) )  /\  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( j  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )  -> 
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  +  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) ) )  <_ 
( sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^ j ) ) ) ) ( ( ( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  +  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
352270, 277, 343, 350, 351syl22anc 1220 . . . . . . . . 9  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) )  /\  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( j  -  M ) )  <_  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )  -> 
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  +  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) ) )  <_ 
( sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^ j ) ) ) ) ( ( ( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  +  sum_ n  e.  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
353268, 352mpand 675 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) )  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) )  -> 
( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  +  ( ( ( U  -  E
)  x.  ( ( ( L  x.  E
)  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) ) )  <_ 
( sum_ n  e.  (