Metamath Proof Explorer

Theorem lgamgulmlem3

Description: Lemma for lgamgulm . (Contributed by Mario Carneiro, 3-Jul-2017)

Ref Expression
Hypotheses lgamgulm.r 
|- ( ph -> R e. NN )
lgamgulm.u 
|- U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
lgamgulm.n 
|- ( ph -> N e. NN )
lgamgulm.a 
|- ( ph -> A e. U )
lgamgulm.l 
|- ( ph -> ( 2 x. R ) <_ N )
Assertion lgamgulmlem3 
|- ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( log ` ( ( A / N ) + 1 ) ) ) ) <_ ( R x. ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 lgamgulm.r 
 |-  ( ph -> R e. NN )
2 lgamgulm.u 
 |-  U = { x e. CC | ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) }
3 lgamgulm.n 
 |-  ( ph -> N e. NN )
4 lgamgulm.a 
 |-  ( ph -> A e. U )
5 lgamgulm.l 
 |-  ( ph -> ( 2 x. R ) <_ N )
6 1 2 lgamgulmlem1 
 |-  ( ph -> U C_ ( CC \ ( ZZ \ NN ) ) )
7 6 4 sseldd 
 |-  ( ph -> A e. ( CC \ ( ZZ \ NN ) ) )
8 7 eldifad 
 |-  ( ph -> A e. CC )
9 3 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
10 9 nnrpd 
 |-  ( ph -> ( N + 1 ) e. RR+ )
11 3 nnrpd 
 |-  ( ph -> N e. RR+ )
12 10 11 rpdivcld 
 |-  ( ph -> ( ( N + 1 ) / N ) e. RR+ )
13 12 relogcld 
 |-  ( ph -> ( log ` ( ( N + 1 ) / N ) ) e. RR )
14 13 recnd 
 |-  ( ph -> ( log ` ( ( N + 1 ) / N ) ) e. CC )
15 8 14 mulcld 
 |-  ( ph -> ( A x. ( log ` ( ( N + 1 ) / N ) ) ) e. CC )
16 3 nncnd 
 |-  ( ph -> N e. CC )
17 3 nnne0d 
 |-  ( ph -> N =/= 0 )
18 8 16 17 divcld 
 |-  ( ph -> ( A / N ) e. CC )
19 1cnd 
 |-  ( ph -> 1 e. CC )
20 18 19 addcld 
 |-  ( ph -> ( ( A / N ) + 1 ) e. CC )
21 7 3 dmgmdivn0 
 |-  ( ph -> ( ( A / N ) + 1 ) =/= 0 )
22 20 21 logcld 
 |-  ( ph -> ( log ` ( ( A / N ) + 1 ) ) e. CC )
23 15 22 subcld 
 |-  ( ph -> ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( log ` ( ( A / N ) + 1 ) ) ) e. CC )
24 23 abscld 
 |-  ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( log ` ( ( A / N ) + 1 ) ) ) ) e. RR )
25 15 18 subcld 
 |-  ( ph -> ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) e. CC )
26 25 abscld 
 |-  ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) e. RR )
27 18 22 subcld 
 |-  ( ph -> ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) e. CC )
28 27 abscld 
 |-  ( ph -> ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) e. RR )
29 26 28 readdcld 
 |-  ( ph -> ( ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) + ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) ) e. RR )
30 1 nnred 
 |-  ( ph -> R e. RR )
31 2re 
 |-  2 e. RR
32 31 a1i 
 |-  ( ph -> 2 e. RR )
33 1red 
 |-  ( ph -> 1 e. RR )
34 30 33 readdcld 
 |-  ( ph -> ( R + 1 ) e. RR )
35 32 34 remulcld 
 |-  ( ph -> ( 2 x. ( R + 1 ) ) e. RR )
36 3 nnsqcld 
 |-  ( ph -> ( N ^ 2 ) e. NN )
37 35 36 nndivred 
 |-  ( ph -> ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) e. RR )
38 30 37 remulcld 
 |-  ( ph -> ( R x. ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) ) e. RR )
39 15 22 18 abs3difd 
 |-  ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( log ` ( ( A / N ) + 1 ) ) ) ) <_ ( ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) + ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) ) )
