Metamath Proof Explorer

Theorem rpvmasumlem

Description: Lemma for rpvmasum . Calculate the "trivial case" estimate sum_ n <_ x ( .1. ( n ) Lam ( 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)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` 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 rpvmasumlem 
|- ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum.g 
 |-  G = ( DChr ` N )
5 rpvmasum.d 
 |-  D = ( Base ` G )
6 rpvmasum.1 
 |-  .1. = ( 0g ` G )
7 reex 
 |-  RR e. _V
8 rpssre 
 |-  RR+ C_ RR
9 7 8 ssexi 
 |-  RR+ e. _V
10 9 a1i 
 |-  ( ph -> RR+ e. _V )
11 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` x ) ) e. Fin )
12 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
13 12 adantl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
14 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
15 13 14 syl 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
16 15 13 nndivred 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
17 16 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
18 11 17 fsumcl 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
19 18 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) e. CC )
20 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
21 20 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
22 21 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
23 19 22 subcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) e. CC )
24 1re 
 |-  1 e. RR
25 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
26 4 1 6 25 3 dchr1re 
 |-  ( ph -> .1. : ( Base ` Z ) --> RR )
27 26 adantr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> .1. : ( Base ` Z ) --> RR )
28 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
29 1 25 2 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
30 fof 
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
31 28 29 30 3syl 
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
32 elfzelz 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
33 ffvelrn 
 |-  ( ( L : ZZ --> ( Base ` Z ) /\ n e. ZZ ) -> ( L ` n ) e. ( Base ` Z ) )
34 31 32 33 syl2an 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
35 27 34 ffvelrnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( .1. ` ( L ` n ) ) e. RR )
36 resubcl 
 |-  ( ( 1 e. RR /\ ( .1. ` ( L ` n ) ) e. RR ) -> ( 1 - ( .1. ` ( L ` n ) ) ) e. RR )
37 24 35 36 sylancr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 - ( .1. ` ( L ` n ) ) ) e. RR )
38 37 16 remulcld 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) e. RR )
39 38 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
40 11 39 fsumcl 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
41 40 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
42 eqidd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) )
43 eqidd 
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) )
44 10 23 41 42 43 offval2 
 |-  ( ph -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) ) )
45 19 22 41 sub32d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) - ( log ` x ) ) )
46 11 17 39 fsumsub 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) - ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) )
47 1cnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. CC )
48 37 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 - ( .1. ` ( L ` n ) ) ) e. CC )
49 47 48 17 subdird 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 - ( 1 - ( .1. ` ( L ` n ) ) ) ) x. ( ( Lam ` n ) / n ) ) = ( ( 1 x. ( ( Lam ` n ) / n ) ) - ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) )
50 ax-1cn 
 |-  1 e. CC
51 35 recnd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( .1. ` ( L ` n ) ) e. CC )
52 nncan 
 |-  ( ( 1 e. CC /\ ( .1. ` ( L ` n ) ) e. CC ) -> ( 1 - ( 1 - ( .1. ` ( L ` n ) ) ) ) = ( .1. ` ( L ` n ) ) )
53 50 51 52 sylancr 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 - ( 1 - ( .1. ` ( L ` n ) ) ) ) = ( .1. ` ( L ` n ) ) )
54 53 oveq1d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 - ( 1 - ( .1. ` ( L ` n ) ) ) ) x. ( ( Lam ` n ) / n ) ) = ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
55 17 mulid2d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( ( Lam ` n ) / n ) ) = ( ( Lam ` n ) / n ) )
56 55 oveq1d 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. ( ( Lam ` n ) / n ) ) - ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = ( ( ( Lam ` n ) / n ) - ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) )
57 49 54 56 3eqtr3rd 
 |-  ( ( ph /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` n ) / n ) - ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
58 57 sumeq2dv 
 |-  ( ph -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) - ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
59 46 58 eqtr3d 
 |-  ( ph -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
60 59 oveq1d 
 |-  ( ph -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) - ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) )
61 60 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) - ( log ` x ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) )
62 45 61 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) )
63 62 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) - sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) )
64 44 63 eqtrd 
 |-  ( ph -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) )
