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

Theorem rpvmasumlem 20652
Description: Lemma for rpvmasum 20691. 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 8844 . . . . . 6  |-  RR  e.  _V
2 rpssre 10380 . . . . . 6  |-  RR+  C_  RR
31, 2ssexi 4175 . . . . 5  |-  RR+  e.  _V
43a1i 10 . . . 4  |-  ( ph  -> 
RR+  e.  _V )
5 fzfid 11051 . . . . . . 7  |-  ( ph  ->  ( 1 ... ( |_ `  x ) )  e.  Fin )
6 elfznn 10835 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  NN )
76adantl 452 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
8 vmacl 20372 . . . . . . . . . 10  |-  ( n  e.  NN  ->  (Λ `  n )  e.  RR )
97, 8syl 15 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n
)  e.  RR )
109, 7nndivred 9810 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  RR )
1110recnd 8877 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n )  /  n
)  e.  CC )
125, 11fsumcl 12222 . . . . . 6  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( (Λ `  n )  /  n )  e.  CC )
1312adantr 451 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( (Λ `  n
)  /  n )  e.  CC )
14 relogcl 19948 . . . . . . 7  |-  ( x  e.  RR+  ->  ( log `  x )  e.  RR )
1514adantl 452 . . . . . 6  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  RR )
1615recnd 8877 . . . . 5  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( log `  x )  e.  CC )
1713, 16subcld 9173 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) )  e.  CC )
18 1re 8853 . . . . . . . . 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 2296 . . . . . . . . . . . 12  |-  ( Base `  Z )  =  (
Base `  Z )
23 rpvmasum.a . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN )
2419, 20, 21, 22, 23dchr1re 20518 . . . . . . . . . . 11  |-  ( ph  ->  .1.  : ( Base `  Z ) --> RR )
2524adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  : (
Base `  Z ) --> RR )
2623nnnn0d 10034 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  NN0 )
27 rpvmasum.l . . . . . . . . . . . . 13  |-  L  =  ( ZRHom `  Z
)
2820, 22, 27znzrhfo 16517 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  L : ZZ -onto-> ( Base `  Z
) )
29 fof 5467 . . . . . . . . . . . 12  |-  ( L : ZZ -onto-> ( Base `  Z )  ->  L : ZZ --> ( Base `  Z
) )
3026, 28, 293syl 18 . . . . . . . . . . 11  |-  ( ph  ->  L : ZZ --> ( Base `  Z ) )
31 elfzelz 10814 . . . . . . . . . . 11  |-  ( n  e.  ( 1 ... ( |_ `  x
) )  ->  n  e.  ZZ )
32 ffvelrn 5679 . . . . . . . . . . 11  |-  ( ( L : ZZ --> ( Base `  Z )  /\  n  e.  ZZ )  ->  ( L `  n )  e.  ( Base `  Z
) )
3330, 31, 32syl2an 463 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
34 ffvelrn 5679 . . . . . . . . . 10  |-  ( (  .1.  : ( Base `  Z ) --> RR  /\  ( L `  n )  e.  ( Base `  Z
) )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
3525, 33, 34syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  RR )
36 resubcl 9127 . . . . . . . . 9  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  e.  RR )
3718, 35, 36sylancr 644 . . . . . . . 8  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  RR )
3837, 10remulcld 8879 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
3938recnd 8877 . . . . . 6  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  (  .1.  `  ( L `  n
) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
405, 39fsumcl 12222 . . . . 5  |-  ( ph  -> 
sum_ n  e.  (
1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  CC )
4140adantr 451 . . . 4  |-  ( (
ph  /\  x  e.  RR+ )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
42 eqidd 2297 . . . 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
) ) ) )
43 eqidd 2297 . . . 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 ) ) ) )
444, 17, 41, 42, 43offval2 6111 . . 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 ) ) ) ) )
4513, 16, 41sub32d 9205 . . . . 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
) ) )
465, 11, 39fsumsub 12266 . . . . . . . 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 ) ) ) )
47 ax-1cn 8811 . . . . . . . . . . . 12  |-  1  e.  CC
4847a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  1  e.  CC )
4937recnd 8877 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
5048, 49, 11subdird 9252 . . . . . . . . . 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 ) ) ) )
5135recnd 8877 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n
) )  e.  CC )
52 nncan 9092 . . . . . . . . . . . 12  |-  ( ( 1  e.  CC  /\  (  .1.  `  ( L `  n ) )  e.  CC )  ->  (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  =  (  .1.  `  ( L `  n )
) )
5347, 51, 52sylancr 644 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  ( 1  -  (  .1.  `  ( L `  n )
) ) )  =  (  .1.  `  ( L `  n )
) )
5453oveq1d 5889 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
1  -  ( 1  -  (  .1.  `  ( L `  n ) ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( (  .1.  `  ( L `  n ) )  x.  ( (Λ `  n
)  /  n ) ) )
5511mulid2d 8869 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  x.  ( (Λ `  n
)  /  n ) )  =  ( (Λ `  n )  /  n
) )
5655oveq1d 5889 . . . . . . . . . 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 ) ) ) )
5750, 54, 563eqtr3rd 2337 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (
(Λ `  n )  /  n )  -  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )  =  ( (  .1.  `  ( L `  n )
)  x.  ( (Λ `  n )  /  n
) ) )
5857sumeq2dv 12192 . . . . . . . 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
) ) )
5946, 58eqtr3d 2330 . . . . . . 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
) ) )
6059oveq1d 5889 . . . . . 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 ) ) )
6160adantr 451 . . . . 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 ) ) )
6245, 61eqtrd 2328 . . . 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 ) ) )
6362mpteq2dva 4122 . . 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 ) ) ) )
6444, 63eqtrd 2328 . 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 ) ) ) )
65 vmadivsum 20647 . . 3  |-  ( x  e.  RR+  |->  ( sum_ n  e.  ( 1 ... ( |_ `  x
) ) ( (Λ `  n )  /  n
)  -  ( log `  x ) ) )  e.  O ( 1 )
662a1i 10 . . . 4  |-  ( ph  -> 
RR+  C_  RR )
6718a1i 10 . . . 4  |-  ( ph  ->  1  e.  RR )
68 prmdvdsfi 20361 . . . . . 6  |-  ( N  e.  NN  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
6923, 68syl 15 . . . . 5  |-  ( ph  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
70 ssrab2 3271 . . . . . . 7  |-  { q  e.  Prime  |  q  ||  N }  C_  Prime
7170sseli 3189 . . . . . 6  |-  ( p  e.  { q  e. 
Prime  |  q  ||  N }  ->  p  e. 
Prime )
72 prmnn 12777 . . . . . . . . . 10  |-  ( p  e.  Prime  ->  p  e.  NN )
7372adantl 452 . . . . . . . . 9  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  NN )
7473nnrpd 10405 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  RR+ )
7574relogcld 19990 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( log `  p )  e.  RR )
76 prmuz2 12792 . . . . . . . . 9  |-  ( p  e.  Prime  ->  p  e.  ( ZZ>= `  2 )
)
7776adantl 452 . . . . . . . 8  |-  ( (
ph  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= `  2 )
)
78 uz2m1nn 10308 . . . . . . . 8  |-  ( p  e.  ( ZZ>= `  2
)  ->  ( p  -  1 )  e.  NN )
7977, 78syl 15 . . . . . . 7  |-  ( (
ph  /\  p  e.  Prime )  ->  ( p  -  1 )  e.  NN )
8075, 79nndivred 9810 . . . . . 6  |-  ( (
ph  /\  p  e.  Prime )  ->  ( ( log `  p )  / 
( p  -  1 ) )  e.  RR )
8171, 80sylan2 460 . . . . 5  |-  ( (
ph  /\  p  e.  { q  e.  Prime  |  q 
||  N } )  ->  ( ( log `  p )  /  (
p  -  1 ) )  e.  RR )
8269, 81fsumrecl 12223 . . . 4  |-  ( ph  -> 
sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
83 fzfid 11051 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1 ... ( |_ `  x ) )  e.  Fin )
84 simpr 447 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  =  0 )
85 0re 8854 . . . . . . . . . . 11  |-  0  e.  RR
8684, 85syl6eqel 2384 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
87 eqid 2296 . . . . . . . . . . . 12  |-  (Unit `  Z )  =  (Unit `  Z )
8823ad3antrrr 710 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  N  e.  NN )
89 rpvmasum.d . . . . . . . . . . . . . 14  |-  D  =  ( Base `  G
)
9019dchrabl 20509 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  G  e.  Abel )
9123, 90syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  e.  Abel )
92 ablgrp 15110 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Abel  ->  G  e. 
Grp )
9389, 21grpidcl 14526 . . . . . . . . . . . . . . . 16  |-  ( G  e.  Grp  ->  .1.  e.  D )
9491, 92, 933syl 18 . . . . . . . . . . . . . . 15  |-  ( ph  ->  .1.  e.  D )
9594ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  .1.  e.  D
)
9633adantlr 695 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( L `  n )  e.  (
Base `  Z )
)
9719, 20, 89, 22, 87, 95, 96dchrn0 20505 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (  .1.  `  ( L `  n
) )  =/=  0  <->  ( L `  n )  e.  (Unit `  Z
) ) )
9897biimpa 470 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  ( L `  n )  e.  (Unit `  Z ) )
9919, 20, 21, 87, 88, 98dchr1 20512 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  =  1 )
10099, 18syl6eqel 2384 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
10186, 100pm2.61dane 2537 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n ) )  e.  RR )
10218, 101, 36sylancr 644 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 1  -  (  .1.  `  ( L `  n )
) )  e.  RR )
10310adantlr 695 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( (Λ `  n
)  /  n )  e.  RR )
104102, 103remulcld 8879 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  RR )
10583, 104fsumrecl 12223 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  e.  RR )
106 0le1 9313 . . . . . . . . . . 11  |-  0  <_  1
10784, 106syl6eqbr 4076 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =  0 )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
10818leidi 9323 . . . . . . . . . . 11  |-  1  <_  1
10999, 108syl6eqbr 4076 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  /\  (  .1.  `  ( L `  n ) )  =/=  0 )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
110107, 109pm2.61dane 2537 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (  .1.  `  ( L `  n ) )  <_  1 )
111 subge0 9303 . . . . . . . . . 10  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  n ) )  e.  RR )  ->  (
0  <_  ( 1  -  (  .1.  `  ( L `  n ) ) )  <->  (  .1.  `  ( L `  n
) )  <_  1
) )
11218, 101, 111sylancr 644 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( 0  <_ 
( 1  -  (  .1.  `  ( L `  n ) ) )  <-> 
(  .1.  `  ( L `  n )
)  <_  1 ) )
113110, 112mpbird 223 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
1  -  (  .1.  `  ( L `  n
) ) ) )
1149adantlr 695 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  (Λ `  n )  e.  RR )
1156adantl 452 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  NN )
116 vmage0 20375 . . . . . . . . . 10  |-  ( n  e.  NN  ->  0  <_  (Λ `  n )
)
117115, 116syl 15 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (Λ `  n ) )
118115nnred 9777 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  n  e.  RR )
119115nngt0d 9805 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <  n
)
120 divge0 9641 . . . . . . . . 9  |-  ( ( ( (Λ `  n
)  e.  RR  /\  0  <_  (Λ `  n )
)  /\  ( n  e.  RR  /\  0  < 
n ) )  -> 
0  <_  ( (Λ `  n )  /  n
) )
121114, 117, 118, 119, 120syl22anc 1183 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
(Λ `  n )  /  n ) )
122102, 103, 113, 121mulge0d 9365 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  0  <_  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) ) )
12383, 104, 122fsumge0 12269 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  sum_ n  e.  ( 1 ... ( |_ `  x ) ) ( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) ) )
124105, 123absidd 11921 . . . . 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 ) ) )
12569adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  Prime  |  q  ||  N }  e.  Fin )
126 inss2 3403 . . . . . . . . 9  |-  ( ( 0 [,] x )  i^i  Prime )  C_  Prime
127 rabss2 3269 . . . . . . . . 9  |-  ( ( ( 0 [,] x
)  i^i  Prime )  C_  Prime  ->  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N }  C_  { q  e. 
Prime  |  q  ||  N } )
128126, 127mp1i 11 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  C_ 
{ q  e.  Prime  |  q  ||  N }
)
129 ssfi 7099 . . . . . . . 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 )
130125, 128, 129syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  e.  Fin )
131 ssrab2 3271 . . . . . . . . . 10  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  (
( 0 [,] x
)  i^i  Prime )
132131, 126sstri 3201 . . . . . . . . 9  |-  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  q  ||  N }  C_  Prime
133132sseli 3189 . . . . . . . 8  |-  ( p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N }  ->  p  e.  Prime )
13480adantlr 695 . . . . . . . 8  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  p
)  /  ( p  -  1 ) )  e.  RR )
135133, 134sylan2 460 . . . . . . 7  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  { q  e.  ( ( 0 [,] x )  i^i  Prime )  |  q  ||  N } )  ->  (
( log `  p
)  /  ( p  -  1 ) )  e.  RR )
136130, 135fsumrecl 12223 . . . . . 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 )
13782adantr 451 . . . . . 6  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  sum_ p  e.  { q  e.  Prime  |  q  ||  N }  ( ( log `  p )  /  ( p  - 
1 ) )  e.  RR )
138 fveq2 5541 . . . . . . . . . . . 12  |-  ( n  =  ( p ^
k )  ->  ( L `  n )  =  ( L `  ( p ^ k
) ) )
139138fveq2d 5545 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (  .1.  `  ( L `  n ) )  =  (  .1.  `  ( L `  ( p ^ k ) ) ) )
140139oveq2d 5890 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
1  -  (  .1.  `  ( L `  n
) ) )  =  ( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) ) )
141 fveq2 5541 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  (Λ `  n )  =  (Λ `  ( p ^ k
) ) )
142 id 19 . . . . . . . . . . 11  |-  ( n  =  ( p ^
k )  ->  n  =  ( p ^
k ) )
143141, 142oveq12d 5892 . . . . . . . . . 10  |-  ( n  =  ( p ^
k )  ->  (
(Λ `  n )  /  n )  =  ( (Λ `  ( p ^ k ) )  /  ( p ^
k ) ) )
144140, 143oveq12d 5892 . . . . . . . . 9  |-  ( n  =  ( p ^
k )  ->  (
( 1  -  (  .1.  `  ( L `  n ) ) )  x.  ( (Λ `  n
)  /  n ) )  =  ( ( 1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  x.  ( (Λ `  (
p ^ k ) )  /  ( p ^ k ) ) ) )
145 rpre 10376 . . . . . . . . . 10  |-  ( x  e.  RR+  ->  x  e.  RR )
146145ad2antrl 708 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR )
14739adantlr 695 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  n  e.  ( 1 ... ( |_ `  x ) ) )  ->  ( ( 1  -  (  .1.  `  ( L `  n ) ) )  x.  (
(Λ `  n )  /  n ) )  e.  CC )
148 simprr 733 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
(Λ `  n )  =  0 )
149148oveq1d 5889 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( (Λ `  n )  /  n )  =  ( 0  /  n ) )
1506ad2antrl 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  NN )
151150nncnd 9778 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  e.  CC )
152150nnne0d 9806 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  ->  n  =/=  0 )
153151, 152div0d 9551 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( 0  /  n
)  =  0 )
154149, 153eqtrd 2328 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( (Λ `  n )  /  n )  =  0 )
155154oveq2d 5890 . . . . . . . . . 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 ) )
15649ad2ant2r 727 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( 1  -  (  .1.  `  ( L `  n ) ) )  e.  CC )
157156mul01d 9027 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  0 )  =  0 )
158155, 157eqtrd 2328 . . . . . . . . 9  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( n  e.  (
1 ... ( |_ `  x ) )  /\  (Λ `  n )  =  0 ) )  -> 
( ( 1  -  (  .1.  `  ( L `  n )
) )  x.  (
(Λ `  n )  /  n ) )  =  0 )
159144, 146, 147, 158fsumvma2 20469 . . . . . . . 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 ) ) ) )
160131a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }  C_  ( ( 0 [,] x )  i^i  Prime ) )
161 fzfid 11051 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  e.  Fin )
16224ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  .1.  : ( Base `  Z
) --> RR )
16330ad2antrr 706 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  L : ZZ --> ( Base `  Z ) )
16472ad2antrl 708 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  NN )
165 elfznn 10835 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  NN )
166165ad2antll 709 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN )
167166nnnn0d 10034 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  NN0 )
168164, 167nnexpcld 11282 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  NN )
169168nnzd 10132 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  ZZ )
170 ffvelrn 5679 . . . . . . . . . . . . . . . . 17  |-  ( ( L : ZZ --> ( Base `  Z )  /\  (
p ^ k )  e.  ZZ )  -> 
( L `  (
p ^ k ) )  e.  ( Base `  Z ) )
171163, 169, 170syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( L `  (
p ^ k ) )  e.  ( Base `  Z ) )
172 ffvelrn 5679 . . . . . . . . . . . . . . . 16  |-  ( (  .1.  : ( Base `  Z ) --> RR  /\  ( L `  ( p ^ k ) )  e.  ( Base `  Z
) )  ->  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )
173162, 171, 172syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(  .1.  `  ( L `  ( p ^ k ) ) )  e.  RR )
174 resubcl 9127 . . . . . . . . . . . . . . 15  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
1  -  (  .1.  `  ( L `  (
p ^ k ) ) ) )  e.  RR )
17518, 173, 174sylancr 644 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  e.  RR )
176 vmacl 20372 . . . . . . . . . . . . . . . 16  |-  ( ( p ^ k )  e.  NN  ->  (Λ `  ( p ^ k
) )  e.  RR )
177168, 176syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  e.  RR )
178177, 168nndivred 9810 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  RR )
179175, 178remulcld 8879 . . . . . . . . . . . . 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 )
180179anassrs 629 . . . . . . . . . . . 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 )
181180recnd 8877 . . . . . . . . . . 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 )
182161, 181fsumcl 12222 . . . . . . . . . 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 )
183133, 182sylan2 460 . . . . . . . . 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 )
184 breq1 4042 . . . . . . . . . . . 12  |-  ( q  =  p  ->  (
q  ||  N  <->  p  ||  N
) )
185184notbid 285 . . . . . . . . . . 11  |-  ( q  =  p  ->  ( -.  q  ||  N  <->  -.  p  ||  N ) )
186 notrab 3458 . . . . . . . . . . 11  |-  ( ( ( 0 [,] x
)  i^i  Prime )  \  { q  e.  ( ( 0 [,] x
)  i^i  Prime )  |  q  ||  N }
)  =  { q  e.  ( ( 0 [,] x )  i^i 
Prime )  |  -.  q  ||  N }
187185, 186elrab2 2938 . . . . . . . . . 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 ) )
188126sseli 3189 . . . . . . . . . . 11  |-  ( p  e.  ( ( 0 [,] x )  i^i 
Prime )  ->  p  e. 
Prime )
18923ad3antrrr 710 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN )
190 simplrr 737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  -.  p  ||  N )
191 simplrl 736 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  p  e.  Prime )
192189nnzd 10132 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  ZZ )
193 coprm 12795 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( p  e.  Prime  /\  N  e.  ZZ )  ->  ( -.  p  ||  N  <->  ( p  gcd  N )  =  1 ) )
194191, 192, 193syl2anc 642 . . . . . . . . . . . . . . . . . . . . 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 ) )
195190, 194mpbid 201 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( p  gcd  N
)  =  1 )
196 prmz 12778 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  e.  Prime  ->  p  e.  ZZ )
197191, 196syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  p  e.  ZZ )
198165adantl 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN )
199198nnnn0d 10034 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
k  e.  NN0 )
200 rpexp1i 12816 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( p  e.  ZZ  /\  N  e.  ZZ  /\  k  e.  NN0 )  ->  (
( p  gcd  N
)  =  1  -> 
( ( p ^
k )  gcd  N
)  =  1 ) )
201197, 192, 199, 200syl3anc 1182 . . . . . . . . . . . . . . . . . . . 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 ) )
202195, 201mpd 14 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( ( p ^
k )  gcd  N
)  =  1 )
203189nnnn0d 10034 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  ->  N  e.  NN0 )
204169anassrs 629 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
p ^ k )  e.  ZZ )
205204adantlrr 701 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
( p ^ k
)  e.  ZZ )
20620, 87, 27znunit 16533 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  e.  NN0  /\  ( p ^ k
)  e.  ZZ )  ->  ( ( L `
 ( p ^
k ) )  e.  (Unit `  Z )  <->  ( ( p ^ k
)  gcd  N )  =  1 ) )
207203, 205, 206syl2anc 642 . . . . . . . . . . . . . . . . . . 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 ) )
208202, 207mpbird 223 . . . . . . . . . . . . . . . . . 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 ) )
20919, 20, 21, 87, 189, 208dchr1 20512 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) )  -> 
(  .1.  `  ( L `  ( p ^ k ) ) )  =  1 )
210209oveq2d 5890 . . . . . . . . . . . . . . . 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 ) )
211 1m1e0 9830 . . . . . . . . . . . . . . . 16  |-  ( 1  -  1 )  =  0
212210, 211syl6eq 2344 . . . . . . . . . . . . . . 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 )
213212oveq1d 5889 . . . . . . . . . . . . . 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
) ) ) )
214178recnd 8877 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( (Λ `  ( p ^ k ) )  /  ( p ^
k ) )  e.  CC )
215214anassrs 629 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
(Λ `  ( p ^
k ) )  / 
( p ^ k
) )  e.  CC )
216215adantlrr 701 . . . . . . . . . . . . . . 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 )
217216mul02d 9026 . . . . . . . . . . . . . 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 )
218213, 217eqtrd 2328 . . . . . . . . . . . . 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 )
219218sumeq2dv 12192 . . . . . . . . . . . 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 )
220 fzfid 11051 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  (
1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) )  e.  Fin )
221220olcd 382 . . . . . . . . . . . . 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 ) )
222 sumz 12211 . . . . . . . . . . . . 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 )
223221, 222syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\ 
-.  p  ||  N
) )  ->  sum_ k  e.  ( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) ) 0  =  0 )
224219, 223eqtrd 2328 . . . . . . . . . . 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 )
225188, 224sylanr1 633 . . . . . . . . . 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 )
226187, 225sylan2b 461 . . . . . . . . 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 )
227 ppifi 20359 . . . . . . . . . 10  |-  ( x  e.  RR  ->  (
( 0 [,] x
)  i^i  Prime )  e. 
Fin )
228146, 227syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( ( 0 [,] x )  i^i  Prime )  e.  Fin )
229160, 183, 226, 228fsumss 12214 . . . . . . . 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 ) ) ) )
230159, 229eqtr4d 2331 . . . . . . 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
) ) ) )
231161, 180fsumrecl 12223 . . . . . . . . 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 )
232133, 231sylan2 460 . . . . . . . 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 )
23375adantlr 695 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR )
23472adantl 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  NN )
235234nnrecred 9807 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR )
236234nnrpd 10405 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR+ )
237236rpreccld 10416 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  RR+ )
238 simplrl 736 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  x  e.  RR+ )
239238relogcld 19990 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  x
)  e.  RR )
240234nnred 9777 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  RR )
24176adantl 452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  ->  p  e.  ( ZZ>= ` 
2 ) )
242 eluz2b2 10306 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ( ZZ>= `  2
)  <->  ( p  e.  NN  /\  1  < 
p ) )
243242simprbi 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( p  e.  ( ZZ>= `  2
)  ->  1  <  p )
244241, 243syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  <  p )
245240, 244rplogcld 19996 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  RR+ )
246239, 245rerpdivcld 10433 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( log `  x
)  /  ( log `  p ) )  e.  RR )
247246flcld 10946 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  ZZ )
248247peano2zd 10136 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 )  e.  ZZ )
249237, 248rpexpcld 11284 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR+ )
250249rpred 10406 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) )  e.  RR )
251235, 250resubcld 9227 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( 1  /  p )  -  (
( 1  /  p
) ^ ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  +  1 ) ) )  e.  RR )
252241, 78syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( p  -  1 )  e.  NN )
253252nnrpd 10405 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( p  -  1 )  e.  RR+ )
254253, 236rpdivcld 10423 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( p  - 
1 )  /  p
)  e.  RR+ )
255251, 254rerpdivcld 10433 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( ( ( 1  /  p )  -  ( ( 1  /  p ) ^ (
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  +  1 ) ) )  /  ( ( p  -  1 )  /  p ) )  e.  RR )
256233, 255remulcld 8879 . . . . . . . . . 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 )
257177recnd 8877 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  e.  CC )
258168nncnd 9778 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  CC )
259168nnne0d 9806 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  =/=  0 )
260257, 258, 259divrecd 9555 . . . . . . . . . . . . . . 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 ) ) ) )
261 simprl 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  Prime )
262 vmappw 20370 . . . . . . . . . . . . . . . . 17  |-  ( ( p  e.  Prime  /\  k  e.  NN )  ->  (Λ `  ( p ^ k
) )  =  ( log `  p ) )
263261, 166, 262syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
(Λ `  ( p ^
k ) )  =  ( log `  p
) )
264164nncnd 9778 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  e.  CC )
265164nnne0d 9806 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  p  =/=  0 )
266 elfzelz 10814 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( 1 ... ( |_ `  (
( log `  x
)  /  ( log `  p ) ) ) )  ->  k  e.  ZZ )
267266ad2antll 709 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
k  e.  ZZ )
268264, 265, 267exprecd 11269 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  =  ( 1  /  ( p ^
k ) ) )
269268eqcomd 2301 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  /  (
p ^ k ) )  =  ( ( 1  /  p ) ^ k ) )
270263, 269oveq12d 5892 . . . . . . . . . . . . . . 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 ) ) )
271260, 270eqtrd 2328 . . . . . . . . . . . . . 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 ) ) )
272271, 178eqeltrrd 2371 . . . . . . . . . . . . 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 )
273272anassrs 629 . . . . . . . . . . . 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 )
27418a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
1  e.  RR )
275 vmage0 20375 . . . . . . . . . . . . . . . . 17  |-  ( ( p ^ k )  e.  NN  ->  0  <_  (Λ `  ( p ^ k ) ) )
276168, 275syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  (Λ `  (
p ^ k ) ) )
277168nnred 9777 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( p ^ k
)  e.  RR )
278168nngt0d 9805 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <  ( p ^ k ) )
279 divge0 9641 . . . . . . . . . . . . . . . 16  |-  ( ( ( (Λ `  (
p ^ k ) )  e.  RR  /\  0  <_  (Λ `  ( p ^ k ) ) )  /\  ( ( p ^ k )  e.  RR  /\  0  <  ( p ^ k
) ) )  -> 
0  <_  ( (Λ `  ( p ^ k
) )  /  (
p ^ k ) ) )
280177, 276, 277, 278, 279syl22anc 1183 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  ( (Λ `  ( p ^ k
) )  /  (
p ^ k ) ) )
28185leidi 9323 . . . . . . . . . . . . . . . . . 18  |-  0  <_  0
282 simpr 447 . . . . . . . . . . . . . . . . . 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 )
283281, 282syl5breqr 4075 . . . . . . . . . . . . . . . . 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 ) ) ) )
28423ad3antrrr 710 . . . . . . . . . . . . . . . . . . 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 )
28594ad2antrr 706 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  ->  .1.  e.  D )
28619, 20, 89, 22, 87, 285, 171dchrn0 20505 . . . . . . . . . . . . . . . . . . . 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
) ) )
287286biimpa 470 . . . . . . . . . . . . . . . . . . 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
) )
28819, 20, 21, 87, 284, 287dchr1 20512 . . . . . . . . . . . . . . . . . 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 )
289106, 288syl5breqr 4075 . . . . . . . . . . . . . . . . 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 ) ) ) )
290283, 289pm2.61dane 2537 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
0  <_  (  .1.  `  ( L `  (
p ^ k ) ) ) )
291 subge02 9305 . . . . . . . . . . . . . . . . 17  |-  ( ( 1  e.  RR  /\  (  .1.  `  ( L `  ( p ^ k
) ) )  e.  RR )  ->  (
0  <_  (  .1.  `  ( L `  (
p ^ k ) ) )  <->  ( 1  -  (  .1.  `  ( L `  ( p ^ k ) ) ) )  <_  1
) )
29218, 173, 291sylancr 644 . . . . . . . . . . . . . . . 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
) )
293290, 292mpbid 201 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  -  (  .1.  `  ( L `  ( p ^ k
) ) ) )  <_  1 )
294175, 274, 178, 280, 293lemul1ad 9712 . . . . . . . . . . . . . 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
) ) ) )
295214mulid2d 8869 . . . . . . . . . . . . . . 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 ) ) )
296295, 271eqtrd 2328 . . . . . . . . . . . . . 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 ) ) )
297294, 296breqtrd 4063 . . . . . . . . . . . . 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 ) ) )
298297anassrs 629 . . . . . . . . . . . 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
) ) )
299161, 180, 273, 298fsumle 12273 . . . . . . . . . . 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 ) ) )
300233recnd 8877 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( log `  p
)  e.  CC )
301164nnrecred 9807 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( 1  /  p
)  e.  RR )
302301, 167reexpcld 11278 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  RR )
303302recnd 8877 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  ( p  e.  Prime  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) ) )  -> 
( ( 1  /  p ) ^ k
)  e.  CC )
304303anassrs 629 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  /\  k  e.  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) ) )  ->  (
( 1  /  p
) ^ k )  e.  CC )
305161, 300, 304fsummulc2 12262 . . . . . . . . . . . 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 ) ) )
306 fzval3 10927 . . . . . . . . . . . . . . . 16  |-  ( ( |_ `  ( ( log `  x )  /  ( log `  p
) ) )  e.  ZZ  ->  ( 1 ... ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) ) )  =  ( 1..^ ( ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  +  1 ) ) )
307247, 306syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1 ... ( |_ `  ( ( log `  x )  /  ( log `  p ) ) ) )  =  ( 1..^ ( ( |_
`  ( ( log `  x )  /  ( log `  p ) ) )  +  1 ) ) )
308307sumeq1d 12190 . . . . . . . . . . . . . 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
) )
309235recnd 8877 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  e.  CC )
310234nngt0d 9805 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <  p )
311 recgt1 9668 . . . . . . . . . . . . . . . . . 18  |-  ( ( p  e.  RR  /\  0  <  p )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
312240, 310, 311syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  <  p  <->  ( 1  /  p )  <  1 ) )
313244, 312mpbid 201 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  <  1 )
314235, 313ltned 8971 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( 1  /  p
)  =/=  1 )
315 1nn0 9997 . . . . . . . . . . . . . . . 16  |-  1  e.  NN0
316315a1i 10 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
1  e.  NN0 )
317 log1 19955 . . . . . . . . . . . . . . . . . . . . 21  |-  ( log `  1 )  =  0
318 simprr 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
1  <_  x )
319 1rp 10374 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  RR+
320 simprl 732 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  ->  x  e.  RR+ )
321 logleb 19973 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1  e.  RR+  /\  x  e.  RR+ )  ->  (
1  <_  x  <->  ( log `  1 )  <_  ( log `  x ) ) )
322319, 320, 321sylancr 644 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( 1  <_  x  <->  ( log `  1 )  <_  ( log `  x
) ) )
323318, 322mpbid 201 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
( log `  1
)  <_  ( log `  x ) )
324317, 323syl5eqbrr 4073 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( x  e.  RR+  /\  1  <_  x ) )  -> 
0  <_  ( log `  x ) )
325324adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( log `  x ) )
326239, 245, 325divge0d 10442 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
0  <_  ( ( log `  x )  / 
( log `  p
) ) )
327 flge0nn0 10964 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( log `  x
)  /  ( log `  p ) )  e.  RR  /\  0  <_ 
( ( log `  x
)  /  ( log `  p ) ) )  ->  ( |_ `  ( ( log `  x
)  /  ( log `  p ) ) )  e.  NN0 )
328246, 326, 327syl2anc 642 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
x  e.  RR+  /\  1  <_  x ) )  /\  p  e.  Prime )  -> 
( |_ `  (
( log `  x
)  /  ( log `  p ) ) )  e.  NN0