40 3 nnrecred 
 |-  ( ph -> ( 1 / N ) e. RR )
41 9 nnrecred 
 |-  ( ph -> ( 1 / ( N + 1 ) ) e. RR )
42 40 41 resubcld 
 |-  ( ph -> ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) e. RR )
43 30 42 remulcld 
 |-  ( ph -> ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) e. RR )
44 32 30 remulcld 
 |-  ( ph -> ( 2 x. R ) e. RR )
45 3 nnred 
 |-  ( ph -> N e. RR )
46 1 nnrpd 
 |-  ( ph -> R e. RR+ )
47 30 46 ltaddrpd 
 |-  ( ph -> R < ( R + R ) )
48 1 nncnd 
 |-  ( ph -> R e. CC )
49 48 2timesd 
 |-  ( ph -> ( 2 x. R ) = ( R + R ) )
50 47 49 breqtrrd 
 |-  ( ph -> R < ( 2 x. R ) )
51 30 44 45 50 5 ltletrd 
 |-  ( ph -> R < N )
52 difrp 
 |-  ( ( R e. RR /\ N e. RR ) -> ( R < N <-> ( N - R ) e. RR+ ) )
53 30 45 52 syl2anc 
 |-  ( ph -> ( R < N <-> ( N - R ) e. RR+ ) )
54 51 53 mpbid 
 |-  ( ph -> ( N - R ) e. RR+ )
55 54 rprecred 
 |-  ( ph -> ( 1 / ( N - R ) ) e. RR )
56 55 40 resubcld 
 |-  ( ph -> ( ( 1 / ( N - R ) ) - ( 1 / N ) ) e. RR )
57 30 56 remulcld 
 |-  ( ph -> ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) e. RR )
58 43 57 readdcld 
 |-  ( ph -> ( ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) + ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) e. RR )
59 8 16 17 divrecd 
 |-  ( ph -> ( A / N ) = ( A x. ( 1 / N ) ) )
60 59 oveq2d 
 |-  ( ph -> ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) = ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A x. ( 1 / N ) ) ) )
61 40 recnd 
 |-  ( ph -> ( 1 / N ) e. CC )
62 8 14 61 subdid 
 |-  ( ph -> ( A x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) = ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A x. ( 1 / N ) ) ) )
63 60 62 eqtr4d 
 |-  ( ph -> ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) = ( A x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) )
64 63 fveq2d 
 |-  ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) = ( abs ` ( A x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) ) )
65 14 61 subcld 
 |-  ( ph -> ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) e. CC )
66 8 65 absmuld 
 |-  ( ph -> ( abs ` ( A x. ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) ) = ( ( abs ` A ) x. ( abs ` ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) ) )
67 64 66 eqtrd 
 |-  ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) = ( ( abs ` A ) x. ( abs ` ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) ) )
68 8 abscld 
 |-  ( ph -> ( abs ` A ) e. RR )
69 65 abscld 
 |-  ( ph -> ( abs ` ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) e. RR )
70 8 absge0d 
 |-  ( ph -> 0 <_ ( abs ` A ) )
71 65 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) )
72 fveq2 
 |-  ( x = A -> ( abs ` x ) = ( abs ` A ) )
73 72 breq1d 
 |-  ( x = A -> ( ( abs ` x ) <_ R <-> ( abs ` A ) <_ R ) )
74 fvoveq1 
 |-  ( x = A -> ( abs ` ( x + k ) ) = ( abs ` ( A + k ) ) )
75 74 breq2d 
 |-  ( x = A -> ( ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
76 75 ralbidv 
 |-  ( x = A -> ( A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) <-> A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
77 73 76 anbi12d 
 |-  ( x = A -> ( ( ( abs ` x ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( x + k ) ) ) <-> ( ( abs ` A ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) ) )
78 77 2 elrab2 
 |-  ( A e. U <-> ( A e. CC /\ ( ( abs ` A ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) ) )