65 vmadivsum 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1)
66 8 a1i 
 |-  ( ph -> RR+ C_ RR )
67 1red 
 |-  ( ph -> 1 e. RR )
68 prmdvdsfi 
 |-  ( N e. NN -> { q e. Prime | q || N } e. Fin )
69 3 68 syl 
 |-  ( ph -> { q e. Prime | q || N } e. Fin )
70 elrabi 
 |-  ( p e. { q e. Prime | q || N } -> p e. Prime )
71 prmnn 
 |-  ( p e. Prime -> p e. NN )
72 71 adantl 
 |-  ( ( ph /\ p e. Prime ) -> p e. NN )
73 72 nnrpd 
 |-  ( ( ph /\ p e. Prime ) -> p e. RR+ )
74 73 relogcld 
 |-  ( ( ph /\ p e. Prime ) -> ( log ` p ) e. RR )
75 prmuz2 
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
76 75 adantl 
 |-  ( ( ph /\ p e. Prime ) -> p e. ( ZZ>= ` 2 ) )
77 uz2m1nn 
 |-  ( p e. ( ZZ>= ` 2 ) -> ( p - 1 ) e. NN )
78 76 77 syl 
 |-  ( ( ph /\ p e. Prime ) -> ( p - 1 ) e. NN )
79 74 78 nndivred 
 |-  ( ( ph /\ p e. Prime ) -> ( ( log ` p ) / ( p - 1 ) ) e. RR )
80 70 79 sylan2 
 |-  ( ( ph /\ p e. { q e. Prime | q || N } ) -> ( ( log ` p ) / ( p - 1 ) ) e. RR )
81 69 80 fsumrecl 
 |-  ( ph -> sum_ p e. { q e. Prime | q || N } ( ( log ` p ) / ( p - 1 ) ) e. RR )
82 fzfid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
83 simpr 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) = 0 ) -> ( .1. ` ( L ` n ) ) = 0 )
84 0re 
 |-  0 e. RR
85 83 84 eqeltrdi 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) = 0 ) -> ( .1. ` ( L ` n ) ) e. RR )
86 eqid 
 |-  ( Unit ` Z ) = ( Unit ` Z )
87 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) =/= 0 ) -> N e. NN )
88 4 dchrabl 
 |-  ( N e. NN -> G e. Abel )
89 ablgrp 
 |-  ( G e. Abel -> G e. Grp )
90 5 6 grpidcl 
 |-  ( G e. Grp -> .1. e. D )
91 3 88 89 90 4syl 
 |-  ( ph -> .1. e. D )
92 91 ad2antrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> .1. e. D )
93 34 adantlr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` n ) e. ( Base ` Z ) )
94 4 1 5 25 86 92 93 dchrn0 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( .1. ` ( L ` n ) ) =/= 0 <-> ( L ` n ) e. ( Unit ` Z ) ) )
95 94 biimpa 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) =/= 0 ) -> ( L ` n ) e. ( Unit ` Z ) )
96 4 1 6 86 87 95 dchr1 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) =/= 0 ) -> ( .1. ` ( L ` n ) ) = 1 )
97 96 24 eqeltrdi 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) =/= 0 ) -> ( .1. ` ( L ` n ) ) e. RR )
98 85 97 pm2.61dane 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( .1. ` ( L ` n ) ) e. RR )
99 24 98 36 sylancr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 - ( .1. ` ( L ` n ) ) ) e. RR )
100 16 adantlr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
101 99 100 remulcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) e. RR )
102 82 101 fsumrecl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) e. RR )
103 0le1 
 |-  0 <_ 1
104 83 103 eqbrtrdi 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) = 0 ) -> ( .1. ` ( L ` n ) ) <_ 1 )
105 24 leidi 
 |-  1 <_ 1
