Metamath Proof Explorer

Theorem pntrlog2bndlem1

Description: The sum of selberg3r and selberg4r . (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypotheses pntsval.1 
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
pntrlog2bnd.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion pntrlog2bndlem1 
|- ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) ) e. <_O(1)

Proof

Step Hyp Ref Expression
1 pntsval.1 
 |-  S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
2 pntrlog2bnd.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
3 1red 
 |-  ( T. -> 1 e. RR )
4 2 selberg34r 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) e. O(1)
5 elioore 
 |-  ( x e. ( 1 (,) +oo ) -> x e. RR )
6 5 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR )
7 1rp 
 |-  1 e. RR+
8 7 a1i 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR+ )
9 1red 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 e. RR )
10 eliooord 
 |-  ( x e. ( 1 (,) +oo ) -> ( 1 < x /\ x < +oo ) )
11 10 adantl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 < x /\ x < +oo ) )
12 11 simpld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 < x )
13 9 6 12 ltled 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 1 <_ x )
14 6 8 13 rpgecld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. RR+ )
15 2 pntrf 
 |-  R : RR+ --> RR
16 15 ffvelrni 
 |-  ( x e. RR+ -> ( R ` x ) e. RR )
17 14 16 syl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. RR )
18 14 relogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR )
19 17 18 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) e. RR )
20 fzfid 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
21 14 adantr 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
22 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
23 22 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
24 23 nnrpd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR+ )
25 21 24 rpdivcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
26 15 ffvelrni 
 |-  ( ( x / n ) e. RR+ -> ( R ` ( x / n ) ) e. RR )
27 25 26 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. RR )
28 fzfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... n ) e. Fin )
29 dvdsssfz1 
 |-  ( n e. NN -> { y e. NN | y || n } C_ ( 1 ... n ) )
30 23 29 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || n } C_ ( 1 ... n ) )
31 28 30 ssfid 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> { y e. NN | y || n } e. Fin )
32 ssrab2 
 |-  { y e. NN | y || n } C_ NN
33 simpr 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> m e. { y e. NN | y || n } )
34 32 33 sseldi 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> m e. NN )
35 vmacl 
 |-  ( m e. NN -> ( Lam ` m ) e. RR )
36 34 35 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( Lam ` m ) e. RR )
37 dvdsdivcl 
 |-  ( ( n e. NN /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. { y e. NN | y || n } )
38 23 37 sylan 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. { y e. NN | y || n } )
39 32 38 sseldi 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( n / m ) e. NN )
40 vmacl 
 |-  ( ( n / m ) e. NN -> ( Lam ` ( n / m ) ) e. RR )
41 39 40 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( Lam ` ( n / m ) ) e. RR )
42 36 41 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. RR )
43 31 42 fsumrecl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. RR )
44 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
45 23 44 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( Lam ` n ) e. RR )
46 24 relogcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` n ) e. RR )
47 45 46 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. RR )
48 43 47 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) e. RR )
49 27 48 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. RR )
50 20 49 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. RR )
51 6 12 rplogcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. RR+ )
52 50 51 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) e. RR )
53 19 52 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) e. RR )
54 53 14 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) e. RR )
55 54 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) e. CC )
56 55 lo1o12 
 |-  ( T. -> ( ( x e. ( 1 (,) +oo ) |-> ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) e. O(1) <-> ( x e. ( 1 (,) +oo ) |-> ( abs ` ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) ) e. <_O(1) ) )
57 4 56 mpbii 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( abs ` ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) ) e. <_O(1) )
58 55 abscld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) e. RR )
59 17 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( R ` x ) e. CC )
60 59 abscld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( R ` x ) ) e. RR )
61 60 18 remulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) e. RR )
62 27 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( R ` ( x / n ) ) e. CC )
63 62 abscld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( R ` ( x / n ) ) ) e. RR )
64 23 nnred 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. RR )
65 1 pntsf 
 |-  S : RR --> RR
66 65 ffvelrni 
 |-  ( n e. RR -> ( S ` n ) e. RR )
67 64 66 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) e. RR )
68 1red 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
69 64 68 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. RR )
70 65 ffvelrni 
 |-  ( ( n - 1 ) e. RR -> ( S ` ( n - 1 ) ) e. RR )
