Metamath Proof Explorer

Theorem rplogsum

Description: The sum of log p / p over the primes p == A (mod N ) is asymptotic to log x / phi ( x ) + O(1) . Equation 9.4.3 of Shapiro, p. 375. (Contributed by Mario Carneiro, 16-Apr-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.u 
|- U = ( Unit ` Z )
rpvmasum.b 
|- ( ph -> A e. U )
rpvmasum.t 
|- T = ( `' L " { A } )
Assertion rplogsum 
|- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( 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.u 
 |-  U = ( Unit ` Z )
5 rpvmasum.b 
 |-  ( ph -> A e. U )
6 rpvmasum.t 
 |-  T = ( `' L " { A } )
7 1 2 3 4 5 6 rpvmasum 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( log ` x ) ) ) e. O(1) )
8 3 phicld 
 |-  ( ph -> ( phi ` N ) e. NN )
9 8 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. NN )
10 9 nncnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( phi ` N ) e. CC )
11 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
12 inss1 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) )
13 ssfi 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
14 11 12 13 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) e. Fin )
15 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) )
16 15 elin1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> p e. ( 1 ... ( |_ ` x ) ) )
17 elfznn 
 |-  ( p e. ( 1 ... ( |_ ` x ) ) -> p e. NN )
18 16 17 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> p e. NN )
19 vmacl 
 |-  ( p e. NN -> ( Lam ` p ) e. RR )
20 nndivre 
 |-  ( ( ( Lam ` p ) e. RR /\ p e. NN ) -> ( ( Lam ` p ) / p ) e. RR )
21 19 20 mpancom 
 |-  ( p e. NN -> ( ( Lam ` p ) / p ) e. RR )
22 18 21 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( Lam ` p ) / p ) e. RR )
23 14 22 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) e. RR )
24 23 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) e. CC )
25 10 24 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) e. CC )
26 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
27 26 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
28 27 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
29 25 28 subcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( log ` x ) ) e. CC )
30 inss1 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( 1 ... ( |_ ` x ) )
31 ssfi 
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) e. Fin )
32 11 30 31 sylancl 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) e. Fin )
33 simpr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) )
34 33 elin1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> p e. ( 1 ... ( |_ ` x ) ) )
35 34 17 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> p e. NN )
36 nnrp 
 |-  ( p e. NN -> p e. RR+ )
37 36 relogcld 
 |-  ( p e. NN -> ( log ` p ) e. RR )
38 37 36 rerpdivcld 
 |-  ( p e. NN -> ( ( log ` p ) / p ) e. RR )
39 35 38 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> ( ( log ` p ) / p ) e. RR )
40 32 39 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) e. RR )
41 40 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) e. CC )
42 10 41 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) e. CC )
43 42 28 subcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) e. CC )
44 10 24 41 subdid 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. ( sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) - sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) ) = ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) ) )
45 19 recnd 
 |-  ( p e. NN -> ( Lam ` p ) e. CC )
46 0re 
 |-  0 e. RR
47 ifcl 
 |-  ( ( ( log ` p ) e. RR /\ 0 e. RR ) -> if ( p e. Prime , ( log ` p ) , 0 ) e. RR )
48 37 46 47 sylancl 
 |-  ( p e. NN -> if ( p e. Prime , ( log ` p ) , 0 ) e. RR )
49 48 recnd 
 |-  ( p e. NN -> if ( p e. Prime , ( log ` p ) , 0 ) e. CC )
50 36 rpcnne0d 
 |-  ( p e. NN -> ( p e. CC /\ p =/= 0 ) )
51 divsubdir 
 |-  ( ( ( Lam ` p ) e. CC /\ if ( p e. Prime , ( log ` p ) , 0 ) e. CC /\ ( p e. CC /\ p =/= 0 ) ) -> ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) = ( ( ( Lam ` p ) / p ) - ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) ) )
52 45 49 50 51 syl3anc 
 |-  ( p e. NN -> ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) = ( ( ( Lam ` p ) / p ) - ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) ) )
53 18 52 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) = ( ( ( Lam ` p ) / p ) - ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) ) )
54 53 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) = sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) / p ) - ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) ) )
55 21 recnd 
 |-  ( p e. NN -> ( ( Lam ` p ) / p ) e. CC )
56 18 55 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( Lam ` p ) / p ) e. CC )
57 48 36 rerpdivcld 
 |-  ( p e. NN -> ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) e. RR )