106 96 105 eqbrtrdi 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ ( .1. ` ( L ` n ) ) =/= 0 ) -> ( .1. ` ( L ` n ) ) <_ 1 )
107 104 106 pm2.61dane 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( .1. ` ( L ` n ) ) <_ 1 )
108 subge0 
 |-  ( ( 1 e. RR /\ ( .1. ` ( L ` n ) ) e. RR ) -> ( 0 <_ ( 1 - ( .1. ` ( L ` n ) ) ) <-> ( .1. ` ( L ` n ) ) <_ 1 ) )
109 24 98 108 sylancr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 0 <_ ( 1 - ( .1. ` ( L ` n ) ) ) <-> ( .1. ` ( L ` n ) ) <_ 1 ) )
110 107 109 mpbird 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( 1 - ( .1. ` ( L ` n ) ) ) )
111 15 adantlr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
112 12 adantl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
113 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
114 112 113 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
115 112 nnred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
116 112 nngt0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 < n )
117 divge0 
 |-  ( ( ( ( Lam ` n ) e. RR /\ 0 <_ ( Lam ` n ) ) /\ ( n e. RR /\ 0 < n ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
118 111 114 115 116 117 syl22anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) / n ) )
119 99 100 110 118 mulge0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) )
120 82 101 119 fsumge0 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) )
121 102 120 absidd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) )
122 69 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> { q e. Prime | q || N } e. Fin )
123 inss2 
 |-  ( ( 0 [,] x ) i^i Prime ) C_ Prime
124 rabss2 
 |-  ( ( ( 0 [,] x ) i^i Prime ) C_ Prime -> { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } C_ { q e. Prime | q || N } )
125 123 124 mp1i 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } C_ { q e. Prime | q || N } )
126 122 125 ssfid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } e. Fin )
127 ssrab2 
 |-  { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } C_ ( ( 0 [,] x ) i^i Prime )
128 127 123 sstri 
 |-  { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } C_ Prime
129 128 sseli 
 |-  ( p e. { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } -> p e. Prime )
130 79 adantlr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( log ` p ) / ( p - 1 ) ) e. RR )
131 129 130 sylan2 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } ) -> ( ( log ` p ) / ( p - 1 ) ) e. RR )
132 126 131 fsumrecl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ p e. { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } ( ( log ` p ) / ( p - 1 ) ) e. RR )
133 81 adantr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ p e. { q e. Prime | q || N } ( ( log ` p ) / ( p - 1 ) ) e. RR )
134 2fveq3 
 |-  ( n = ( p ^ k ) -> ( .1. ` ( L ` n ) ) = ( .1. ` ( L ` ( p ^ k ) ) ) )
135 134 oveq2d 
 |-  ( n = ( p ^ k ) -> ( 1 - ( .1. ` ( L ` n ) ) ) = ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) )
136 fveq2 
 |-  ( n = ( p ^ k ) -> ( Lam ` n ) = ( Lam ` ( p ^ k ) ) )
137 id 
 |-  ( n = ( p ^ k ) -> n = ( p ^ k ) )
