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

Theorem rpvmasumlem 21183
Description: Lemma for rpvmasum 21222. 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 9083 . . . . . 6  |-  RR  e.  _V
2 rpssre 10624 . . . . . 6  |-  RR+  C_  RR
31, 2ssexi 4350 . . . . 5  |-  RR+  e.  _V
43a1i 11 . . . 4  |-  ( ph  -> 
RR+  e.  _V )
5 fzfid 11314 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  x ) )  e.  Fin )
6 elfznn 11082 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
76adantl 454 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
8 vmacl 20903 . . . . . . . . . 10  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
97, 8syl 16 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
109, 7nndivred 10050 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
1110recnd 9116 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
125, 11fsumcl 12529 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  e.  CC )
1312adantr 453 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
14 relogcl 20475 . . . . . . 7  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
1514adantl 454 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
1615recnd 9116 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
1713, 16subcld 9413 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) )  e.  CC )
18 1re 9092 . . . . . . . . 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 21049 . . . . . . . . . . 11  |-  ( ph  ->  .1.  : ( Base `  Z ) --> RR )
2524adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  : (
Base `  Z ) --> RR )
2623nnnn0d 10276 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN0 )
27 rpvmasum.l . . . . . . . . . . . . 13  |-  L  =  ( ZRHom `  Z
)
2820, 22, 27znzrhfo 16830 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
29 fof 5655 . . . . . . . . . . . 12  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
3026, 28, 293syl 19 . . . . . . . . . . 11  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
31 elfzelz 11061 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
32 ffvelrn 5870 . . . . . . . . . . 11  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3330, 31, 32syl2an 465 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
3425, 33ffvelrnd 5873 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  RR )
35 resubcl 9367 . . . . . . . . 9  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  e.  RR )
3618, 34, 35sylancr 646 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  RR )
3736, 10remulcld 9118 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
3837recnd 9116 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
395, 38fsumcl 12529 . . . . 5  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4039adantr 453 . . . 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 6324 . . 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 9445 . . . . 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 12573 . . . . . . . 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 9050 . . . . . . . . . . . 12  |-  1  e.  CC
4746a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
4836recnd 9116 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
4947, 48, 11subdird 9492 . . . . . . . . . 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 9116 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  CC )
51 nncan 9332 . . . . . . . . . . . 12  |-  ( ( 1  e.  CC  /\  (  .1.  `  ( L `  n ) )  e.  CC )  ->  (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  =  (  .1.  `  ( L `  n )
) )
5246, 50, 51sylancr 646 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  ( 1  -  (  .1.  `  ( L `  n )
) ) )  =  (  .1.  `  ( L `  n )
) )
5352oveq1d 6098 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) ) )
5411mulid2d 9108 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( (Λ `  n
)  /  n ) )  =  ( (Λ `  n )  /  n
) )
5554oveq1d 6098 . . . . . . . . . 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 2479 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  -  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
5756sumeq2dv 12499 . . . . . . . 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 6098 . . . . . 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 453 . . . . 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 4297 . . 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
) ) )  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 21178 . . 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 20892 . . . . . 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 3092 . . . . . 6  |-  ( p  e.  { q  e. 
Prime  |  q  ||  N }  ->  p  e. 
Prime )
70 prmnn 13084 . . . . . . . . . 10  |-  ( p  e.  Prime  ->  p  e.  NN )
7170adantl 454 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  NN )
7271nnrpd 10649 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  RR+ )
7372relogcld 20520 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( log `  p )  e.  RR )
74 prmuz2 13099 . . . . . . . . 9  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
7574adantl 454 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= `  2 )
)
76 uz2m1nn 10552 . . . . . . . 8  |-  ( p  e.  ( ZZ>= `  2
)  ->  ( p  -  1 )  e.  NN )
7775, 76syl 16 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( p  -  1 )  e.  NN )
7873, 77nndivred 10050 . . . . . 6  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( log `  p )  / 
( p  -  1 ) )  e.  RR )
7969, 78sylan2 462 . . . . 5  |-  ( (
ph  /\  p  e.  { q  e.  Prime  |  q 
||  N } )  ->  ( ( log `  p )  /  (
p  -  1 ) )  e.  RR )
8068, 79fsumrecl 12530 . . . 4  |-  ( ph  -> 
sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
81 fzfid 11314 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
82 simpr 449 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  =  0 )
83 0re 9093 . . . . . . . . . . 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 712 . . . . . . . . . . . 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 21040 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN  ->  G  e.  Abel )
89 ablgrp 15419 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  ->  G  e. 
Grp )
9087, 21grpidcl 14835 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Grp  ->  .1.  e.  D )
9123, 88, 89, 904syl 20 . . . . . . . . . . . . . . 15  |-  ( ph  ->  .1.  e.  D )
9291ad2antrr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  e.  D
)
9333adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
9419, 20, 87, 22, 85, 92, 93dchrn0 21036 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (  .1.  `  ( L `  n
) )  =/=  0  <->  ( L `  n )  e.  (Unit `  Z
) ) )
9594biimpa 472 . . . . . . . . . . . 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 21043 . . . . . . . . . . 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 646 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n )
) )  e.  RR )
10010adantlr 697 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n
)  /  n )  e.  RR )
10199, 100remulcld 9118 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  RR )
10281, 101fsumrecl 12530 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
103 0le1 9553 . . . . . . . . . . 11  |-  0  <_  1
10482, 103syl6eqbr 4251 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
10518leidi 9563 . . . . . . . . . . 11  |-  1  <_  1
10696, 105syl6eqbr 4251 . . . . . . . . . 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 9543 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
0  <_  ( 1  -  (  .1.  `  ( L `  n ) ) )  <->  (  .1.  `  ( L `  n
) )  <_  1
) )
10918, 98, 108sylancr 646 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  <_ 
( 1  -  (  .1.  `  ( L `  n ) ) )  <-> 
(  .1.  `  ( L `  n )
)  <_  1 ) )
110107, 109mpbird 225 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
1  -  (  .1.  `  ( L `  n
) ) ) )
1119adantlr 697 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n )  e.  RR )
1126adantl 454 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
113 vmage0 20906 . . . . . . . . . 10  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
114112, 113syl 16 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
115112nnred 10017 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
116112nngt0d 10045 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <  n
)
117 divge0 9881 . . . . . . . . 9  |-  ( ( ( (Λ `  n
)  e.  RR  /\  0  <_  (Λ `  n )
)  /\  ( n  e.  RR  /\  0  < 
n ) )  -> 
0  <_  ( (Λ `  n )  /  n
) )
118111, 114, 115, 116, 117syl22anc 1186 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
(Λ `  n )  /  n ) )
11999, 100, 110, 118mulge0d 9605 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )
12081, 101, 119fsumge0 12576 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )
121102, 120absidd 12227 . . . . 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 453 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
123 inss2 3564 . . . . . . . . 9  |-  ( ( 0 [,] x )  i^i  Prime )  C_  Prime
124 rabss2 3428 . . . . . . . . 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 7331 . . . . . . . 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 644 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  e.  Fin )
128 ssrab2 3430 . . . . . . . . . 10  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  (
( 0 [,] x
)  i^i  Prime )
129128, 123sstri 3359 . . . . . . . . 9  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  Prime
130129sseli 3346 . . . . . . . 8  |-  ( p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N }  ->  p  e.  Prime )
13178adantlr 697 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  p
)  /  ( p  -  1 ) )  e.  RR )
132130, 131sylan2 462 . . . . . . 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 12530 . . . . . 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 453 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
135 fveq2 5730 . . . . . . . . . . . 12  |-  ( n  =  ( p ^
k )  ->  ( L `  n )  =  ( L `  ( p ^ k
) ) )
136135fveq2d 5734 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (  .1.  `  ( L `  n ) )  =  (  .1.  `  ( L `  ( p ^ k ) ) ) )
137136oveq2d 6099 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  =  ( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) ) )
138 fveq2 5730 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (Λ `  n )  =  (Λ `  ( p ^ k
) ) )
139 id 21 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  n  =  ( p ^
k ) )
140138, 139oveq12d 6101 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
(Λ `  n )  /  n )  =  ( (Λ `  ( p ^ k ) )  /  ( p ^
k ) ) )
141137, 140oveq12d 6101 . . . . . . . . 9  |-  ( n  =  ( p ^
k )  ->  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) ) )
142 rpre 10620 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  x  e.  RR )
143142ad2antrl 710 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
14438adantlr 697 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
145 simprr 735 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
(Λ `  n )  =  0 )
146145oveq1d 6098 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( (Λ `  n )  /  n )  =  ( 0  /  n ) )
1476ad2antrl 710 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  NN )
148147nncnd 10018 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  CC )
149147nnne0d 10046 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  =/=  0 )
150148, 149div0d 9791 . . . . . . . . . . . 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 6099 . . . . . . . . . 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 ) )
15348ad2ant2r 729 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
154153mul01d 9267 . . . . . . . . . 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 21000 . . . . . . . 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 11314 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  e.  Fin )
15924ad2antrr 708 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  .1.  : ( Base `  Z
) --> RR )
16030ad2antrr 708 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  L : ZZ --> ( Base `  Z ) )
16170ad2antrl 710 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  NN )
162 elfznn 11082 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  NN )
163162ad2antll 711 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN )
164163nnnn0d 10276 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN0 )
165161, 164nnexpcld 11546 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  NN )
166165nnzd 10376 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  ZZ )
167160, 166ffvelrnd 5873 . . . . . . . . . . . . . . . 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 5873 . . . . . . . . . . . . . . 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 9367 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  e.  RR )
17018, 168, 169sylancr 646 . . . . . . . . . . . . . 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 20903 . . . . . . . . . . . . . . . 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 10050 . . . . . . . . . . . . . 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 9118 . . . . . . . . . . . . 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 631 . . . . . . . . . . . 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 9116 . . . . . . . . . . 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 12529 . . . . . . . . . 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 462 . . . . . . . . 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 4217 . . . . . . . . . . . 12  |-  ( q  =  p  ->  (
q  ||  N  <->  p  ||  N
) )
180179notbid 287 . . . . . . . . . . 11  |-  ( q  =  p  ->  ( -.  q  ||  N  <->  -.  p  ||  N ) )
181 notrab 3620 . . . . . . . . . . 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 3096 . . . . . . . . . 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 3346 . . . . . . . . . . 11  |-  ( p  e.  ( ( 0 [,] x )  i^i 
Prime )  ->  p  e. 
Prime )
18423ad3antrrr 712 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN )
185 simplrr 739 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  -.  p  ||  N )
186 simplrl 738 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  p  e.  Prime )
187184nnzd 10376 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  ZZ )
188 coprm 13102 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( p  e.  Prime  /\  N  e.  ZZ )  ->  ( -.  p  ||  N  <->  ( p  gcd  N )  =  1 ) )
189186, 187, 188syl2anc 644 . . . . . . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . . . . . . 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 13085 . . . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN )
194193nnnn0d 10276 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN0 )
195 rpexp1i 13123 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  NN0 )  ->  (
( p  gcd  N
)  =  1  -> 
( ( p ^
k )  gcd  N
)  =  1 ) )
196192, 187, 194, 195syl3anc 1185 . . . . . . . . . . . . . . . . . . . 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 10276 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN0 )
199166anassrs 631 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
p ^ k )  e.  ZZ )
200199adantlrr 703 . . . . . . . . . . . . . . . . . . . 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 16846 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  ( p ^ k
)  e.  ZZ )  ->  ( ( L `
 ( p ^
k ) )  e.  (Unit `  Z )  <->  ( ( p ^ k
)  gcd  N )  =  1 ) )
202198, 200, 201syl2anc 644 . . . . . . . . . . . . . . . . . . 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 225 . . . . . . . . . . . . . . . . . 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 21043 . . . . . . . . . . . . . . . . 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 6099 . . . . . . . . . . . . . . . 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 10070 . . . . . . . . . . . . . . . 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 6098 . . . . . . . . . . . . . 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 9116 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  CC )
210209anassrs 631 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) )  e.  CC )
211210adantlrr 703 . . . . . . . . . . . . . . 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 9266 . . . . . . . . . . . . . 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 12499 . . . . . . . . . . . 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 11314 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  (
1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) )  e.  Fin )
216215olcd 384 . . . . . . . . . . . . 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 12518 . . . . . . . . . . . . 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 635 . . . . . . . . . 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 463 . . . . . . . . 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 20890 . . . . . . . . . 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 12521 . . . . . . . 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 12530 . . . . . . . . 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 462 . . . . . . . 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 697 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR )
22970adantl 454 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  NN )
230229nnrecred 10047 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR )
231229nnrpd 10649 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR+ )
232231rpreccld 10660 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR+ )
233 simplrl 738 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  x  e.  RR+ )
234233relogcld 20520 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  x
)  e.  RR )
235229nnred 10017 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR )
23674adantl 454 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= ` 
2 ) )
237 eluz2b2 10550 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
238237simprbi 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  e.  ( ZZ>= `  2
)  ->  1  <  p )
239236, 238syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  <  p )
240235, 239rplogcld 20526 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR+ )
241234, 240rerpdivcld 10677 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  x
)  /  ( log `  p ) )  e.  RR )
242241flcld 11209 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  ZZ )
243242peano2zd 10380 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  ZZ )
244232, 243rpexpcld 11548 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR+ )
245244rpred 10650 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR )
246230, 245resubcld 9467 . . . . . . . . . . . 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 10649 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( p  -  1 )  e.  RR+ )
249248, 231rpdivcld 10667 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( p  - 
1 )  /  p
)  e.  RR+ )
250246, 249rerpdivcld 10677 . . . . . . . . . . 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 9118 . . . . . . . . . 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 9116 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  e.  CC )
253165nncnd 10018 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  CC )
254165nnne0d 10046 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  =/=  0 )
255252, 253, 254divrecd 9795 . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  Prime )
257 vmappw 20901 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  Prime  /\  k  e.  NN )  ->  (Λ `  ( p ^ k
) )  =  ( log `  p ) )
258256, 163, 257syl2anc 644 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  =  ( log `  p
) )
259161nncnd 10018 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  CC )
260161nnne0d 10046 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  =/=  0 )
261 elfzelz 11061 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  ZZ )
262261ad2antll 711 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  ZZ )
263259, 260, 262exprecd 11533 . . . . . . . . . . . . . . . . 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 6101 . . . . . . . . . . . . . . 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 631 . . . . . . . . . . . 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 )
26918a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
1  e.  RR )
270 vmage0 20906 . . . . . . . . . . . . . . . . 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 10017 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  RR )
273165nngt0d 10045 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <  ( p ^ k ) )
274 divge0 9881 . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  ( (Λ `  ( p ^ k
) )  /  (
p ^ k ) ) )
27683leidi 9563 . . . . . . . . . . . . . . . . . 18  |-  0  <_  0
277 simpr 449 . . . . . . . . . . . . . . . . . 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 4250 . . . . . . . . . . . . . . . . 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 712 . . . . . . . . . . . . . . . . . . 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 708 . . . . . . . . . . . . . . . . . . . . 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 21036 . . . . . . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . . . . . . . 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 21043 . . . . . . . . . . . . . . . . . 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 4250 . . . . . . . . . . . . . . . . 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 9545 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
0  <_  (  .1.  `  ( L `  (
p ^ k ) ) )  <->  ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  <_  1
) )
28718, 168, 286sylancr 646 . . . . . . . . . . . . . . . 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 203 . . . . . . . . . . . . . . 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 9952 . . . . . . . . . . . . . 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 9108 . . . . . . . . . . . . . . 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 4238 . . . . . . . . . . . . 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 631 . . . . . . . . . . . 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 12580 . . . . . . . . . . 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 9116 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  CC )
296161nnrecred 10047 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  /  p
)  e.  RR )
297296, 164reexpcld 11542 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  RR )
298297recnd 9116 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  CC )
299298anassrs 631 . . . . . . . . . . . . 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 12569 . . . . . . . . . . . 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 11182 . . . . . . . . . . . . . . . 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 12497 . . . . . . . . . . . . . 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 9116 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  CC )
305229nngt0d 10045 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <  p )
306 recgt1 9908 . . . . . . . . . . . . . . . . . 18  |-  ( ( p  e.  RR  /\  0  <  p )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
307235, 305, 306syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
308239, 307mpbid 203 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  <  1 )
309230, 308ltned 9211 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  =/=  1 )
310 1nn0 10239 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
311310a1i 11 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  e.  NN0 )
312 log1 20482 . . . . . . . . . . . . . . . . . . . . 21  |-  ( log `  1 )  =  0
313 simprr 735 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
314 1rp 10618 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR+
315 simprl 734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
316 logleb 20500 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR+  /\  x  e.  RR+ )  ->  (
1  <_  x  <->  ( log `  1 )  <_  ( log `  x ) ) )
317314, 315, 316sylancr 646 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  <_  x  <->  ( log `  1 )  <_  ( log `  x
) ) )
318313, 317mpbid 203 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  1
)  <_  ( log `  x ) )
319312, 318syl5eqbrr 4248 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( log `  x ) )
320319adantr 453 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( log `  x ) )
321234, 240, 320divge0d 10686 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( ( log `  x )  / 
( log `  p
) ) )
322 flge0nn0 11227 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( log `  x
)  /  ( log `  p ) )  e.  RR  /\  0  <_ 
( ( log `  x
)  /  ( log `  p ) ) )  ->  ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  e.  NN0 )
323241, 321, 322syl2anc 644 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  NN0 )
324 nn0p1nn 10261 . . . . . . . . . . . . . . . . 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 10523 . . . . . . . . . . . . . . . 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 12647 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\