71 69 70 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. RR )
72 67 71 resubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) e. RR )
73 63 72 remulcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
74 20 73 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) e. RR )
75 74 51 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) e. RR )
76 61 75 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) e. RR )
77 76 14 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) e. RR )
78 18 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) e. CC )
79 59 78 mulcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( R ` x ) x. ( log ` x ) ) e. CC )
80 50 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. CC )
81 51 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( log ` x ) =/= 0 )
82 80 78 81 divcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) e. CC )
83 79 82 subcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) e. CC )
84 83 abscld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) e. RR )
85 80 abscld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) e. RR )
86 85 51 rerpdivcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) e. RR )
87 61 86 resubcld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) ) e. RR )
88 49 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. CC )
89 88 abscld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) e. RR )
90 20 89 fsumrecl 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) e. RR )
91 20 88 fsumabs 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) )
92 48 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) e. CC )
93 62 92 absmuld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) = ( ( abs ` ( R ` ( x / n ) ) ) x. ( abs ` ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) )
94 92 abscld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) e. RR )
95 62 absge0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( R ` ( x / n ) ) ) )
96 43 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) e. CC )
97 47 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) x. ( log ` n ) ) e. CC )
98 96 97 abs2dif2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) <_ ( ( abs ` sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) + ( abs ` ( ( Lam ` n ) x. ( log ` n ) ) ) ) )
99 71 recnd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) e. CC )
100 96 97 addcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) e. CC )
101 99 100 pncan2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( S ` ( n - 1 ) ) + ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) ) - ( S ` ( n - 1 ) ) ) = ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
102 elfzuz 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ( ZZ>= ` 1 ) )
103 102 adantl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ( ZZ>= ` 1 ) )
104 elfznn 
 |-  ( k e. ( 1 ... n ) -> k e. NN )
105 104 adantl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> k e. NN )
106 vmacl 
 |-  ( k e. NN -> ( Lam ` k ) e. RR )
107 105 106 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> ( Lam ` k ) e. RR )
108 105 nnrpd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> k e. RR+ )
109 108 relogcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> ( log ` k ) e. RR )
110 107 109 remulcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( Lam ` k ) x. ( log ` k ) ) e. RR )
111 fzfid 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> ( 1 ... k ) e. Fin )
112 dvdsssfz1 
 |-  ( k e. NN -> { y e. NN | y || k } C_ ( 1 ... k ) )
113 105 112 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> { y e. NN | y || k } C_ ( 1 ... k ) )
114 111 113 ssfid 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> { y e. NN | y || k } e. Fin )
115 ssrab2 
 |-  { y e. NN | y || k } C_ NN
116 simpr 
 |-  ( ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) /\ m e. { y e. NN | y || k } ) -> m e. { y e. NN | y || k } )
117 115 116 sseldi 
 |-  ( ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) /\ m e. { y e. NN | y || k } ) -> m e. NN )
118 117 35 syl 
 |-  ( ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) /\ m e. { y e. NN | y || k } ) -> ( Lam ` m ) e. RR )
119 dvdsdivcl 
 |-  ( ( k e. NN /\ m e. { y e. NN | y || k } ) -> ( k / m ) e. { y e. NN | y || k } )
120 105 119 sylan 
 |-  ( ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) /\ m e. { y e. NN | y || k } ) -> ( k / m ) e. { y e. NN | y || k } )
121 115 120 sseldi 
 |-  ( ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) /\ m e. { y e. NN | y || k } ) -> ( k / m ) e. NN )
122 vmacl 
 |-  ( ( k / m ) e. NN -> ( Lam ` ( k / m ) ) e. RR )
123 121 122 syl 
 |-  ( ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) /\ m e. { y e. NN | y || k } ) -> ( Lam ` ( k / m ) ) e. RR )
124 118 123 remulcld 
 |-  ( ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) /\ m e. { y e. NN | y || k } ) -> ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) e. RR )
125 114 124 fsumrecl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) e. RR )
126 110 125 readdcld 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) e. RR )
127 126 recnd 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ k e. ( 1 ... n ) ) -> ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) e. CC )
128 fveq2 
 |-  ( k = n -> ( Lam ` k ) = ( Lam ` n ) )
