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

Theorem rpvmasumlem 22716
Description: Lemma for rpvmasum 22755. 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 9365 . . . . . 6  |-  RR  e.  _V
2 rpssre 10993 . . . . . 6  |-  RR+  C_  RR
31, 2ssexi 4432 . . . . 5  |-  RR+  e.  _V
43a1i 11 . . . 4  |-  ( ph  -> 
RR+  e.  _V )
5 fzfid 11787 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  x ) )  e.  Fin )
6 elfznn 11470 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
76adantl 466 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
8 vmacl 22436 . . . . . . . . . 10  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
97, 8syl 16 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
109, 7nndivred 10362 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
1110recnd 9404 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
125, 11fsumcl 13202 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  e.  CC )
1312adantr 465 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
14 relogcl 22007 . . . . . . 7  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
1514adantl 466 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
1615recnd 9404 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
1713, 16subcld 9711 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) )  e.  CC )
18 1re 9377 . . . . . . . . 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 2438 . . . . . . . . . . . 12  |-  ( Base `  Z )  =  (
Base `  Z )
23 rpvmasum.a . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN )
2419, 20, 21, 22, 23dchr1re 22582 . . . . . . . . . . 11  |-  ( ph  ->  .1.  : ( Base `  Z ) --> RR )
2524adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  : (
Base `  Z ) --> RR )
2623nnnn0d 10628 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN0 )
27 rpvmasum.l . . . . . . . . . . . . 13  |-  L  =  ( ZRHom `  Z
)
2820, 22, 27znzrhfo 17960 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
29 fof 5615 . . . . . . . . . . . 12  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
3026, 28, 293syl 20 . . . . . . . . . . 11  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
31 elfzelz 11445 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
32 ffvelrn 5836 . . . . . . . . . . 11  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3330, 31, 32syl2an 477 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3425, 33ffvelrnd 5839 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  RR )
35 resubcl 9665 . . . . . . . . 9  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  e.  RR )
3618, 34, 35sylancr 663 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  RR )
3736, 10remulcld 9406 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
3837recnd 9404 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
395, 38fsumcl 13202 . . . . 5  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4039adantr 465 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
41 eqidd 2439 . . . 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 2439 . . . 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 6331 . . 3  |-  ( ph  ->  ( ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  oF  -  ( 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 9743 . . . . 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 13247 . . . . . . . 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 1cnd 9394 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
4736recnd 9404 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
4846, 47, 11subdird 9793 . . . . . . . . . 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 ) ) ) )
49 ax-1cn 9332 . . . . . . . . . . . 12  |-  1  e.  CC
5034recnd 9404 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  CC )
51 nncan 9630 . . . . . . . . . . . 12  |-  ( ( 1  e.  CC  /\  (  .1.  `  ( L `  n ) )  e.  CC )  ->  (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  =  (  .1.  `  ( L `  n )
) )
5249, 50, 51sylancr 663 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  ( 1  -  (  .1.  `  ( L `  n )
) ) )  =  (  .1.  `  ( L `  n )
) )
5352oveq1d 6101 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) ) )
5411mulid2d 9396 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( (Λ `  n
)  /  n ) )  =  ( (Λ `  n )  /  n
) )
5554oveq1d 6101 . . . . . . . . . 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 ) ) ) )
5648, 53, 553eqtr3rd 2479 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  -  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
5756sumeq2dv 13172 . . . . . . . 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 2472 . . . . . . 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 6101 . . . . . 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 465 . . . . 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 2470 . . . 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 4373 . . 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 2470 . 2  |-  ( ph  ->  ( ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  -  ( log `  x
) ) )  oF  -  ( 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 22711 . . 3  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) ) )  e.  O(1)
652a1i 11 . . . 4  |-  ( ph  -> 
RR+  C_  RR )
66 1red 9393 . . . 4  |-  ( ph  ->  1  e.  RR )
67 prmdvdsfi 22425 . . . . . 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 3109 . . . . . 6  |-  ( p  e.  { q  e. 
Prime  |  q  ||  N }  ->  p  e. 
Prime )
70 prmnn 13758 . . . . . . . . . 10  |-  ( p  e.  Prime  ->  p  e.  NN )
7170adantl 466 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  NN )
7271nnrpd 11018 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  RR+ )
7372relogcld 22052 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( log `  p )  e.  RR )
74 prmuz2 13773 . . . . . . . . 9  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
7574adantl 466 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= `  2 )
)
76 uz2m1nn 10921 . . . . . . . 8  |-  ( p  e.  ( ZZ>= `  2
)  ->  ( p  -  1 )  e.  NN )
7775, 76syl 16 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( p  -  1 )  e.  NN )
7873, 77nndivred 10362 . . . . . 6  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( log `  p )  / 
( p  -  1 ) )  e.  RR )
7969, 78sylan2 474 . . . . 5  |-  ( (
ph  /\  p  e.  { q  e.  Prime  |  q 
||  N } )  ->  ( ( log `  p )  /  (
p  -  1 ) )  e.  RR )
8068, 79fsumrecl 13203 . . . 4  |-  ( ph  -> 
sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
81 fzfid 11787 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
82 simpr 461 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  =  0 )
83 0re 9378 . . . . . . . . . . 11  |-  0  e.  RR
8482, 83syl6eqel 2526 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
85 eqid 2438 . . . . . . . . . . . 12  |-  (Unit `  Z )  =  (Unit `  Z )
8623ad3antrrr 729 . . . . . . . . . . . 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 22573 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  G  e.  Abel )
89 ablgrp 16273 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  ->  G  e. 
Grp )
9087, 21grpidcl 15557 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Grp  ->  .1.  e.  D )
9123, 88, 89, 904syl 21 . . . . . . . . . . . . . . 15  |-  ( ph  ->  .1.  e.  D )
9291ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  e.  D
)
9333adantlr 714 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
9419, 20, 87, 22, 85, 92, 93dchrn0 22569 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (  .1.  `  ( L `  n
) )  =/=  0  <->  ( L `  n )  e.  (Unit `  Z
) ) )
9594biimpa 484 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  ( L `  n )  e.  (Unit `  Z ) )
9619, 20, 21, 85, 86, 95dchr1 22576 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  =  1 )
9796, 18syl6eqel 2526 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
9884, 97pm2.61dane 2684 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
9918, 98, 35sylancr 663 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n )
) )  e.  RR )
10010adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n
)  /  n )  e.  RR )
10199, 100remulcld 9406 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  RR )
10281, 101fsumrecl 13203 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
103 0le1 9855 . . . . . . . . . . 11  |-  0  <_  1
10482, 103syl6eqbr 4324 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
10518leidi 9866 . . . . . . . . . . 11  |-  1  <_  1
10696, 105syl6eqbr 4324 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
107104, 106pm2.61dane 2684 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
108 subge0 9844 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
0  <_  ( 1  -  (  .1.  `  ( L `  n ) ) )  <->  (  .1.  `  ( L `  n
) )  <_  1
) )
10918, 98, 108sylancr 663 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  <_ 
( 1  -  (  .1.  `  ( L `  n ) ) )  <-> 
(  .1.  `  ( L `  n )
)  <_  1 ) )
110107, 109mpbird 232 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
1  -  (  .1.  `  ( L `  n
) ) ) )
1119adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n )  e.  RR )
1126adantl 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
113 vmage0 22439 . . . . . . . . . 10  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
114112, 113syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
115112nnred 10329 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
116112nngt0d 10357 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <  n
)
117 divge0 10190 . . . . . . . . 9  |-  ( ( ( (Λ `  n
)  e.  RR  /\  0  <_  (Λ `  n )
)  /\  ( n  e.  RR  /\  0  < 
n ) )  -> 
0  <_  ( (Λ `  n )  /  n
) )
118111, 114, 115, 116, 117syl22anc 1219 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
(Λ `  n )  /  n ) )
11999, 100, 110, 118mulge0d 9908 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )
12081, 101, 119fsumge0 13250 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )
121102, 120absidd 12901 . . . . 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 ) ) )
12268adantr 465 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
123 inss2 3566 . . . . . . . . 9  |-  ( ( 0 [,] x )  i^i  Prime )  C_  Prime
124 rabss2 3430 . . . . . . . . 9  |-  ( ( ( 0 [,] x
)  i^i  Prime )  C_  Prime  ->  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N }  C_  { q  e. 
Prime  |  q  ||  N } )
125123, 124mp1i 12 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  C_ 
{ q  e.  Prime  |  q  ||  N }
)
126 ssfi 7525 . . . . . . . 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 )
127122, 125, 126syl2anc 661 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  e.  Fin )
128 ssrab2 3432 . . . . . . . . . 10  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  (
( 0 [,] x
)  i^i  Prime )
129128, 123sstri 3360 . . . . . . . . 9  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  Prime
130129sseli 3347 . . . . . . . 8  |-  ( p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N }  ->  p  e.  Prime )
13178adantlr 714 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  p
)  /  ( p  -  1 ) )  e.  RR )
132130, 131sylan2 474 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N } )  ->  (
( log `  p
)  /  ( p  -  1 ) )  e.  RR )
133127, 132fsumrecl 13203 . . . . . 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 )
13480adantr 465 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
135 fveq2 5686 . . . . . . . . . . . 12  |-  ( n  =  ( p ^
k )  ->  ( L `  n )  =  ( L `  ( p ^ k
) ) )
136135fveq2d 5690 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (  .1.  `  ( L `  n ) )  =  (  .1.  `  ( L `  ( p ^ k ) ) ) )
137136oveq2d 6102 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  =  ( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) ) )
138 fveq2 5686 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (Λ `  n )  =  (Λ `  ( p ^ k
) ) )
139 id 22 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  n  =  ( p ^
k ) )
140138, 139oveq12d 6104 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
(Λ `  n )  /  n )  =  ( (Λ `  ( p ^ k ) )  /  ( p ^
k ) ) )
141137, 140oveq12d 6104 . . . . . . . . 9  |-  ( n  =  ( p ^
k )  ->  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) ) )
142 rpre 10989 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  x  e.  RR )
143142ad2antrl 727 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
14438adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
145 simprr 756 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
(Λ `  n )  =  0 )
146145oveq1d 6101 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( (Λ `  n )  /  n )  =  ( 0  /  n ) )
1476ad2antrl 727 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  NN )
148147nncnd 10330 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  CC )
149147nnne0d 10358 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  =/=  0 )
150148, 149div0d 10098 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( 0  /  n
)  =  0 )
151146, 150eqtrd 2470 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( (Λ `  n )  /  n )  =  0 )
152151oveq2d 6102 . . . . . . . . . 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 ) )
15347ad2ant2r 746 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
154153mul01d 9560 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  0 )  =  0 )
155152, 154eqtrd 2470 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) )  =  0 )
156141, 143, 144, 155fsumvma2 22533 . . . . . . . 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 ) ) ) )
157128a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  C_  ( ( 0 [,] x )  i^i  Prime ) )
158 fzfid 11787 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  e.  Fin )
15924ad2antrr 725 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  .1.  : ( Base `  Z
) --> RR )
16030ad2antrr 725 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  L : ZZ --> ( Base `  Z ) )
16170ad2antrl 727 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  NN )
162 elfznn 11470 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  NN )
163162ad2antll 728 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN )
164163nnnn0d 10628 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN0 )
165161, 164nnexpcld 12021 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  NN )
166165nnzd 10738 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  ZZ )
167160, 166ffvelrnd 5839 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( L `  (
p ^ k ) )  e.  ( Base `  Z ) )
168159, 167ffvelrnd 5839 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(  .1.  `  ( L `  ( p ^ k ) ) )  e.  RR )
169 resubcl 9665 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  e.  RR )
17018, 168, 169sylancr 663 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  e.  RR )
171 vmacl 22436 . . . . . . . . . . . . . . . 16  |-  ( ( p ^ k )  e.  NN  ->  (Λ `  ( p ^ k
) )  e.  RR )
172165, 171syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  e.  RR )
173172, 165nndivred 10362 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  RR )
174170, 173remulcld 9406 . . . . . . . . . . . . 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 )
175174anassrs 648 . . . . . . . . . . . 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 )
176175recnd 9404 . . . . . . . . . . 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 )
177158, 176fsumcl 13202 . . . . . . . . . 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 )
178130, 177sylan2 474 . . . . . . . . 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 )
179 breq1 4290 . . . . . . . . . . . 12  |-  ( q  =  p  ->  (
q  ||  N  <->  p  ||  N
) )
180179notbid 294 . . . . . . . . . . 11  |-  ( q  =  p  ->  ( -.  q  ||  N  <->  -.  p  ||  N ) )
181 notrab 3622 . . . . . . . . . . 11  |-  ( ( ( 0 [,] x
)  i^i  Prime )  \  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }
)  =  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  -.  q  ||  N }
182180, 181elrab2 3114 . . . . . . . . . 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 ) )
183123sseli 3347 . . . . . . . . . . 11  |-  ( p  e.  ( ( 0 [,] x )  i^i 
Prime )  ->  p  e. 
Prime )
18423ad3antrrr 729 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN )
185 simplrr 760 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  -.  p  ||  N )
186 simplrl 759 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  p  e.  Prime )
187184nnzd 10738 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  ZZ )
188 coprm 13778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( p  e.  Prime  /\  N  e.  ZZ )  ->  ( -.  p  ||  N  <->  ( p  gcd  N )  =  1 ) )
189186, 187, 188syl2anc 661 . . . . . . . . . . . . . . . . . . . . 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 ) )
190185, 189mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( p  gcd  N
)  =  1 )
191 prmz 13759 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  Prime  ->  p  e.  ZZ )
192186, 191syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  p  e.  ZZ )
193162adantl 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN )
194193nnnn0d 10628 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN0 )
195 rpexp1i 13799 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  NN0 )  ->  (
( p  gcd  N
)  =  1  -> 
( ( p ^
k )  gcd  N
)  =  1 ) )
196192, 187, 194, 195syl3anc 1218 . . . . . . . . . . . . . . . . . . . 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 ) )
197190, 196mpd 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 )
198184nnnn0d 10628 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN0 )
199166anassrs 648 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
p ^ k )  e.  ZZ )
200199adantlrr 720 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( p ^ k
)  e.  ZZ )
20120, 85, 27znunit 17976 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  ( p ^ k
)  e.  ZZ )  ->  ( ( L `
 ( p ^
k ) )  e.  (Unit `  Z )  <->  ( ( p ^ k
)  gcd  N )  =  1 ) )
202198, 200, 201syl2anc 661 . . . . . . . . . . . . . . . . . . 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 ) )
203197, 202mpbird 232 . . . . . . . . . . . . . . . . . 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 ) )
20419, 20, 21, 85, 184, 203dchr1 22576 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
(  .1.  `  ( L `  ( p ^ k ) ) )  =  1 )
205204oveq2d 6102 . . . . . . . . . . . . . . . 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 ) )
206 1m1e0 10382 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
207205, 206syl6eq 2486 . . . . . . . . . . . . . . 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 )
208207oveq1d 6101 . . . . . . . . . . . . . 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
) ) ) )
209173recnd 9404 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  CC )
210209anassrs 648 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) )  e.  CC )
211210adantlrr 720 . . . . . . . . . . . . . . 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 )
212211mul02d 9559 . . . . . . . . . . . . . 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 )
213208, 212eqtrd 2470 . . . . . . . . . . . . 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 )
214213sumeq2dv 13172 . . . . . . . . . . . 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 )
215 fzfid 11787 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  (
1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) )  e.  Fin )
216215olcd 393 . . . . . . . . . . . . 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 ) )
217 sumz 13191 . . . . . . . . . . . . 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 )
218216, 217syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) 0  =  0 )
219214, 218eqtrd 2470 . . . . . . . . . . 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 )
220183, 219sylanr1 652 . . . . . . . . . 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 )
221182, 220sylan2b 475 . . . . . . . . 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 )
222 ppifi 22423 . . . . . . . . . 10  |-  ( x  e.  RR  ->  (
( 0 [,] x
)  i^i  Prime )  e. 
Fin )
223143, 222syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 0 [,] x )  i^i  Prime )  e.  Fin )
224157, 178, 221, 223fsumss 13194 . . . . . . . 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 ) ) ) )
225156, 224eqtr4d 2473 . . . . . . 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
) ) ) )
226158, 175fsumrecl 13203 . . . . . . . . 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 )
227130, 226sylan2 474 . . . . . . . 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 )
22873adantlr 714 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR )
22970adantl 466 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  NN )
230229nnrecred 10359 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR )
231229nnrpd 11018 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR+ )
232231rpreccld 11029 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR+ )
233 simplrl 759 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  x  e.  RR+ )
234233relogcld 22052 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  x
)  e.  RR )
235229nnred 10329 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR )
23674adantl 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= ` 
2 ) )
237 eluz2b2 10919 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
238237simprbi 464 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  e.  ( ZZ>= `  2
)  ->  1  <  p )
239236, 238syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  <  p )
240235, 239rplogcld 22058 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR+ )
241234, 240rerpdivcld 11046 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  x
)  /  ( log `  p ) )  e.  RR )
242241flcld 11640 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  ZZ )
243242peano2zd 10742 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  ZZ )
244232, 243rpexpcld 12023 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR+ )
245244rpred 11019 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR )
246230, 245resubcld 9768 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p )  -  (
( 1  /  p
) ^ ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  +  1 ) ) )  e.  RR )
247236, 76syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( p  -  1 )  e.  NN )
248247nnrpd 11018 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( p  -  1 )  e.  RR+ )
249248, 231rpdivcld 11036 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( p  - 
1 )  /  p
)  e.  RR+ )
250246, 249rerpdivcld 11046 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( ( 1  /  p )  -  ( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) ) )  /  ( ( p  -  1 )  /  p ) )  e.  RR )
251228, 250remulcld 9406 . . . . . . . . . 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 )
252172recnd 9404 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  e.  CC )
253165nncnd 10330 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  CC )
254165nnne0d 10358 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  =/=  0 )
255252, 253, 254divrecd 10102 . . . . . . . . . . . . . . 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 ) ) ) )
256 simprl 755 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  Prime )
257 vmappw 22434 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  Prime  /\  k  e.  NN )  ->  (Λ `  ( p ^ k
) )  =  ( log `  p ) )
258256, 163, 257syl2anc 661 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  =  ( log `  p
) )
259161nncnd 10330 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  CC )
260161nnne0d 10358 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  =/=  0 )
261 elfzelz 11445 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  ZZ )
262261ad2antll 728 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  ZZ )
263259, 260, 262exprecd 12008 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  =  ( 1  /  ( p ^
k ) ) )
264263eqcomd 2443 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  /  (
p ^ k ) )  =  ( ( 1  /  p ) ^ k ) )
265258, 264oveq12d 6104 . . . . . . . . . . . . . . 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 ) ) )
266255, 265eqtrd 2470 . . . . . . . . . . . . . 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 ) ) )
267266, 173eqeltrrd 2513 . . . . . . . . . . . . 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 )
268267anassrs 648 . . . . . . . . . . . 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 )
269 1red 9393 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
1  e.  RR )
270 vmage0 22439 . . . . . . . . . . . . . . . . 17  |-  ( ( p ^ k )  e.  NN  ->  0  <_  (Λ `  ( p ^ k ) ) )
271165, 270syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  (Λ `  (
p ^ k ) ) )
272165nnred 10329 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  RR )
273165nngt0d 10357 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <  ( p ^ k ) )
274 divge0 10190 . . . . . . . . . . . . . . . 16  |-  ( ( ( (Λ `  (
p ^ k ) )  e.  RR  /\  0  <_  (Λ `  ( p ^ k ) ) )  /\  ( ( p ^ k )  e.  RR  /\  0  <  ( p ^ k
) ) )  -> 
0  <_  ( (Λ `  ( p ^ k
) )  /  (
p ^ k ) ) )
275172, 271, 272, 273, 274syl22anc 1219 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  ( (Λ `  ( p ^ k
) )  /  (
p ^ k ) ) )
27683leidi 9866 . . . . . . . . . . . . . . . . . 18  |-  0  <_  0
277 simpr 461 . . . . . . . . . . . . . . . . . 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 )
278276, 277syl5breqr 4323 . . . . . . . . . . . . . . . . 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 ) ) ) )
27923ad3antrrr 729 . . . . . . . . . . . . . . . . . . 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 )
28091ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  .1.  e.  D )
28119, 20, 87, 22, 85, 280, 167dchrn0 22569 . . . . . . . . . . . . . . . . . . . 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
) ) )
282281biimpa 484 . . . . . . . . . . . . . . . . . . 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
) )
28319, 20, 21, 85, 279, 282dchr1 22576 . . . . . . . . . . . . . . . . . 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 )
284103, 283syl5breqr 4323 . . . . . . . . . . . . . . . . 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 ) ) ) )
285278, 284pm2.61dane 2684 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  (  .1.  `  ( L `  (
p ^ k ) ) ) )
286 subge02 9847 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
0  <_  (  .1.  `  ( L `  (
p ^ k ) ) )  <->  ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  <_  1
) )
28718, 168, 286sylancr 663 . . . . . . . . . . . . . . . 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
) )
288285, 287mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  <_  1 )
289170, 269, 173, 275, 288lemul1ad 10264 . . . . . . . . . . . . . 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
) ) ) )
290209mulid2d 9396 . . . . . . . . . . . . . . 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 ) ) )
291290, 266eqtrd 2470 . . . . . . . . . . . . . 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 ) ) )
292289, 291breqtrd 4311 . . . . . . . . . . . . 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 ) ) )
293292anassrs 648 . . . . . . . . . . . 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
) ) )
294158, 175, 268, 293fsumle 13254 . . . . . . . . . . 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 ) ) )
295228recnd 9404 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  CC )
296161nnrecred 10359 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  /  p
)  e.  RR )
297296, 164reexpcld 12017 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  RR )
298297recnd 9404 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  CC )
299298anassrs 648 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
( 1  /  p
) ^ k )  e.  CC )
300158, 295, 299fsummulc2 13243 . . . . . . . . . . . 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 ) ) )
301 fzval3 11597 . . . . . . . . . . . . . . . 16  |-  ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  e.  ZZ  ->  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) )  =  ( 1..^ ( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 ) ) )
302242, 301syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  =  ( 1..^ ( ( |_
`  ( ( log `  x )  /  ( log `  p ) ) )  +  1 ) ) )
303302sumeq1d 13170 . . . . . . . . . . . . . 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
) )
304230recnd 9404 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  CC )
305229nngt0d 10357 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <  p )
306 recgt1 10220 . . . . . . . . . . . . . . . . . 18  |-  ( ( p  e.  RR  /\  0  <  p )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
307235, 305, 306syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
308239, 307mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  <  1 )
309230, 308ltned 9502 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  =/=  1 )
310 1nn0 10587 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
311310a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  e.  NN0 )
312 log1 22014 . . . . . . . . . . . . . . . . . . . . 21  |-  ( log `  1 )  =  0
313 simprr 756 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
314 1rp 10987 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR+
315 simprl 755 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
316 logleb 22032 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR+  /\  x  e.  RR+ )  ->  (
1  <_  x  <->  ( log `  1 )  <_  ( log `  x ) ) )
317314, 315, 316sylancr 663 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  <_  x  <->  ( log `  1 )  <_  ( log `  x
) ) )
318313, 317mpbid 210 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  1
)  <_  ( log `  x ) )
319312, 318syl5eqbrr 4321 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( log `  x ) )
320319adantr 465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( log `  x ) )
321234, 240, 320divge0d 11055 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( ( log `  x )  / 
( log `  p
) ) )
322 flge0nn0 11658 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( log `  x
)  /  ( log `  p ) )  e.  RR  /\  0  <_ 
( ( log `  x
)  /  ( log `  p ) ) )  ->  ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  e.  NN0 )
323241, 321, 322syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  NN0 )
324 nn0p1nn 10611 . . . . . . . . . . . . . . . . 17  |-  ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  e. 
NN0  ->  ( ( |_
`  ( ( log `  x )  /  ( log `  p ) ) )  +  1 )  e.  NN )
325323, 324syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  NN )
326 nnuz 10888 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
327325, 326syl6eleq 2528 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  ( ZZ>= `  1 )
)
328304, 309, 311, 327geoserg 13320 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\