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

Theorem pntlemo 22815
Description: Lemma for pnt 22822. Combine all the estimates to establish a smaller eventual bound on  R ( Z )  /  Z. (Contributed by Mario Carneiro, 14-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 ) )
pntlem1.C  |-  ( ph  ->  A. z  e.  ( 1 (,) +oo )
( ( ( ( abs `  ( R `
 z ) )  x.  ( log `  z
) )  -  (
( 2  /  ( log `  z ) )  x.  sum_ i  e.  ( 1 ... ( |_
`  ( z  /  Y ) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) ) ) )  /  z )  <_  C )
Assertion
Ref Expression
pntlemo  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  <_  ( U  -  ( F  x.  ( U ^ 3 ) ) ) )
Distinct variable groups:    z, C    y, z, u, L    y, K, z    z, M    z, N    u, i, y, z, R    z, U    z, W    y, X, z    i, Y, z    u, a, y, z, E    u, Z, z
Allowed substitution hints:    ph( y, z, u, i, a)    A( y, z, u, i, a)    B( y, z, u, i, a)    C( y, u, i, a)    D( y, z, u, i, a)    R( a)    U( y, u, i, a)    E( i)    F( y, z, u, i, a)    K( u, i, a)    L( i, a)    M( y, u, i, a)    N( y, u, i, a)    W( y, u, i, a)    X( u, i, a)    Y( y, u, a)    Z( y, i, a)

Proof of Theorem pntlemo
Dummy variable  n is distinct from all other variables.
StepHypRef Expression
1 pntlem1.r . . . . . . . . . 10  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
2 pntlem1.a . . . . . . . . . 10  |-  ( ph  ->  A  e.  RR+ )
3 pntlem1.b . . . . . . . . . 10  |-  ( ph  ->  B  e.  RR+ )
4 pntlem1.l . . . . . . . . . 10  |-  ( ph  ->  L  e.  ( 0 (,) 1 ) )
5 pntlem1.d . . . . . . . . . 10  |-  D  =  ( A  +  1 )
6 pntlem1.f . . . . . . . . . 10  |-  F  =  ( ( 1  -  ( 1  /  D
) )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )
7 pntlem1.u . . . . . . . . . 10  |-  ( ph  ->  U  e.  RR+ )
8 pntlem1.u2 . . . . . . . . . 10  |-  ( ph  ->  U  <_  A )
9 pntlem1.e . . . . . . . . . 10  |-  E  =  ( U  /  D
)
10 pntlem1.k . . . . . . . . . 10  |-  K  =  ( exp `  ( B  /  E ) )
11 pntlem1.y . . . . . . . . . 10  |-  ( ph  ->  ( Y  e.  RR+  /\  1  <_  Y )
)
12 pntlem1.x . . . . . . . . . 10  |-  ( ph  ->  ( X  e.  RR+  /\  Y  <  X ) )
13 pntlem1.c . . . . . . . . . 10  |-  ( ph  ->  C  e.  RR+ )
14 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
) ) ) ) )
15 pntlem1.z . . . . . . . . . 10  |-  ( ph  ->  Z  e.  ( W [,) +oo ) )
161, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15pntlemb 22805 . . . . . . . . 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
) ) ) ) )
1716simp1d 995 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR+ )
181pntrf 22771 . . . . . . . . 9  |-  R : RR+
--> RR
1918ffvelrni 5839 . . . . . . . 8  |-  ( Z  e.  RR+  ->  ( R `
 Z )  e.  RR )
2017, 19syl 16 . . . . . . 7  |-  ( ph  ->  ( R `  Z
)  e.  RR )
2120, 17rerpdivcld 11050 . . . . . 6  |-  ( ph  ->  ( ( R `  Z )  /  Z
)  e.  RR )
2221recnd 9408 . . . . 5  |-  ( ph  ->  ( ( R `  Z )  /  Z
)  e.  CC )
2322abscld 12918 . . . 4  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  e.  RR )
2417relogcld 22031 . . . 4  |-  ( ph  ->  ( log `  Z
)  e.  RR )
2523, 24remulcld 9410 . . 3  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  e.  RR )
267rpred 11023 . . . . . 6  |-  ( ph  ->  U  e.  RR )
27 3re 10391 . . . . . . . 8  |-  3  e.  RR
2827a1i 11 . . . . . . 7  |-  ( ph  ->  3  e.  RR )
2924, 28readdcld 9409 . . . . . 6  |-  ( ph  ->  ( ( log `  Z
)  +  3 )  e.  RR )
3026, 29remulcld 9410 . . . . 5  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  e.  RR )
31 2re 10387 . . . . . . 7  |-  2  e.  RR
3231a1i 11 . . . . . 6  |-  ( ph  ->  2  e.  RR )
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 22803 . . . . . . . . . . 11  |-  ( ph  ->  ( E  e.  RR+  /\  K  e.  RR+  /\  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E )  e.  RR+ ) ) )
3433simp3d 997 . . . . . . . . . 10  |-  ( ph  ->  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E
)  e.  RR+ )
)
3534simp3d 997 . . . . . . . . 9  |-  ( ph  ->  ( U  -  E
)  e.  RR+ )
3635rpred 11023 . . . . . . . 8  |-  ( ph  ->  ( U  -  E
)  e.  RR )
371, 2, 3, 4, 5, 6pntlemd 22802 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  e.  RR+  /\  D  e.  RR+  /\  F  e.  RR+ ) )
3837simp1d 995 . . . . . . . . . . 11  |-  ( ph  ->  L  e.  RR+ )
3933simp1d 995 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
40 2z 10674 . . . . . . . . . . . 12  |-  2  e.  ZZ
41 rpexpcl 11880 . . . . . . . . . . . 12  |-  ( ( E  e.  RR+  /\  2  e.  ZZ )  ->  ( E ^ 2 )  e.  RR+ )
4239, 40, 41sylancl 657 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  e.  RR+ )
4338, 42rpmulcld 11039 . . . . . . . . . 10  |-  ( ph  ->  ( L  x.  ( E ^ 2 ) )  e.  RR+ )
44 3nn0 10593 . . . . . . . . . . . . 13  |-  3  e.  NN0
45 2nn 10475 . . . . . . . . . . . . 13  |-  2  e.  NN
4644, 45decnncl 10764 . . . . . . . . . . . 12  |- ; 3 2  e.  NN
47 nnrp 10996 . . . . . . . . . . . 12  |-  (; 3 2  e.  NN  -> ; 3
2  e.  RR+ )
4846, 47ax-mp 5 . . . . . . . . . . 11  |- ; 3 2  e.  RR+
49 rpmulcl 11008 . . . . . . . . . . 11  |-  ( (; 3
2  e.  RR+  /\  B  e.  RR+ )  ->  (; 3 2  x.  B )  e.  RR+ )
5048, 3, 49sylancr 658 . . . . . . . . . 10  |-  ( ph  ->  (; 3 2  x.  B
)  e.  RR+ )
5143, 50rpdivcld 11040 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  RR+ )
5251rpred 11023 . . . . . . . 8  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  RR )
5336, 52remulcld 9410 . . . . . . 7  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  e.  RR )
5453, 24remulcld 9410 . . . . . 6  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  e.  RR )
5532, 54remulcld 9410 . . . . 5  |-  ( ph  ->  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  RR )
5630, 55resubcld 9772 . . . 4  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  -  ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  e.  RR )
5713rpred 11023 . . . 4  |-  ( ph  ->  C  e.  RR )
5856, 57readdcld 9409 . . 3  |-  ( ph  ->  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  -  (
2  x.  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  +  C )  e.  RR )
597rpcnd 11025 . . . . . 6  |-  ( ph  ->  U  e.  CC )
6053recnd 9408 . . . . . 6  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  e.  CC )
6124recnd 9408 . . . . . 6  |-  ( ph  ->  ( log `  Z
)  e.  CC )
6259, 60, 61subdird 9797 . . . . 5  |-  ( ph  ->  ( ( U  -  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) ) )  x.  ( log `  Z
) )  =  ( ( U  x.  ( log `  Z ) )  -  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )
6338rpcnd 11025 . . . . . . . . . . 11  |-  ( ph  ->  L  e.  CC )
6442rpcnd 11025 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
6550rpcnne0d 11032 . . . . . . . . . . 11  |-  ( ph  ->  ( (; 3 2  x.  B
)  e.  CC  /\  (; 3 2  x.  B )  =/=  0 ) )
66 div23 10009 . . . . . . . . . . 11  |-  ( ( L  e.  CC  /\  ( E ^ 2 )  e.  CC  /\  (
(; 3 2  x.  B
)  e.  CC  /\  (; 3 2  x.  B )  =/=  0 ) )  ->  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  =  ( ( L  /  (; 3 2  x.  B ) )  x.  ( E ^
2 ) ) )
6763, 64, 65, 66syl3anc 1213 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  =  ( ( L  /  (; 3 2  x.  B ) )  x.  ( E ^
2 ) ) )
689oveq1i 6100 . . . . . . . . . . . 12  |-  ( E ^ 2 )  =  ( ( U  /  D ) ^ 2 )
6937simp2d 996 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  RR+ )
7069rpcnd 11025 . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  CC )
7169rpne0d 11028 . . . . . . . . . . . . 13  |-  ( ph  ->  D  =/=  0 )
7259, 70, 71sqdivd 12017 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U  /  D ) ^ 2 )  =  ( ( U ^ 2 )  /  ( D ^
2 ) ) )
7368, 72syl5eq 2485 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  =  ( ( U ^ 2 )  /  ( D ^
2 ) ) )
7473oveq2d 6106 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  x.  ( E ^ 2 ) )  =  ( ( L  /  (; 3 2  x.  B
) )  x.  (
( U ^ 2 )  /  ( D ^ 2 ) ) ) )
7538, 50rpdivcld 11040 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  /  (; 3 2  x.  B ) )  e.  RR+ )
7675rpcnd 11025 . . . . . . . . . . 11  |-  ( ph  ->  ( L  /  (; 3 2  x.  B ) )  e.  CC )
7759sqcld 12002 . . . . . . . . . . 11  |-  ( ph  ->  ( U ^ 2 )  e.  CC )
78 rpexpcl 11880 . . . . . . . . . . . . 13  |-  ( ( D  e.  RR+  /\  2  e.  ZZ )  ->  ( D ^ 2 )  e.  RR+ )
7969, 40, 78sylancl 657 . . . . . . . . . . . 12  |-  ( ph  ->  ( D ^ 2 )  e.  RR+ )
8079rpcnne0d 11032 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D ^
2 )  e.  CC  /\  ( D ^ 2 )  =/=  0 ) )
81 divass 10008 . . . . . . . . . . . 12  |-  ( ( ( L  /  (; 3 2  x.  B ) )  e.  CC  /\  ( U ^ 2 )  e.  CC  /\  ( ( D ^ 2 )  e.  CC  /\  ( D ^ 2 )  =/=  0 ) )  -> 
( ( ( L  /  (; 3 2  x.  B
) )  x.  ( U ^ 2 ) )  /  ( D ^
2 ) )  =  ( ( L  / 
(; 3 2  x.  B
) )  x.  (
( U ^ 2 )  /  ( D ^ 2 ) ) ) )
82 div23 10009 . . . . . . . . . . . 12  |-  ( ( ( L  /  (; 3 2  x.  B ) )  e.  CC  /\  ( U ^ 2 )  e.  CC  /\  ( ( D ^ 2 )  e.  CC  /\  ( D ^ 2 )  =/=  0 ) )  -> 
( ( ( L  /  (; 3 2  x.  B
) )  x.  ( U ^ 2 ) )  /  ( D ^
2 ) )  =  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) )
8381, 82eqtr3d 2475 . . . . . . . . . . 11  |-  ( ( ( L  /  (; 3 2  x.  B ) )  e.  CC  /\  ( U ^ 2 )  e.  CC  /\  ( ( D ^ 2 )  e.  CC  /\  ( D ^ 2 )  =/=  0 ) )  -> 
( ( L  / 
(; 3 2  x.  B
) )  x.  (
( U ^ 2 )  /  ( D ^ 2 ) ) )  =  ( ( ( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) )  x.  ( U ^ 2 ) ) )
8476, 77, 80, 83syl3anc 1213 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  x.  (
( U ^ 2 )  /  ( D ^ 2 ) ) )  =  ( ( ( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) )  x.  ( U ^ 2 ) ) )
8567, 74, 843eqtrd 2477 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  =  ( ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) )
8685oveq2d 6106 . . . . . . . 8  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  =  ( ( U  -  E )  x.  (
( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
87 df-3 10377 . . . . . . . . . . . . 13  |-  3  =  ( 2  +  1 )
8887oveq2i 6101 . . . . . . . . . . . 12  |-  ( U ^ 3 )  =  ( U ^ (
2  +  1 ) )
89 2nn0 10592 . . . . . . . . . . . . 13  |-  2  e.  NN0
90 expp1 11868 . . . . . . . . . . . . 13  |-  ( ( U  e.  CC  /\  2  e.  NN0 )  -> 
( U ^ (
2  +  1 ) )  =  ( ( U ^ 2 )  x.  U ) )
9159, 89, 90sylancl 657 . . . . . . . . . . . 12  |-  ( ph  ->  ( U ^ (
2  +  1 ) )  =  ( ( U ^ 2 )  x.  U ) )
9288, 91syl5eq 2485 . . . . . . . . . . 11  |-  ( ph  ->  ( U ^ 3 )  =  ( ( U ^ 2 )  x.  U ) )
9377, 59mulcomd 9403 . . . . . . . . . . 11  |-  ( ph  ->  ( ( U ^
2 )  x.  U
)  =  ( U  x.  ( U ^
2 ) ) )
9492, 93eqtrd 2473 . . . . . . . . . 10  |-  ( ph  ->  ( U ^ 3 )  =  ( U  x.  ( U ^
2 ) ) )
9594oveq2d 6106 . . . . . . . . 9  |-  ( ph  ->  ( F  x.  ( U ^ 3 ) )  =  ( F  x.  ( U  x.  ( U ^ 2 ) ) ) )
9637simp3d 997 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  RR+ )
9796rpcnd 11025 . . . . . . . . . 10  |-  ( ph  ->  F  e.  CC )
9897, 59, 77mulassd 9405 . . . . . . . . 9  |-  ( ph  ->  ( ( F  x.  U )  x.  ( U ^ 2 ) )  =  ( F  x.  ( U  x.  ( U ^ 2 ) ) ) )
99 1cnd 9398 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
10069rpreccld 11033 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  /  D
)  e.  RR+ )
101100rpcnd 11025 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  /  D
)  e.  CC )
10299, 101, 59subdird 9797 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  -  ( 1  /  D
) )  x.  U
)  =  ( ( 1  x.  U )  -  ( ( 1  /  D )  x.  U ) ) )
10359mulid2d 9400 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  x.  U
)  =  U )
10459, 70, 71divrec2d 10107 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( U  /  D
)  =  ( ( 1  /  D )  x.  U ) )
1059, 104syl5req 2486 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1  /  D )  x.  U
)  =  E )
106103, 105oveq12d 6108 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  x.  U )  -  (
( 1  /  D
)  x.  U ) )  =  ( U  -  E ) )
107102, 106eqtr2d 2474 . . . . . . . . . . . . 13  |-  ( ph  ->  ( U  -  E
)  =  ( ( 1  -  ( 1  /  D ) )  x.  U ) )
108107oveq1d 6105 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )  =  ( ( ( 1  -  ( 1  /  D ) )  x.  U )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) ) )
1096oveq1i 6100 . . . . . . . . . . . . 13  |-  ( F  x.  U )  =  ( ( ( 1  -  ( 1  /  D ) )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  U )
11099, 101subcld 9715 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  -  (
1  /  D ) )  e.  CC )
11175, 79rpdivcld 11040 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  e.  RR+ )
112111rpcnd 11025 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  e.  CC )
113110, 112, 59mul32d 9575 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 1  -  ( 1  /  D ) )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  U )  =  ( ( ( 1  -  ( 1  /  D ) )  x.  U )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) ) )
114109, 113syl5eq 2485 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  U
)  =  ( ( ( 1  -  (
1  /  D ) )  x.  U )  x.  ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) ) ) )
115108, 114eqtr4d 2476 . . . . . . . . . . 11  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )  =  ( F  x.  U ) )
116115oveq1d 6105 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  ( U ^ 2 ) )  =  ( ( F  x.  U )  x.  ( U ^ 2 ) ) )
11735rpcnd 11025 . . . . . . . . . . 11  |-  ( ph  ->  ( U  -  E
)  e.  CC )
118117, 112, 77mulassd 9405 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  ( U ^ 2 ) )  =  ( ( U  -  E )  x.  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
119116, 118eqtr3d 2475 . . . . . . . . 9  |-  ( ph  ->  ( ( F  x.  U )  x.  ( U ^ 2 ) )  =  ( ( U  -  E )  x.  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
12095, 98, 1193eqtr2d 2479 . . . . . . . 8  |-  ( ph  ->  ( F  x.  ( U ^ 3 ) )  =  ( ( U  -  E )  x.  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
12186, 120eqtr4d 2476 . . . . . . 7  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  =  ( F  x.  ( U ^ 3 ) ) )
122121oveq2d 6106 . . . . . 6  |-  ( ph  ->  ( U  -  (
( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) ) )  =  ( U  -  ( F  x.  ( U ^ 3 ) ) ) )
123122oveq1d 6105 . . . . 5  |-  ( ph  ->  ( ( U  -  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) ) )  x.  ( log `  Z
) )  =  ( ( U  -  ( F  x.  ( U ^ 3 ) ) )  x.  ( log `  Z ) ) )
12462, 123eqtr3d 2475 . . . 4  |-  ( ph  ->  ( ( U  x.  ( log `  Z ) )  -  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  =  ( ( U  -  ( F  x.  ( U ^ 3 ) ) )  x.  ( log `  Z ) ) )
12526, 24remulcld 9410 . . . . 5  |-  ( ph  ->  ( U  x.  ( log `  Z ) )  e.  RR )
126125, 54resubcld 9772 . . . 4  |-  ( ph  ->  ( ( U  x.  ( log `  Z ) )  -  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  RR )
127124, 126eqeltrrd 2516 . . 3  |-  ( ph  ->  ( ( U  -  ( F  x.  ( U ^ 3 ) ) )  x.  ( log `  Z ) )  e.  RR )
12817rpred 11023 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR )
12916simp2d 996 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  Z  /\  _e  <_  ( sqr `  Z )  /\  ( sqr `  Z )  <_ 
( Z  /  Y
) ) )
130129simp1d 995 . . . . . . . 8  |-  ( ph  ->  1  <  Z )
131128, 130rplogcld 22037 . . . . . . 7  |-  ( ph  ->  ( log `  Z
)  e.  RR+ )
13232, 131rerpdivcld 11050 . . . . . 6  |-  ( ph  ->  ( 2  /  ( log `  Z ) )  e.  RR )
133 fzfid 11791 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
13417adantr 462 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  RR+ )
135 elfznn 11474 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  NN )
136135adantl 463 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  NN )
137136nnrpd 11022 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  RR+ )
138134, 137rpdivcld 11040 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  /  n )  e.  RR+ )
13918ffvelrni 5839 . . . . . . . . . . . 12  |-  ( ( Z  /  n )  e.  RR+  ->  ( R `
 ( Z  /  n ) )  e.  RR )
140138, 139syl 16 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( R `  ( Z  /  n
) )  e.  RR )
141140, 134rerpdivcld 11050 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  RR )
142141recnd 9408 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  CC )
143142abscld 12918 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  RR )
144137relogcld 22031 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  RR )
145143, 144remulcld 9410 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  RR )
146133, 145fsumrecl 13207 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  RR )
147132, 146remulcld 9410 . . . . 5  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  e.  RR )
148147, 57readdcld 9409 . . . 4  |-  ( ph  ->  ( ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  +  C )  e.  RR )
14920recnd 9408 . . . . . . . . . . 11  |-  ( ph  ->  ( R `  Z
)  e.  CC )
150149abscld 12918 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  ( R `  Z )
)  e.  RR )
151150recnd 9408 . . . . . . . . 9  |-  ( ph  ->  ( abs `  ( R `  Z )
)  e.  CC )
152151, 61mulcld 9402 . . . . . . . 8  |-  ( ph  ->  ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) )  e.  CC )
153132recnd 9408 . . . . . . . . 9  |-  ( ph  ->  ( 2  /  ( log `  Z ) )  e.  CC )
154140recnd 9408 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( R `  ( Z  /  n
) )  e.  CC )
155154abscld 12918 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( R `  ( Z  /  n ) ) )  e.  RR )
156155, 144remulcld 9410 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  x.  ( log `  n
) )  e.  RR )
157133, 156fsumrecl 13207 . . . . . . . . . 10  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  e.  RR )
158157recnd 9408 . . . . . . . . 9  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  e.  CC )
159153, 158mulcld 9402 . . . . . . . 8  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )  e.  CC )
16017rpcnd 11025 . . . . . . . 8  |-  ( ph  ->  Z  e.  CC )
16117rpne0d 11028 . . . . . . . 8  |-  ( ph  ->  Z  =/=  0 )
162152, 159, 160, 161divsubdird 10142 . . . . . . 7  |-  ( ph  ->  ( ( ( ( abs `  ( R `
 Z ) )  x.  ( log `  Z
) )  -  (
( 2  /  ( log `  Z ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) ) ) )  /  Z )  =  ( ( ( ( abs `  ( R `
 Z ) )  x.  ( log `  Z
) )  /  Z
)  -  ( ( ( 2  /  ( log `  Z ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) ) )  /  Z ) ) )
163151, 61, 160, 161div23d 10140 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  ( R `  Z
) )  x.  ( log `  Z ) )  /  Z )  =  ( ( ( abs `  ( R `  Z
) )  /  Z
)  x.  ( log `  Z ) ) )
164149, 160, 161absdivd 12937 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  =  ( ( abs `  ( R `
 Z ) )  /  ( abs `  Z
) ) )
16517rprege0d 11030 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Z  e.  RR  /\  0  <_  Z )
)
166 absid 12781 . . . . . . . . . . . . 13  |-  ( ( Z  e.  RR  /\  0  <_  Z )  -> 
( abs `  Z
)  =  Z )
167165, 166syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  Z
)  =  Z )
168167oveq2d 6106 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  ( R `  Z )
)  /  ( abs `  Z ) )  =  ( ( abs `  ( R `  Z )
)  /  Z ) )
169164, 168eqtrd 2473 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  =  ( ( abs `  ( R `
 Z ) )  /  Z ) )
170169oveq1d 6105 . . . . . . . . 9  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  =  ( ( ( abs `  ( R `  Z
) )  /  Z
)  x.  ( log `  Z ) ) )
171163, 170eqtr4d 2476 . . . . . . . 8  |-  ( ph  ->  ( ( ( abs `  ( R `  Z
) )  x.  ( log `  Z ) )  /  Z )  =  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) ) )
172153, 158, 160, 161divassd 10138 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )  /  Z )  =  ( ( 2  / 
( log `  Z
) )  x.  ( sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
) ) )
173160adantr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  CC )
174161adantr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  =/=  0 )
175154, 173, 174absdivd 12937 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  ( abs `  Z
) ) )
176167adantr 462 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  Z )  =  Z )
177176oveq2d 6106 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  / 
( abs `  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z ) )
178175, 177eqtrd 2473 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z ) )
179178oveq1d 6105 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z )  x.  ( log `  n
) ) )
180155recnd 9408 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( R `  ( Z  /  n ) ) )  e.  CC )
181144recnd 9408 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  CC )
18217rpcnne0d 11032 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Z  e.  CC  /\  Z  =/=  0 ) )
183182adantr 462 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  e.  CC  /\  Z  =/=  0 ) )
184 div23 10009 . . . . . . . . . . . . . 14  |-  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  e.  CC  /\  ( log `  n )  e.  CC  /\  ( Z  e.  CC  /\  Z  =/=  0 ) )  -> 
( ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) )  /  Z )  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z )  x.  ( log `  n
) ) )
185180, 181, 183, 184syl3anc 1213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
)  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z )  x.  ( log `  n
) ) )
186179, 185eqtr4d 2476 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
) )
187186sumeq2dv 13176 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( abs `  ( R `
 ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
) )
188156recnd 9408 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  x.  ( log `  n
) )  e.  CC )
189133, 160, 188, 161fsumdivc 13249 . . . . . . . . . . 11  |-  ( ph  ->  ( sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
)  =  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) )  /  Z ) )
190187, 189eqtr4d 2476 . . . . . . . . . 10  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  (
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
) )
191190oveq2d 6106 . . . . . . . . 9  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  =  ( ( 2  /  ( log `  Z ) )  x.  ( sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
) ) )
192172, 191eqtr4d 2476 . . . . . . . 8  |-  ( ph  ->  ( ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )  /  Z )  =  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) ) )
193171, 192oveq12d 6108 . . . . . . 7  |-  ( ph  ->  ( ( ( ( abs `  ( R `
 Z ) )  x.  ( log `  Z
) )  /  Z
)  -  ( ( ( 2  /  ( log `  Z ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) ) )  /  Z ) )  =  ( ( ( abs `  ( ( R `  Z )  /  Z
) )  x.  ( log `  Z ) )  -  ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) ) ) )
194162, 193eqtrd 2473 . . . . . 6  |-  ( ph  ->  ( ( ( ( abs `  ( R `
 Z ) )  x.  ( log `  Z
) )  -  (
( 2  /  ( log `  Z ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) ) ) )  /  Z )  =  ( ( ( abs `  ( ( R `  Z )  /  Z
) )  x.  ( log `  Z ) )  -  ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) ) ) )
195 1re 9381 . . . . . . . . 9  |-  1  e.  RR
196 rexr 9425 . . . . . . . . 9  |-  ( 1  e.  RR  ->  1  e.  RR* )
197 elioopnf 11379 . . . . . . . . 9  |-  ( 1  e.  RR*  ->  ( Z  e.  ( 1 (,) +oo )  <->  ( Z  e.  RR  /\  1  < 
Z ) ) )
198195, 196, 197mp2b 10 . . . . . . . 8  |-  ( Z  e.  ( 1 (,) +oo )  <->  ( Z  e.  RR  /\  1  < 
Z ) )
199128, 130, 198sylanbrc 659 . . . . . . 7  |-  ( ph  ->  Z  e.  ( 1 (,) +oo ) )
200 pntlem1.C . . . . . . 7  |-  ( ph  ->  A. z  e.  ( 1 (,) +oo )
( ( ( ( abs `  ( R `
 z ) )  x.  ( log `  z
) )  -  (
( 2  /  ( log `  z ) )  x.  sum_ i  e.  ( 1 ... ( |_
`  ( z  /  Y ) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) ) ) )  /  z )  <_  C )
201 fveq2 5688 . . . . . . . . . . . . 13  |-  ( z  =  Z  ->  ( R `  z )  =  ( R `  Z ) )
202201fveq2d 5692 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  ( abs `  ( R `  z ) )  =  ( abs `  ( R `  Z )
) )
203 fveq2 5688 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  ( log `  z )  =  ( log `  Z
) )
204202, 203oveq12d 6108 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
( abs `  ( R `  z )
)  x.  ( log `  z ) )  =  ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) ) )
205203oveq2d 6106 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  (
2  /  ( log `  z ) )  =  ( 2  /  ( log `  Z ) ) )
206 oveq2 6098 . . . . . . . . . . . . . . . . 17  |-  ( i  =  n  ->  (
z  /  i )  =  ( z  /  n ) )
207206fveq2d 5692 . . . . . . . . . . . . . . . 16  |-  ( i  =  n  ->  ( R `  ( z  /  i ) )  =  ( R `  ( z  /  n
) ) )
208207fveq2d 5692 . . . . . . . . . . . . . . 15  |-  ( i  =  n  ->  ( abs `  ( R `  ( z  /  i
) ) )  =  ( abs `  ( R `  ( z  /  n ) ) ) )
209 fveq2 5688 . . . . . . . . . . . . . . 15  |-  ( i  =  n  ->  ( log `  i )  =  ( log `  n
) )
210208, 209oveq12d 6108 . . . . . . . . . . . . . 14  |-  ( i  =  n  ->  (
( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) )  =  ( ( abs `  ( R `  ( z  /  n ) ) )  x.  ( log `  n
) ) )
211210cbvsumv 13169 . . . . . . . . . . . . 13  |-  sum_ i  e.  ( 1 ... ( |_ `  ( z  /  Y ) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) )  = 
sum_ n  e.  (
1 ... ( |_ `  ( z  /  Y
) ) ) ( ( abs `  ( R `  ( z  /  n ) ) )  x.  ( log `  n
) )
212 oveq1 6097 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  (
z  /  Y )  =  ( Z  /  Y ) )
213212fveq2d 5692 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  ( |_ `  ( z  /  Y ) )  =  ( |_ `  ( Z  /  Y ) ) )
214213oveq2d 6106 . . . . . . . . . . . . . 14  |-  ( z  =  Z  ->  (
1 ... ( |_ `  ( z  /  Y
) ) )  =  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
215 simpl 454 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  z  =  Z )
216215oveq1d 6105 . . . . . . . . . . . . . . . . 17  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( z  /  n )  =  ( Z  /  n ) )
217216fveq2d 5692 . . . . . . . . . . . . . . . 16  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( R `  ( z  /  n
) )  =  ( R `  ( Z  /  n ) ) )
218217fveq2d 5692 . . . . . . . . . . . . . . 15  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( abs `  ( R `  ( z  /  n ) ) )  =  ( abs `  ( R `  ( Z  /  n ) ) ) )
219218oveq1d 6105 . . . . . . . . . . . . . 14  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( ( abs `  ( R `  (
z  /  n ) ) )  x.  ( log `  n ) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )
220214, 219sumeq12rdv 13180 . . . . . . . . . . . . 13  |-  ( z  =  Z  ->  sum_ n  e.  ( 1 ... ( |_ `  ( z  /  Y ) ) ) ( ( abs `  ( R `  ( z  /  n ) ) )  x.  ( log `  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )
221211, 220syl5eq 2485 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  sum_ i  e.  ( 1 ... ( |_ `  ( z  /  Y ) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) )  = 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) ) )
222205, 221oveq12d 6108 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
( 2  /  ( log `  z ) )  x.  sum_ i  e.  ( 1 ... ( |_
`  ( z  /  Y ) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) ) )  =  ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) ) )
223204, 222oveq12d 6108 . . . . . . . . . 10  |-  ( z  =  Z  ->  (
( ( abs `  ( R `  z )
)  x.  ( log `  z ) )  -  ( ( 2  / 
( log `  z
) )  x.  sum_ i  e.  ( 1 ... ( |_ `  ( z  /  Y
) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) ) ) )  =  ( ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) )  -  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) ) ) )
224 id 22 . . . . . . . . . 10  |-  ( z  =  Z  ->  z  =  Z )
225223, 224oveq12d 6108 . . . . . . . . 9  |-  ( z  =  Z  ->  (
( ( ( abs `  ( R `  z
) )  x.  ( log `  z ) )  -  ( ( 2  /  ( log `  z
) )  x.  sum_ i  e.  ( 1 ... ( |_ `  ( z  /  Y
) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) ) ) )  /  z )  =  ( ( ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) )  -  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) ) )  /  Z ) )
226225breq1d 4299 . . . . . . . 8  |-  ( z  =  Z  ->  (
( ( ( ( abs `  ( R `
 z ) )  x.  ( log `  z
) )  -  (
( 2  /  ( log `  z ) )  x.  sum_ i  e.  ( 1 ... ( |_
`  ( z  /  Y ) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) ) ) )  /  z )  <_  C  <->  ( (
( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) )  -  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) ) )  /  Z )  <_  C ) )
227226rspcv 3066 . . . . . . 7  |-  ( Z  e.  ( 1 (,) +oo )  ->  ( A. z  e.  ( 1 (,) +oo ) ( ( ( ( abs `  ( R `  z
) )  x.  ( log `  z ) )  -  ( ( 2  /  ( log `  z
) )  x.  sum_ i  e.  ( 1 ... ( |_ `  ( z  /  Y
) ) ) ( ( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) ) ) )  /  z )  <_  C  ->  (
( ( ( abs `  ( R `  Z
) )  x.  ( log `  Z ) )  -  ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) ) )  /  Z )  <_  C ) )
228199, 200, 227sylc 60 . . . . . 6  |-  ( ph  ->  ( ( ( ( abs `  ( R `
 Z ) )  x.  ( log `  Z
) )  -  (
( 2  /  ( log `  Z ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) ) ) )  /  Z )  <_  C )
229194, 228eqbrtrrd 4311 . . . . 5  |-  ( ph  ->  ( ( ( abs `  ( ( R `  Z )  /  Z
) )  x.  ( log `  Z ) )  -  ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) ) )  <_  C
)
23025, 147, 57lesubadd2d 9934 . . . . 5  |-  ( ph  ->  ( ( ( ( abs `  ( ( R `  Z )  /  Z ) )  x.  ( log `  Z
) )  -  (
( 2  /  ( log `  Z ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) )  <_  C  <->  ( ( abs `  ( ( R `
 Z )  /  Z ) )  x.  ( log `  Z
) )  <_  (
( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  +  C ) ) )
231229, 230mpbid 210 . . . 4  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  <_ 
( ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  +  C ) )
232 2cnd 10390 . . . . . . 7  |-  ( ph  ->  2  e.  CC )
233143recnd 9408 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  CC )
234233, 181mulcld 9402 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  CC )
235133, 234fsumcl 13206 . . . . . . 7  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  CC )
236131rpne0d 11028 . . . . . . 7  |-  ( ph  ->  ( log `  Z
)  =/=  0 )
237232, 235, 61, 236div23d 10140 . . . . . 6  |-  ( ph  ->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) )  / 
( log `  Z
) )  =  ( ( 2  /  ( log `  Z ) )  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) )
23824resqcld 12030 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  RR )
23952, 238remulcld 9410 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  e.  RR )
24036, 239remulcld 9410 . . . . . . . . . 10  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR )
241 remulcl 9363 . . . . . . . . . 10  |-  ( ( 2  e.  RR  /\  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR )  ->  ( 2  x.  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  e.  RR )
24231, 240, 241sylancr 658 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  (
( U  -  E
)  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  e.  RR )
24330, 24remulcld 9410 . . . . . . . . 9  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) )  e.  RR )
244 remulcl 9363 . . . . . . . . . 10  |-  ( ( 2  e.  RR  /\  sum_
n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  RR )  ->  ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) )  e.  RR )
24531, 146, 244sylancr 658 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  e.  RR )
24626adantr 462 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  U  e.  RR )
247246, 136nndivred 10366 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  RR )
248247, 143resubcld 9772 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  e.  RR )
249248, 144remulcld 9410 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
250133, 249fsumrecl 13207 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR )
25132, 250remulcld 9410 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  e.  RR )
252243, 245resubcld 9772 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  x.  ( log `  Z ) )  -  ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) )  e.  RR )
253 pntlem1.m . . . . . . . . . . . 12  |-  M  =  ( ( |_ `  ( ( log `  X
)  /  ( log `  K ) ) )  +  1 )
254 pntlem1.n . . . . . . . . . . . 12  |-  N  =  ( |_ `  (
( ( log `  Z
)  /  ( log `  K ) )  / 
2 ) )
255 pntlem1.U . . . . . . . . . . . 12  |-  ( ph  ->  A. z  e.  ( Y [,) +oo )
( abs `  (
( R `  z
)  /  z ) )  <_  U )
256 pntlem1.K . . . . . . . . . . . 12  |-  ( 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 ) )
2571, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 253, 254, 255, 256pntlemf 22813 . . . . . . . . . . 11  |-  ( 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 ) ) )
258 2pos 10409 . . . . . . . . . . . . 13  |-  0  <  2
259258a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  2 )
260 lemul2 10178 . . . . . . . . . . . 12  |-  ( ( ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR  /\ 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
( 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 ) )  <->  ( 2  x.  ( ( U  -  E )  x.  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  <_ 
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
261240, 250, 32, 259, 260syl112anc 1217 . . . . . . . . . . 11  |-  ( 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 ) )  <->  ( 2  x.  ( ( U  -  E )  x.  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  <_ 
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) ) )
262257, 261mpbid 210 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  (
( U  -  E
)  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  <_ 
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) ) )
263247recnd 9408 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  CC )
264263, 233, 181subdird 9797 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  =  ( ( ( U  /  n )  x.  ( log `  n ) )  -  ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) ) )
265264sumeq2dv 13176 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  x.  ( log `  n
) )  -  (
( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) )
266247, 144remulcld 9410 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  e.  RR )
267266recnd 9408 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  e.  CC )
268133, 267, 234fsumsub 13251 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  x.  ( log `  n ) )  -  ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) )  -  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) ) )
269265, 268eqtrd 2473 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  =  (
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  -  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) )
270269oveq2d 6106 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  =  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n ) )  -  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) ) )
271133, 266fsumrecl 13207 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  e.  RR )
272271recnd 9408 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  e.  CC )
273232, 272, 235subdid 9796 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  ( sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  -  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) )  =  ( ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n ) ) )  -  ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) ) )
274270, 273eqtrd 2473 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  =  ( ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n ) ) )  -  ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) ) )
275 remulcl 9363 . . . . . . . . . . . . 13  |-  ( ( 2  e.  RR  /\  sum_
n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  e.  RR )  ->  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n ) ) )  e.  RR )
27631, 271, 275sylancr 658 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  e.  RR )
2771, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 253, 254, 255, 256pntlemk 22814 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  <_ 
( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) ) )
278276, 243, 245, 277lesub1dd 9951 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) ) )  -  ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) )  <_  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  x.  ( log `  Z
) )  -  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) ) )
279274, 278eqbrtrd 4309 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  <_  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  x.  ( log `  Z
) )  -  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) ) )
280242, 251, 252, 262, 279letrd 9524 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  (
( U  -  E
)  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  <_ 
( ( ( U  x.  ( ( log `  Z )  +  3 ) )  x.  ( log `  Z ) )  -  ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) ) ) )
281242, 243, 245, 280lesubd 9939 . . . . . . . 8  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  <_  ( (
( U  x.  (
( log `  Z
)  +  3 ) )  x.  ( log `  Z ) )  -  ( 2  x.  (
( U  -  E
)  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) ) ) )
28230recnd 9408 . . . . . . . . . 10  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  e.  CC )
28355recnd 9408 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  CC )
284282, 283, 61subdird 9797 . . . . . . . . 9  |-  ( ph  ->  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  -  (
2  x.  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  x.  ( log `  Z
) )  =  ( ( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) )  -  ( ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  x.  ( log `  Z
) ) ) )
28554recnd 9408 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  e.  CC )
286232, 285, 61mulassd 9405 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  x.  ( log `  Z
) )  =  ( 2  x.  ( ( ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  x.  ( log `  Z ) ) ) )
28760, 61, 61mulassd 9405 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  x.  ( log `  Z ) )  =  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( ( log `  Z
)  x.  ( log `  Z ) ) ) )
28861sqvald 12001 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  =  ( ( log `  Z )  x.  ( log `  Z ) ) )
289288oveq2d 6106 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( ( log `  Z
) ^ 2 ) )  =  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( ( log `  Z
)  x.  ( log `  Z ) ) ) )
29051rpcnd 11025 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  CC )
291238recnd 9408 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  CC )
292117, 290, 291mulassd 9405 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( ( log `  Z
) ^ 2 ) )  =  ( ( U  -  E )  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )
293287, 289, 2923eqtr2d 2479 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  x.  ( log `  Z ) )  =  ( ( U  -  E )  x.  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )
294293oveq2d 6106 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  (
( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  x.  ( log `  Z ) ) )  =  ( 2  x.  ( ( U  -  E )  x.  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) ) )
295286, 294eqtrd 2473 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  x.  ( log `  Z
) )  =  ( 2  x.  ( ( U  -  E )  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) ) )
296295oveq2d 6106 . . . . . . . . 9  |-  ( ph  ->  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  x.  ( log `  Z ) )  -  ( ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  x.  ( log `  Z
) ) )  =  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  x.  ( log `  Z ) )  -  ( 2  x.  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) ) ) )
297284, 296eqtrd 2473 . . . . . . . 8  |-  ( ph  ->  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  -  (
2  x.  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  x.  ( log `  Z
) )  =  ( ( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) )  -  ( 2  x.  (
( U  -  E
)  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) ) ) )
298281, 297breqtrrd 4315 . . . . . . 7  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  <_  ( (
( U  x.  (
( log `  Z
)  +  3 ) )  -  ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  x.  ( log `  Z
) ) )
299245, 56, 131ledivmul2d 11073 . . . . . . 7  |-  ( ph  ->  ( ( ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) )  / 
( log `  Z
) )  <_  (
( U  x.  (
( log `  Z
)  +  3 ) )  -  ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  <-> 
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  <_  ( (
( U  x.  (
( log `  Z
)  +  3 ) )  -  ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  x.  ( log `  Z
) ) ) )
300298, 299mpbird 232 . . . . . 6  |-  ( ph  ->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) ) )  / 
( log `  Z
) )  <_  (
( U  x.  (
( log `  Z
)  +  3 ) )  -  ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) ) )
301237, 300eqbrtrrd 4311 . . . . 5  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  <_  ( ( U  x.  ( ( log `  Z )  +  3 ) )  -  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) ) )
302147, 56, 57, 301leadd1dd 9949 . . . 4  |-  ( ph  ->  ( ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  +  C )  <_  ( ( ( U  x.  ( ( log `  Z )  +  3 ) )  -  ( 2  x.  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  +  C ) )
30325, 148, 58, 231, 302letrd 9524 . . 3  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  <_ 
( ( ( U  x.  ( ( log `  Z )  +  3 ) )  -  (
2  x.  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  +  C ) )
304 remulcl 9363 . . . . . . . . 9  |-  ( ( U  e.  RR  /\  3  e.  RR )  ->  ( U  x.  3 )  e.  RR )
30526, 27, 304sylancl 657 . . . . . . . 8  |-  ( ph  ->  ( U  x.  3 )  e.  RR )
306305, 57readdcld 9409 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  3 )  +  C
)  e.  RR )
30716simp3d 997 . . . . . . . 8  |-  ( ph  ->  ( ( 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
) ) ) )
308307simp3d 997 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  3 )  +  C
)  <_  ( (
( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )
309306, 54, 125, 308leadd2dd 9950 . . . . . 6  |-  ( ph  ->  ( ( U  x.  ( log `  Z ) )  +  ( ( U  x.  3 )  +  C ) )  <_  ( ( U  x.  ( log `  Z
) )  +  ( ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )
31028recnd 9408 . . . . . . . . 9  |-  ( ph  ->  3  e.  CC )
31159, 61, 310adddid 9406 . . . . . . . 8  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  =  ( ( U  x.  ( log `  Z ) )  +  ( U  x.  3 ) ) )
312311oveq1d 6105 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  +  C )  =  ( ( ( U  x.  ( log `  Z ) )  +  ( U  x.  3 ) )  +  C
) )
313125recnd 9408 . . . . . . . 8  |-  ( ph  ->  ( U  x.  ( log `  Z ) )  e.  CC )
31459, 310mulcld 9402 . . . . . . . 8  |-  ( ph  ->  ( U  x.  3 )  e.  CC )
31513rpcnd 11025 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
316313, 314, 315addassd 9404 . . . . . . 7  |-  ( ph  ->  ( ( ( U  x.  ( log `  Z
) )  +  ( U  x.  3 ) )  +  C )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( U  x.  3 )  +  C ) ) )
317312, 316eqtrd 2473 . . . . . 6  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  +  C )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( U  x.  3 )  +  C ) ) )
3182852timesd 10563 . . . . . . . 8  |-  ( ph  ->  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  =  ( ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  +  ( ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )
319318oveq2d 6106 . . . . . . 7  |-  ( ph  ->  ( ( ( U  x.  ( log `  Z
) )  -  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  +  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  =  ( ( ( U  x.  ( log `  Z ) )  -  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  +  ( ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  +  ( ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) ) )
320313, 285, 285nppcan3d 9742 . . . . . . 7  |-  ( ph  ->  ( ( ( U  x.  ( log `  Z
) )  -  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  +  ( ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  +  ( ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )
321319, 320eqtrd 2473 . . . . . 6  |-  ( ph  ->  ( ( ( U  x.  ( log `  Z
) )  -  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  +  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) ) )
322309, 317, 3213brtr4d 4319 . . . . 5  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  +  C )  <_  ( ( ( U  x.  ( log `  Z ) )  -  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  +  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  (