129 fveq2 
 |-  ( k = n -> ( log ` k ) = ( log ` n ) )
130 128 129 oveq12d 
 |-  ( k = n -> ( ( Lam ` k ) x. ( log ` k ) ) = ( ( Lam ` n ) x. ( log ` n ) ) )
131 breq2 
 |-  ( k = n -> ( y || k <-> y || n ) )
132 131 rabbidv 
 |-  ( k = n -> { y e. NN | y || k } = { y e. NN | y || n } )
133 fvoveq1 
 |-  ( k = n -> ( Lam ` ( k / m ) ) = ( Lam ` ( n / m ) ) )
134 133 oveq2d 
 |-  ( k = n -> ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) = ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
135 134 adantr 
 |-  ( ( k = n /\ m e. { y e. NN | y || n } ) -> ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) = ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
136 132 135 sumeq12rdv 
 |-  ( k = n -> sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) = sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
137 130 136 oveq12d 
 |-  ( k = n -> ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
138 103 127 137 fsumm1 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ k e. ( 1 ... n ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) = ( sum_ k e. ( 1 ... ( n - 1 ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) + ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) ) )
139 1 pntsval2 
 |-  ( n e. RR -> ( S ` n ) = sum_ k e. ( 1 ... ( |_ ` n ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
140 64 139 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) = sum_ k e. ( 1 ... ( |_ ` n ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
141 23 nnzd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ZZ )
142 flid 
 |-  ( n e. ZZ -> ( |_ ` n ) = n )
143 141 142 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` n ) = n )
144 143 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` n ) ) = ( 1 ... n ) )
145 144 sumeq1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ k e. ( 1 ... ( |_ ` n ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) = sum_ k e. ( 1 ... n ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
146 140 145 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) = sum_ k e. ( 1 ... n ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
147 1 pntsval2 
 |-  ( ( n - 1 ) e. RR -> ( S ` ( n - 1 ) ) = sum_ k e. ( 1 ... ( |_ ` ( n - 1 ) ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
148 69 147 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) = sum_ k e. ( 1 ... ( |_ ` ( n - 1 ) ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
149 1zzd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. ZZ )
150 141 149 zsubcld 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( n - 1 ) e. ZZ )
151 flid 
 |-  ( ( n - 1 ) e. ZZ -> ( |_ ` ( n - 1 ) ) = ( n - 1 ) )
152 150 151 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( n - 1 ) ) = ( n - 1 ) )
153 152 oveq2d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( n - 1 ) ) ) = ( 1 ... ( n - 1 ) ) )
154 153 sumeq1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> sum_ k e. ( 1 ... ( |_ ` ( n - 1 ) ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) = sum_ k e. ( 1 ... ( n - 1 ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
155 148 154 eqtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` ( n - 1 ) ) = sum_ k e. ( 1 ... ( n - 1 ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) )
156 96 97 addcomd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) = ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) )
157 155 156 oveq12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` ( n - 1 ) ) + ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) ) = ( sum_ k e. ( 1 ... ( n - 1 ) ) ( ( ( Lam ` k ) x. ( log ` k ) ) + sum_ m e. { y e. NN | y || k } ( ( Lam ` m ) x. ( Lam ` ( k / m ) ) ) ) + ( ( ( Lam ` n ) x. ( log ` n ) ) + sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) ) )
158 138 146 157 3eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( S ` n ) = ( ( S ` ( n - 1 ) ) + ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) ) )
159 158 oveq1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) = ( ( ( S ` ( n - 1 ) ) + ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) ) - ( S ` ( n - 1 ) ) ) )
160 vmage0 
 |-  ( m e. NN -> 0 <_ ( Lam ` m ) )
161 34 160 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> 0 <_ ( Lam ` m ) )
162 vmage0 
 |-  ( ( n / m ) e. NN -> 0 <_ ( Lam ` ( n / m ) ) )
163 39 162 syl 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> 0 <_ ( Lam ` ( n / m ) ) )
164 36 41 161 163 mulge0d 
 |-  ( ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) /\ m e. { y e. NN | y || n } ) -> 0 <_ ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
