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

Theorem pntlemo 22859
Description: Lemma for pnt 22866. 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 22849 . . . . . . . . 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 1000 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR+ )
181pntrf 22815 . . . . . . . . 9  |-  R : RR+
--> RR
1918ffvelrni 5845 . . . . . . . 8  |-  ( Z  e.  RR+  ->  ( R `
 Z )  e.  RR )
2017, 19syl 16 . . . . . . 7  |-  ( ph  ->  ( R `  Z
)  e.  RR )
2120, 17rerpdivcld 11057 . . . . . 6  |-  ( ph  ->  ( ( R `  Z )  /  Z
)  e.  RR )
2221recnd 9415 . . . . 5  |-  ( ph  ->  ( ( R `  Z )  /  Z
)  e.  CC )
2322abscld 12925 . . . 4  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  e.  RR )
2417relogcld 22075 . . . 4  |-  ( ph  ->  ( log `  Z
)  e.  RR )
2523, 24remulcld 9417 . . 3  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  e.  RR )
267rpred 11030 . . . . . 6  |-  ( ph  ->  U  e.  RR )
27 3re 10398 . . . . . . . 8  |-  3  e.  RR
2827a1i 11 . . . . . . 7  |-  ( ph  ->  3  e.  RR )
2924, 28readdcld 9416 . . . . . 6  |-  ( ph  ->  ( ( log `  Z
)  +  3 )  e.  RR )
3026, 29remulcld 9417 . . . . 5  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  e.  RR )
31 2re 10394 . . . . . . 7  |-  2  e.  RR
3231a1i 11 . . . . . 6  |-  ( ph  ->  2  e.  RR )
331, 2, 3, 4, 5, 6, 7, 8, 9, 10pntlemc 22847 . . . . . . . . . . 11  |-  ( ph  ->  ( E  e.  RR+  /\  K  e.  RR+  /\  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E )  e.  RR+ ) ) )
3433simp3d 1002 . . . . . . . . . 10  |-  ( ph  ->  ( E  e.  ( 0 (,) 1 )  /\  1  <  K  /\  ( U  -  E
)  e.  RR+ )
)
3534simp3d 1002 . . . . . . . . 9  |-  ( ph  ->  ( U  -  E
)  e.  RR+ )
3635rpred 11030 . . . . . . . 8  |-  ( ph  ->  ( U  -  E
)  e.  RR )
371, 2, 3, 4, 5, 6pntlemd 22846 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  e.  RR+  /\  D  e.  RR+  /\  F  e.  RR+ ) )
3837simp1d 1000 . . . . . . . . . . 11  |-  ( ph  ->  L  e.  RR+ )
3933simp1d 1000 . . . . . . . . . . . 12  |-  ( ph  ->  E  e.  RR+ )
40 2z 10681 . . . . . . . . . . . 12  |-  2  e.  ZZ
41 rpexpcl 11887 . . . . . . . . . . . 12  |-  ( ( E  e.  RR+  /\  2  e.  ZZ )  ->  ( E ^ 2 )  e.  RR+ )
4239, 40, 41sylancl 662 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  e.  RR+ )
4338, 42rpmulcld 11046 . . . . . . . . . 10  |-  ( ph  ->  ( L  x.  ( E ^ 2 ) )  e.  RR+ )
44 3nn0 10600 . . . . . . . . . . . . 13  |-  3  e.  NN0
45 2nn 10482 . . . . . . . . . . . . 13  |-  2  e.  NN
4644, 45decnncl 10771 . . . . . . . . . . . 12  |- ; 3 2  e.  NN
47 nnrp 11003 . . . . . . . . . . . 12  |-  (; 3 2  e.  NN  -> ; 3
2  e.  RR+ )
4846, 47ax-mp 5 . . . . . . . . . . 11  |- ; 3 2  e.  RR+
49 rpmulcl 11015 . . . . . . . . . . 11  |-  ( (; 3
2  e.  RR+  /\  B  e.  RR+ )  ->  (; 3 2  x.  B )  e.  RR+ )
5048, 3, 49sylancr 663 . . . . . . . . . 10  |-  ( ph  ->  (; 3 2  x.  B
)  e.  RR+ )
5143, 50rpdivcld 11047 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  RR+ )
5251rpred 11030 . . . . . . . 8  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  RR )
5336, 52remulcld 9417 . . . . . . 7  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  e.  RR )
5453, 24remulcld 9417 . . . . . 6  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  e.  RR )
5532, 54remulcld 9417 . . . . 5  |-  ( ph  ->  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  RR )
5630, 55resubcld 9779 . . . 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 11030 . . . 4  |-  ( ph  ->  C  e.  RR )
5856, 57readdcld 9416 . . 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 11032 . . . . . 6  |-  ( ph  ->  U  e.  CC )
6053recnd 9415 . . . . . 6  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  e.  CC )
6124recnd 9415 . . . . . 6  |-  ( ph  ->  ( log `  Z
)  e.  CC )
6259, 60, 61subdird 9804 . . . . 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 11032 . . . . . . . . . . 11  |-  ( ph  ->  L  e.  CC )
6442rpcnd 11032 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  e.  CC )
6550rpcnne0d 11039 . . . . . . . . . . 11  |-  ( ph  ->  ( (; 3 2  x.  B
)  e.  CC  /\  (; 3 2  x.  B )  =/=  0 ) )
66 div23 10016 . . . . . . . . . . 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 1218 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  =  ( ( L  /  (; 3 2  x.  B ) )  x.  ( E ^
2 ) ) )
689oveq1i 6104 . . . . . . . . . . . 12  |-  ( E ^ 2 )  =  ( ( U  /  D ) ^ 2 )
6937simp2d 1001 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  RR+ )
7069rpcnd 11032 . . . . . . . . . . . . 13  |-  ( ph  ->  D  e.  CC )
7169rpne0d 11035 . . . . . . . . . . . . 13  |-  ( ph  ->  D  =/=  0 )
7259, 70, 71sqdivd 12024 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( U  /  D ) ^ 2 )  =  ( ( U ^ 2 )  /  ( D ^
2 ) ) )
7368, 72syl5eq 2487 . . . . . . . . . . 11  |-  ( ph  ->  ( E ^ 2 )  =  ( ( U ^ 2 )  /  ( D ^
2 ) ) )
7473oveq2d 6110 . . . . . . . . . 10  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  x.  ( E ^ 2 ) )  =  ( ( L  /  (; 3 2  x.  B
) )  x.  (
( U ^ 2 )  /  ( D ^ 2 ) ) ) )
7538, 50rpdivcld 11047 . . . . . . . . . . . 12  |-  ( ph  ->  ( L  /  (; 3 2  x.  B ) )  e.  RR+ )
7675rpcnd 11032 . . . . . . . . . . 11  |-  ( ph  ->  ( L  /  (; 3 2  x.  B ) )  e.  CC )
7759sqcld 12009 . . . . . . . . . . 11  |-  ( ph  ->  ( U ^ 2 )  e.  CC )
78 rpexpcl 11887 . . . . . . . . . . . . 13  |-  ( ( D  e.  RR+  /\  2  e.  ZZ )  ->  ( D ^ 2 )  e.  RR+ )
7969, 40, 78sylancl 662 . . . . . . . . . . . 12  |-  ( ph  ->  ( D ^ 2 )  e.  RR+ )
8079rpcnne0d 11039 . . . . . . . . . . 11  |-  ( ph  ->  ( ( D ^
2 )  e.  CC  /\  ( D ^ 2 )  =/=  0 ) )
81 divass 10015 . . . . . . . . . . . 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 10016 . . . . . . . . . . . 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 2477 . . . . . . . . . . 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 1218 . . . . . . . . . 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 2479 . . . . . . . . 9  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  =  ( ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) )
8685oveq2d 6110 . . . . . . . 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 10384 . . . . . . . . . . . . 13  |-  3  =  ( 2  +  1 )
8887oveq2i 6105 . . . . . . . . . . . 12  |-  ( U ^ 3 )  =  ( U ^ (
2  +  1 ) )
89 2nn0 10599 . . . . . . . . . . . . 13  |-  2  e.  NN0
90 expp1 11875 . . . . . . . . . . . . 13  |-  ( ( U  e.  CC  /\  2  e.  NN0 )  -> 
( U ^ (
2  +  1 ) )  =  ( ( U ^ 2 )  x.  U ) )
9159, 89, 90sylancl 662 . . . . . . . . . . . 12  |-  ( ph  ->  ( U ^ (
2  +  1 ) )  =  ( ( U ^ 2 )  x.  U ) )
9288, 91syl5eq 2487 . . . . . . . . . . 11  |-  ( ph  ->  ( U ^ 3 )  =  ( ( U ^ 2 )  x.  U ) )
9377, 59mulcomd 9410 . . . . . . . . . . 11  |-  ( ph  ->  ( ( U ^
2 )  x.  U
)  =  ( U  x.  ( U ^
2 ) ) )
9492, 93eqtrd 2475 . . . . . . . . . 10  |-  ( ph  ->  ( U ^ 3 )  =  ( U  x.  ( U ^
2 ) ) )
9594oveq2d 6110 . . . . . . . . 9  |-  ( ph  ->  ( F  x.  ( U ^ 3 ) )  =  ( F  x.  ( U  x.  ( U ^ 2 ) ) ) )
9637simp3d 1002 . . . . . . . . . . 11  |-  ( ph  ->  F  e.  RR+ )
9796rpcnd 11032 . . . . . . . . . 10  |-  ( ph  ->  F  e.  CC )
9897, 59, 77mulassd 9412 . . . . . . . . 9  |-  ( ph  ->  ( ( F  x.  U )  x.  ( U ^ 2 ) )  =  ( F  x.  ( U  x.  ( U ^ 2 ) ) ) )
99 1cnd 9405 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  CC )
10069rpreccld 11040 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  /  D
)  e.  RR+ )
101100rpcnd 11032 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  /  D
)  e.  CC )
10299, 101, 59subdird 9804 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  -  ( 1  /  D
) )  x.  U
)  =  ( ( 1  x.  U )  -  ( ( 1  /  D )  x.  U ) ) )
10359mulid2d 9407 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  x.  U
)  =  U )
10459, 70, 71divrec2d 10114 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( U  /  D
)  =  ( ( 1  /  D )  x.  U ) )
1059, 104syl5req 2488 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1  /  D )  x.  U
)  =  E )
106103, 105oveq12d 6112 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  x.  U )  -  (
( 1  /  D
)  x.  U ) )  =  ( U  -  E ) )
107102, 106eqtr2d 2476 . . . . . . . . . . . . 13  |-  ( ph  ->  ( U  -  E
)  =  ( ( 1  -  ( 1  /  D ) )  x.  U ) )
108107oveq1d 6109 . . . . . . . . . . . 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 6104 . . . . . . . . . . . . 13  |-  ( F  x.  U )  =  ( ( ( 1  -  ( 1  /  D ) )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  U )
11099, 101subcld 9722 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  -  (
1  /  D ) )  e.  CC )
11175, 79rpdivcld 11047 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  e.  RR+ )
112111rpcnd 11032 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) )  e.  CC )
113110, 112, 59mul32d 9582 . . . . . . . . . . . . 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 2487 . . . . . . . . . . . 12  |-  ( ph  ->  ( F  x.  U
)  =  ( ( ( 1  -  (
1  /  D ) )  x.  U )  x.  ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) ) ) )
115108, 114eqtr4d 2478 . . . . . . . . . . 11  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )  =  ( F  x.  U ) )
116115oveq1d 6109 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  / 
(; 3 2  x.  B
) )  /  ( D ^ 2 ) ) )  x.  ( U ^ 2 ) )  =  ( ( F  x.  U )  x.  ( U ^ 2 ) ) )
11735rpcnd 11032 . . . . . . . . . . 11  |-  ( ph  ->  ( U  -  E
)  e.  CC )
118117, 112, 77mulassd 9412 . . . . . . . . . 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 2477 . . . . . . . . 9  |-  ( ph  ->  ( ( F  x.  U )  x.  ( U ^ 2 ) )  =  ( ( U  -  E )  x.  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
12095, 98, 1193eqtr2d 2481 . . . . . . . 8  |-  ( ph  ->  ( F  x.  ( U ^ 3 ) )  =  ( ( U  -  E )  x.  ( ( ( L  /  (; 3 2  x.  B
) )  /  ( D ^ 2 ) )  x.  ( U ^
2 ) ) ) )
12186, 120eqtr4d 2478 . . . . . . 7  |-  ( ph  ->  ( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  =  ( F  x.  ( U ^ 3 ) ) )
122121oveq2d 6110 . . . . . 6  |-  ( ph  ->  ( U  -  (
( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) ) )  =  ( U  -  ( F  x.  ( U ^ 3 ) ) ) )
123122oveq1d 6109 . . . . 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 2477 . . . 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 9417 . . . . 5  |-  ( ph  ->  ( U  x.  ( log `  Z ) )  e.  RR )
126125, 54resubcld 9779 . . . 4  |-  ( ph  ->  ( ( U  x.  ( log `  Z ) )  -  ( ( ( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  RR )
127124, 126eqeltrrd 2518 . . 3  |-  ( ph  ->  ( ( U  -  ( F  x.  ( U ^ 3 ) ) )  x.  ( log `  Z ) )  e.  RR )
12817rpred 11030 . . . . . . . 8  |-  ( ph  ->  Z  e.  RR )
12916simp2d 1001 . . . . . . . . 9  |-  ( ph  ->  ( 1  <  Z  /\  _e  <_  ( sqr `  Z )  /\  ( sqr `  Z )  <_ 
( Z  /  Y
) ) )
130129simp1d 1000 . . . . . . . 8  |-  ( ph  ->  1  <  Z )
131128, 130rplogcld 22081 . . . . . . 7  |-  ( ph  ->  ( log `  Z
)  e.  RR+ )
13232, 131rerpdivcld 11057 . . . . . 6  |-  ( ph  ->  ( 2  /  ( log `  Z ) )  e.  RR )
133 fzfid 11798 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
13417adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  RR+ )
135 elfznn 11481 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  NN )
136135adantl 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  NN )
137136nnrpd 11029 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  RR+ )
138134, 137rpdivcld 11047 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  /  n )  e.  RR+ )
13918ffvelrni 5845 . . . . . . . . . . . 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 11057 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  RR )
142141recnd 9415 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( R `  ( Z  /  n ) )  /  Z )  e.  CC )
143142abscld 12925 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  RR )
144137relogcld 22075 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  RR )
145143, 144remulcld 9417 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  RR )
146133, 145fsumrecl 13214 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  RR )
147132, 146remulcld 9417 . . . . 5  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  e.  RR )
148147, 57readdcld 9416 . . . 4  |-  ( ph  ->  ( ( ( 2  /  ( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  +  C )  e.  RR )
14920recnd 9415 . . . . . . . . . . 11  |-  ( ph  ->  ( R `  Z
)  e.  CC )
150149abscld 12925 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  ( R `  Z )
)  e.  RR )
151150recnd 9415 . . . . . . . . 9  |-  ( ph  ->  ( abs `  ( R `  Z )
)  e.  CC )
152151, 61mulcld 9409 . . . . . . . 8  |-  ( ph  ->  ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) )  e.  CC )
153132recnd 9415 . . . . . . . . 9  |-  ( ph  ->  ( 2  /  ( log `  Z ) )  e.  CC )
154140recnd 9415 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( R `  ( Z  /  n
) )  e.  CC )
155154abscld 12925 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( R `  ( Z  /  n ) ) )  e.  RR )
156155, 144remulcld 9417 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  x.  ( log `  n
) )  e.  RR )
157133, 156fsumrecl 13214 . . . . . . . . . 10  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  e.  RR )
158157recnd 9415 . . . . . . . . 9  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  e.  CC )
159153, 158mulcld 9409 . . . . . . . 8  |-  ( ph  ->  ( ( 2  / 
( log `  Z
) )  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )  e.  CC )
16017rpcnd 11032 . . . . . . . 8  |-  ( ph  ->  Z  e.  CC )
16117rpne0d 11035 . . . . . . . 8  |-  ( ph  ->  Z  =/=  0 )
162152, 159, 160, 161divsubdird 10149 . . . . . . 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 10147 . . . . . . . . 9  |-  ( ph  ->  ( ( ( abs `  ( R `  Z
) )  x.  ( log `  Z ) )  /  Z )  =  ( ( ( abs `  ( R `  Z
) )  /  Z
)  x.  ( log `  Z ) ) )
164149, 160, 161absdivd 12944 . . . . . . . . . . 11  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  =  ( ( abs `  ( R `
 Z ) )  /  ( abs `  Z
) ) )
16517rprege0d 11037 . . . . . . . . . . . . 13  |-  ( ph  ->  ( Z  e.  RR  /\  0  <_  Z )
)
166 absid 12788 . . . . . . . . . . . . 13  |-  ( ( Z  e.  RR  /\  0  <_  Z )  -> 
( abs `  Z
)  =  Z )
167165, 166syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( abs `  Z
)  =  Z )
168167oveq2d 6110 . . . . . . . . . . 11  |-  ( ph  ->  ( ( abs `  ( R `  Z )
)  /  ( abs `  Z ) )  =  ( ( abs `  ( R `  Z )
)  /  Z ) )
169164, 168eqtrd 2475 . . . . . . . . . 10  |-  ( ph  ->  ( abs `  (
( R `  Z
)  /  Z ) )  =  ( ( abs `  ( R `
 Z ) )  /  Z ) )
