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

Theorem pntlemk 20861
Description: Lemma for pnt 20869. Evaluate the naive part of the estimate. (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 ) )
Assertion
Ref Expression
pntlemk  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  <_ 
( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) ) )
Distinct variable groups:    z, C    y, n, z, u, L   
n, K, y, z   
n, M, z    ph, n    n, N, z    R, n, u, y, z    U, n, z    n, W, z   
n, X, y, z   
n, Y, z    n, a, u, y, z, E   
n, Z, u, z
Allowed substitution hints:    ph( y, z, u, a)    A( y, z, u, n, a)    B( y, z, u, n, a)    C( y, u, n, a)    D( y, z, u, n, a)    R( a)    U( y, u, a)    F( y, z, u, n, a)    K( u, a)    L( a)    M( y, u, a)    N( y, u, a)    W( y, u, a)    X( u, a)    Y( y, u, a)    Z( y, a)

Proof of Theorem pntlemk
StepHypRef Expression
1 2re 9902 . . . . 5  |-  2  e.  RR
2 fzfid 11124 . . . . . 6  |-  ( ph  ->  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  e.  Fin )
3 elfznn 10908 . . . . . . . . . 10  |-  ( n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) )  ->  n  e.  NN )
43adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  NN )
54nnrpd 10478 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  n  e.  RR+ )
65relogcld 20079 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  RR )
76, 4nndivred 9881 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( log `  n )  /  n )  e.  RR )
82, 7fsumrecl 12298 . . . . 5  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( log `  n
)  /  n )  e.  RR )
9 remulcl 8909 . . . . 5  |-  ( ( 2  e.  RR  /\  sum_
n  e.  ( 1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( log `  n
)  /  n )  e.  RR )  -> 
( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) )  e.  RR )
101, 8, 9sylancr 644 . . . 4  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) )  e.  RR )
11 pntlem1.r . . . . . . . . 9  |-  R  =  ( a  e.  RR+  |->  ( (ψ `  a )  -  a ) )
12 pntlem1.a . . . . . . . . 9  |-  ( ph  ->  A  e.  RR+ )
13 pntlem1.b . . . . . . . . 9  |-  ( ph  ->  B  e.  RR+ )
14 pntlem1.l . . . . . . . . 9  |-  ( ph  ->  L  e.  ( 0 (,) 1 ) )
15 pntlem1.d . . . . . . . . 9  |-  D  =  ( A  +  1 )
16 pntlem1.f . . . . . . . . 9  |-  F  =  ( ( 1  -  ( 1  /  D
) )  x.  (
( L  /  (; 3 2  x.  B ) )  /  ( D ^
2 ) ) )
17 pntlem1.u . . . . . . . . 9  |-  ( ph  ->  U  e.  RR+ )
18 pntlem1.u2 . . . . . . . . 9  |-  ( ph  ->  U  <_  A )
19 pntlem1.e . . . . . . . . 9  |-  E  =  ( U  /  D
)
20 pntlem1.k . . . . . . . . 9  |-  K  =  ( exp `  ( B  /  E ) )
21 pntlem1.y . . . . . . . . 9  |-  ( ph  ->  ( Y  e.  RR+  /\  1  <_  Y )
)
22 pntlem1.x . . . . . . . . 9  |-  ( ph  ->  ( X  e.  RR+  /\  Y  <  X ) )
23 pntlem1.c . . . . . . . . 9  |-  ( ph  ->  C  e.  RR+ )
24 pntlem1.w . . . . . . . . 9  |-  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
) ) ) ) )
25 pntlem1.z . . . . . . . . 9  |-  ( ph  ->  Z  e.  ( W [,)  +oo ) )
2611, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25pntlemb 20852 . . . . . . . 8  |-  ( 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
) ) ) ) )
2726simp1d 967 . . . . . . 7  |-  ( ph  ->  Z  e.  RR+ )
2827relogcld 20079 . . . . . 6  |-  ( ph  ->  ( log `  Z
)  e.  RR )
29 peano2re 9072 . . . . . 6  |-  ( ( log `  Z )  e.  RR  ->  (
( log `  Z
)  +  1 )  e.  RR )
3028, 29syl 15 . . . . 5  |-  ( ph  ->  ( ( log `  Z
)  +  1 )  e.  RR )
3130resqcld 11361 . . . 4  |-  ( ph  ->  ( ( ( log `  Z )  +  1 ) ^ 2 )  e.  RR )
32 3re 9904 . . . . . 6  |-  3  e.  RR
33 readdcl 8907 . . . . . 6  |-  ( ( ( log `  Z
)  e.  RR  /\  3  e.  RR )  ->  ( ( log `  Z
)  +  3 )  e.  RR )
3428, 32, 33sylancl 643 . . . . 5  |-  ( ph  ->  ( ( log `  Z
)  +  3 )  e.  RR )
3534, 28remulcld 8950 . . . 4  |-  ( ph  ->  ( ( ( log `  Z )  +  3 )  x.  ( log `  Z ) )  e.  RR )
3627rpred 10479 . . . . . . . . . . 11  |-  ( ph  ->  Z  e.  RR )
3721simpld 445 . . . . . . . . . . 11  |-  ( ph  ->  Y  e.  RR+ )
3836, 37rerpdivcld 10506 . . . . . . . . . 10  |-  ( ph  ->  ( Z  /  Y
)  e.  RR )
39 1re 8924 . . . . . . . . . . . 12  |-  1  e.  RR
4039a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  1  e.  RR )
4127rpsqrcld 11984 . . . . . . . . . . . 12  |-  ( ph  ->  ( sqr `  Z
)  e.  RR+ )
4241rpred 10479 . . . . . . . . . . 11  |-  ( ph  ->  ( sqr `  Z
)  e.  RR )
43 ere 12461 . . . . . . . . . . . . 13  |-  _e  e.  RR
4443a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  _e  e.  RR )
45 1lt2 9975 . . . . . . . . . . . . . . 15  |-  1  <  2
46 egt2lt3 12575 . . . . . . . . . . . . . . . 16  |-  ( 2  <  _e  /\  _e  <  3 )
4746simpli 444 . . . . . . . . . . . . . . 15  |-  2  <  _e
4839, 1, 43lttri 9032 . . . . . . . . . . . . . . 15  |-  ( ( 1  <  2  /\  2  <  _e )  ->  1  <  _e )
4945, 47, 48mp2an 653 . . . . . . . . . . . . . 14  |-  1  <  _e
5039, 43, 49ltleii 9028 . . . . . . . . . . . . 13  |-  1  <_  _e
5150a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  1  <_  _e )
5226simp2d 968 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1  <  Z  /\  _e  <_  ( sqr `  Z )  /\  ( sqr `  Z )  <_ 
( Z  /  Y
) ) )
5352simp2d 968 . . . . . . . . . . . 12  |-  ( ph  ->  _e  <_  ( sqr `  Z ) )
5440, 44, 42, 51, 53letrd 9060 . . . . . . . . . . 11  |-  ( ph  ->  1  <_  ( sqr `  Z ) )
5552simp3d 969 . . . . . . . . . . 11  |-  ( ph  ->  ( sqr `  Z
)  <_  ( Z  /  Y ) )
5640, 42, 38, 54, 55letrd 9060 . . . . . . . . . 10  |-  ( ph  ->  1  <_  ( Z  /  Y ) )
57 flge1nn 11038 . . . . . . . . . 10  |-  ( ( ( Z  /  Y
)  e.  RR  /\  1  <_  ( Z  /  Y ) )  -> 
( |_ `  ( Z  /  Y ) )  e.  NN )
5838, 56, 57syl2anc 642 . . . . . . . . 9  |-  ( ph  ->  ( |_ `  ( Z  /  Y ) )  e.  NN )
5958nnrpd 10478 . . . . . . . 8  |-  ( ph  ->  ( |_ `  ( Z  /  Y ) )  e.  RR+ )
6059relogcld 20079 . . . . . . 7  |-  ( ph  ->  ( log `  ( |_ `  ( Z  /  Y ) ) )  e.  RR )
6160, 40readdcld 8949 . . . . . 6  |-  ( ph  ->  ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 )  e.  RR )
6261resqcld 11361 . . . . 5  |-  ( ph  ->  ( ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^ 2 )  e.  RR )
63 logdivbnd 20811 . . . . . . 7  |-  ( ( |_ `  ( Z  /  Y ) )  e.  NN  ->  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n )  <_  ( ( ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 )  /  2
) )
6458, 63syl 15 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( log `  n
)  /  n )  <_  ( ( ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 )  /  2
) )
651a1i 10 . . . . . . 7  |-  ( ph  ->  2  e.  RR )
66 2pos 9915 . . . . . . . 8  |-  0  <  2
6766a1i 10 . . . . . . 7  |-  ( ph  ->  0  <  2 )
68 lemuldiv2 9723 . . . . . . 7  |-  ( (
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( log `  n
)  /  n )  e.  RR  /\  (
( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 )  e.  RR  /\  ( 2  e.  RR  /\  0  <  2 ) )  ->  ( (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n ) )  <_  ( (
( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 )  <->  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n )  <_  ( ( ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 )  /  2
) ) )
698, 62, 65, 67, 68syl112anc 1186 . . . . . 6  |-  ( ph  ->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( log `  n
)  /  n ) )  <_  ( (
( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 )  <->  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n )  <_  ( ( ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 )  /  2
) ) )
7064, 69mpbird 223 . . . . 5  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) )  <_  (
( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^
2 ) )
71 reflcl 11017 . . . . . . . . . 10  |-  ( ( Z  /  Y )  e.  RR  ->  ( |_ `  ( Z  /  Y ) )  e.  RR )
7238, 71syl 15 . . . . . . . . 9  |-  ( ph  ->  ( |_ `  ( Z  /  Y ) )  e.  RR )
73 flle 11020 . . . . . . . . . 10  |-  ( ( Z  /  Y )  e.  RR  ->  ( |_ `  ( Z  /  Y ) )  <_ 
( Z  /  Y
) )
7438, 73syl 15 . . . . . . . . 9  |-  ( ph  ->  ( |_ `  ( Z  /  Y ) )  <_  ( Z  /  Y ) )
7521simprd 449 . . . . . . . . . . 11  |-  ( ph  ->  1  <_  Y )
76 1rp 10447 . . . . . . . . . . . . 13  |-  1  e.  RR+
7776a1i 10 . . . . . . . . . . . 12  |-  ( ph  ->  1  e.  RR+ )
7877, 37, 27lediv2d 10503 . . . . . . . . . . 11  |-  ( ph  ->  ( 1  <_  Y  <->  ( Z  /  Y )  <_  ( Z  / 
1 ) ) )
7975, 78mpbid 201 . . . . . . . . . 10  |-  ( ph  ->  ( Z  /  Y
)  <_  ( Z  /  1 ) )
8036recnd 8948 . . . . . . . . . . 11  |-  ( ph  ->  Z  e.  CC )
8180div1d 9615 . . . . . . . . . 10  |-  ( ph  ->  ( Z  /  1
)  =  Z )
8279, 81breqtrd 4126 . . . . . . . . 9  |-  ( ph  ->  ( Z  /  Y
)  <_  Z )
8372, 38, 36, 74, 82letrd 9060 . . . . . . . 8  |-  ( ph  ->  ( |_ `  ( Z  /  Y ) )  <_  Z )
8459, 27logled 20083 . . . . . . . 8  |-  ( ph  ->  ( ( |_ `  ( Z  /  Y
) )  <_  Z  <->  ( log `  ( |_
`  ( Z  /  Y ) ) )  <_  ( log `  Z
) ) )
8583, 84mpbid 201 . . . . . . 7  |-  ( ph  ->  ( log `  ( |_ `  ( Z  /  Y ) ) )  <_  ( log `  Z
) )
8660, 28, 40, 85leadd1dd 9473 . . . . . 6  |-  ( ph  ->  ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 )  <_ 
( ( log `  Z
)  +  1 ) )
87 0re 8925 . . . . . . . . 9  |-  0  e.  RR
8887a1i 10 . . . . . . . 8  |-  ( ph  ->  0  e.  RR )
89 log1 20041 . . . . . . . . 9  |-  ( log `  1 )  =  0
9058nnge1d 9875 . . . . . . . . . 10  |-  ( ph  ->  1  <_  ( |_ `  ( Z  /  Y
) ) )
91 logleb 20059 . . . . . . . . . . 11  |-  ( ( 1  e.  RR+  /\  ( |_ `  ( Z  /  Y ) )  e.  RR+ )  ->  ( 1  <_  ( |_ `  ( Z  /  Y
) )  <->  ( log `  1 )  <_  ( log `  ( |_ `  ( Z  /  Y
) ) ) ) )
9276, 59, 91sylancr 644 . . . . . . . . . 10  |-  ( ph  ->  ( 1  <_  ( |_ `  ( Z  /  Y ) )  <->  ( log `  1 )  <_  ( log `  ( |_ `  ( Z  /  Y
) ) ) ) )
9390, 92mpbid 201 . . . . . . . . 9  |-  ( ph  ->  ( log `  1
)  <_  ( log `  ( |_ `  ( Z  /  Y ) ) ) )
9489, 93syl5eqbrr 4136 . . . . . . . 8  |-  ( ph  ->  0  <_  ( log `  ( |_ `  ( Z  /  Y ) ) ) )
9560lep1d 9775 . . . . . . . 8  |-  ( ph  ->  ( log `  ( |_ `  ( Z  /  Y ) ) )  <_  ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) )
9688, 60, 61, 94, 95letrd 9060 . . . . . . 7  |-  ( ph  ->  0  <_  ( ( log `  ( |_ `  ( Z  /  Y
) ) )  +  1 ) )
9788, 61, 30, 96, 86letrd 9060 . . . . . . 7  |-  ( ph  ->  0  <_  ( ( log `  Z )  +  1 ) )
9861, 30, 96, 97le2sqd 11370 . . . . . 6  |-  ( ph  ->  ( ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 )  <_  ( ( log `  Z )  +  1 )  <->  ( ( ( log `  ( |_
`  ( Z  /  Y ) ) )  +  1 ) ^
2 )  <_  (
( ( log `  Z
)  +  1 ) ^ 2 ) ) )
9986, 98mpbid 201 . . . . 5  |-  ( ph  ->  ( ( ( log `  ( |_ `  ( Z  /  Y ) ) )  +  1 ) ^ 2 )  <_ 
( ( ( log `  Z )  +  1 ) ^ 2 ) )
10010, 62, 31, 70, 99letrd 9060 . . . 4  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) )  <_  (
( ( log `  Z
)  +  1 ) ^ 2 ) )
10128resqcld 11361 . . . . . . 7  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  RR )
10265, 28remulcld 8950 . . . . . . 7  |-  ( ph  ->  ( 2  x.  ( log `  Z ) )  e.  RR )
103101, 102readdcld 8949 . . . . . 6  |-  ( ph  ->  ( ( ( log `  Z ) ^ 2 )  +  ( 2  x.  ( log `  Z
) ) )  e.  RR )
104 loge 20042 . . . . . . 7  |-  ( log `  _e )  =  1
10541rpge0d 10483 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  ( sqr `  Z ) )
10642, 42, 105, 54lemulge12d 9782 . . . . . . . . . 10  |-  ( ph  ->  ( sqr `  Z
)  <_  ( ( sqr `  Z )  x.  ( sqr `  Z
) ) )
10727rprege0d 10486 . . . . . . . . . . 11  |-  ( ph  ->  ( Z  e.  RR  /\  0  <_  Z )
)
108 remsqsqr 11832 . . . . . . . . . . 11  |-  ( ( Z  e.  RR  /\  0  <_  Z )  -> 
( ( sqr `  Z
)  x.  ( sqr `  Z ) )  =  Z )
109107, 108syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( sqr `  Z
)  x.  ( sqr `  Z ) )  =  Z )
110106, 109breqtrd 4126 . . . . . . . . 9  |-  ( ph  ->  ( sqr `  Z
)  <_  Z )
11144, 42, 36, 53, 110letrd 9060 . . . . . . . 8  |-  ( ph  ->  _e  <_  Z )
112 epr 12577 . . . . . . . . 9  |-  _e  e.  RR+
113 logleb 20059 . . . . . . . . 9  |-  ( ( _e  e.  RR+  /\  Z  e.  RR+ )  ->  (
_e  <_  Z  <->  ( log `  _e )  <_  ( log `  Z ) ) )
114112, 27, 113sylancr 644 . . . . . . . 8  |-  ( ph  ->  ( _e  <_  Z  <->  ( log `  _e )  <_  ( log `  Z
) ) )
115111, 114mpbid 201 . . . . . . 7  |-  ( ph  ->  ( log `  _e )  <_  ( log `  Z
) )
116104, 115syl5eqbrr 4136 . . . . . 6  |-  ( ph  ->  1  <_  ( log `  Z ) )
11740, 28, 103, 116leadd2dd 9474 . . . . 5  |-  ( ph  ->  ( ( ( ( log `  Z ) ^ 2 )  +  ( 2  x.  ( log `  Z ) ) )  +  1 )  <_  ( ( ( ( log `  Z
) ^ 2 )  +  ( 2  x.  ( log `  Z
) ) )  +  ( log `  Z
) ) )
11828recnd 8948 . . . . . 6  |-  ( ph  ->  ( log `  Z
)  e.  CC )
119 binom21 11309 . . . . . 6  |-  ( ( log `  Z )  e.  CC  ->  (
( ( log `  Z
)  +  1 ) ^ 2 )  =  ( ( ( ( log `  Z ) ^ 2 )  +  ( 2  x.  ( log `  Z ) ) )  +  1 ) )
120118, 119syl 15 . . . . 5  |-  ( ph  ->  ( ( ( log `  Z )  +  1 ) ^ 2 )  =  ( ( ( ( log `  Z
) ^ 2 )  +  ( 2  x.  ( log `  Z
) ) )  +  1 ) )
121118sqvald 11332 . . . . . . 7  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  =  ( ( log `  Z )  x.  ( log `  Z ) ) )
122 df-3 9892 . . . . . . . . . 10  |-  3  =  ( 2  +  1 )
123122oveq1i 5952 . . . . . . . . 9  |-  ( 3  x.  ( log `  Z
) )  =  ( ( 2  +  1 )  x.  ( log `  Z ) )
124 2cn 9903 . . . . . . . . . . 11  |-  2  e.  CC
125124a1i 10 . . . . . . . . . 10  |-  ( ph  ->  2  e.  CC )
126 ax-1cn 8882 . . . . . . . . . . 11  |-  1  e.  CC
127126a1i 10 . . . . . . . . . 10  |-  ( ph  ->  1  e.  CC )
128125, 127, 118adddird 8947 . . . . . . . . 9  |-  ( ph  ->  ( ( 2  +  1 )  x.  ( log `  Z ) )  =  ( ( 2  x.  ( log `  Z
) )  +  ( 1  x.  ( log `  Z ) ) ) )
129123, 128syl5eq 2402 . . . . . . . 8  |-  ( ph  ->  ( 3  x.  ( log `  Z ) )  =  ( ( 2  x.  ( log `  Z
) )  +  ( 1  x.  ( log `  Z ) ) ) )
130118mulid2d 8940 . . . . . . . . 9  |-  ( ph  ->  ( 1  x.  ( log `  Z ) )  =  ( log `  Z
) )
131130oveq2d 5958 . . . . . . . 8  |-  ( ph  ->  ( ( 2  x.  ( log `  Z
) )  +  ( 1  x.  ( log `  Z ) ) )  =  ( ( 2  x.  ( log `  Z
) )  +  ( log `  Z ) ) )
132129, 131eqtr2d 2391 . . . . . . 7  |-  ( ph  ->  ( ( 2  x.  ( log `  Z
) )  +  ( log `  Z ) )  =  ( 3  x.  ( log `  Z
) ) )
133121, 132oveq12d 5960 . . . . . 6  |-  ( ph  ->  ( ( ( log `  Z ) ^ 2 )  +  ( ( 2  x.  ( log `  Z ) )  +  ( log `  Z
) ) )  =  ( ( ( log `  Z )  x.  ( log `  Z ) )  +  ( 3  x.  ( log `  Z
) ) ) )
134118sqcld 11333 . . . . . . 7  |-  ( ph  ->  ( ( log `  Z
) ^ 2 )  e.  CC )
135 mulcl 8908 . . . . . . . 8  |-  ( ( 2  e.  CC  /\  ( log `  Z )  e.  CC )  -> 
( 2  x.  ( log `  Z ) )  e.  CC )
136124, 118, 135sylancr 644 . . . . . . 7  |-  ( ph  ->  ( 2  x.  ( log `  Z ) )  e.  CC )
137134, 136, 118addassd 8944 . . . . . 6  |-  ( ph  ->  ( ( ( ( log `  Z ) ^ 2 )  +  ( 2  x.  ( log `  Z ) ) )  +  ( log `  Z ) )  =  ( ( ( log `  Z ) ^ 2 )  +  ( ( 2  x.  ( log `  Z ) )  +  ( log `  Z
) ) ) )
138 3cn 9905 . . . . . . . 8  |-  3  e.  CC
139138a1i 10 . . . . . . 7  |-  ( ph  ->  3  e.  CC )
140118, 139, 118adddird 8947 . . . . . 6  |-  ( ph  ->  ( ( ( log `  Z )  +  3 )  x.  ( log `  Z ) )  =  ( ( ( log `  Z )  x.  ( log `  Z ) )  +  ( 3  x.  ( log `  Z
) ) ) )
141133, 137, 1403eqtr4rd 2401 . . . . 5  |-  ( ph  ->  ( ( ( log `  Z )  +  3 )  x.  ( log `  Z ) )  =  ( ( ( ( log `  Z ) ^ 2 )  +  ( 2  x.  ( log `  Z ) ) )  +  ( log `  Z ) ) )
142117, 120, 1413brtr4d 4132 . . . 4  |-  ( ph  ->  ( ( ( log `  Z )  +  1 ) ^ 2 )  <_  ( ( ( log `  Z )  +  3 )  x.  ( log `  Z
) ) )
14310, 31, 35, 100, 142letrd 9060 . . 3  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) )  <_  (
( ( log `  Z
)  +  3 )  x.  ( log `  Z
) ) )
14410, 35, 17lemul2d 10519 . . 3  |-  ( ph  ->  ( ( 2  x. 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( log `  n
)  /  n ) )  <_  ( (
( log `  Z
)  +  3 )  x.  ( log `  Z
) )  <->  ( U  x.  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) ) )  <_ 
( U  x.  (
( ( log `  Z
)  +  3 )  x.  ( log `  Z
) ) ) ) )
145143, 144mpbid 201 . 2  |-  ( ph  ->  ( U  x.  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n ) ) )  <_  ( U  x.  ( (
( log `  Z
)  +  3 )  x.  ( log `  Z
) ) ) )
14617rpred 10479 . . . . . . . . 9  |-  ( ph  ->  U  e.  RR )
147146adantr 451 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  U  e.  RR )
148147recnd 8948 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  U  e.  CC )
1496recnd 8948 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( log `  n )  e.  CC )
1505rpcnne0d 10488 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( n  e.  CC  /\  n  =/=  0 ) )
151 div23 9530 . . . . . . . 8  |-  ( ( U  e.  CC  /\  ( log `  n )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( U  x.  ( log `  n
) )  /  n
)  =  ( ( U  /  n )  x.  ( log `  n
) ) )
152 divass 9529 . . . . . . . 8  |-  ( ( U  e.  CC  /\  ( log `  n )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( U  x.  ( log `  n
) )  /  n
)  =  ( U  x.  ( ( log `  n )  /  n
) ) )
153151, 152eqtr3d 2392 . . . . . . 7  |-  ( ( U  e.  CC  /\  ( log `  n )  e.  CC  /\  (
n  e.  CC  /\  n  =/=  0 ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  =  ( U  x.  ( ( log `  n )  /  n ) ) )
154148, 149, 150, 153syl3anc 1182 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( U  /  n )  x.  ( log `  n
) )  =  ( U  x.  ( ( log `  n )  /  n ) ) )
155154sumeq2dv 12267 . . . . 5  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  = 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( U  x.  ( ( log `  n )  /  n ) ) )
156146recnd 8948 . . . . . 6  |-  ( ph  ->  U  e.  CC )
1577recnd 8948 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) )  ->  ( ( log `  n )  /  n )  e.  CC )
1582, 156, 157fsummulc2 12337 . . . . 5  |-  ( ph  ->  ( U  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) )  =  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( U  x.  ( ( log `  n
)  /  n ) ) )
159155, 158eqtr4d 2393 . . . 4  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( U  /  n
)  x.  ( log `  n ) )  =  ( U  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n )  /  n
) ) )
160159oveq2d 5958 . . 3  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  =  ( 2  x.  ( U  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n ) ) ) )
1618recnd 8948 . . . 4  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  ( Z  /  Y
) ) ) ( ( log `  n
)  /  n )  e.  CC )
162125, 156, 161mul12d 9108 . . 3  |-  ( ph  ->  ( 2  x.  ( U  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n ) ) )  =  ( U  x.  ( 2  x.  sum_ n  e.  ( 1 ... ( |_
`  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n ) ) ) )
163160, 162eqtrd 2390 . 2  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  =  ( U  x.  (
2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( log `  n
)  /  n ) ) ) )
16434recnd 8948 . . 3  |-  ( ph  ->  ( ( log `  Z
)  +  3 )  e.  CC )
165156, 164, 118mulassd 8945 . 2  |-  ( ph  ->  ( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) )  =  ( U  x.  (
( ( log `  Z
)  +  3 )  x.  ( log `  Z
) ) ) )
166145, 163, 1653brtr4d 4132 1  |-  ( ph  ->  ( 2  x.  sum_ n  e.  ( 1 ... ( |_ `  ( Z  /  Y ) ) ) ( ( U  /  n )  x.  ( log `  n
) ) )  <_ 
( ( U  x.  ( ( log `  Z
)  +  3 ) )  x.  ( log `  Z ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1642    e. wcel 1710    =/= wne 2521   A.wral 2619   E.wrex 2620   class class class wbr 4102    e. cmpt 4156   ` cfv 5334  (class class class)co 5942   CCcc 8822   RRcr 8823   0cc0 8824   1c1 8825    + caddc 8827    x. cmul 8829    +oocpnf 8951    < clt 8954    <_ cle 8955    - cmin 9124    / cdiv 9510   NNcn 9833   2c2 9882   3c3 9883   4c4 9884  ;cdc 10213   RR+crp 10443   (,)cioo 10745   [,)cico 10747   [,]cicc 10748   ...cfz 10871   |_cfl 11013   ^cexp 11194   sqrcsqr 11808   abscabs 11809   sum_csu 12249   expce 12434   _eceu 12435   logclog 20013  ψcchp 20436
This theorem is referenced by:  pntlemo  20862
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-inf2 7429  ax-cnex 8880  ax-resscn 8881  ax-1cn 8882  ax-icn 8883  ax-addcl 8884  ax-addrcl 8885  ax-mulcl 8886  ax-mulrcl 8887  ax-mulcom 8888  ax-addass 8889  ax-mulass 8890  ax-distr 8891  ax-i2m1 8892  ax-1ne0 8893  ax-1rid 8894  ax-rnegex 8895  ax-rrecex 8896  ax-cnre 8897  ax-pre-lttri 8898  ax-pre-lttrn 8899  ax-pre-ltadd 8900  ax-pre-mulgt0 8901  ax-pre-sup 8902  ax-addf 8903  ax-mulf 8904
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rmo 2627  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-iin 3987  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-se 4432  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-isom 5343  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-of 6162  df-1st 6206  df-2nd 6207  df-riota 6388  df-recs 6472  df-rdg 6507  df-1o 6563  df-2o 6564  df-oadd 6567  df-er 6744  df-map 6859  df-pm 6860  df-ixp 6903  df-en 6949  df-dom 6950  df-sdom 6951  df-fin 6952  df-fi 7252  df-sup 7281  df-oi 7312  df-card 7659  df-cda 7881  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-sub 9126  df-neg 9127  df-div 9511  df-nn 9834  df-2 9891  df-3 9892  df-4 9893  df-5 9894  df-6 9895  df-7 9896  df-8 9897  df-9 9898  df-10 9899  df-n0 10055  df-z 10114  df-dec 10214  df-uz 10320  df-q 10406  df-rp 10444  df-xneg 10541  df-xadd 10542  df-xmul 10543  df-ioo 10749  df-ioc 10750  df-ico 10751  df-icc 10752  df-fz 10872  df-fzo 10960  df-fl 11014  df-mod 11063  df-seq 11136  df-exp 11195  df-fac 11379  df-bc 11406  df-hash 11428  df-shft 11652  df-cj 11674  df-re 11675  df-im 11676  df-sqr 11810  df-abs 11811  df-limsup 12035  df-clim 12052  df-rlim 12053  df-sum 12250  df-ef 12440  df-e 12441  df-sin 12442  df-cos 12443  df-pi 12445  df-struct 13241  df-ndx 13242  df-slot 13243  df-base 13244  df-sets 13245  df-ress 13246  df-plusg 13312  df-mulr 13313  df-starv 13314  df-sca 13315  df-vsca 13316  df-tset 13318  df-ple 13319  df-ds 13321  df-unif 13322  df-hom 13323  df-cco 13324  df-rest 13420  df-topn 13421  df-topgen 13437  df-pt 13438  df-prds 13441  df-xrs 13496  df-0g 13497  df-gsum 13498  df-qtop 13503  df-imas 13504  df-xps 13506  df-mre 13581  df-mrc 13582  df-acs 13584  df-mnd 14460  df-submnd 14509  df-mulg 14585  df-cntz 14886  df-cmn 15184  df-xmet 16469  df-met 16470  df-bl 16471  df-mopn 16472  df-fbas 16473  df-fg 16474  df-cnfld 16477  df-top 16736  df-bases 16738  df-topon 16739  df-topsp 16740  df-cld 16856  df-ntr 16857  df-cls 16858  df-nei 16935  df-lp 16968  df-perf 16969  df-cn 17057  df-cnp 17058  df-haus 17143  df-tx 17357  df-hmeo 17546  df-fil 17637  df-fm 17729  df-flim 17730  df-flf 17731  df-xms 17981  df-ms 17982  df-tms 17983  df-cncf 18479  df-limc 19314  df-dv 19315  df-log 20015  df-em 20392
  Copyright terms: Public domain W3C validator