79 78 simprbi 
 |-  ( A e. U -> ( ( abs ` A ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
80 4 79 syl 
 |-  ( ph -> ( ( abs ` A ) <_ R /\ A. k e. NN0 ( 1 / R ) <_ ( abs ` ( A + k ) ) ) )
81 80 simpld 
 |-  ( ph -> ( abs ` A ) <_ R )
82 10 11 relogdivd 
 |-  ( ph -> ( log ` ( ( N + 1 ) / N ) ) = ( ( log ` ( N + 1 ) ) - ( log ` N ) ) )
83 logdifbnd 
 |-  ( N e. RR+ -> ( ( log ` ( N + 1 ) ) - ( log ` N ) ) <_ ( 1 / N ) )
84 11 83 syl 
 |-  ( ph -> ( ( log ` ( N + 1 ) ) - ( log ` N ) ) <_ ( 1 / N ) )
85 82 84 eqbrtrd 
 |-  ( ph -> ( log ` ( ( N + 1 ) / N ) ) <_ ( 1 / N ) )
86 13 40 85 abssuble0d 
 |-  ( ph -> ( abs ` ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) = ( ( 1 / N ) - ( log ` ( ( N + 1 ) / N ) ) ) )
87 logdiflbnd 
 |-  ( N e. RR+ -> ( 1 / ( N + 1 ) ) <_ ( ( log ` ( N + 1 ) ) - ( log ` N ) ) )
88 11 87 syl 
 |-  ( ph -> ( 1 / ( N + 1 ) ) <_ ( ( log ` ( N + 1 ) ) - ( log ` N ) ) )
89 88 82 breqtrrd 
 |-  ( ph -> ( 1 / ( N + 1 ) ) <_ ( log ` ( ( N + 1 ) / N ) ) )
90 41 13 40 89 lesub2dd 
 |-  ( ph -> ( ( 1 / N ) - ( log ` ( ( N + 1 ) / N ) ) ) <_ ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) )