170169oveq1d 6109 . . . . . . . . 9  |-  ( ph  ->  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) )  =  ( ( ( abs `  ( R `  Z
) )  /  Z
)  x.  ( log `  Z ) ) )
171163, 170eqtr4d 2478 . . . . . . . 8  |-  ( ph  ->  ( ( ( abs `  ( R `  Z
) )  x.  ( log `  Z ) )  /  Z )  =  ( ( abs `  (
( R `  Z
)  /  Z ) )  x.  ( log `  Z ) ) )
172153, 158, 160, 161divassd 10145 . . . . . . . . 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 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  e.  CC )
174161adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  Z  =/=  0 )
175154, 173, 174absdivd 12944 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  ( abs `  Z
) ) )
176167adantr 465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  Z )  =  Z )
177176oveq2d 6110 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  / 
( abs `  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z ) )
178175, 177eqtrd 2475 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z ) )
179178oveq1d 6109 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  /  Z )  x.  ( log `  n
) ) )
180155recnd 9415 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( R `  ( Z  /  n ) ) )  e.  CC )
181144recnd 9415 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  CC )
18217rpcnne0d 11039 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Z  e.  CC  /\  Z  =/=  0 ) )
183182adantr 465 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( Z  e.  CC  /\  Z  =/=  0 ) )
184 div23 10016 . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . 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 2478 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  =  ( ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n
) )  /  Z
) )
187186sumeq2dv 13183 . . . . . . . . . . 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 9415 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( R `  ( Z  /  n
) ) )  x.  ( log `  n
) )  e.  CC )
189133, 160, 188, 161fsumdivc 13256 . . . . . . . . . . 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 2478 . . . . . . . . . 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 6110 . . . . . . . . 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 2478 . . . . . . . 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 6112 . . . . . . 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 2475 . . . . . 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 9388 . . . . . . . . 9  |-  1  e.  RR
196 rexr 9432 . . . . . . . . 9  |-  ( 1  e.  RR  ->  1  e.  RR* )
197 elioopnf 11386 . . . . . . . . 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 664 . . . . . . 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 5694 . . . . . . . . . . . . 13  |-  ( z  =  Z  ->  ( R `  z )  =  ( R `  Z ) )
202201fveq2d 5698 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  ( abs `  ( R `  z ) )  =  ( abs `  ( R `  Z )
) )
203 fveq2 5694 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  ( log `  z )  =  ( log `  Z
) )
204202, 203oveq12d 6112 . . . . . . . . . . 11  |-  ( z  =  Z  ->  (
( abs `  ( R `  z )
)  x.  ( log `  z ) )  =  ( ( abs `  ( R `  Z )
)  x.  ( log `  Z ) ) )
205203oveq2d 6110 . . . . . . . . . . . 12  |-  ( z  =  Z  ->  (
2  /  ( log `  z ) )  =  ( 2  /  ( log `  Z ) ) )
206 oveq2 6102 . . . . . . . . . . . . . . . . 17  |-  ( i  =  n  ->  (
z  /  i )  =  ( z  /  n ) )
207206fveq2d 5698 . . . . . . . . . . . . . . . 16  |-  ( i  =  n  ->  ( R `  ( z  /  i ) )  =  ( R `  ( z  /  n
) ) )
208207fveq2d 5698 . . . . . . . . . . . . . . 15  |-  ( i  =  n  ->  ( abs `  ( R `  ( z  /  i
) ) )  =  ( abs `  ( R `  ( z  /  n ) ) ) )
209 fveq2 5694 . . . . . . . . . . . . . . 15  |-  ( i  =  n  ->  ( log `  i )  =  ( log `  n
) )
210208, 209oveq12d 6112 . . . . . . . . . . . . . 14  |-  ( i  =  n  ->  (
( abs `  ( R `  ( z  /  i ) ) )  x.  ( log `  i ) )  =  ( ( abs `  ( R `  ( z  /  n ) ) )  x.  ( log `  n
) ) )
211210cbvsumv 13176 . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . . 16  |-  ( z  =  Z  ->  (
z  /  Y )  =  ( Z  /  Y ) )
213212fveq2d 5698 . . . . . . . . . . . . . . 15  |-  ( z  =  Z  ->  ( |_ `  ( z  /  Y ) )  =  ( |_ `  ( Z  /  Y ) ) )
214213oveq2d 6110 . . . . . . . . . . . . . 14  |-  ( z  =  Z  ->  (
1 ... ( |_ `  ( z  /  Y
) ) )  =  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )
215 simpl 457 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  z  =  Z )
216215oveq1d 6109 . . . . . . . . . . . . . . . . 17  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( z  /  n )  =  ( Z  /  n ) )
217216fveq2d 5698 . . . . . . . . . . . . . . . 16  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( R `  ( z  /  n
) )  =  ( R `  ( Z  /  n ) ) )
218217fveq2d 5698 . . . . . . . . . . . . . . 15  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( abs `  ( R `  ( z  /  n ) ) )  =  ( abs `  ( R `  ( Z  /  n ) ) ) )
219218oveq1d 6109 . . . . . . . . . . . . . 14  |-  ( ( z  =  Z  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) )  ->  ( ( abs `  ( R `  (
z  /  n ) ) )  x.  ( log `  n ) )  =  ( ( abs `  ( R `  ( Z  /  n ) ) )  x.  ( log `  n ) ) )
220214, 219sumeq12rdv 13187 . . . . . . . . . . . . 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 2487 . . . . . . . . . . . 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 6112 . . . . . . . . . . 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 6112 . . . . . . . . . 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 6112 . . . . . . . . 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 4305 . . . . . . . 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 3072 . . . . . . 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 4317 . . . . 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 9941 . . . . 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 10397 . . . . . . 7  |-  ( ph  ->  2  e.  CC )
233143recnd 9415 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  e.  CC )
234233, 181mulcld 9409 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  CC )
235133, 234fsumcl 13213 . . . . . . 7  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) )  x.  ( log `  n
) )  e.  CC )
236131rpne0d 11035 . . . . . . 7  |-  ( ph  ->  ( log `  Z
)  =/=  0 )
237232, 235, 61, 236div23d 10147 . . . . . 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 12037 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  RR )
23952, 238remulcld 9417 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( L  x.  ( E ^
2 ) )  / 
(; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) )  e.  RR )
24036, 239remulcld 9417 . . . . . . . . . 10  |-  ( ph  ->  ( ( U  -  E )  x.  (
( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) )  e.  RR )
241 remulcl 9370 . . . . . . . . . 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 663 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  (
( U  -  E
)  x.  ( ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  x.  (
( log `  Z
) ^ 2 ) ) ) )  e.  RR )
24330, 24remulcld 9417 . . . . . . . . 9  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) )  e.  RR )
244 remulcl 9370 . . . . . . . . . 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 663 . . . . . . . . 9  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) )  x.  ( log `  n ) ) )  e.  RR )
24626adantr 465 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  U  e.  RR )
247246, 136nndivred 10373 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  RR )
248247, 143resubcld 9779 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  -  ( abs `  ( ( R `  ( Z  /  n ) )  /  Z ) ) )  e.  RR )
249248, 144remulcld 9417 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( (
( U  /  n
)  -  ( abs `  ( ( R `  ( Z  /  n
) )  /  Z
) ) )  x.  ( log `  n
) )  e.  RR )
250133, 249fsumrecl 13214 . . . . . . . . . . 11  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( ( U  /  n )  -  ( abs `  ( ( R `
 ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n
) )  e.  RR )
25132, 250remulcld 9417 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( ( U  /  n )  -  ( abs `  (
( R `  ( Z  /  n ) )  /  Z ) ) )  x.  ( log `  n ) ) )  e.  RR )
252243, 245resubcld 9779 . . . . . . . . . 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 22857 . . . . . . . . . . 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 10416 . . . . . . . . . . . . 13  |-  0  <  2
259258a1i 11 . . . . . . . . . . . 12  |-  ( ph  ->  0  <  2 )
260 lemul2 10185 . . . . . . . . . . . 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 1222 . . . . . . . . . . 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 9415 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( U  /  n )  e.  CC )
264263, 233, 181subdird 9804 . . . . . . . . . . . . . . 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 13183 . . . . . . . . . . . . . 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 9417 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  e.  RR )
267266recnd 9415 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  e.  CC )
268133, 267, 234fsumsub 13258 . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . 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 6110 . . . . . . . . . . . 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 13214 . . . . . . . . . . . . . 14  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  e.  RR )
272271recnd 9415 . . . . . . . . . . . . 13  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  e.  CC )
273232, 272, 235subdid 9803 . . . . . . . . . . . 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 2475 . . . . . . . . . . 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 9370 . . . . . . . . . . . . 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 663 . . . . . . . . . . . 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 22858 . . . . . . . . . . . 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 9958 . . . . . . . . . . 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 4315 . . . . . . . . . 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 9531 . . . . . . . . 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 9946 . . . . . . . 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 9415 . . . . . . . . . 10  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  e.  CC )
28355recnd 9415 . . . . . . . . . 10  |-  ( ph  ->  ( 2  x.  (
( ( U  -  E )  x.  (
( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )  e.  CC )
284282, 283, 61subdird 9804 . . . . . . . . 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 9415 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( U  -  E )  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) )  e.  CC )
286232, 285, 61mulassd 9412 . . . . . . . . . . 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 9412 . . . . . . . . . . . . 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 12008 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  =  ( ( log `  Z )  x.  ( log `  Z ) ) )
289288oveq2d 6110 . . . . . . . . . . . . 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 11032 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) )  e.  CC )
291238recnd 9415 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  CC )
292117, 290, 291mulassd 9412 . . . . . . . . . . . . 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 2481 . . . . . . . . . . . 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 6110 . . . . . . . . . . 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 2475 . . . . . . . . . 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 6110 . . . . . . . . 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 2475 . . . . . . . 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 4321 . . . . . . 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 11080 . . . . . . 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 4317 . . . . 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 9956 . . . 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 9531 . . 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 9370 . . . . . . . . 9  |-  ( ( U  e.  RR  /\  3  e.  RR )  ->  ( U  x.  3 )  e.  RR )
30526, 27, 304sylancl 662 . . . . . . . 8  |-  ( ph  ->  ( U  x.  3 )  e.  RR )
306305, 57readdcld 9416 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  3 )  +  C
)  e.  RR )
30716simp3d 1002 . . . . . . . 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 1002 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  3 )  +  C
)  <_  ( (
( U  -  E
)  x.  ( ( L  x.  ( E ^ 2 ) )  /  (; 3 2  x.  B
) ) )  x.  ( log `  Z
) ) )
309306, 54, 125, 308leadd2dd 9957 . . . . . 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 9415 . . . . . . . . 9  |-  ( ph  ->  3  e.  CC )
31159, 61, 310adddid 9413 . . . . . . . 8  |-  ( ph  ->  ( U  x.  (
( log `  Z
)  +  3 ) )  =  ( ( U  x.  ( log `  Z ) )  +  ( U  x.  3 ) ) )
312311oveq1d 6109 . . . . . . 7  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  +  C )  =  ( ( ( U  x.  ( log `  Z ) )  +  ( U  x.  3 ) )  +  C
) )
313125recnd 9415 . . . . . . . 8  |-  ( ph  ->  ( U  x.  ( log `  Z ) )  e.  CC )
31459, 310mulcld 9409 . . . . . . . 8  |-  ( ph  ->  ( U  x.  3 )  e.  CC )
31513rpcnd 11032 . . . . . . . 8  |-  ( ph  ->  C  e.  CC )
316313, 314, 315addassd 9411 . . . . . . 7  |-  ( ph  ->  ( ( ( U  x.  ( log `  Z
) )  +  ( U  x.  3 ) )  +  C )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( U  x.  3 )  +  C ) ) )
317312, 316eqtrd 2475 . . . . . 6  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  +  C )  =  ( ( U  x.  ( log `  Z
) )  +  ( ( U  x.  3 )  +  C ) ) )
3182852timesd 10570 . . . . . . . 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 6110 . . . . . . 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 9749 . . . . . . 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 2475 . . . . . 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 4325 . . . . 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.  (