138 136 137 oveq12d 
 |-  ( n = ( p ^ k ) -> ( ( Lam ` n ) / n ) = ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) )
139 135 138 oveq12d 
 |-  ( n = ( p ^ k ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) = ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) )
140 rpre 
 |-  ( x e. RR+ -> x e. RR )
141 140 ad2antrl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
142 39 adantlr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
143 simprr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( Lam ` n ) = 0 )
144 143 oveq1d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( ( Lam ` n ) / n ) = ( 0 / n ) )
145 12 ad2antrl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> n e. NN )
146 145 nncnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> n e. CC )
147 145 nnne0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> n =/= 0 )
148 146 147 div0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( 0 / n ) = 0 )
149 144 148 eqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( ( Lam ` n ) / n ) = 0 )
150 149 oveq2d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) = ( ( 1 - ( .1. ` ( L ` n ) ) ) x. 0 ) )
151 48 ad2ant2r 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( 1 - ( .1. ` ( L ` n ) ) ) e. CC )
152 151 mul01d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. 0 ) = 0 )
153 150 152 eqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ ( Lam ` n ) = 0 ) ) -> ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) = 0 )
154 139 141 142 153 fsumvma2 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) = sum_ p e. ( ( 0 [,] x ) i^i Prime ) sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) )
155 127 a1i 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } C_ ( ( 0 [,] x ) i^i Prime ) )
156 fzfid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) e. Fin )
157 26 ad2antrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> .1. : ( Base ` Z ) --> RR )
158 31 ad2antrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> L : ZZ --> ( Base ` Z ) )
159 71 ad2antrl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> p e. NN )
160 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) -> k e. NN )
161 160 ad2antll 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> k e. NN )
162 161 nnnn0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> k e. NN0 )
163 159 162 nnexpcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( p ^ k ) e. NN )
164 163 nnzd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( p ^ k ) e. ZZ )
165 158 164 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( L ` ( p ^ k ) ) e. ( Base ` Z ) )
166 157 165 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( .1. ` ( L ` ( p ^ k ) ) ) e. RR )
167 resubcl 
 |-  ( ( 1 e. RR /\ ( .1. ` ( L ` ( p ^ k ) ) ) e. RR ) -> ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) e. RR )
168 24 166 167 sylancr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) e. RR )
169 vmacl 
 |-  ( ( p ^ k ) e. NN -> ( Lam ` ( p ^ k ) ) e. RR )
170 163 169 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( Lam ` ( p ^ k ) ) e. RR )
171 170 163 nndivred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) e. RR )
172 168 171 remulcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) e. RR )
173 172 anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) e. RR )
174 173 recnd 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) e. CC )
175 156 174 fsumcl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) e. CC )
176 129 175 sylan2 
 |-  ( ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) e. CC )
177 breq1 
 |-  ( q = p -> ( q || N <-> p || N ) )
178 177 notbid 
 |-  ( q = p -> ( -. q || N <-> -. p || N ) )
179 notrab 
 |-  ( ( ( 0 [,] x ) i^i Prime ) \ { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } ) = { q e. ( ( 0 [,] x ) i^i Prime ) | -. q || N }
180 178 179 elrab2 
 |-  ( 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 ) )
181 123 sseli 
 |-  ( p e. ( ( 0 [,] x ) i^i Prime ) -> p e. Prime )
182 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> N e. NN )
183 simplrr 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> -. p || N )
184 simplrl 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> p e. Prime )
185 182 nnzd 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> N e. ZZ )
186 coprm 
 |-  ( ( p e. Prime /\ N e. ZZ ) -> ( -. p || N <-> ( p gcd N ) = 1 ) )
187 184 185 186 syl2anc 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( -. p || N <-> ( p gcd N ) = 1 ) )
188 183 187 mpbid 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( p gcd N ) = 1 )
189 prmz 
 |-  ( p e. Prime -> p e. ZZ )
190 184 189 syl 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> p e. ZZ )
191 160 adantl 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> k e. NN )
192 191 nnnn0d 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> k e. NN0 )
193 rpexp1i 
 |-  ( ( p e. ZZ /\ N e. ZZ /\ k e. NN0 ) -> ( ( p gcd N ) = 1 -> ( ( p ^ k ) gcd N ) = 1 ) )
194 190 185 192 193 syl3anc 
 |-  ( ( ( ( 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 ) )
195 188 194 mpd 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( p ^ k ) gcd N ) = 1 )
196 182 nnnn0d 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> N e. NN0 )
197 164 anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( p ^ k ) e. ZZ )
198 197 adantlrr 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( p ^ k ) e. ZZ )
199 1 86 2 znunit 
 |-  ( ( N e. NN0 /\ ( p ^ k ) e. ZZ ) -> ( ( L ` ( p ^ k ) ) e. ( Unit ` Z ) <-> ( ( p ^ k ) gcd N ) = 1 ) )
200 196 198 199 syl2anc 
 |-  ( ( ( ( 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 ) )
201 195 200 mpbird 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( L ` ( p ^ k ) ) e. ( Unit ` Z ) )
202 4 1 6 86 182 201 dchr1 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( .1. ` ( L ` ( p ^ k ) ) ) = 1 )
203 202 oveq2d 
 |-  ( ( ( ( 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 ) )
204 1m1e0 
 |-  ( 1 - 1 ) = 0
205 203 204 eqtrdi 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) = 0 )
206 205 oveq1d 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = ( 0 x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) )
207 171 recnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) e. CC )
208 207 anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) e. CC )
209 208 adantlrr 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) e. CC )
210 209 mul02d 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( 0 x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = 0 )
211 206 210 eqtrd 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = 0 )
212 211 sumeq2dv 
 |-  ( ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) 0 )
213 fzfid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) -> ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) e. Fin )
214 213 olcd 
 |-  ( ( ( 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 ) )
215 sumz 
 |-  ( ( ( 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 )
216 214 215 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ -. p || N ) ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) 0 = 0 )
217 212 216 eqtrd 
 |-  ( ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = 0 )
218 181 217 sylanr1 
 |-  ( ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = 0 )
219 180 218 sylan2b 
 |-  ( ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = 0 )
220 ppifi 
 |-  ( x e. RR -> ( ( 0 [,] x ) i^i Prime ) e. Fin )
221 141 220 syl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( 0 [,] x ) i^i Prime ) e. Fin )
222 155 176 219 221 fsumss 
 |-  ( ( 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. ( ( Lam ` ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) )
223 154 222 eqtr4d 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) )
224 156 173 fsumrecl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) e. RR )
225 129 224 sylan2 
 |-  ( ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) e. RR )
