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

Theorem pntlemf 20754
Description: Lemma for pnt 20763. Add up the pieces in pntlemi 20753 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 20744 . . . . . 6  |-  ( ph  ->  ( E  e.  RR+  /\  K  e.  RR+  /\  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E )  e.  RR+ ) ) )
1211simp3d 969 . . . . 5  |-  ( ph  ->  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E
)  e.  RR+ )
)
1312simp3d 969 . . . 4  |-  ( ph  ->  ( U  -  E
)  e.  RR+ )
141, 2, 3, 4, 5, 6pntlemd 20743 . . . . . . . 8  |-  ( ph  ->  ( L  e.  RR+  /\  D  e.  RR+  /\  F  e.  RR+ ) )
1514simp1d 967 . . . . . . 7  |-  ( ph  ->  L  e.  RR+ )
1611simp1d 967 . . . . . . . 8  |-  ( ph  ->  E  e.  RR+ )
17 2z 10054 . . . . . . . 8  |-  2  e.  ZZ
18 rpexpcl 11122 . . . . . . . 8  |-  ( ( E  e.  RR+  /\  2  e.  ZZ )  ->  ( E ^ 2 )  e.  RR+ )
1916, 17, 18sylancl 643 . . . . . . 7  |-  ( ph  ->  ( E ^ 2 )  e.  RR+ )
2015, 19rpmulcld 10406 . . . . . 6  |-  ( ph  ->  ( L  x.  ( E ^ 2 ) )  e.  RR+ )
21 3nn0 9983 . . . . . . . . 9  |-  3  e.  NN0
22 2nn 9877 . . . . . . . . 9  |-  2  e.  NN
2321, 22decnncl 10137 . . . . . . . 8  |- ; 3 2  e.  NN
24 nnrp 10363 . . . . . . . 8  |-  (; 3 2  e.  NN  -> ; 3
2  e.  RR+ )
2523, 24ax-mp 8 . . . . . . 7  |- ; 3 2  e.  RR+
26 rpmulcl 10375 . . . . . . 7  |-  ( (; 3
2  e.  RR+  /\  B  e.  RR+ )  ->  (; 3 2  x.  B )  e.  RR+ )
2725, 3, 26sylancr 644 . . . . . 6  |-  ( ph  ->  (; 3 2  x.  B
)  e.  RR+ )
2820, 27rpdivcld 10407 . . . . 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 20746 . . . . . . . . 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 967 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR+ )
3635rpred 10390 . . . . . . 7  |-  ( ph  ->  Z  e.  RR )
3734simp2d 968 . . . . . . . 8  |-  ( ph  ->  ( 1  <  Z  /\  _e  <_  ( sqr `  Z )  /\  ( sqr `  Z )  <_ 
( Z  /  Y
) ) )
3837simp1d 967 . . . . . . 7  |-  ( ph  ->  1  <  Z )
3936, 38rplogcld 19980 . . . . . 6  |-  ( ph  ->  ( log `  Z
)  e.  RR+ )
40 rpexpcl 11122 . . . . . 6  |-  ( ( ( log `  Z
)  e.  RR+  /\  2  e.  ZZ )  ->  (
( log `  Z
) ^ 2 )  e.  RR+ )
4139, 17, 40sylancl 643 . . . . 5  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  RR+ )
4228, 41rpmulcld 10406 . . . 4  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  e.  RR+ )
4313, 42rpmulcld 10406 . . 3  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR+ )
4443rpred 10390 . 2  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR )
4515, 16rpmulcld 10406 . . . . . . 7  |-  ( ph  ->  ( L  x.  E
)  e.  RR+ )
46 8re 9824 . . . . . . . 8  |-  8  e.  RR
47 8pos 9836 . . . . . . . 8  |-  0  <  8
4846, 47elrpii 10357 . . . . . . 7  |-  8  e.  RR+
49 rpdivcl 10376 . . . . . . 7  |-  ( ( ( L  x.  E
)  e.  RR+  /\  8  e.  RR+ )  ->  (
( L  x.  E
)  /  8 )  e.  RR+ )
5045, 48, 49sylancl 643 . . . . . 6  |-  ( ph  ->  ( ( L  x.  E )  /  8
)  e.  RR+ )
5150, 39rpmulcld 10406 . . . . 5  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) )  e.  RR+ )
5213, 51rpmulcld 10406 . . . 4  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  e.  RR+ )
5352rpred 10390 . . 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 20747 . . . . . . 7  |-  ( ph  ->  ( M  e.  NN  /\  N  e.  ( ZZ>= `  M )  /\  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 )  <_  ( N  -  M )
) )
5756simp1d 967 . . . . . 6  |-  ( ph  ->  M  e.  NN )
5856simp2d 968 . . . . . 6  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
59 nnuz 10263 . . . . . . 7  |-  NN  =  ( ZZ>= `  1 )
6059uztrn2 10245 . . . . . 6  |-  ( ( M  e.  NN  /\  N  e.  ( ZZ>= `  M ) )  ->  N  e.  NN )
6157, 58, 60syl2anc 642 . . . . 5  |-  ( ph  ->  N  e.  NN )
6261nnred 9761 . . . 4  |-  ( ph  ->  N  e.  RR )
6357nnred 9761 . . . 4  |-  ( ph  ->  M  e.  RR )
6462, 63resubcld 9211 . . 3  |-  ( ph  ->  ( N  -  M
)  e.  RR )
6553, 64remulcld 8863 . 2  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( N  -  M ) )  e.  RR )
66 fzfid 11035 . . 3  |-  ( ph  ->  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
677rpred 10390 . . . . . 6  |-  ( ph  ->  U  e.  RR )
68 elfznn 10819 . . . . . 6  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  NN )
69 nndivre 9781 . . . . . 6  |-  ( ( U  e.  RR  /\  n  e.  NN )  ->  ( U  /  n
)  e.  RR )
7067, 68, 69syl2an 463 . . . . 5  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  RR )
7135adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  RR+ )
7268adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  NN )
7372nnrpd 10389 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  RR+ )
7471, 73rpdivcld 10407 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  /  n )  e.  RR+ )
751pntrf 20712 . . . . . . . . . 10  |-  R : RR+
--> RR
7675ffvelrni 5664 . . . . . . . . 9  |-  ( ( Z  /  n )  e.  RR+  ->  ( R `
 ( Z  /  n ) )  e.  RR )
7774, 76syl 15 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( R `  ( Z  /  n
) )  e.  RR )
7877, 71rerpdivcld 10417 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  RR )
7978recnd 8861 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  CC )
8079abscld 11918 . . . . 5  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  RR )
8170, 80resubcld 9211 . . . 4  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  e.  RR )
8273relogcld 19974 . . . 4  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  RR )
8381, 82remulcld 8863 . . 3  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
8466, 83fsumrecl 12207 . 2  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR )
8545rpcnd 10392 . . . . . . . . 9  |-  ( ph  ->  ( L  x.  E
)  e.  CC )
8611simp2d 968 . . . . . . . . . . . . 13  |-  ( ph  ->  K  e.  RR+ )
8786rpred 10390 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  RR )
8812simp2d 968 . . . . . . . . . . . 12  |-  ( ph  ->  1  <  K )
8987, 88rplogcld 19980 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  K
)  e.  RR+ )
9039, 89rpdivcld 10407 . . . . . . . . . 10  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  e.  RR+ )
9190rpcnd 10392 . . . . . . . . 9  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  e.  CC )
92 rpcnne0 10371 . . . . . . . . . 10  |-  ( 8  e.  RR+  ->  ( 8  e.  CC  /\  8  =/=  0 ) )
9348, 92mp1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 8  e.  CC  /\  8  =/=  0 ) )
94 4re 9819 . . . . . . . . . . 11  |-  4  e.  RR
95 4pos 9832 . . . . . . . . . . 11  |-  0  <  4
9694, 95elrpii 10357 . . . . . . . . . 10  |-  4  e.  RR+
97 rpcnne0 10371 . . . . . . . . . 10  |-  ( 4  e.  RR+  ->  ( 4  e.  CC  /\  4  =/=  0 ) )
9896, 97mp1i 11 . . . . . . . . 9  |-  ( ph  ->  ( 4  e.  CC  /\  4  =/=  0 ) )
99 divmuldiv 9460 . . . . . . . . 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 ) ) )
10085, 91, 93, 98, 99syl22anc 1183 . . . . . . . 8  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 ) )  =  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  /  ( log `  K ) ) )  /  ( 8  x.  4 ) ) )
10110fveq2i 5528 . . . . . . . . . . . . . 14  |-  ( log `  K )  =  ( log `  ( exp `  ( B  /  E
) ) )
1023, 16rpdivcld 10407 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( B  /  E
)  e.  RR+ )
103102rpred 10390 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( B  /  E
)  e.  RR )
104103relogefd 19979 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( log `  ( exp `  ( B  /  E ) ) )  =  ( B  /  E ) )
105101, 104syl5eq 2327 . . . . . . . . . . . . 13  |-  ( ph  ->  ( log `  K
)  =  ( B  /  E ) )
106105oveq2d 5874 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  =  ( ( log `  Z
)  /  ( B  /  E ) ) )
10739rpcnd 10392 . . . . . . . . . . . . 13  |-  ( ph  ->  ( log `  Z
)  e.  CC )
1083rpcnne0d 10399 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  e.  CC  /\  B  =/=  0 ) )
10916rpcnne0d 10399 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  e.  CC  /\  E  =/=  0 ) )
110 divdiv2 9472 . . . . . . . . . . . . 13  |-  ( ( ( log `  Z
)  e.  CC  /\  ( B  e.  CC  /\  B  =/=  0 )  /\  ( E  e.  CC  /\  E  =/=  0 ) )  -> 
( ( log `  Z
)  /  ( B  /  E ) )  =  ( ( ( log `  Z )  x.  E )  /  B ) )
111107, 108, 109, 110syl3anc 1182 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  Z
)  /  ( B  /  E ) )  =  ( ( ( log `  Z )  x.  E )  /  B ) )
112106, 111eqtrd 2315 . . . . . . . . . . 11  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  =  ( ( ( log `  Z )  x.  E
)  /  B ) )
113112oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  /  ( log `  K ) ) )  =  ( ( L  x.  E )  x.  ( ( ( log `  Z )  x.  E
)  /  B ) ) )
11416rpcnd 10392 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  CC )
115107, 114mulcld 8855 . . . . . . . . . . 11  |-  ( ph  ->  ( ( log `  Z
)  x.  E )  e.  CC )
116 divass 9442 . . . . . . . . . . 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 ) ) )
11785, 115, 108, 116syl3anc 1182 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  x.  E ) )  /  B )  =  ( ( L  x.  E )  x.  ( ( ( log `  Z )  x.  E
)  /  B ) ) )
11815rpcnd 10392 . . . . . . . . . . . . 13  |-  ( ph  ->  L  e.  CC )
119118, 114, 107, 114mul4d 9024 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  x.  E ) )  =  ( ( L  x.  ( log `  Z ) )  x.  ( E  x.  E
) ) )
120114sqvald 11242 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E ^ 2 )  =  ( E  x.  E ) )
121120oveq2d 5874 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  x.  ( log `  Z ) )  x.  ( E ^ 2 ) )  =  ( ( L  x.  ( log `  Z
) )  x.  ( E  x.  E )
) )
122114sqcld 11243 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
123118, 107, 122mul32d 9022 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( L  x.  ( log `  Z ) )  x.  ( E ^ 2 ) )  =  ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) ) )
124119, 121, 1233eqtr2d 2321 . . . . . . . . . . 11  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  x.  E ) )  =  ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) ) )
125124oveq1d 5873 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  x.  E ) )  /  B )  =  ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
) )
126113, 117, 1253eqtr2d 2321 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  E )  x.  (
( log `  Z
)  /  ( log `  K ) ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
) )
127 8t4e32 10214 . . . . . . . . . 10  |-  ( 8  x.  4 )  = ; 3
2
128127a1i 10 . . . . . . . . 9  |-  ( ph  ->  ( 8  x.  4 )  = ; 3 2 )
129126, 128oveq12d 5876 . . . . . . . 8  |-  ( ph  ->  ( ( ( L  x.  E )  x.  ( ( log `  Z
)  /  ( log `  K ) ) )  /  ( 8  x.  4 ) )  =  ( ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
)  / ; 3 2 ) )
13020rpcnd 10392 . . . . . . . . . . 11  |-  ( ph  ->  ( L  x.  ( E ^ 2 ) )  e.  CC )
131130, 107mulcld 8855 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z ) )  e.  CC )
132 rpcnne0 10371 . . . . . . . . . . 11  |-  (; 3 2  e.  RR+  ->  (; 3 2  e.  CC  /\ ; 3
2  =/=  0 ) )
13325, 132mp1i 11 . . . . . . . . . 10  |-  ( ph  ->  (; 3 2  e.  CC  /\ ; 3
2  =/=  0 ) )
134 divdiv1 9471 . . . . . . . . . 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 ) ) )
135131, 108, 133, 134syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
)  / ; 3 2 )  =  ( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  ( B  x. ; 3 2 ) ) )
13623nncni 9756 . . . . . . . . . . 11  |- ; 3 2  e.  CC
1373rpcnd 10392 . . . . . . . . . . 11  |-  ( ph  ->  B  e.  CC )
138 mulcom 8823 . . . . . . . . . . 11  |-  ( (; 3
2  e.  CC  /\  B  e.  CC )  ->  (; 3 2  x.  B
)  =  ( B  x. ; 3 2 ) )
139136, 137, 138sylancr 644 . . . . . . . . . 10  |-  ( ph  ->  (; 3 2  x.  B
)  =  ( B  x. ; 3 2 ) )
140139oveq2d 5874 . . . . . . . . 9  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  (; 3 2  x.  B ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  ( B  x. ; 3 2 ) ) )
14127rpcnne0d 10399 . . . . . . . . . 10  |-  ( ph  ->  ( (; 3 2  x.  B
)  e.  CC  /\  (; 3 2  x.  B )  =/=  0 ) )
142 div23 9443 . . . . . . . . . 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 ) ) )
143130, 107, 141, 142syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  x.  ( log `  Z
) )  /  (; 3 2  x.  B ) )  =  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  ( log `  Z ) ) )
144135, 140, 1433eqtr2d 2321 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( L  x.  ( E ^ 2 ) )  x.  ( log `  Z
) )  /  B
)  / ; 3 2 )  =  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  ( log `  Z ) ) )
145100, 129, 1443eqtrd 2319 . . . . . . 7  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 ) )  =  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  ( log `  Z ) ) )
146145oveq1d 5873 . . . . . 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
) ) )
14750rpcnd 10392 . . . . . . 7  |-  ( ph  ->  ( ( L  x.  E )  /  8
)  e.  CC )
14890rpred 10390 . . . . . . . . 9  |-  ( ph  ->  ( ( log `  Z
)  /  ( log `  K ) )  e.  RR )
149 4nn 9879 . . . . . . . . 9  |-  4  e.  NN
150 nndivre 9781 . . . . . . . . 9  |-  ( ( ( ( log `  Z
)  /  ( log `  K ) )  e.  RR  /\  4  e.  NN )  ->  (
( ( log `  Z
)  /  ( log `  K ) )  / 
4 )  e.  RR )
151148, 149, 150sylancl 643 . . . . . . . 8  |-  ( ph  ->  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 )  e.  RR )
152151recnd 8861 . . . . . . 7  |-  ( ph  ->  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 )  e.  CC )
153147, 107, 152mul32d 9022 . . . . . 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
) ) )
154107sqvald 11242 . . . . . . . 8  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  =  ( ( log `  Z )  x.  ( log `  Z ) ) )
155154oveq2d 5874 . . . . . . 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 ) ) ) )
15628rpcnd 10392 . . . . . . . 8  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  CC )
157156, 107, 107mulassd 8858 . . . . . . 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 ) ) ) )
158155, 157eqtr4d 2318 . . . . . 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
) ) )
159146, 153, 1583eqtr4d 2325 . . . . 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 ) ) )
16056simp3d 969 . . . . . 6  |-  ( ph  ->  ( ( ( log `  Z )  /  ( log `  K ) )  /  4 )  <_ 
( N  -  M
) )
161151, 64, 51lemul2d 10430 . . . . . 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 )
) ) )
162160, 161mpbid 201 . . . . 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 )
) )
163159, 162eqbrtrrd 4045 . . . 4  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  <_  ( (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) )  x.  ( N  -  M
) ) )
16442rpred 10390 . . . . 5  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  e.  RR )
16551rpred 10390 . . . . . 6  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) )  e.  RR )
166165, 64remulcld 8863 . . . . 5  |-  ( ph  ->  ( ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) )  x.  ( N  -  M )
)  e.  RR )
167164, 166, 13lemul2d 10430 . . . 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
) ) ) ) )
168163, 167mpbid 201 . . 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
) ) ) )
16913rpcnd 10392 . . . 4  |-  ( ph  ->  ( U  -  E
)  e.  CC )
17051rpcnd 10392 . . . 4  |-  ( ph  ->  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) )  e.  CC )
17164recnd 8861 . . . 4  |-  ( ph  ->  ( N  -  M
)  e.  CC )
172169, 170, 171mulassd 8858 . . 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 )
) ) )
173168, 172breqtrrd 4049 . 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 ) ) )
174 fzfid 11035 . . . 4  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
17561nnzd 10116 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
17686, 175rpexpcld 11268 . . . . . . . . . . 11  |-  ( ph  ->  ( K ^ N
)  e.  RR+ )
17735, 176rpdivcld 10407 . . . . . . . . . 10  |-  ( ph  ->  ( Z  /  ( K ^ N ) )  e.  RR+ )
178177rprege0d 10397 . . . . . . . . 9  |-  ( ph  ->  ( ( Z  / 
( K ^ N
) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ N ) ) ) )
179 flge0nn0 10948 . . . . . . . . 9  |-  ( ( ( Z  /  ( K ^ N ) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ N ) ) )  ->  ( |_ `  ( Z  /  ( K ^ N ) ) )  e.  NN0 )
180 nn0p1nn 10003 . . . . . . . . 9  |-  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  e.  NN0  ->  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  NN )
181178, 179, 1803syl 18 . . . . . . . 8  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  NN )
182181, 59syl6eleq 2373 . . . . . . 7  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  ( ZZ>= `  1
) )
183 fzss1 10830 . . . . . . 7  |-  ( ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 )  e.  ( ZZ>= `  1 )  ->  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
184182, 183syl 15 . . . . . 6  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
185184sselda 3180 . . . . 5  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
186185, 83syldan 456 . . . 4  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
187174, 186fsumrecl 12207 . . 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 10804 . . . . 5  |-  ( N  e.  ( ZZ>= `  M
)  ->  N  e.  ( M ... N ) )
18958, 188syl 15 . . . 4  |-  ( ph  ->  N  e.  ( M ... N ) )
190 oveq1 5865 . . . . . . . 8  |-  ( m  =  M  ->  (
m  -  M )  =  ( M  -  M ) )
191190oveq2d 5874 . . . . . . 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 5866 . . . . . . . . . . . 12  |-  ( m  =  M  ->  ( K ^ m )  =  ( K ^ M
) )
193192oveq2d 5874 . . . . . . . . . . 11  |-  ( m  =  M  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ M ) ) )
194193fveq2d 5529 . . . . . . . . . 10  |-  ( m  =  M  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^ M ) ) ) )
195194oveq1d 5873 . . . . . . . . 9  |-  ( m  =  M  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 ) )
196195oveq1d 5873 . . . . . . . 8  |-  ( m  =  M  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
197196sumeq1d 12174 . . . . . . 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 4036 . . . . . 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 307 . . . . 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 5865 . . . . . . . 8  |-  ( m  =  j  ->  (
m  -  M )  =  ( j  -  M ) )
201200oveq2d 5874 . . . . . . 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 5866 . . . . . . . . . . . 12  |-  ( m  =  j  ->  ( K ^ m )  =  ( K ^ j
) )
203202oveq2d 5874 . . . . . . . . . . 11  |-  ( m  =  j  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ j ) ) )
204203fveq2d 5529 . . . . . . . . . 10  |-  ( m  =  j  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^
j ) ) ) )
205204oveq1d 5873 . . . . . . . . 9  |-  ( m  =  j  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ j ) ) )  +  1 ) )
206205oveq1d 5873 . . . . . . . 8  |-  ( m  =  j  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
207206sumeq1d 12174 . . . . . . 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 4036 . . . . . 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 307 . . . . 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 5865 . . . . . . . 8  |-  ( m  =  ( j  +  1 )  ->  (
m  -  M )  =  ( ( j  +  1 )  -  M ) )
211210oveq2d 5874 . . . . . . 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 5866 . . . . . . . . . . . 12  |-  ( m  =  ( j  +  1 )  ->  ( K ^ m )  =  ( K ^ (
j  +  1 ) ) )
213212oveq2d 5874 . . . . . . . . . . 11  |-  ( m  =  ( j  +  1 )  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ ( j  +  1 ) ) ) )
214213fveq2d 5529 . . . . . . . . . 10  |-  ( m  =  ( j  +  1 )  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) ) )
215214oveq1d 5873 . . . . . . . . 9  |-  ( m  =  ( j  +  1 )  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  +  1 ) )
216215oveq1d 5873 . . . . . . . 8  |-  ( m  =  ( j  +  1 )  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
217216sumeq1d 12174 . . . . . . 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 4036 . . . . . 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 307 . . . . 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 5865 . . . . . . . 8  |-  ( m  =  N  ->  (
m  -  M )  =  ( N  -  M ) )
221220oveq2d 5874 . . . . . . 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 5866 . . . . . . . . . . . 12  |-  ( m  =  N  ->  ( K ^ m )  =  ( K ^ N
) )
223222oveq2d 5874 . . . . . . . . . . 11  |-  ( m  =  N  ->  ( Z  /  ( K ^
m ) )  =  ( Z  /  ( K ^ N ) ) )
224223fveq2d 5529 . . . . . . . . . 10  |-  ( m  =  N  ->  ( |_ `  ( Z  / 
( K ^ m
) ) )  =  ( |_ `  ( Z  /  ( K ^ N ) ) ) )
225224oveq1d 5873 . . . . . . . . 9  |-  ( m  =  N  ->  (
( |_ `  ( Z  /  ( K ^
m ) ) )  +  1 )  =  ( ( |_ `  ( Z  /  ( K ^ N ) ) )  +  1 ) )
226225oveq1d 5873 . . . . . . . 8  |-  ( m  =  N  ->  (
( ( |_ `  ( Z  /  ( K ^ m ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y
) ) )  =  ( ( ( |_
`  ( Z  / 
( K ^ N
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
227226sumeq1d 12174 . . . . . . 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 4036 . . . . . 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 307 . . . . 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 9762 . . . . . . . . . 10  |-  ( ph  ->  M  e.  CC )
231230subidd 9145 . . . . . . . . 9  |-  ( ph  ->  ( M  -  M
)  =  0 )
232231oveq2d 5874 . . . . . . . 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 10392 . . . . . . . . 9  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  E )  /  8
)  x.  ( log `  Z ) ) )  e.  CC )
234233mul01d 9011 . . . . . . . 8  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  0 )  =  0 )
235232, 234eqtrd 2315 . . . . . . 7  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  x.  ( M  -  M ) )  =  0 )
236 fzfid 11035 . . . . . . . 8  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
23757nnzd 10116 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  ZZ )
23886, 237rpexpcld 11268 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( K ^ M
)  e.  RR+ )
23935, 238rpdivcld 10407 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Z  /  ( K ^ M ) )  e.  RR+ )
240239rprege0d 10397 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( Z  / 
( K ^ M
) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ M ) ) ) )
241 flge0nn0 10948 . . . . . . . . . . . . 13  |-  ( ( ( Z  /  ( K ^ M ) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ M ) ) )  ->  ( |_ `  ( Z  /  ( K ^ M ) ) )  e.  NN0 )
242 nn0p1nn 10003 . . . . . . . . . . . . 13  |-  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  e.  NN0  ->  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  NN )
243240, 241, 2423syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  NN )
244243, 59syl6eleq 2373 . . . . . . . . . . 11  |-  ( ph  ->  ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  ( ZZ>= `  1
) )
245 fzss1 10830 . . . . . . . . . . 11  |-  ( ( ( |_ `  ( Z  /  ( K ^ M ) ) )  +  1 )  e.  ( ZZ>= `  1 )  ->  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
246244, 245syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
247246sselda 3180 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
248247, 83syldan 456 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
249 elfzle2 10800 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  <_  ( |_ `  ( Z  /  Y ) ) )
250249adantl 452 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  <_  ( |_ `  ( Z  /  Y ) ) )
25129simpld 445 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Y  e.  RR+ )
25235, 251rpdivcld 10407 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( Z  /  Y
)  e.  RR+ )
253252rpred 10390 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Z  /  Y
)  e.  RR )
254 elfzelz 10798 . . . . . . . . . . . . 13  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  ZZ )
255 flge 10937 . . . . . . . . . . . . 13  |-  ( ( ( Z  /  Y
)  e.  RR  /\  n  e.  ZZ )  ->  ( n  <_  ( Z  /  Y )  <->  n  <_  ( |_ `  ( Z  /  Y ) ) ) )
256253, 254, 255syl2an 463 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( n  <_  ( Z  /  Y
)  <->  n  <_  ( |_
`  ( Z  /  Y ) ) ) )
257250, 256mpbird 223 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  <_  ( Z  /  Y ) )
25872, 257jca 518 . . . . . . . . . 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 20749 . . . . . . . . . 10  |-  ( (
ph  /\  ( n  e.  NN  /\  n  <_ 
( Z  /  Y
) ) )  -> 
0  <_  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) ) )
261258, 260syldan 456 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  0  <_  ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
262247, 261syldan 456 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  0  <_  ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) ) )
263236, 248, 262fsumge0 12253 . . . . . . 7  |-  ( ph  ->  0  <_  sum_ n  e.  ( ( ( |_
`  ( Z  / 
( K ^ M
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )
264235, 263eqbrtrd 4043 . . . . . 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 10 . . . . 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 2283 . . . . . . . . . 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 20753 . . . . . . . . 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 451 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  e.  RR+ )
270269rpred 10390 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( U  -  E )  x.  ( ( ( L  x.  E )  / 
8 )  x.  ( log `  Z ) ) )  e.  RR )
271 elfzoelz 10875 . . . . . . . . . . . . . 14  |-  ( j  e.  ( M..^ N
)  ->  j  e.  ZZ )
272271adantl 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  j  e.  ZZ )
273272zred 10117 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  j  e.  RR )
27457adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  M  e.  NN )
275274nnred 9761 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  M  e.  RR )
276273, 275resubcld 9211 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( j  -  M )  e.  RR )
277270, 276remulcld 8863 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( U  -  E )  x.  ( ( ( L  x.  E )  /  8 )  x.  ( log `  Z
) ) )  x.  ( j  -  M
) )  e.  RR )
278 fzfid 11035 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  e.  Fin )
279 ssun1 3338 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Z  e.  RR )
28186adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  K  e.  RR+ )
282272peano2zd 10120 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( j  +  1 )  e.  ZZ )
283281, 282rpexpcld 11268 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
( j  +  1 ) )  e.  RR+ )
284280, 283rerpdivcld 10417 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ (
j  +  1 ) ) )  e.  RR )
285281, 272rpexpcld 11268 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
j )  e.  RR+ )
286280, 285rerpdivcld 10417 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ j
) )  e.  RR )
28787adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  K  e.  RR )
288 1re 8837 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR
289 ltle 8910 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR  /\  K  e.  RR )  ->  ( 1  <  K  ->  1  <_  K )
)
290288, 87, 289sylancr 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( 1  <  K  ->  1  <_  K )
)
29188, 290mpd 14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  <_  K )
292291adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  1  <_  K
)
293 uzid 10242 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ZZ  ->  j  e.  ( ZZ>= `  j )
)
294 peano2uz 10272 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( ZZ>= `  j
)  ->  ( j  +  1 )  e.  ( ZZ>= `  j )
)
295272, 293, 2943syl 18 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( j  +  1 )  e.  (
ZZ>= `  j ) )
296287, 292, 295leexp2ad 11277 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
j )  <_  ( K ^ ( j  +  1 ) ) )
29735adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Z  e.  RR+ )
298285, 283, 297lediv2d 10414 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( K ^ j )  <_ 
( K ^ (
j  +  1 ) )  <->  ( Z  / 
( K ^ (
j  +  1 ) ) )  <_  ( Z  /  ( K ^
j ) ) ) )
299296, 298mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ (
j  +  1 ) ) )  <_  ( Z  /  ( K ^
j ) ) )
300 flword2 10943 . . . . . . . . . . . . . . . . . 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 1182 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  ( K ^ j ) ) )  e.  ( ZZ>= `  ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) ) ) )
302 eluzp1p1 10253 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  ( Z  /  ( K ^
j ) ) )  e.  ( ZZ>= `  ( |_ `  ( Z  / 
( K ^ (
j  +  1 ) ) ) ) )  ->  ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 )  e.  (
ZZ>= `  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ) )
303301, 302syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 )  e.  (
ZZ>= `  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ) )
304286flcld 10930 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  ( K ^ j ) ) )  e.  ZZ )
305252adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  /  Y )  e.  RR+ )
306305rpred 10390 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  /  Y )  e.  RR )
307306flcld 10930 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  Y
) )  e.  ZZ )
308251adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  e.  RR+ )
309308rpred 10390 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  e.  RR )
310285rpred 10390 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( K ^
j )  e.  RR )
31130simpld 445 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  X  e.  RR+ )
312311rpred 10390 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  X  e.  RR )
313312adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  X  e.  RR )
31430simprd 449 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  Y  <  X )
315314adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  <  X
)
316 elfzofz 10889 . . . . . . . . . . . . . . . . . . . . . . 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 20748 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( M ... N ) )  ->  ( X  <  ( K ^ j
)  /\  ( K ^ j )  <_ 
( sqr `  Z
) ) )
318316, 317sylan2 460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( X  < 
( K ^ j
)  /\  ( K ^ j )  <_ 
( sqr `  Z
) ) )
319318simpld 445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  X  <  ( K ^ j ) )
320309, 313, 310, 315, 319lttrd 8977 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  <  ( K ^ j ) )
321309, 310, 320ltled 8967 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  Y  <_  ( K ^ j ) )
322308, 285, 297lediv2d 10414 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Y  <_ 
( K ^ j
)  <->  ( Z  / 
( K ^ j
) )  <_  ( Z  /  Y ) ) )
323321, 322mpbid 201 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ j
) )  <_  ( Z  /  Y ) )
324 flwordi 10942 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( Z  /  ( K ^ j ) )  e.  RR  /\  ( Z  /  Y )  e.  RR  /\  ( Z  /  ( K ^
j ) )  <_ 
( Z  /  Y
) )  ->  ( |_ `  ( Z  / 
( K ^ j
) ) )  <_ 
( |_ `  ( Z  /  Y ) ) )
325286, 306, 323, 324syl3anc 1182 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  ( K ^ j ) ) )  <_  ( |_ `  ( Z  /  Y
) ) )
326 eluz2 10236 . . . . . . . . . . . . . . . . 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 1136 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( |_ `  ( Z  /  Y
) )  e.  (
ZZ>= `  ( |_ `  ( Z  /  ( K ^ j ) ) ) ) )
328 fzsplit2 10815 . . . . . . . . . . . . . . . 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 642 . . . . . . . . . . . . . . 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 3227 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  C_  ( (
( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
331297, 283rpdivcld 10407 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( Z  / 
( K ^ (
j  +  1 ) ) )  e.  RR+ )
332331rprege0d 10397 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( Z  /  ( K ^
( j  +  1 ) ) )  e.  RR  /\  0  <_ 
( Z  /  ( K ^ ( j  +  1 ) ) ) ) )
333 flge0nn0 10948 . . . . . . . . . . . . . . . . 17  |-  ( ( ( Z  /  ( K ^ ( j  +  1 ) ) )  e.  RR  /\  0  <_  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  ->  ( |_ `  ( Z  /  ( K ^ ( j  +  1 ) ) ) )  e.  NN0 )
334 nn0p1nn 10003 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  e.  NN0  ->  ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 )  e.  NN )
335332, 333, 3343syl 18 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 )  e.  NN )
336335, 59syl6eleq 2373 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 )  e.  (
ZZ>= `  1 ) )
337 fzss1 10830 . . . . . . . . . . . . . . 15  |-  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 )  e.  ( ZZ>= `  1 )  ->  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) 
C_  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
338336, 337syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  C_  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )
339330, 338sstrd 3189 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  ( K ^
j ) ) ) )  C_  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )
340339sselda 3180 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( M..^ N ) )  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ (
j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  / 
( K ^ j
) ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
34183adantlr 695 . . . . . . . . . . . 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 456 . . . . . . . . . . 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 12207 . . . . . . . . . 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 11035 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
345 ssun2 3339 . . . . . . . . . . . . . . 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 3227 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  C_  ( (
( |_ `  ( Z  /  ( K ^
( j  +  1 ) ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )
347346, 338sstrd 3189 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( M..^ N ) )  ->  ( ( ( |_ `  ( Z  /  ( K ^
j ) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) )  C_  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )
348347sselda 3180 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  j  e.  ( M..^ N ) )  /\  n  e.  ( ( ( |_
`  ( Z  / 
( K ^ j
) ) )  +  1 ) ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
349348, 341syldan 456 . . . . . . . . . . 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 12207 . . . . . . . . . 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 9256 . . . . . . . . . 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 1183 . . . . . . . . 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 656 . . . . . . . 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