91 86 90 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) <_ ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) )
92 68 30 69 42 70 71 81 91 lemul12ad 
 |-  ( ph -> ( ( abs ` A ) x. ( abs ` ( ( log ` ( ( N + 1 ) / N ) ) - ( 1 / N ) ) ) ) <_ ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) )
93 67 92 eqbrtrd 
 |-  ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) <_ ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) )
94 1 2 3 4 5 lgamgulmlem2 
 |-  ( ph -> ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) <_ ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )
95 26 28 43 57 93 94 le2addd 
 |-  ( ph -> ( ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) + ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) ) <_ ( ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) + ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) )
96 16 48 subcld 
 |-  ( ph -> ( N - R ) e. CC )
97 16 19 addcld 
 |-  ( ph -> ( N + 1 ) e. CC )
98 30 51 gtned 
 |-  ( ph -> N =/= R )
99 16 48 98 subne0d 
 |-  ( ph -> ( N - R ) =/= 0 )
100 9 nnne0d 
 |-  ( ph -> ( N + 1 ) =/= 0 )
101 96 97 99 100 subrecd 
 |-  ( ph -> ( ( 1 / ( N - R ) ) - ( 1 / ( N + 1 ) ) ) = ( ( ( N + 1 ) - ( N - R ) ) / ( ( N - R ) x. ( N + 1 ) ) ) )
102 16 19 48 pnncand 
 |-  ( ph -> ( ( N + 1 ) - ( N - R ) ) = ( 1 + R ) )
103 19 48 102 comraddd 
 |-  ( ph -> ( ( N + 1 ) - ( N - R ) ) = ( R + 1 ) )
104 103 oveq1d 
 |-  ( ph -> ( ( ( N + 1 ) - ( N - R ) ) / ( ( N - R ) x. ( N + 1 ) ) ) = ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) )
105 101 104 eqtr2d 
 |-  ( ph -> ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) = ( ( 1 / ( N - R ) ) - ( 1 / ( N + 1 ) ) ) )
106 105 oveq2d 
 |-  ( ph -> ( R x. ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) ) = ( R x. ( ( 1 / ( N - R ) ) - ( 1 / ( N + 1 ) ) ) ) )
107 97 100 reccld 
 |-  ( ph -> ( 1 / ( N + 1 ) ) e. CC )
108 96 99 reccld 
 |-  ( ph -> ( 1 / ( N - R ) ) e. CC )
109 61 107 108 npncan3d 
 |-  ( ph -> ( ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) + ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) = ( ( 1 / ( N - R ) ) - ( 1 / ( N + 1 ) ) ) )
110 109 eqcomd 
 |-  ( ph -> ( ( 1 / ( N - R ) ) - ( 1 / ( N + 1 ) ) ) = ( ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) + ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) )
111 110 oveq2d 
 |-  ( ph -> ( R x. ( ( 1 / ( N - R ) ) - ( 1 / ( N + 1 ) ) ) ) = ( R x. ( ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) + ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) )
112 42 recnd 
 |-  ( ph -> ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) e. CC )
113 56 recnd 
 |-  ( ph -> ( ( 1 / ( N - R ) ) - ( 1 / N ) ) e. CC )
114 48 112 113 adddid 
 |-  ( ph -> ( R x. ( ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) + ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) = ( ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) + ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) )
115 106 111 114 3eqtrd 
 |-  ( ph -> ( R x. ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) ) = ( ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) + ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) )
116 54 10 rpmulcld 
 |-  ( ph -> ( ( N - R ) x. ( N + 1 ) ) e. RR+ )
117 34 116 rerpdivcld 
 |-  ( ph -> ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) e. RR )
118 46 rpge0d 
 |-  ( ph -> 0 <_ R )
119 2z 
 |-  2 e. ZZ
120 119 a1i 
 |-  ( ph -> 2 e. ZZ )
121 11 120 rpexpcld 
 |-  ( ph -> ( N ^ 2 ) e. RR+ )
122 121 rphalfcld 
 |-  ( ph -> ( ( N ^ 2 ) / 2 ) e. RR+ )
123 0le1 
 |-  0 <_ 1
124 123 a1i 
 |-  ( ph -> 0 <_ 1 )
125 30 33 118 124 addge0d 
 |-  ( ph -> 0 <_ ( R + 1 ) )
126 16 sqvald 
 |-  ( ph -> ( N ^ 2 ) = ( N x. N ) )
127 126 oveq1d 
 |-  ( ph -> ( ( N ^ 2 ) / 2 ) = ( ( N x. N ) / 2 ) )
128 32 recnd 
 |-  ( ph -> 2 e. CC )
129 2ne0 
 |-  2 =/= 0
130 129 a1i 
 |-  ( ph -> 2 =/= 0 )
131 16 16 128 130 div23d 
 |-  ( ph -> ( ( N x. N ) / 2 ) = ( ( N / 2 ) x. N ) )
132 127 131 eqtrd 
 |-  ( ph -> ( ( N ^ 2 ) / 2 ) = ( ( N / 2 ) x. N ) )
133 45 rehalfcld 
 |-  ( ph -> ( N / 2 ) e. RR )
134 45 30 resubcld 
 |-  ( ph -> ( N - R ) e. RR )
135 45 33 readdcld 
 |-  ( ph -> ( N + 1 ) e. RR )
136 2rp 
 |-  2 e. RR+
137 136 a1i 
 |-  ( ph -> 2 e. RR+ )
138 11 rpge0d 
 |-  ( ph -> 0 <_ N )
139 45 137 138 divge0d 
 |-  ( ph -> 0 <_ ( N / 2 ) )
140 30 45 137 lemuldiv2d 
 |-  ( ph -> ( ( 2 x. R ) <_ N <-> R <_ ( N / 2 ) ) )
141 5 140 mpbid 
 |-  ( ph -> R <_ ( N / 2 ) )
142 16 2halvesd 
 |-  ( ph -> ( ( N / 2 ) + ( N / 2 ) ) = N )
143 133 recnd 
 |-  ( ph -> ( N / 2 ) e. CC )
144 16 143 143 subaddd 
 |-  ( ph -> ( ( N - ( N / 2 ) ) = ( N / 2 ) <-> ( ( N / 2 ) + ( N / 2 ) ) = N ) )
145 142 144 mpbird 
 |-  ( ph -> ( N - ( N / 2 ) ) = ( N / 2 ) )
146 141 145 breqtrrd 
 |-  ( ph -> R <_ ( N - ( N / 2 ) ) )
147 30 45 133 146 lesubd 
 |-  ( ph -> ( N / 2 ) <_ ( N - R ) )
148 45 lep1d 
 |-  ( ph -> N <_ ( N + 1 ) )
149 133 134 45 135 139 138 147 148 lemul12ad 
 |-  ( ph -> ( ( N / 2 ) x. N ) <_ ( ( N - R ) x. ( N + 1 ) ) )
150 132 149 eqbrtrd 
 |-  ( ph -> ( ( N ^ 2 ) / 2 ) <_ ( ( N - R ) x. ( N + 1 ) ) )
151 122 116 34 125 150 lediv2ad 
 |-  ( ph -> ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) <_ ( ( R + 1 ) / ( ( N ^ 2 ) / 2 ) ) )
152 1 peano2nnd 
 |-  ( ph -> ( R + 1 ) e. NN )
153 152 nncnd 
 |-  ( ph -> ( R + 1 ) e. CC )
154 36 nncnd 
 |-  ( ph -> ( N ^ 2 ) e. CC )
155 36 nnne0d 
 |-  ( ph -> ( N ^ 2 ) =/= 0 )
156 153 154 128 155 130 divdiv2d 
 |-  ( ph -> ( ( R + 1 ) / ( ( N ^ 2 ) / 2 ) ) = ( ( ( R + 1 ) x. 2 ) / ( N ^ 2 ) ) )
157 153 128 mulcomd 
 |-  ( ph -> ( ( R + 1 ) x. 2 ) = ( 2 x. ( R + 1 ) ) )
158 157 oveq1d 
 |-  ( ph -> ( ( ( R + 1 ) x. 2 ) / ( N ^ 2 ) ) = ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) )
159 156 158 eqtr2d 
 |-  ( ph -> ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) = ( ( R + 1 ) / ( ( N ^ 2 ) / 2 ) ) )
160 151 159 breqtrrd 
 |-  ( ph -> ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) <_ ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) )
161 117 37 30 118 160 lemul2ad 
 |-  ( ph -> ( R x. ( ( R + 1 ) / ( ( N - R ) x. ( N + 1 ) ) ) ) <_ ( R x. ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) ) )
162 115 161 eqbrtrrd 
 |-  ( ph -> ( ( R x. ( ( 1 / N ) - ( 1 / ( N + 1 ) ) ) ) + ( R x. ( ( 1 / ( N - R ) ) - ( 1 / N ) ) ) ) <_ ( R x. ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) ) )
163 29 58 38 95 162 letrd 
 |-  ( ph -> ( ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( A / N ) ) ) + ( abs ` ( ( A / N ) - ( log ` ( ( A / N ) + 1 ) ) ) ) ) <_ ( R x. ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) ) )
164 24 29 38 39 163 letrd 
 |-  ( ph -> ( abs ` ( ( A x. ( log ` ( ( N + 1 ) / N ) ) ) - ( log ` ( ( A / N ) + 1 ) ) ) ) <_ ( R x. ( ( 2 x. ( R + 1 ) ) / ( N ^ 2 ) ) ) )