226 74 adantlr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( log ` p ) e. RR )
227 71 adantl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> p e. NN )
228 227 nnrecred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 / p ) e. RR )
229 227 nnrpd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> p e. RR+ )
230 229 rpreccld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 / p ) e. RR+ )
231 simplrl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> x e. RR+ )
232 231 relogcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( log ` x ) e. RR )
233 227 nnred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> p e. RR )
234 75 adantl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> p e. ( ZZ>= ` 2 ) )
235 eluz2gt1 
 |-  ( p e. ( ZZ>= ` 2 ) -> 1 < p )
236 234 235 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 1 < p )
237 233 236 rplogcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( log ` p ) e. RR+ )
238 232 237 rerpdivcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( log ` x ) / ( log ` p ) ) e. RR )
239 238 flcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) e. ZZ )
240 239 peano2zd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) e. ZZ )
241 230 240 rpexpcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) e. RR+ )
242 241 rpred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) e. RR )
243 228 242 resubcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) e. RR )
244 234 77 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( p - 1 ) e. NN )
245 244 nnrpd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( p - 1 ) e. RR+ )
246 245 229 rpdivcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( p - 1 ) / p ) e. RR+ )
247 243 246 rerpdivcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) e. RR )
248 226 247 remulcld 
 |-  ( ( ( 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 )
249 170 recnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( Lam ` ( p ^ k ) ) e. CC )
250 163 nncnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( p ^ k ) e. CC )
251 163 nnne0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( p ^ k ) =/= 0 )
252 249 250 251 divrecd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) = ( ( Lam ` ( p ^ k ) ) x. ( 1 / ( p ^ k ) ) ) )
253 simprl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> p e. Prime )
254 vmappw 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
255 253 161 254 syl2anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
256 159 nncnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> p e. CC )
257 159 nnne0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> p =/= 0 )
258 elfzelz 
 |-  ( k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) -> k e. ZZ )
259 258 ad2antll 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> k e. ZZ )
260 256 257 259 exprecd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( 1 / p ) ^ k ) = ( 1 / ( p ^ k ) ) )
261 260 eqcomd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( 1 / ( p ^ k ) ) = ( ( 1 / p ) ^ k ) )
262 255 261 oveq12d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( Lam ` ( p ^ k ) ) x. ( 1 / ( p ^ k ) ) ) = ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
263 252 262 eqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) = ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
264 263 171 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) e. RR )
265 264 anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) e. RR )
266 1red 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> 1 e. RR )
267 vmage0 
 |-  ( ( p ^ k ) e. NN -> 0 <_ ( Lam ` ( p ^ k ) ) )
268 163 267 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> 0 <_ ( Lam ` ( p ^ k ) ) )
269 163 nnred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( p ^ k ) e. RR )
270 163 nngt0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> 0 < ( p ^ k ) )
271 divge0 
 |-  ( ( ( ( Lam ` ( p ^ k ) ) e. RR /\ 0 <_ ( Lam ` ( p ^ k ) ) ) /\ ( ( p ^ k ) e. RR /\ 0 < ( p ^ k ) ) ) -> 0 <_ ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) )