58 57 recnd 
 |-  ( p e. NN -> ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) e. CC )
59 18 58 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) e. CC )
60 14 56 59 fsumsub 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) / p ) - ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) ) = ( sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) - sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) ) )
61 inss2 
 |-  ( Prime i^i T ) C_ T
62 sslin 
 |-  ( ( Prime i^i T ) C_ T -> ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( ( 1 ... ( |_ ` x ) ) i^i T ) )
63 61 62 mp1i 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( ( 1 ... ( |_ ` x ) ) i^i T ) )
64 35 58 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) e. CC )
65 eldif 
 |-  ( p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) <-> ( p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) /\ -. p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) )
66 incom 
 |-  ( Prime i^i T ) = ( T i^i Prime )
67 66 ineq2i 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) = ( ( 1 ... ( |_ ` x ) ) i^i ( T i^i Prime ) )
68 inass 
 |-  ( ( ( 1 ... ( |_ ` x ) ) i^i T ) i^i Prime ) = ( ( 1 ... ( |_ ` x ) ) i^i ( T i^i Prime ) )
69 67 68 eqtr4i 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) = ( ( ( 1 ... ( |_ ` x ) ) i^i T ) i^i Prime )
70 69 elin2 
 |-  ( p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) <-> ( p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) /\ p e. Prime ) )
71 70 simplbi2 
 |-  ( p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) -> ( p e. Prime -> p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) )
72 71 con3dimp 
 |-  ( ( p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) /\ -. p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> -. p e. Prime )
73 65 72 sylbi 
 |-  ( p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> -. p e. Prime )
74 73 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) ) -> -. p e. Prime )
75 74 iffalsed 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) ) -> if ( p e. Prime , ( log ` p ) , 0 ) = 0 )
76 75 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) ) -> ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) = ( 0 / p ) )
77 eldifi 
 |-  ( p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) )
78 77 18 sylan2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) ) -> p e. NN )
79 div0 
 |-  ( ( p e. CC /\ p =/= 0 ) -> ( 0 / p ) = 0 )
80 50 79 syl 
 |-  ( p e. NN -> ( 0 / p ) = 0 )
81 78 80 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) ) -> ( 0 / p ) = 0 )
82 76 81 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( ( 1 ... ( |_ ` x ) ) i^i T ) \ ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) ) -> ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) = 0 )
83 63 64 82 14 fsumss 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) = sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) )
84 inss2 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ ( Prime i^i T )
85 inss1 
 |-  ( Prime i^i T ) C_ Prime
86 84 85 sstri 
 |-  ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) C_ Prime
87 86 33 sselid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> p e. Prime )
88 87 iftrued 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> if ( p e. Prime , ( log ` p ) , 0 ) = ( log ` p ) )
89 88 oveq1d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ) -> ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) = ( ( log ` p ) / p ) )
90 89 sumeq2dv 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) = sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) )
91 83 90 eqtr3d 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) = sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) )
92 91 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) - sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( if ( p e. Prime , ( log ` p ) , 0 ) / p ) ) = ( sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) - sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) )
93 54 60 92 3eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) = ( sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) - sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) )
94 93 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) = ( ( phi ` N ) x. ( sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) - sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) ) )
95 25 42 28 nnncan2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( log ` x ) ) - ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) ) = ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) ) )
96 44 94 95 3eqtr4d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) = ( ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( log ` x ) ) - ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) ) )
97 96 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) ) = ( x e. RR+ |-> ( ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( log ` x ) ) - ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) ) ) )
98 19 48 resubcld 
 |-  ( p e. NN -> ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) e. RR )
99 98 36 rerpdivcld 
 |-  ( p e. NN -> ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) e. RR )
100 18 99 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) e. RR )
101 14 100 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) e. RR )
102 101 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) e. CC )
103 rpssre 
 |-  RR+ C_ RR
104 8 nncnd 
 |-  ( ph -> ( phi ` N ) e. CC )
105 o1const 
 |-  ( ( RR+ C_ RR /\ ( phi ` N ) e. CC ) -> ( x e. RR+ |-> ( phi ` N ) ) e. O(1) )
106 103 104 105 sylancr 
 |-  ( ph -> ( x e. RR+ |-> ( phi ` N ) ) e. O(1) )
