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

Theorem rpvmasumlem 21134
Description: Lemma for rpvmasum 21173. Calculate the "trivial case" estimate  sum_ n  <_  x (  .1.  (
n )Λ ( n )  /  n )  =  log x  +  O
( 1 ), where  .1.  ( x ) is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 2-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z  |-  Z  =  (ℤ/n `  N )
rpvmasum.l  |-  L  =  ( ZRHom `  Z
)
rpvmasum.a  |-  ( ph  ->  N  e.  NN )
rpvmasum.g  |-  G  =  (DChr `  N )
rpvmasum.d  |-  D  =  ( Base `  G
)
rpvmasum.1  |-  .1.  =  ( 0g `  G )
Assertion
Ref Expression
rpvmasumlem  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )  e.  O ( 1 ) )
Distinct variable groups:    x, n,  .1.    n, N, x    ph, n, x    n, Z, x    D, n, x    n, L, x
Allowed substitution hints:    G( x, n)

Proof of Theorem rpvmasumlem
Dummy variables  k  p  q are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 9037 . . . . . 6  |-  RR  e.  _V
2 rpssre 10578 . . . . . 6  |-  RR+  C_  RR
31, 2ssexi 4308 . . . . 5  |-  RR+  e.  _V
43a1i 11 . . . 4  |-  ( ph  -> 
RR+  e.  _V )
5 fzfid 11267 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  x ) )  e.  Fin )
6 elfznn 11036 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
76adantl 453 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
8 vmacl 20854 . . . . . . . . . 10  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
97, 8syl 16 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
109, 7nndivred 10004 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
1110recnd 9070 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
125, 11fsumcl 12482 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  e.  CC )
1312adantr 452 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
14 relogcl 20426 . . . . . . 7  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
1514adantl 453 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
1615recnd 9070 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
1713, 16subcld 9367 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) )  e.  CC )
18 1re 9046 . . . . . . . . 9  |-  1  e.  RR
19 rpvmasum.g . . . . . . . . . . . 12  |-  G  =  (DChr `  N )
20 rpvmasum.z . . . . . . . . . . . 12  |-  Z  =  (ℤ/n `  N )
21 rpvmasum.1 . . . . . . . . . . . 12  |-  .1.  =  ( 0g `  G )
22 eqid 2404 . . . . . . . . . . . 12  |-  ( Base `  Z )  =  (
Base `  Z )
23 rpvmasum.a . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN )
2419, 20, 21, 22, 23dchr1re 21000 . . . . . . . . . . 11  |-  ( ph  ->  .1.  : ( Base `  Z ) --> RR )
2524adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  : (
Base `  Z ) --> RR )
2623nnnn0d 10230 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN0 )
27 rpvmasum.l . . . . . . . . . . . . 13  |-  L  =  ( ZRHom `  Z
)
2820, 22, 27znzrhfo 16783 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
29 fof 5612 . . . . . . . . . . . 12  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
3026, 28, 293syl 19 . . . . . . . . . . 11  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
31 elfzelz 11015 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
32 ffvelrn 5827 . . . . . . . . . . 11  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3330, 31, 32syl2an 464 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3425, 33ffvelrnd 5830 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  RR )
35 resubcl 9321 . . . . . . . . 9  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  e.  RR )
3618, 34, 35sylancr 645 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  RR )
3736, 10remulcld 9072 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
3837recnd 9070 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
395, 38fsumcl 12482 . . . . 5  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4039adantr 452 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
41 eqidd 2405 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) ) )
42 eqidd 2405 . . . 4  |-  ( ph  ->  ( x  e.  RR+  |->  sum_
n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )  =  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) ) )
434, 17, 40, 41, 42offval2 6281 . . 3  |-  ( ph  ->  ( ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  o F  -  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) ) )  =  ( x  e.  RR+  |->  ( (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) ) ) )
4413, 16, 40sub32d 9399 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )  =  ( ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )  -  ( log `  x
) ) )
455, 11, 38fsumsub 12526 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  -  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) ) )
46 ax-1cn 9004 . . . . . . . . . . . 12  |-  1  e.  CC
4746a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
4836recnd 9070 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
4947, 48, 11subdird 9446 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( 1  x.  ( (Λ `  n )  /  n
) )  -  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) ) )
5034recnd 9070 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  CC )
51 nncan 9286 . . . . . . . . . . . 12  |-  ( ( 1  e.  CC  /\  (  .1.  `  ( L `  n ) )  e.  CC )  ->  (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  =  (  .1.  `  ( L `  n )
) )
5246, 50, 51sylancr 645 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  ( 1  -  (  .1.  `  ( L `  n )
) ) )  =  (  .1.  `  ( L `  n )
) )
5352oveq1d 6055 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) ) )
5411mulid2d 9062 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( (Λ `  n
)  /  n ) )  =  ( (Λ `  n )  /  n
) )
5554oveq1d 6055 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  x.  ( (Λ `  n )  /  n
) )  -  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )  =  ( ( (Λ `  n
)  /  n )  -  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) ) ) )
5649, 53, 553eqtr3rd 2445 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  -  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
5756sumeq2dv 12452 . . . . . . . 8  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( (Λ `  n
)  /  n )  -  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )
5845, 57eqtr3d 2438 . . . . . . 7  |-  ( ph  ->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (Λ `  n
)  /  n )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )  =  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) ) )
5958oveq1d 6055 . . . . . 6  |-  ( ph  ->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )  -  ( log `  x
) )  =  (
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )
6059adantr 452 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( 1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) ) )  -  ( log `  x ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )
6144, 60eqtrd 2436 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  -  ( log `  x ) )  -  sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )  =  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) )
6261mpteq2dva 4255 . . 3  |-  ( ph  ->  ( x  e.  RR+  |->  ( ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) )  -  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( 1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_
`  x ) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n )  /  n
) )  -  ( log `  x ) ) ) )
6343, 62eqtrd 2436 . 2  |-  ( ph  ->  ( ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  o F  -  ( x  e.  RR+  |->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) ) )  =  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) )  -  ( log `  x ) ) ) )
64 vmadivsum 21129 . . 3  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) ) )  e.  O ( 1 )
652a1i 11 . . . 4  |-  ( ph  -> 
RR+  C_  RR )
6618a1i 11 . . . 4  |-  ( ph  ->  1  e.  RR )
67 prmdvdsfi 20843 . . . . . 6  |-  ( N  e.  NN  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
6823, 67syl 16 . . . . 5  |-  ( ph  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
69 elrabi 3050 . . . . . 6  |-  ( p  e.  { q  e. 
Prime  |  q  ||  N }  ->  p  e. 
Prime )
70 prmnn 13037 . . . . . . . . . 10  |-  ( p  e.  Prime  ->  p  e.  NN )
7170adantl 453 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  NN )
7271nnrpd 10603 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  RR+ )
7372relogcld 20471 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( log `  p )  e.  RR )
74 prmuz2 13052 . . . . . . . . 9  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
7574adantl 453 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= `  2 )
)
76 uz2m1nn 10506 . . . . . . . 8  |-  ( p  e.  ( ZZ>= `  2
)  ->  ( p  -  1 )  e.  NN )
7775, 76syl 16 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( p  -  1 )  e.  NN )
7873, 77nndivred 10004 . . . . . 6  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( log `  p )  / 
( p  -  1 ) )  e.  RR )
7969, 78sylan2 461 . . . . 5  |-  ( (
ph  /\  p  e.  { q  e.  Prime  |  q 
||  N } )  ->  ( ( log `  p )  /  (
p  -  1 ) )  e.  RR )
8068, 79fsumrecl 12483 . . . 4  |-  ( ph  -> 
sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
81 fzfid 11267 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
82 simpr 448 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  =  0 )
83 0re 9047 . . . . . . . . . . 11  |-  0  e.  RR
8482, 83syl6eqel 2492 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
85 eqid 2404 . . . . . . . . . . . 12  |-  (Unit `  Z )  =  (Unit `  Z )
8623ad3antrrr 711 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  N  e.  NN )
87 rpvmasum.d . . . . . . . . . . . . . 14  |-  D  =  ( Base `  G
)
8819dchrabl 20991 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  G  e.  Abel )
8923, 88syl 16 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  e.  Abel )
90 ablgrp 15372 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  ->  G  e. 
Grp )
9187, 21grpidcl 14788 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Grp  ->  .1.  e.  D )
9289, 90, 913syl 19 . . . . . . . . . . . . . . 15  |-  ( ph  ->  .1.  e.  D )
9392ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  e.  D
)
9433adantlr 696 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
9519, 20, 87, 22, 85, 93, 94dchrn0 20987 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (  .1.  `  ( L `  n
) )  =/=  0  <->  ( L `  n )  e.  (Unit `  Z
) ) )
9695biimpa 471 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  ( L `  n )  e.  (Unit `  Z ) )
9719, 20, 21, 85, 86, 96dchr1 20994 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  =  1 )
9897, 18syl6eqel 2492 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
9984, 98pm2.61dane 2645 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
10018, 99, 35sylancr 645 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n )
) )  e.  RR )
10110adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n
)  /  n )  e.  RR )
102100, 101remulcld 9072 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  RR )
10381, 102fsumrecl 12483 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
104 0le1 9507 . . . . . . . . . . 11  |-  0  <_  1
10582, 104syl6eqbr 4209 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
10618leidi 9517 . . . . . . . . . . 11  |-  1  <_  1
10797, 106syl6eqbr 4209 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
108105, 107pm2.61dane 2645 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
109 subge0 9497 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
0  <_  ( 1  -  (  .1.  `  ( L `  n ) ) )  <->  (  .1.  `  ( L `  n
) )  <_  1
) )
11018, 99, 109sylancr 645 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  <_ 
( 1  -  (  .1.  `  ( L `  n ) ) )  <-> 
(  .1.  `  ( L `  n )
)  <_  1 ) )
111108, 110mpbird 224 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
1  -  (  .1.  `  ( L `  n
) ) ) )
1129adantlr 696 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n )  e.  RR )
1136adantl 453 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
114 vmage0 20857 . . . . . . . . . 10  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
115113, 114syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
116113nnred 9971 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
117113nngt0d 9999 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <  n
)
118 divge0 9835 . . . . . . . . 9  |-  ( ( ( (Λ `  n
)  e.  RR  /\  0  <_  (Λ `  n )
)  /\  ( n  e.  RR  /\  0  < 
n ) )  -> 
0  <_  ( (Λ `  n )  /  n
) )
119112, 115, 116, 117, 118syl22anc 1185 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
(Λ `  n )  /  n ) )
120100, 101, 111, 119mulge0d 9559 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )
12181, 102, 120fsumge0 12529 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )
122103, 121absidd 12180 . . . . 5  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( abs `  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( 1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) ) )  =  sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( ( 1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) ) )
12368adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
124 inss2 3522 . . . . . . . . 9  |-  ( ( 0 [,] x )  i^i  Prime )  C_  Prime
125 rabss2 3386 . . . . . . . . 9  |-  ( ( ( 0 [,] x
)  i^i  Prime )  C_  Prime  ->  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N }  C_  { q  e. 
Prime  |  q  ||  N } )
126124, 125mp1i 12 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  C_ 
{ q  e.  Prime  |  q  ||  N }
)
127 ssfi 7288 . . . . . . . 8  |-  ( ( { q  e.  Prime  |  q  ||  N }  e.  Fin  /\  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  { q  e.  Prime  |  q  ||  N } )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  e.  Fin )
128123, 126, 127syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  e.  Fin )
129 ssrab2 3388 . . . . . . . . . 10  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  (
( 0 [,] x
)  i^i  Prime )
130129, 124sstri 3317 . . . . . . . . 9  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  Prime
131130sseli 3304 . . . . . . . 8  |-  ( p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N }  ->  p  e.  Prime )
13278adantlr 696 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  p
)  /  ( p  -  1 ) )  e.  RR )
133131, 132sylan2 461 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N } )  ->  (
( log `  p
)  /  ( p  -  1 ) )  e.  RR )
134128, 133fsumrecl 12483 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ p  e.  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
13580adantr 452 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
136 fveq2 5687 . . . . . . . . . . . 12  |-  ( n  =  ( p ^
k )  ->  ( L `  n )  =  ( L `  ( p ^ k
) ) )
137136fveq2d 5691 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (  .1.  `  ( L `  n ) )  =  (  .1.  `  ( L `  ( p ^ k ) ) ) )
138137oveq2d 6056 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  =  ( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) ) )
139 fveq2 5687 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (Λ `  n )  =  (Λ `  ( p ^ k
) ) )
140 id 20 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  n  =  ( p ^
k ) )
141139, 140oveq12d 6058 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
(Λ `  n )  /  n )  =  ( (Λ `  ( p ^ k ) )  /  ( p ^
k ) ) )
142138, 141oveq12d 6058 . . . . . . . . 9  |-  ( n  =  ( p ^
k )  ->  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) ) )
143 rpre 10574 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  x  e.  RR )
144143ad2antrl 709 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
14538adantlr 696 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
146 simprr 734 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
(Λ `  n )  =  0 )
147146oveq1d 6055 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( (Λ `  n )  /  n )  =  ( 0  /  n ) )
1486ad2antrl 709 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  NN )
149148nncnd 9972 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  CC )
150148nnne0d 10000 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  =/=  0 )
151149, 150div0d 9745 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( 0  /  n
)  =  0 )
152147, 151eqtrd 2436 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( (Λ `  n )  /  n )  =  0 )
153152oveq2d 6056 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) )  =  ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  0 ) )
15448ad2ant2r 728 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
155154mul01d 9221 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  0 )  =  0 )
156153, 155eqtrd 2436 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) )  =  0 )
157142, 144, 145, 156fsumvma2 20951 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  sum_ p  e.  ( ( 0 [,] x )  i^i  Prime )
sum_ k  e.  ( 1 ... ( |_
`  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) ) )
158129a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  C_  ( ( 0 [,] x )  i^i  Prime ) )
159 fzfid 11267 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  e.  Fin )
16024ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  .1.  : ( Base `  Z
) --> RR )
16130ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  L : ZZ --> ( Base `  Z ) )
16270ad2antrl 709 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  NN )
163 elfznn 11036 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  NN )
164163ad2antll 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN )
165164nnnn0d 10230 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN0 )
166162, 165nnexpcld 11499 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  NN )
167166nnzd 10330 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  ZZ )
168161, 167ffvelrnd 5830 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( L `  (
p ^ k ) )  e.  ( Base `  Z ) )
169160, 168ffvelrnd 5830 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(  .1.  `  ( L `  ( p ^ k ) ) )  e.  RR )
170 resubcl 9321 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  e.  RR )
17118, 169, 170sylancr 645 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  e.  RR )
172 vmacl 20854 . . . . . . . . . . . . . . . 16  |-  ( ( p ^ k )  e.  NN  ->  (Λ `  ( p ^ k
) )  e.  RR )
173166, 172syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  e.  RR )
174173, 166nndivred 10004 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  RR )
175171, 174remulcld 9072 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  e.  RR )
176175anassrs 630 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  e.  RR )
177176recnd 9070 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  e.  CC )
178159, 177fsumcl 12482 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  e.  CC )
179131, 178sylan2 461 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N } )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  e.  CC )
180 breq1 4175 . . . . . . . . . . . 12  |-  ( q  =  p  ->  (
q  ||  N  <->  p  ||  N
) )
181180notbid 286 . . . . . . . . . . 11  |-  ( q  =  p  ->  ( -.  q  ||  N  <->  -.  p  ||  N ) )
182 notrab 3578 . . . . . . . . . . 11  |-  ( ( ( 0 [,] x
)  i^i  Prime )  \  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }
)  =  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  -.  q  ||  N }
183181, 182elrab2 3054 . . . . . . . . . 10  |-  ( p  e.  ( ( ( 0 [,] x )  i^i  Prime )  \  {
q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q 
||  N } )  <-> 
( p  e.  ( ( 0 [,] x
)  i^i  Prime )  /\  -.  p  ||  N ) )
184124sseli 3304 . . . . . . . . . . 11  |-  ( p  e.  ( ( 0 [,] x )  i^i 
Prime )  ->  p  e. 
Prime )
18523ad3antrrr 711 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN )
186 simplrr 738 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  -.  p  ||  N )
187 simplrl 737 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  p  e.  Prime )
188185nnzd 10330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  ZZ )
189 coprm 13055 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( p  e.  Prime  /\  N  e.  ZZ )  ->  ( -.  p  ||  N  <->  ( p  gcd  N )  =  1 ) )
190187, 188, 189syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( -.  p  ||  N 
<->  ( p  gcd  N
)  =  1 ) )
191186, 190mpbid 202 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( p  gcd  N
)  =  1 )
192 prmz 13038 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  Prime  ->  p  e.  ZZ )
193187, 192syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  p  e.  ZZ )
194163adantl 453 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN )
195194nnnn0d 10230 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN0 )
196 rpexp1i 13076 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  NN0 )  ->  (
( p  gcd  N
)  =  1  -> 
( ( p ^
k )  gcd  N
)  =  1 ) )
197193, 188, 195, 196syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( ( p  gcd  N )  =  1  -> 
( ( p ^
k )  gcd  N
)  =  1 ) )
198191, 197mpd 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( ( p ^
k )  gcd  N
)  =  1 )
199185nnnn0d 10230 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN0 )
200167anassrs 630 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
p ^ k )  e.  ZZ )
201200adantlrr 702 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( p ^ k
)  e.  ZZ )
20220, 85, 27znunit 16799 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  ( p ^ k
)  e.  ZZ )  ->  ( ( L `
 ( p ^
k ) )  e.  (Unit `  Z )  <->  ( ( p ^ k
)  gcd  N )  =  1 ) )
203199, 201, 202syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( ( L `  ( p ^ k
) )  e.  (Unit `  Z )  <->  ( (
p ^ k )  gcd  N )  =  1 ) )
204198, 203mpbird 224 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( L `  (
p ^ k ) )  e.  (Unit `  Z ) )
20519, 20, 21, 85, 185, 204dchr1 20994 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
(  .1.  `  ( L `  ( p ^ k ) ) )  =  1 )
206205oveq2d 6056 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  =  ( 1  -  1 ) )
207 1m1e0 10024 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
208206, 207syl6eq 2452 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  =  0 )
209208oveq1d 6055 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  =  ( 0  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) ) )
210174recnd 9070 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  CC )
211210anassrs 630 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) )  e.  CC )
212211adantlrr 702 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  CC )
213212mul02d 9220 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( 0  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  =  0 )
214209, 213eqtrd 2436 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  =  0 )
215214sumeq2dv 12452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  =  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) 0 )
216 fzfid 11267 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  (
1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) )  e.  Fin )
217216olcd 383 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  (
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  C_  ( ZZ>=
`  1 )  \/  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  e.  Fin ) )
218 sumz 12471 . . . . . . . . . . . . 13  |-  ( ( ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  C_  ( ZZ>=
`  1 )  \/  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  e.  Fin )  ->  sum_ k  e.  ( 1 ... ( |_
`  ( ( log `  x )  /  ( log `  p ) ) ) ) 0  =  0 )
219217, 218syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) 0  =  0 )
220215, 219eqtrd 2436 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  =  0 )
221184, 220sylanr1 634 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  (
( 0 [,] x
)  i^i  Prime )  /\  -.  p  ||  N ) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  =  0 )
222183, 221sylan2b 462 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  ( (
( 0 [,] x
)  i^i  Prime )  \  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  =  0 )
223 ppifi 20841 . . . . . . . . . 10  |-  ( x  e.  RR  ->  (
( 0 [,] x
)  i^i  Prime )  e. 
Fin )
224144, 223syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 0 [,] x )  i^i  Prime )  e.  Fin )
225158, 179, 222, 224fsumss 12474 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ p  e.  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N } sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  =  sum_ p  e.  ( ( 0 [,] x )  i^i  Prime )
sum_ k  e.  ( 1 ... ( |_
`  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) ) )
226157, 225eqtr4d 2439 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  sum_ p  e.  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N } sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) ) )
227159, 176fsumrecl 12483 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  e.  RR )
228131, 227sylan2 461 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N } )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  e.  RR )
22973adantlr 696 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR )
23070adantl 453 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  NN )
231230nnrecred 10001 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR )
232230nnrpd 10603 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR+ )
233232rpreccld 10614 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR+ )
234 simplrl 737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  x  e.  RR+ )
235234relogcld 20471 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  x
)  e.  RR )
236230nnred 9971 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR )
23774adantl 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= ` 
2 ) )
238 eluz2b2 10504 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
239238simprbi 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  e.  ( ZZ>= `  2
)  ->  1  <  p )
240237, 239syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  <  p )
241236, 240rplogcld 20477 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR+ )
242235, 241rerpdivcld 10631 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  x
)  /  ( log `  p ) )  e.  RR )
243242flcld 11162 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  ZZ )
244243peano2zd 10334 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  ZZ )
245233, 244rpexpcld 11501 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR+ )
246245rpred 10604 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR )
247231, 246resubcld 9421 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p )  -  (
( 1  /  p
) ^ ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  +  1 ) ) )  e.  RR )
248237, 76syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( p  -  1 )  e.  NN )
249248nnrpd 10603 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( p  -  1 )  e.  RR+ )
250249, 232rpdivcld 10621 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( p  - 
1 )  /  p
)  e.  RR+ )
251247, 250rerpdivcld 10631 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( ( 1  /  p )  -  ( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) ) )  /  ( ( p  -  1 )  /  p ) )  e.  RR )
252229, 251remulcld 9072 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  p
)  x.  ( ( ( 1  /  p
)  -  ( ( 1  /  p ) ^ ( ( |_
`  ( ( log `  x )  /  ( log `  p ) ) )  +  1 ) ) )  /  (
( p  -  1 )  /  p ) ) )  e.  RR )
253173recnd 9070 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  e.  CC )
254166nncnd 9972 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  CC )
255166nnne0d 10000 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  =/=  0 )
256253, 254, 255divrecd 9749 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  =  ( (Λ `  (
p ^ k ) )  x.  ( 1  /  ( p ^
k ) ) ) )
257 simprl 733 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  Prime )
258 vmappw 20852 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  Prime  /\  k  e.  NN )  ->  (Λ `  ( p ^ k
) )  =  ( log `  p ) )
259257, 164, 258syl2anc 643 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  =  ( log `  p
) )
260162nncnd 9972 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  CC )
261162nnne0d 10000 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  =/=  0 )
262 elfzelz 11015 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  ZZ )
263262ad2antll 710 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  ZZ )
264260, 261, 263exprecd 11486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  =  ( 1  /  ( p ^
k ) ) )
265264eqcomd 2409 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  /  (
p ^ k ) )  =  ( ( 1  /  p ) ^ k ) )
266259, 265oveq12d 6058 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  x.  ( 1  / 
( p ^ k
) ) )  =  ( ( log `  p
)  x.  ( ( 1  /  p ) ^ k ) ) )
267256, 266eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  =  ( ( log `  p
)  x.  ( ( 1  /  p ) ^ k ) ) )
268267, 174eqeltrrd 2479 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( log `  p
)  x.  ( ( 1  /  p ) ^ k ) )  e.  RR )
269268anassrs 630 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
( log `  p
)  x.  ( ( 1  /  p ) ^ k ) )  e.  RR )
27018a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
1  e.  RR )
271 vmage0 20857 . . . . . . . . . . . . . . . . 17  |-  ( ( p ^ k )  e.  NN  ->  0  <_  (Λ `  ( p ^ k ) ) )
272166, 271syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  (Λ `  (
p ^ k ) ) )
273166nnred 9971 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  RR )
274166nngt0d 9999 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <  ( p ^ k ) )
275 divge0 9835 . . . . . . . . . . . . . . . 16  |-  ( ( ( (Λ `  (
p ^ k ) )  e.  RR  /\  0  <_  (Λ `  ( p ^ k ) ) )  /\  ( ( p ^ k )  e.  RR  /\  0  <  ( p ^ k
) ) )  -> 
0  <_  ( (Λ `  ( p ^ k
) )  /  (
p ^ k ) ) )
276173, 272, 273, 274, 275syl22anc 1185 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  ( (Λ `  ( p ^ k
) )  /  (
p ^ k ) ) )
27783leidi 9517 . . . . . . . . . . . . . . . . . 18  |-  0  <_  0
278 simpr 448 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  =  0 )  ->  (  .1.  `  ( L `  ( p ^ k
) ) )  =  0 )
279277, 278syl5breqr 4208 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  =  0 )  ->  0  <_  (  .1.  `  ( L `  ( p ^ k ) ) ) )
28023ad3antrrr 711 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  =/=  0 )  ->  N  e.  NN )
28192ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  .1.  e.  D )
28219, 20, 87, 22, 85, 281, 168dchrn0 20987 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (  .1.  `  ( L `  ( p ^ k ) ) )  =/=  0  <->  ( L `  ( p ^ k ) )  e.  (Unit `  Z
) ) )
283282biimpa 471 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  =/=  0 )  ->  ( L `  ( p ^ k ) )  e.  (Unit `  Z
) )
28419, 20, 21, 85, 280, 283dchr1 20994 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  =/=  0 )  ->  (  .1.  `  ( L `  ( p ^ k
) ) )  =  1 )
285104, 284syl5breqr 4208 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  =/=  0 )  ->  0  <_  (  .1.  `  ( L `  ( p ^ k ) ) ) )
286279, 285pm2.61dane 2645 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  (  .1.  `  ( L `  (
p ^ k ) ) ) )
287 subge02 9499 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
0  <_  (  .1.  `  ( L `  (
p ^ k ) ) )  <->  ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  <_  1
) )
28818, 169, 287sylancr 645 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 0  <_  (  .1.  `  ( L `  ( p ^ k
) ) )  <->  ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  <_  1
) )
289286, 288mpbid 202 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  <_  1 )
290171, 270, 174, 276, 289lemul1ad 9906 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  <_ 
( 1  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) ) )
291210mulid2d 9062 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  =  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )
292291, 267eqtrd 2436 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  =  ( ( log `  p
)  x.  ( ( 1  /  p ) ^ k ) ) )
293290, 292breqtrd 4196 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  <_ 
( ( log `  p
)  x.  ( ( 1  /  p ) ^ k ) ) )
294293anassrs 630 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) )  <_  ( ( log `  p )  x.  ( ( 1  /  p ) ^ k
) ) )
295159, 176, 269, 294fsumle 12533 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ( ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  x.  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) ) )  <_  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ( ( log `  p )  x.  (
( 1  /  p
) ^ k ) ) )
296229recnd 9070 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  CC )
297162nnrecred 10001 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  /  p
)  e.  RR )
298297, 165reexpcld 11495 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  RR )
299298recnd 9070 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  CC )
300299anassrs 630 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
( 1  /  p
) ^ k )  e.  CC )
301159, 296, 300fsummulc2 12522 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  p
)  x.  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( 1  /  p ) ^ k ) )  =  sum_ k  e.  ( 1 ... ( |_
`  ( ( log `  x )  /  ( log `  p ) ) ) ) ( ( log `  p )  x.  ( ( 1  /  p ) ^
k ) ) )
302 fzval3 11135 . . . . . . . . . . . . . . . 16  |-  ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  e.  ZZ  ->  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) )  =  ( 1..^ ( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 ) ) )
303243, 302syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  =  ( 1..^ ( ( |_
`  ( ( log `  x )  /  ( log `  p ) ) )  +  1 ) ) )
304303sumeq1d 12450 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ( ( 1  /  p ) ^
k )  =  sum_ k  e.  ( 1..^ ( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 ) ) ( ( 1  /  p ) ^ k
) )
305231recnd 9070 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  CC )
306230nngt0d 9999 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <  p )
307 recgt1 9862 . . . . . . . . . . . . . . . . . 18  |-  ( ( p  e.  RR  /\  0  <  p )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
308236, 306, 307syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
309240, 308mpbid 202 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  <  1 )
310231, 309ltned 9165 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  =/=  1 )
311 1nn0 10193 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
312311a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  e.  NN0 )
313 log1 20433 . . . . . . . . . . . . . . . . . . . . 21  |-  ( log `  1 )  =  0
314 simprr 734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
315 1rp 10572 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR+
316 simprl 733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
317 logleb 20451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR+  /\  x  e.  RR+ )  ->  (
1  <_  x  <->  ( log `  1 )  <_  ( log `  x ) ) )
318315, 316, 317sylancr 645 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  <_  x  <->  ( log `  1 )  <_  ( log `  x
) ) )
319314, 318mpbid 202 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  1
)  <_  ( log `  x ) )
320313, 319syl5eqbrr 4206 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( log `  x ) )
321320adantr 452 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( log `  x ) )
322235, 241, 321divge0d 10640 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( ( log `  x )  / 
( log `  p
) ) )
323 flge0nn0 11180 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( log `  x
)  /  ( log `  p ) )  e.  RR  /\  0  <_ 
( ( log `  x
)  /  ( log `  p ) ) )  ->  ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  e.  NN0 )
324242, 322, 323syl2anc 643 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  NN0 )
325 nn0p1nn 10215 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  e. 
NN0  ->  ( ( |_
`  ( ( log `  x )  /  ( log `  p ) ) )  +  1 )  e.  NN )
326324, 325syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  NN )
327 nnuz 10477 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
328326, 327syl6eleq 2494 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  ( ZZ>= `  1 )
)
329305, 310, 312, 328geoserg 12600 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\