272 170 268 269 270 271 syl22anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> 0 <_ ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) )
273 84 leidi 
 |-  0 <_ 0
274 simpr 
 |-  ( ( ( ( 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 )
275 273 274 breqtrrid 
 |-  ( ( ( ( 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 ) ) ) )
276 3 ad3antrrr 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) /\ ( .1. ` ( L ` ( p ^ k ) ) ) =/= 0 ) -> N e. NN )
277 91 ad2antrr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> .1. e. D )
278 4 1 5 25 86 277 165 dchrn0 
 |-  ( ( ( 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 ) ) )
279 278 biimpa 
 |-  ( ( ( ( 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 ) )
280 4 1 6 86 276 279 dchr1 
 |-  ( ( ( ( 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 )
281 103 280 breqtrrid 
 |-  ( ( ( ( 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 ) ) ) )
282 275 281 pm2.61dane 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> 0 <_ ( .1. ` ( L ` ( p ^ k ) ) ) )
283 subge02 
 |-  ( ( 1 e. RR /\ ( .1. ` ( L ` ( p ^ k ) ) ) e. RR ) -> ( 0 <_ ( .1. ` ( L ` ( p ^ k ) ) ) <-> ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) <_ 1 ) )
284 24 166 283 sylancr 
 |-  ( ( ( 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 ) )
285 282 284 mpbid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) <_ 1 )
286 168 266 171 272 285 lemul1ad 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ ( 1 x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) )
287 207 mulid2d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( 1 x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) )
288 287 263 eqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( 1 x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) = ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
289 286 288 breqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
290 289 anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
291 156 173 265 290 fsumle 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) )
292 226 recnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( log ` p ) e. CC )
293 159 nnrecred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( 1 / p ) e. RR )
294 293 162 reexpcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( 1 / p ) ^ k ) e. RR )
295 294 recnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( p e. Prime /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) ) -> ( ( 1 / p ) ^ k ) e. CC )
296 295 anassrs 
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) /\ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ) -> ( ( 1 / p ) ^ k ) e. CC )
297 156 292 296 fsummulc2 
 |-  ( ( ( 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 ) ) )
298 fzval3 
 |-  ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) e. ZZ -> ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) = ( 1 ..^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) )
299 239 298 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) = ( 1 ..^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) )
300 299 sumeq1d 
 |-  ( ( ( 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 ) )
301 228 recnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 / p ) e. CC )
302 227 nngt0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 0 < p )
303 recgt1 
 |-  ( ( p e. RR /\ 0 < p ) -> ( 1 < p <-> ( 1 / p ) < 1 ) )
304 233 302 303 syl2anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 < p <-> ( 1 / p ) < 1 ) )
305 236 304 mpbid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 / p ) < 1 )
306 228 305 ltned 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 / p ) =/= 1 )
307 1nn0 
 |-  1 e. NN0
308 307 a1i 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 1 e. NN0 )
309 log1 
 |-  ( log ` 1 ) = 0