165 31 42 164 fsumge0 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
166 43 165 absidd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) = sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) )
167 vmage0 
 |-  ( n e. NN -> 0 <_ ( Lam ` n ) )
168 23 167 syl 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( Lam ` n ) )
169 23 nnge1d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ n )
170 64 169 logge0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( log ` n ) )
171 45 46 168 170 mulge0d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( Lam ` n ) x. ( log ` n ) ) )
172 47 171 absidd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( Lam ` n ) x. ( log ` n ) ) ) = ( ( Lam ` n ) x. ( log ` n ) ) )
173 166 172 oveq12d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) + ( abs ` ( ( Lam ` n ) x. ( log ` n ) ) ) ) = ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) + ( ( Lam ` n ) x. ( log ` n ) ) ) )
174 101 159 173 3eqtr4d 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( S ` n ) - ( S ` ( n - 1 ) ) ) = ( ( abs ` sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) ) + ( abs ` ( ( Lam ` n ) x. ( log ` n ) ) ) ) )
175 98 174 breqtrrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) <_ ( ( S ` n ) - ( S ` ( n - 1 ) ) ) )
176 94 72 63 95 175 lemul2ad 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( R ` ( x / n ) ) ) x. ( abs ` ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) <_ ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) )
177 93 176 eqbrtrd 
 |-  ( ( ( T. /\ x e. ( 1 (,) +oo ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) <_ ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) )
178 20 89 73 177 fsumle 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) )
179 85 90 74 91 178 letrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) <_ sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) )
180 85 74 51 179 lediv1dd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) <_ ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) )
181 86 75 61 180 lesub2dd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) <_ ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) ) )
182 59 78 absmuld 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( R ` x ) x. ( log ` x ) ) ) = ( ( abs ` ( R ` x ) ) x. ( abs ` ( log ` x ) ) ) )
183 6 13 logge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ ( log ` x ) )
184 18 183 absidd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( log ` x ) ) = ( log ` x ) )
185 184 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( R ` x ) ) x. ( abs ` ( log ` x ) ) ) = ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) )
186 182 185 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( R ` x ) x. ( log ` x ) ) ) = ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) )
187 80 78 81 absdivd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( abs ` ( log ` x ) ) ) )
188 184 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( abs ` ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) )
189 187 188 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) = ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) )
190 186 189 oveq12d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( ( R ` x ) x. ( log ` x ) ) ) - ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) = ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) ) )
191 79 82 abs2difd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( ( R ` x ) x. ( log ` x ) ) ) - ( abs ` ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) <_ ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) )
192 190 191 eqbrtrrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( ( abs ` sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) ) / ( log ` x ) ) ) <_ ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) )
193 76 87 84 181 192 letrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) <_ ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) )
194 76 84 14 193 lediv1dd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) <_ ( ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) / x ) )
195 53 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) e. CC )
196 6 recnd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x e. CC )
197 14 rpne0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> x =/= 0 )
198 195 196 197 absdivd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) = ( ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) / ( abs ` x ) ) )
199 14 rpge0d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> 0 <_ x )
200 6 199 absidd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` x ) = x )
201 200 oveq2d 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) / ( abs ` x ) ) = ( ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) / x ) )
202 198 201 eqtrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( abs ` ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) = ( ( abs ` ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) ) / x ) )
203 194 202 breqtrrd 
 |-  ( ( T. /\ x e. ( 1 (,) +oo ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) <_ ( abs ` ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) )
204 203 adantrr 
 |-  ( ( T. /\ ( x e. ( 1 (,) +oo ) /\ 1 <_ x ) ) -> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) <_ ( abs ` ( ( ( ( R ` x ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( R ` ( x / n ) ) x. ( sum_ m e. { y e. NN | y || n } ( ( Lam ` m ) x. ( Lam ` ( n / m ) ) ) - ( ( Lam ` n ) x. ( log ` n ) ) ) ) / ( log ` x ) ) ) / x ) ) )
205 3 57 58 77 204 lo1le 
 |-  ( T. -> ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) ) e. <_O(1) )
206 205 mptru 
 |-  ( x e. ( 1 (,) +oo ) |-> ( ( ( ( abs ` ( R ` x ) ) x. ( log ` x ) ) - ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( R ` ( x / n ) ) ) x. ( ( S ` n ) - ( S ` ( n - 1 ) ) ) ) / ( log ` x ) ) ) / x ) ) e. <_O(1)