107 103 a1i 
 |-  ( ph -> RR+ C_ RR )
108 1red 
 |-  ( ph -> 1 e. RR )
109 2re 
 |-  2 e. RR
110 109 a1i 
 |-  ( ph -> 2 e. RR )
111 breq1 
 |-  ( ( log ` p ) = if ( p e. Prime , ( log ` p ) , 0 ) -> ( ( log ` p ) <_ ( Lam ` p ) <-> if ( p e. Prime , ( log ` p ) , 0 ) <_ ( Lam ` p ) ) )
112 breq1 
 |-  ( 0 = if ( p e. Prime , ( log ` p ) , 0 ) -> ( 0 <_ ( Lam ` p ) <-> if ( p e. Prime , ( log ` p ) , 0 ) <_ ( Lam ` p ) ) )
113 37 adantr 
 |-  ( ( p e. NN /\ p e. Prime ) -> ( log ` p ) e. RR )
114 vmaprm 
 |-  ( p e. Prime -> ( Lam ` p ) = ( log ` p ) )
115 114 adantl 
 |-  ( ( p e. NN /\ p e. Prime ) -> ( Lam ` p ) = ( log ` p ) )
116 115 eqcomd 
 |-  ( ( p e. NN /\ p e. Prime ) -> ( log ` p ) = ( Lam ` p ) )
117 113 116 eqled 
 |-  ( ( p e. NN /\ p e. Prime ) -> ( log ` p ) <_ ( Lam ` p ) )
118 vmage0 
 |-  ( p e. NN -> 0 <_ ( Lam ` p ) )
119 118 adantr 
 |-  ( ( p e. NN /\ -. p e. Prime ) -> 0 <_ ( Lam ` p ) )
120 111 112 117 119 ifbothda 
 |-  ( p e. NN -> if ( p e. Prime , ( log ` p ) , 0 ) <_ ( Lam ` p ) )
121 19 48 subge0d 
 |-  ( p e. NN -> ( 0 <_ ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) <-> if ( p e. Prime , ( log ` p ) , 0 ) <_ ( Lam ` p ) ) )
122 120 121 mpbird 
 |-  ( p e. NN -> 0 <_ ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) )
123 98 36 122 divge0d 
 |-  ( p e. NN -> 0 <_ ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) )
124 18 123 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ) -> 0 <_ ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) )
125 14 100 124 fsumge0 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) )
126 101 125 absidd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) = sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) )
127 17 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( 1 ... ( |_ ` x ) ) ) -> p e. NN )
128 127 99 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) e. RR )
129 11 128 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) e. RR )
130 109 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 2 e. RR )
131 127 123 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ p e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) )
132 12 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( 1 ... ( |_ ` x ) ) i^i T ) C_ ( 1 ... ( |_ ` x ) ) )
133 11 128 131 132 fsumless 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) <_ sum_ p e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) )
134 107 sselda 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
135 134 flcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( |_ ` x ) e. ZZ )
136 rplogsumlem2 
 |-  ( ( |_ ` x ) e. ZZ -> sum_ p e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) <_ 2 )
137 135 136 syl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) <_ 2 )
138 101 129 130 133 137 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) <_ 2 )
139 126 138 eqbrtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) <_ 2 )
140 139 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) <_ 2 )
141 107 102 108 110 140 elo1d 
 |-  ( ph -> ( x e. RR+ |-> sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) e. O(1) )
142 10 102 106 141 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( ( Lam ` p ) - if ( p e. Prime , ( log ` p ) , 0 ) ) / p ) ) ) e. O(1) )
143 97 142 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( log ` x ) ) - ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) ) ) e. O(1) )
144 29 43 143 o1dif 
 |-  ( ph -> ( ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` p ) / p ) ) - ( log ` x ) ) ) e. O(1) <-> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) ) e. O(1) ) )
145 7 144 mpbid 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ p e. ( ( 1 ... ( |_ ` x ) ) i^i ( Prime i^i T ) ) ( ( log ` p ) / p ) ) - ( log ` x ) ) ) e. O(1) )