310 simprr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
311 1rp 
 |-  1 e. RR+
312 simprl 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
313 logleb 
 |-  ( ( 1 e. RR+ /\ x e. RR+ ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
314 311 312 313 sylancr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
315 310 314 mpbid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` 1 ) <_ ( log ` x ) )
316 309 315 eqbrtrrid 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( log ` x ) )
317 316 adantr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 0 <_ ( log ` x ) )
318 232 237 317 divge0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 0 <_ ( ( log ` x ) / ( log ` p ) ) )
319 flge0nn0 
 |-  ( ( ( ( log ` x ) / ( log ` p ) ) e. RR /\ 0 <_ ( ( log ` x ) / ( log ` p ) ) ) -> ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) e. NN0 )
320 238 318 319 syl2anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) e. NN0 )
321 nn0p1nn 
 |-  ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) e. NN0 -> ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) e. NN )
322 320 321 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) e. NN )
323 nnuz 
 |-  NN = ( ZZ>= ` 1 )
324 322 323 eleqtrdi 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) e. ( ZZ>= ` 1 ) )
325 301 306 308 324 geoserg 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ..^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ( ( 1 / p ) ^ k ) = ( ( ( ( 1 / p ) ^ 1 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) )
326 301 exp1d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( 1 / p ) ^ 1 ) = ( 1 / p ) )
327 326 oveq1d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( ( 1 / p ) ^ 1 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) = ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) )
328 227 nncnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> p e. CC )
329 1cnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 1 e. CC )
330 229 rpcnne0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( p e. CC /\ p =/= 0 ) )
331 divsubdir 
 |-  ( ( p e. CC /\ 1 e. CC /\ ( p e. CC /\ p =/= 0 ) ) -> ( ( p - 1 ) / p ) = ( ( p / p ) - ( 1 / p ) ) )
332 328 329 330 331 syl3anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( p - 1 ) / p ) = ( ( p / p ) - ( 1 / p ) ) )
333 divid 
 |-  ( ( p e. CC /\ p =/= 0 ) -> ( p / p ) = 1 )
