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

Theorem pntlemo 20756
Description: Lemma for pnt 20763. 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 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
) ) ) ) )
1716simp1d 967 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR+ )
181pntrf 20712 . . . . . . . . 9  |-  R : RR+
--> RR
1918ffvelrni 5664 . . . . . . . 8  |-  ( Z  e.  RR+  ->  ( R `
 Z )  e.  RR )
2017, 19syl 15 . . . . . . 7  |-  ( ph  ->  ( R `  Z
)  e.  RR )
2120, 17rerpdivcld 10417 . . . . . 6  |-  ( ph  ->  ( ( R `  Z )  /  Z
)  e.  RR )
2221recnd 8861 . . . . 5  |-  ( ph  ->  ( ( R `  Z )  /  Z
)  e.  CC )
2322abscld 11918 . . . 4  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  e.  RR )
2417relogcld 19974 . . . 4  |-  ( ph  ->  ( log `  Z
)  e.  RR )
2523, 24remulcld 8863 . . 3  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  e.  RR )
267rpred 10390 . . . . . 6  |-  ( ph  ->  U  e.  RR )
27 3re 9817 . . . . . . . 8  |-  3  e.  RR
2827a1i 10 . . . . . . 7  |-  ( ph  ->  3  e.  RR )
2924, 28readdcld 8862 . . . . . 6  |-  ( ph  ->  ( ( log `  Z
)  +  3 )  e.  RR )
3026, 29remulcld 8863 . . . . 5  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  e.  RR )
31 2re 9815 . . . . . . 7  |-  2  e.  RR
3231a1i 10 . . . . . 6  |-  ( ph  ->  2  e.  RR )
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 20744 . . . . . . . . . . 11  |-  ( ph  ->  ( E  e.  RR+  /\  K  e.  RR+  /\  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E )  e.  RR+ ) ) )
3433simp3d 969 . . . . . . . . . 10  |-  ( ph  ->  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E
)  e.  RR+ )
)
3534simp3d 969 . . . . . . . . 9  |-  ( ph  ->  ( U  -  E
)  e.  RR+ )
3635rpred 10390 . . . . . . . 8  |-  ( ph  ->  ( U  -  E
)  e.  RR )
371, 2, 3, 4, 5, 6pntlemd 20743 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  e.  RR+  /\  D  e.  RR+  /\  F  e.  RR+ ) )
3837simp1d 967 . . . . . . . . . . 11  |-  ( ph  ->  L  e.  RR+ )
3933simp1d 967 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
40 2z 10054 . . . . . . . . . . . 12  |-  2  e.  ZZ
41 rpexpcl 11122 . . . . . . . . . . . 12  |-  ( ( E  e.  RR+  /\  2  e.  ZZ )  ->  ( E ^ 2 )  e.  RR+ )
4239, 40, 41sylancl 643 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  e.  RR+ )
4338, 42rpmulcld 10406 . . . . . . . . . 10  |-  ( ph  ->  ( L  x.  ( E ^ 2 ) )  e.  RR+ )
44 3nn0 9983 . . . . . . . . . . . . 13  |-  3  e.  NN0
45 2nn 9877 . . . . . . . . . . . . 13  |-  2  e.  NN
4644, 45decnncl 10137 . . . . . . . . . . . 12  |- ; 3 2  e.  NN
47 nnrp 10363 . . . . . . . . . . . 12  |-  (; 3 2  e.  NN  -> ; 3
2  e.  RR+ )
4846, 47ax-mp 8 . . . . . . . . . . 11  |- ; 3 2  e.  RR+
49 rpmulcl 10375 . . . . . . . . . . 11  |-  ( (; 3
2  e.  RR+  /\  B  e.  RR+ )  ->  (; 3 2  x.  B )  e.  RR+ )
5048, 3, 49sylancr 644 . . . . . . . . . 10  |-  ( ph  ->  (; 3 2  x.  B
)  e.  RR+ )
5143, 50rpdivcld 10407 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  RR+ )
5251rpred 10390 . . . . . . . 8  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  RR )
5336, 52remulcld 8863 . . . . . . 7  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  e.  RR )
5453, 24remulcld 8863 . . . . . 6  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  e.  RR )
5532, 54remulcld 8863 . . . . 5  |-  ( ph  ->  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  RR )
5630, 55resubcld 9211 . . . 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 10390 . . . 4  |-  ( ph  ->  C  e.  RR )
5856, 57readdcld 8862 . . 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 10392 . . . . . 6  |-  ( ph  ->  U  e.  CC )
6053recnd 8861 . . . . . 6  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  e.  CC )
6124recnd 8861 . . . . . 6  |-  ( ph  ->  ( log `  Z
)  e.  CC )
6259, 60, 61subdird 9236 . . . . 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 10392 . . . . . . . . . . 11  |-  ( ph  ->  L  e.  CC )
6442rpcnd 10392 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
6550rpcnne0d 10399 . . . . . . . . . . 11  |-  ( ph  ->  ( (; 3 2  x.  B
)  e.  CC  /\  (; 3 2  x.  B )  =/=  0 ) )
66 div23 9443 . . . . . . . . . . 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 1182 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  =  ( ( L  /  (; 3 2  x.  B ) )  x.  ( E ^
2 ) ) )
689oveq1i 5868 . . . . . . . . . . . 12  |-  ( E ^ 2 )  =  ( ( U  /  D ) ^ 2 )
6937simp2d 968 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  RR+ )
7069rpcnd 10392 . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  CC )
7169rpne0d 10395 . . . . . . . . . . . . 13  |-  ( ph  ->  D  =/=  0 )
7259, 70, 71sqdivd 11258 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U  /  D ) ^ 2 )  =  ( ( U ^ 2 )  /  ( D ^
2 ) ) )
7368, 72syl5eq 2327 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  =  ( ( U ^ 2 )  /  ( D ^
2 ) ) )
7473oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  x.  ( E ^ 2 ) )  =  ( ( L  /  (; 3 2  x.  B
) )  x.  (
( U ^ 2 )  /  ( D ^ 2 ) ) ) )
7538, 50rpdivcld 10407 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  /  (; 3 2  x.  B ) )  e.  RR+ )
7675rpcnd 10392 . . . . . . . . . . 11  |-  ( ph  ->  ( L  /  (; 3 2  x.  B ) )  e.  CC )
7759sqcld 11243 . . . . . . . . . . 11  |-  ( ph  ->  ( U ^ 2 )  e.  CC )
78 rpexpcl 11122 . . . . . . . . . . . . 13  |-  ( ( D  e.  RR+  /\  2  e.  ZZ )  ->  ( D ^ 2 )  e.  RR+ )
7969, 40, 78sylancl 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( D ^ 2 )  e.  RR+ )
8079rpcnne0d 10399 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D ^
2 )  e.  CC  /\  ( D ^ 2 )  =/=  0 ) )
81 divass 9442 . . . . . . . . . . . 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 9443 . . . . . . . . . . . 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 2317 . . . . . . . . . . 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 1182 . . . . . . . . . 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 2319 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  =  ( ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) )
8685oveq2d 5874 . . . . . . . 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 9805 . . . . . . . . . . . . 13  |-  3  =  ( 2  +  1 )
8887oveq2i 5869 . . . . . . . . . . . 12  |-  ( U ^ 3 )  =  ( U ^ (
2  +  1 ) )
89 2nn0 9982 . . . . . . . . . . . . 13  |-  2  e.  NN0
90 expp1 11110 . . . . . . . . . . . . 13  |-  ( ( U  e.  CC  /\  2  e.  NN0 )  -> 
( U ^ (
2  +  1 ) )  =  ( ( U ^ 2 )  x.  U ) )
9159, 89, 90sylancl 643 . . . . . . . . . . . 12  |-  ( ph  ->  ( U ^ (
2  +  1 ) )  =  ( ( U ^ 2 )  x.  U ) )
9288, 91syl5eq 2327 . . . . . . . . . . 11  |-  ( ph  ->  ( U ^ 3 )  =  ( ( U ^ 2 )  x.  U ) )
9377, 59mulcomd 8856 . . . . . . . . . . 11  |-  ( ph  ->  ( ( U ^
2 )  x.  U
)  =  ( U  x.  ( U ^
2 ) ) )
9492, 93eqtrd 2315 . . . . . . . . . 10  |-  ( ph  ->  ( U ^ 3 )  =  ( U  x.  ( U ^
2 ) ) )
9594oveq2d 5874 . . . . . . . . 9  |-  ( ph  ->  ( F  x.  ( U ^ 3 ) )  =  ( F  x.  ( U  x.  ( U ^ 2 ) ) ) )
9637simp3d 969 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  RR+ )
9796rpcnd 10392 . . . . . . . . . 10  |-  ( ph  ->  F  e.  CC )
9897, 59, 77mulassd 8858 . . . . . . . . 9  |-  ( ph  ->  ( ( F  x.  U )  x.  ( U ^ 2 ) )  =  ( F  x.  ( U  x.  ( U ^ 2 ) ) ) )
99 ax-1cn 8795 . . . . . . . . . . . . . . . 16  |-  1  e.  CC
10099a1i 10 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
10169rpreccld 10400 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  /  D
)  e.  RR+ )
102101rpcnd 10392 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  /  D
)  e.  CC )
103100, 102, 59subdird 9236 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  -  ( 1  /  D
) )  x.  U
)  =  ( ( 1  x.  U )  -  ( ( 1  /  D )  x.  U ) ) )
10459mulid2d 8853 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  x.  U
)  =  U )
10559, 70, 71divrec2d 9540 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( U  /  D
)  =  ( ( 1  /  D )  x.  U ) )
1069, 105syl5req 2328 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1  /  D )  x.  U
)  =  E )
107104, 106oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  x.  U )  -  (
( 1  /  D
)  x.  U ) )  =  ( U  -  E ) )
108103, 107eqtr2d 2316 . . . . . . . . . . . . 13  |-  ( ph  ->  ( U  -  E
)  =  ( ( 1  -  ( 1  /  D ) )  x.  U ) )
109108oveq1d 5873 . . . . . . . . . . . 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 ) ) ) )
1106oveq1i 5868 . . . . . . . . . . . . 13  |-  ( F  x.  U )  =  ( ( ( 1  -  ( 1  /  D ) )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  U )
111100, 102subcld 9157 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  -  (
1  /  D ) )  e.  CC )
11275, 79rpdivcld 10407 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  e.  RR+ )
113112rpcnd 10392 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  e.  CC )
114111, 113, 59mul32d 9022 . . . . . . . . . . . . 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 ) ) ) )
115110, 114syl5eq 2327 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  U
)  =  ( ( ( 1  -  (
1  /  D ) )  x.  U )  x.  ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) ) ) )
116109, 115eqtr4d 2318 . . . . . . . . . . 11  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )  =  ( F  x.  U ) )
117116oveq1d 5873 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  ( U ^ 2 ) )  =  ( ( F  x.  U )  x.  ( U ^ 2 ) ) )
11835rpcnd 10392 . . . . . . . . . . 11  |-  ( ph  ->  ( U  -  E
)  e.  CC )
119118, 113, 77mulassd 8858 . . . . . . . . . 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 ) ) ) )
120117, 119eqtr3d 2317 . . . . . . . . 9  |-  ( ph  ->  ( ( F  x.  U )  x.  ( U ^ 2 ) )  =  ( ( U  -  E )  x.  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
12195, 98, 1203eqtr2d 2321 . . . . . . . 8  |-  ( ph  ->  ( F  x.  ( U ^ 3 ) )  =  ( ( U  -  E )  x.  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
12286, 121eqtr4d 2318 . . . . . . 7  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  =  ( F  x.  ( U ^ 3 ) ) )
123122oveq2d 5874 . . . . . 6  |-  ( ph  ->  ( U  -  (
( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) ) )  =  ( U  -  ( F  x.  ( U ^ 3 ) ) ) )
124123oveq1d 5873 . . . . 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 ) ) )
12562, 124eqtr3d 2317 . . . 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 ) ) )
12626, 24remulcld 8863 . . . . 5  |-  ( ph  ->  ( U  x.  ( log `  Z ) )  e.  RR )
127126, 54resubcld 9211 . . . 4  |-  ( ph  ->  ( ( U  x.  ( log `  Z ) )  -  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  RR )
128125, 127eqeltrrd 2358 . . 3  |-  ( ph  ->  ( ( U  -  ( F  x.  ( U ^ 3 ) ) )  x.  ( log `  Z ) )  e.  RR )
12917rpred 10390 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR )
13016simp2d 968 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  Z  /\  _e  <_  ( sqr `  Z )  /\  ( sqr `  Z )  <_ 
( Z  /  Y
) ) )
131130simp1d 967 . . . . . . . 8  |-  ( ph  ->  1  <  Z )
132129, 131rplogcld 19980 . . . . . . 7  |-  ( ph  ->  ( log `  Z
)  e.  RR+ )
13332, 132rerpdivcld 10417 . . . . . 6  |-  ( ph  ->  ( 2  /  ( log `  Z ) )  e.  RR )
134 fzfid 11035 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
13517adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  RR+ )
136 elfznn 10819 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  NN )
137136adantl 452 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  NN )
138137nnrpd 10389 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  RR+ )
139135, 138rpdivcld 10407 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  /  n )  e.  RR+ )
14018ffvelrni 5664 . . . . . . . . . . . 12  |-  ( ( Z  /  n )  e.  RR+  ->  ( R `
 ( Z  /  n ) )  e.  RR )
141139, 140syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( R `  ( Z  /  n
) )  e.  RR )
142141, 135rerpdivcld 10417 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  RR )
143142recnd 8861 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  CC )
144143abscld 11918 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  RR )
145138relogcld 19974 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  RR )
146144, 145remulcld 8863 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  RR )
147134, 146fsumrecl 12207 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  RR )
148133, 147remulcld 8863 . . . . 5  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  e.  RR )
149148, 57readdcld 8862 . . . 4  |-  ( ph  ->  ( ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  +  C )  e.  RR )
15020recnd 8861 . . . . . . . . . . 11  |-  ( ph  ->  ( R `  Z
)  e.  CC )
151150abscld 11918 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  ( R `  Z )
)  e.  RR )
152151recnd 8861 . . . . . . . . 9  |-  ( ph  ->  ( abs `  ( R `  Z )
)  e.  CC )
153152, 61mulcld 8855 . . . . . . . 8  |-  ( ph  ->  ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) )  e.  CC )
154133recnd 8861 . . . . . . . . 9  |-  ( ph  ->  ( 2  /  ( log `  Z ) )  e.  CC )
155141recnd 8861 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( R `  ( Z  /  n
) )  e.  CC )
156155abscld 11918 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( R `  ( Z  /  n ) ) )  e.  RR )
157156, 145remulcld 8863 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  x.  ( log `  n
) )  e.  RR )
158134, 157fsumrecl 12207 . . . . . . . . . 10  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  e.  RR )
159158recnd 8861 . . . . . . . . 9  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  e.  CC )
160154, 159mulcld 8855 . . . . . . . 8  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )  e.  CC )
16117rpcnd 10392 . . . . . . . 8  |-  ( ph  ->  Z  e.  CC )
16217rpne0d 10395 . . . . . . . 8  |-  ( ph  ->  Z  =/=  0 )
163153, 160, 161, 162divsubdird 9575 . . . . . . 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 ) ) )
164152, 61, 161, 162div23d 9573 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  ( R `  Z
) )  x.  ( log `  Z ) )  /  Z )  =  ( ( ( abs `  ( R `  Z
) )  /  Z
)  x.  ( log `  Z ) ) )
165150, 161, 162absdivd 11937 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  =  ( ( abs `  ( R `
 Z ) )  /  ( abs `  Z
) ) )
16617rprege0d 10397 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Z  e.  RR  /\  0  <_  Z )
)
167 absid 11781 . . . . . . . . . . . . 13  |-  ( ( Z  e.  RR  /\  0  <_  Z )  -> 
( abs `  Z
)  =  Z )
168166, 167syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  Z
)  =  Z )
169168oveq2d 5874 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  ( R `  Z )
)  /  ( abs `  Z ) )  =  ( ( abs `  ( R `  Z )
)  /  Z ) )
170165, 169eqtrd 2315 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  =  ( ( abs `  ( R `
 Z ) )  /  Z ) )
171170oveq1d 5873 . . . . . . . . 9  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  =  ( ( ( abs `  ( R `  Z
) )  /  Z
)  x.  ( log `  Z ) ) )
172164, 171eqtr4d 2318 . . . . . . . 8  |-  ( ph  ->  ( ( ( abs `  ( R `  Z
) )  x.  ( log `  Z ) )  /  Z )  =  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) ) )
173154, 159, 161, 162divassd 9571 . . . . . . . . 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
) ) )
174161adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  CC )
175162adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  =/=  0 )
176155, 174, 175absdivd 11937 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  ( abs `  Z
) ) )
177168adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  Z )  =  Z )
178177oveq2d 5874 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  / 
( abs `  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z ) )
179176, 178eqtrd 2315 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z ) )
180179oveq1d 5873 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z )  x.  ( log `  n
) ) )
181156recnd 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( R `  ( Z  /  n ) ) )  e.  CC )
182145recnd 8861 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  CC )
18317rpcnne0d 10399 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Z  e.  CC  /\  Z  =/=  0 ) )
184183adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  e.  CC  /\  Z  =/=  0 ) )
185 div23 9443 . . . . . . . . . . . . . 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
) ) )
186181, 182, 184, 185syl3anc 1182 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
)  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z )  x.  ( log `  n
) ) )
187180, 186eqtr4d 2318 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
) )
188187sumeq2dv 12176 . . . . . . . . . . 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
) )
189157recnd 8861 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  x.  ( log `  n
) )  e.  CC )
190134, 161, 189, 162fsumdivc 12248 . . . . . . . . . . 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 ) )
191188, 190eqtr4d 2318 . . . . . . . . . 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
) )
192191oveq2d 5874 . . . . . . . . 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
) ) )
193173, 192eqtr4d 2318 . . . . . . . 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 ) ) ) )
194172, 193oveq12d 5876 . . . . . . 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 ) ) ) ) )
195163, 194eqtrd 2315 . . . . . 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 ) ) ) ) )
196 1re 8837 . . . . . . . . 9  |-  1  e.  RR
197 rexr 8877 . . . . . . . . 9  |-  ( 1  e.  RR  ->  1  e.  RR* )
198 elioopnf 10737 . . . . . . . . 9  |-  ( 1  e.  RR*  ->  ( Z  e.  ( 1 (,) 
+oo )  <->  ( Z  e.  RR  /\  1  < 
Z ) ) )
199196, 197, 198mp2b 9 . . . . . . . 8  |-  ( Z  e.  ( 1 (,) 
+oo )  <->  ( Z  e.  RR  /\  1  < 
Z ) )
200129, 131, 199sylanbrc 645 . . . . . . 7  |-  ( ph  ->  Z  e.  ( 1 (,)  +oo ) )
201 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 )
202 fveq2 5525 . . . . . . . . . . . . 13  |-  ( z  =  Z  ->  ( R `  z )  =  ( R `  Z ) )
203202fveq2d 5529 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  ( abs `  ( R `  z ) )  =  ( abs `  ( R `  Z )
) )
204 fveq2 5525 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  ( log `  z )  =  ( log `  Z
) )
205203, 204oveq12d 5876 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
( abs `  ( R `  z )
)  x.  ( log `  z ) )  =  ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) ) )
206204oveq2d 5874 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  (
2  /  ( log `  z ) )  =  ( 2  /  ( log `  Z ) ) )
207 oveq2 5866 . . . . . . . . . . . . . . . . 17  |-  ( i  =  n  ->  (
z  /  i )  =  ( z  /  n ) )
208207fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( i  =  n  ->  ( R `  ( z  /  i ) )  =  ( R `  ( z  /  n
) ) )
209208fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( i  =  n  ->  ( abs `  ( R `  ( z  /  i
) ) )  =  ( abs `  ( R `  ( z  /  n ) ) ) )
210 fveq2 5525 . . . . . . . . . . . . . . 15  |-  ( i  =  n  ->  ( log `  i )  =  ( log `  n
) )
211209, 210oveq12d 5876 . . . . . . . . . . . . . 14  |-  ( i  =  n  ->  (
( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) )  =  ( ( abs `  ( R `  ( z  /  n ) ) )  x.  ( log `  n
) ) )
212211cbvsumv 12169 . . . . . . . . . . . . 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
) )
213 oveq1 5865 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  (
z  /  Y )  =  ( Z  /  Y ) )
214213fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  ( |_ `  ( z  /  Y ) )  =  ( |_ `  ( Z  /  Y ) ) )
215214oveq2d 5874 . . . . . . . . . . . . . 14  |-  ( z  =  Z  ->  (
1 ... ( |_ `  ( z  /  Y
) ) )  =  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
216 simpl 443 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  z  =  Z )
217216oveq1d 5873 . . . . . . . . . . . . . . . . 17  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( z  /  n )  =  ( Z  /  n ) )
218217fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( R `  ( z  /  n
) )  =  ( R `  ( Z  /  n ) ) )
219218fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( abs `  ( R `  ( z  /  n ) ) )  =  ( abs `  ( R `  ( Z  /  n ) ) ) )
220219oveq1d 5873 . . . . . . . . . . . . . 14  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( ( abs `  ( R `  (
z  /  n ) ) )  x.  ( log `  n ) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )
221215, 220sumeq12rdv 12180 . . . . . . . . . . . . 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 ) ) )
222212, 221syl5eq 2327 . . . . . . . . . . . 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
) ) )
223206, 222oveq12d 5876 . . . . . . . . . . 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 ) ) ) )
224205, 223oveq12d 5876 . . . . . . . . . 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 ) ) ) ) )
225 id 19 . . . . . . . . . 10  |-  ( z  =  Z  ->  z  =  Z )
226224, 225oveq12d 5876 . . . . . . . . 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 ) )
227226breq1d 4033 . . . . . . . 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 ) )
228227rspcv 2880 . . . . . . 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 ) )
229200, 201, 228sylc 56 . . . . . 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 )
230195, 229eqbrtrrd 4045 . . . . 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
)
23125, 148, 57lesubadd2d 9371 . . . . 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 ) ) )
232230, 231mpbid 201 . . . 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 ) )
233 2cn 9816 . . . . . . . 8  |-  2  e.  CC
234233a1i 10 . . . . . . 7  |-  ( ph  ->  2  e.  CC )
235144recnd 8861 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  CC )
236235, 182mulcld 8855 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  CC )
237134, 236fsumcl 12206 . . . . . . 7  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  CC )
238132rpne0d 10395 . . . . . . 7  |-  ( ph  ->  ( log `  Z
)  =/=  0 )
239234, 237, 61, 238div23d 9573 . . . . . 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
) ) ) )
24024resqcld 11271 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  RR )
24152, 240remulcld 8863 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  e.  RR )
24236, 241remulcld 8863 . . . . . . . . . 10  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR )
243 remulcl 8822 . . . . . . . . . 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 )
24431, 242, 243sylancr 644 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  (
( U  -  E
)  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  e.  RR )
24530, 24remulcld 8863 . . . . . . . . 9  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) )  e.  RR )
246 remulcl 8822 . . . . . . . . . 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 )
24731, 147, 246sylancr 644 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  e.  RR )
24826adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  U  e.  RR )
249248, 137nndivred 9794 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  RR )
250249, 144resubcld 9211 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  e.  RR )
251250, 145remulcld 8863 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
252134, 251fsumrecl 12207 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR )
25332, 252remulcld 8863 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  e.  RR )
254245, 247resubcld 9211 . . . . . . . . . 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 )
255 pntlem1.m . . . . . . . . . . . 12  |-  M  =  ( ( |_ `  ( ( log `  X
)  /  ( log `  K ) ) )  +  1 )
256 pntlem1.n . . . . . . . . . . . 12  |-  N  =  ( |_ `  (
( ( log `  Z
)  /  ( log `  K ) )  / 
2 ) )
257 pntlem1.U . . . . . . . . . . . 12  |-  ( ph  ->  A. z  e.  ( Y [,)  +oo )
( abs `  (
( R `  z
)  /  z ) )  <_  U )
258 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 ) )
2591, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 255, 256, 257, 258pntlemf 20754 . . . . . . . . . . 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 ) ) )
260 2pos 9828 . . . . . . . . . . . . 13  |-  0  <  2
261260a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  2 )
262 lemul2 9609 . . . . . . . . . . . 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 ) ) ) ) )
263242, 252, 32, 261, 262syl112anc 1186 . . . . . . . . . . 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 ) ) ) ) )
264259, 263mpbid 201 . . . . . . . . . 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 ) ) ) )
265249recnd 8861 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  CC )
266265, 235, 182subdird 9236 . . . . . . . . . . . . . . 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 ) ) ) )
267266sumeq2dv 12176 . . . . . . . . . . . . . 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
) ) ) )
268249, 145remulcld 8863 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  e.  RR )
269268recnd 8861 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  e.  CC )
270134, 269, 236fsumsub 12250 . . . . . . . . . . . . . 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 ) ) ) )
271267, 270eqtrd 2315 . . . . . . . . . . . . 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
) ) ) )
272271oveq2d 5874 . . . . . . . . . . . 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
) ) ) ) )
273134, 268fsumrecl 12207 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  e.  RR )
274273recnd 8861 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  e.  CC )
275234, 274, 237subdid 9235 . . . . . . . . . . . 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
) ) ) ) )
276272, 275eqtrd 2315 . . . . . . . . . . 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
) ) ) ) )
277 remulcl 8822 . . . . . . . . . . . . 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 )
27831, 273, 277sylancr 644 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  e.  RR )
2791, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 255, 256, 257, 258pntlemk 20755 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  <_ 
( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) ) )
280278, 245, 247, 279lesub1dd 9388 . . . . . . . . . . 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
) ) ) ) )
281276, 280eqbrtrd 4043 . . . . . . . . . 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
) ) ) ) )
282244, 253, 254, 264, 281letrd 8973 . . . . . . . . 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
) ) ) ) )
283244, 245, 247, 282lesubd 9376 . . . . . . . 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 ) ) ) ) ) )
28430recnd 8861 . . . . . . . . . 10  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  e.  CC )
28555recnd 8861 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  CC )
286284, 285, 61subdird 9236 . . . . . . . . 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
) ) ) )
28754recnd 8861 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  e.  CC )
288234, 287, 61mulassd 8858 . . . . . . . . . . 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 ) ) ) )
28960, 61, 61mulassd 8858 . . . . . . . . . . . . 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 ) ) ) )
29061sqvald 11242 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  =  ( ( log `  Z )  x.  ( log `  Z ) ) )
291290oveq2d 5874 . . . . . . . . . . . . 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 ) ) ) )
29251rpcnd 10392 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  CC )
293240recnd 8861 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  CC )
294118, 292, 293mulassd 8858 . . . . . . . . . . . . 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 ) ) ) )
295289, 291, 2943eqtr2d 2321 . . . . . . . . . . . 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 ) ) ) )
296295oveq2d 5874 . . . . . . . . . . 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 ) ) ) ) )
297288, 296eqtrd 2315 . . . . . . . . . 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 ) ) ) ) )
298297oveq2d 5874 . . . . . . . . 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 ) ) ) ) ) )
299286, 298eqtrd 2315 . . . . . . . 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 ) ) ) ) ) )
300283, 299breqtrrd 4049 . . . . . . 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
) ) )
301247, 56, 132ledivmul2d 10440 . . . . . . 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
) ) ) )
302300, 301mpbird 223 . . . . . 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
) ) ) ) )
303239, 302eqbrtrrd 4045 . . . . 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
) ) ) ) )
304148, 56, 57, 303leadd1dd 9386 . . . 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 ) )
30525, 149, 58, 232, 304letrd 8973 . . 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 ) )
306 remulcl 8822 . . . . . . . . 9  |-  ( ( U  e.  RR  /\  3  e.  RR )  ->  ( U  x.  3 )  e.  RR )
30726, 27, 306sylancl 643 . . . . . . . 8  |-  ( ph  ->  ( U  x.  3 )  e.  RR )
308307, 57readdcld 8862 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  3 )  +  C
)  e.  RR )
30916simp3d 969 . . . . . . . 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
) ) ) )
310309simp3d 969 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  3 )  +  C
)  <_  ( (
( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )
311308, 54, 126, 310leadd2dd 9387 . . . . . 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
) ) ) )
31228recnd 8861 . . . . . . . . 9  |-  ( ph  ->  3  e.  CC )
31359, 61, 312adddid 8859 . . . . . . . 8  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  =  ( ( U  x.  ( log `  Z ) )  +  ( U  x.  3 ) ) )
314313oveq1d 5873 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  +  C )  =  ( ( ( U  x.  ( log `  Z ) )  +  ( U  x.  3 ) )  +  C
) )
315126recnd 8861 . . . . . . . 8  |-  ( ph  ->  ( U  x.  ( log `  Z ) )  e.  CC )
31659, 312mulcld 8855 . . . . . . . 8  |-  ( ph  ->  ( U  x.  3 )  e.  CC )
31713rpcnd 10392 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
318315, 316, 317addassd 8857 . . . . . . 7  |-  ( ph  ->  ( ( ( U  x.  ( log `  Z
) )  +  ( U  x.  3 ) )  +  C )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( U  x.  3 )  +  C ) ) )
319314, 318eqtrd 2315 . . . . . 6  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  +  C )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( U  x.  3 )  +  C ) ) )
3202872timesd 9954 . . . . . . . 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
) ) ) )
321320oveq2d 5874 . . . . . . 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
) ) ) ) )
322315, 287, 287nppcan3d 9184 . . . . . . 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
) ) ) )
323321, 322eqtrd 2315 . . . . . 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
) )