334 330 333 syl 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( p / p ) = 1 )
335 334 oveq1d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( p / p ) - ( 1 / p ) ) = ( 1 - ( 1 / p ) ) )
336 332 335 eqtr2d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 - ( 1 / p ) ) = ( ( p - 1 ) / p ) )
337 327 336 oveq12d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( ( ( 1 / p ) ^ 1 ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( 1 - ( 1 / p ) ) ) = ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) )
338 300 325 337 3eqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 / p ) ^ k ) = ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) )
339 338 oveq2d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( log ` p ) x. sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 / p ) ^ k ) ) = ( ( log ` p ) x. ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) ) )
340 297 339 eqtr3d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( log ` p ) x. ( ( 1 / p ) ^ k ) ) = ( ( log ` p ) x. ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) ) )
341 291 340 breqtrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ ( ( log ` p ) x. ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) ) )
342 241 rpge0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 0 <_ ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) )
343 228 242 subge02d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 0 <_ ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) <-> ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( 1 / p ) ) )
344 342 343 mpbid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( 1 / p ) )
345 245 rpcnne0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( p - 1 ) e. CC /\ ( p - 1 ) =/= 0 ) )
346 dmdcan 
 |-  ( ( ( ( p - 1 ) e. CC /\ ( p - 1 ) =/= 0 ) /\ ( p e. CC /\ p =/= 0 ) /\ 1 e. CC ) -> ( ( ( p - 1 ) / p ) x. ( 1 / ( p - 1 ) ) ) = ( 1 / p ) )
347 345 330 329 346 syl3anc 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( ( p - 1 ) / p ) x. ( 1 / ( p - 1 ) ) ) = ( 1 / p ) )
348 344 347 breqtrrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( ( ( p - 1 ) / p ) x. ( 1 / ( p - 1 ) ) ) )
349 244 nnrecred 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( 1 / ( p - 1 ) ) e. RR )
350 243 349 246 ledivmuld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) <_ ( 1 / ( p - 1 ) ) <-> ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) <_ ( ( ( p - 1 ) / p ) x. ( 1 / ( p - 1 ) ) ) ) )
351 348 350 mpbird 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) <_ ( 1 / ( p - 1 ) ) )
352 247 349 237 lemul2d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) <_ ( 1 / ( p - 1 ) ) <-> ( ( log ` p ) x. ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) ) <_ ( ( log ` p ) x. ( 1 / ( p - 1 ) ) ) ) )
353 351 352 mpbid 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( log ` p ) x. ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) ) <_ ( ( log ` p ) x. ( 1 / ( p - 1 ) ) ) )
354 244 nncnd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( p - 1 ) e. CC )
355 244 nnne0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( p - 1 ) =/= 0 )
356 292 354 355 divrecd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( log ` p ) / ( p - 1 ) ) = ( ( log ` p ) x. ( 1 / ( p - 1 ) ) ) )
357 353 356 breqtrrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( log ` p ) x. ( ( ( 1 / p ) - ( ( 1 / p ) ^ ( ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) + 1 ) ) ) / ( ( p - 1 ) / p ) ) ) <_ ( ( log ` p ) / ( p - 1 ) ) )
358 224 248 130 341 357 letrd 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> sum_ k e. ( 1 ... ( |_ ` ( ( log ` x ) / ( log ` p ) ) ) ) ( ( 1 - ( .1. ` ( L ` ( p ^ k ) ) ) ) x. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ ( ( log ` p ) / ( p - 1 ) ) )
359 129 358 sylan2 
 |-  ( ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ ( ( log ` p ) / ( p - 1 ) ) )
360 126 225 131 359 fsumle 
 |-  ( ( 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. ( ( Lam ` ( p ^ k ) ) / ( p ^ k ) ) ) <_ sum_ p e. { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } ( ( log ` p ) / ( p - 1 ) ) )
361 223 360 eqbrtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) <_ sum_ p e. { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } ( ( log ` p ) / ( p - 1 ) ) )
362 80 adantlr 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. { q e. Prime | q || N } ) -> ( ( log ` p ) / ( p - 1 ) ) e. RR )
363 237 245 rpdivcld 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> ( ( log ` p ) / ( p - 1 ) ) e. RR+ )
364 363 rpge0d 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. Prime ) -> 0 <_ ( ( log ` p ) / ( p - 1 ) ) )
365 70 364 sylan2 
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ p e. { q e. Prime | q || N } ) -> 0 <_ ( ( log ` p ) / ( p - 1 ) ) )
366 122 362 365 125 fsumless 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ p e. { q e. ( ( 0 [,] x ) i^i Prime ) | q || N } ( ( log ` p ) / ( p - 1 ) ) <_ sum_ p e. { q e. Prime | q || N } ( ( log ` p ) / ( p - 1 ) ) )
367 102 132 133 361 366 letrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) <_ sum_ p e. { q e. Prime | q || N } ( ( log ` p ) / ( p - 1 ) ) )
368 121 367 eqbrtrd 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) <_ sum_ p e. { q e. Prime | q || N } ( ( log ` p ) / ( p - 1 ) ) )
369 66 41 67 81 368 elo1d 
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) e. O(1) )
370 o1sub 
 |-  ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) e. O(1) /\ ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) e. O(1) ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) ) e. O(1) )
371 65 369 370 sylancr 
 |-  ( ph -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) / n ) - ( log ` x ) ) ) oF - ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( 1 - ( .1. ` ( L ` n ) ) ) x. ( ( Lam ` n ) / n ) ) ) ) e. O(1) )
372 64 371 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( .1. ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )