Metamath Proof Explorer


Theorem chebbnd1lem3

Description: Lemma for chebbnd1 : get a lower bound on ppi ( N ) / ( N / log ( N ) ) that is independent of N . (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Hypothesis chebbnd1lem2.1
|- M = ( |_ ` ( N / 2 ) )
Assertion chebbnd1lem3
|- ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) < ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) )

Proof

Step Hyp Ref Expression
1 chebbnd1lem2.1
 |-  M = ( |_ ` ( N / 2 ) )
2 2rp
 |-  2 e. RR+
3 relogcl
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
4 2 3 ax-mp
 |-  ( log ` 2 ) e. RR
5 1re
 |-  1 e. RR
6 2re
 |-  2 e. RR
7 ere
 |-  _e e. RR
8 6 7 remulcli
 |-  ( 2 x. _e ) e. RR
9 2pos
 |-  0 < 2
10 epos
 |-  0 < _e
11 6 7 9 10 mulgt0ii
 |-  0 < ( 2 x. _e )
12 8 11 gt0ne0ii
 |-  ( 2 x. _e ) =/= 0
13 5 8 12 redivcli
 |-  ( 1 / ( 2 x. _e ) ) e. RR
14 4 13 resubcli
 |-  ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. RR
15 2ne0
 |-  2 =/= 0
16 14 6 15 redivcli
 |-  ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) e. RR
17 16 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) e. RR )
18 6 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 2 e. RR )
19 8re
 |-  8 e. RR
20 19 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 8 e. RR )
21 simpl
 |-  ( ( N e. RR /\ 8 <_ N ) -> N e. RR )
22 2lt8
 |-  2 < 8
23 6 19 22 ltleii
 |-  2 <_ 8
24 23 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 2 <_ 8 )
25 simpr
 |-  ( ( N e. RR /\ 8 <_ N ) -> 8 <_ N )
26 18 20 21 24 25 letrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> 2 <_ N )
27 ppinncl
 |-  ( ( N e. RR /\ 2 <_ N ) -> ( ppi ` N ) e. NN )
28 26 27 syldan
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ppi ` N ) e. NN )
29 28 nnred
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ppi ` N ) e. RR )
30 rehalfcl
 |-  ( N e. RR -> ( N / 2 ) e. RR )
31 30 adantr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( N / 2 ) e. RR )
32 31 flcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( |_ ` ( N / 2 ) ) e. ZZ )
33 1 32 eqeltrid
 |-  ( ( N e. RR /\ 8 <_ N ) -> M e. ZZ )
34 33 zred
 |-  ( ( N e. RR /\ 8 <_ N ) -> M e. RR )
35 remulcl
 |-  ( ( 2 e. RR /\ M e. RR ) -> ( 2 x. M ) e. RR )
36 6 34 35 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. M ) e. RR )
37 5 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 1 e. RR )
38 1lt2
 |-  1 < 2
39 38 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 1 < 2 )
40 2t1e2
 |-  ( 2 x. 1 ) = 2
41 4nn
 |-  4 e. NN
42 4z
 |-  4 e. ZZ
43 42 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 4 e. ZZ )
44 4t2e8
 |-  ( 4 x. 2 ) = 8
45 44 25 eqbrtrid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 4 x. 2 ) <_ N )
46 4re
 |-  4 e. RR
47 46 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 4 e. RR )
48 9 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 0 < 2 )
49 lemuldiv
 |-  ( ( 4 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 4 x. 2 ) <_ N <-> 4 <_ ( N / 2 ) ) )
50 47 21 18 48 49 syl112anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( 4 x. 2 ) <_ N <-> 4 <_ ( N / 2 ) ) )
51 45 50 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> 4 <_ ( N / 2 ) )
52 flge
 |-  ( ( ( N / 2 ) e. RR /\ 4 e. ZZ ) -> ( 4 <_ ( N / 2 ) <-> 4 <_ ( |_ ` ( N / 2 ) ) ) )
53 31 42 52 sylancl
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 4 <_ ( N / 2 ) <-> 4 <_ ( |_ ` ( N / 2 ) ) ) )
54 51 53 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> 4 <_ ( |_ ` ( N / 2 ) ) )
55 54 1 breqtrrdi
 |-  ( ( N e. RR /\ 8 <_ N ) -> 4 <_ M )
56 eluz2
 |-  ( M e. ( ZZ>= ` 4 ) <-> ( 4 e. ZZ /\ M e. ZZ /\ 4 <_ M ) )
57 43 33 55 56 syl3anbrc
 |-  ( ( N e. RR /\ 8 <_ N ) -> M e. ( ZZ>= ` 4 ) )
58 eluznn
 |-  ( ( 4 e. NN /\ M e. ( ZZ>= ` 4 ) ) -> M e. NN )
59 41 57 58 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> M e. NN )
60 59 nnge1d
 |-  ( ( N e. RR /\ 8 <_ N ) -> 1 <_ M )
61 lemul2
 |-  ( ( 1 e. RR /\ M e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 1 <_ M <-> ( 2 x. 1 ) <_ ( 2 x. M ) ) )
62 37 34 18 48 61 syl112anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 1 <_ M <-> ( 2 x. 1 ) <_ ( 2 x. M ) ) )
63 60 62 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. 1 ) <_ ( 2 x. M ) )
64 40 63 eqbrtrrid
 |-  ( ( N e. RR /\ 8 <_ N ) -> 2 <_ ( 2 x. M ) )
65 37 18 36 39 64 ltletrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> 1 < ( 2 x. M ) )
66 36 65 rplogcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( 2 x. M ) ) e. RR+ )
67 66 rpred
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( 2 x. M ) ) e. RR )
68 2nn
 |-  2 e. NN
69 nnmulcl
 |-  ( ( 2 e. NN /\ M e. NN ) -> ( 2 x. M ) e. NN )
70 68 59 69 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. M ) e. NN )
71 67 70 nndivred
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) e. RR )
72 29 71 remulcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) e. RR )
73 rehalfcl
 |-  ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) e. RR -> ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) e. RR )
74 72 73 syl
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) e. RR )
75 0red
 |-  ( ( N e. RR /\ 8 <_ N ) -> 0 e. RR )
76 8pos
 |-  0 < 8
77 76 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 0 < 8 )
78 75 20 21 77 25 ltletrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> 0 < N )
79 21 78 elrpd
 |-  ( ( N e. RR /\ 8 <_ N ) -> N e. RR+ )
80 79 relogcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` N ) e. RR )
81 80 79 rerpdivcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` N ) / N ) e. RR )
82 29 81 remulcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) e. RR )
83 14 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. RR )
84 ppinncl
 |-  ( ( ( 2 x. M ) e. RR /\ 2 <_ ( 2 x. M ) ) -> ( ppi ` ( 2 x. M ) ) e. NN )
85 36 64 84 syl2anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ppi ` ( 2 x. M ) ) e. NN )
86 85 nnred
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ppi ` ( 2 x. M ) ) e. RR )
87 86 71 remulcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` ( 2 x. M ) ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) e. RR )
88 remulcl
 |-  ( ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. RR /\ ( 2 x. M ) e. RR ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) x. ( 2 x. M ) ) e. RR )
89 14 36 88 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) x. ( 2 x. M ) ) e. RR )
90 4pos
 |-  0 < 4
91 46 90 elrpii
 |-  4 e. RR+
92 rpexpcl
 |-  ( ( 4 e. RR+ /\ M e. ZZ ) -> ( 4 ^ M ) e. RR+ )
93 91 33 92 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 4 ^ M ) e. RR+ )
94 59 nnrpd
 |-  ( ( N e. RR /\ 8 <_ N ) -> M e. RR+ )
95 93 94 rpdivcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( 4 ^ M ) / M ) e. RR+ )
96 95 relogcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( ( 4 ^ M ) / M ) ) e. RR )
97 86 67 remulcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) e. RR )
98 94 relogcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` M ) e. RR )
99 epr
 |-  _e e. RR+
100 rerpdivcl
 |-  ( ( M e. RR /\ _e e. RR+ ) -> ( M / _e ) e. RR )
101 34 99 100 sylancl
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( M / _e ) e. RR )
102 93 relogcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( 4 ^ M ) ) e. RR )
103 7 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> _e e. RR )
104 egt2lt3
 |-  ( 2 < _e /\ _e < 3 )
105 104 simpri
 |-  _e < 3
106 3lt4
 |-  3 < 4
107 3re
 |-  3 e. RR
108 7 107 46 lttri
 |-  ( ( _e < 3 /\ 3 < 4 ) -> _e < 4 )
109 105 106 108 mp2an
 |-  _e < 4
110 109 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> _e < 4 )
111 103 47 34 110 55 ltletrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> _e < M )
112 103 34 111 ltled
 |-  ( ( N e. RR /\ 8 <_ N ) -> _e <_ M )
113 7 leidi
 |-  _e <_ _e
114 logdivlt
 |-  ( ( ( _e e. RR /\ _e <_ _e ) /\ ( M e. RR /\ _e <_ M ) ) -> ( _e < M <-> ( ( log ` M ) / M ) < ( ( log ` _e ) / _e ) ) )
115 7 113 114 mpanl12
 |-  ( ( M e. RR /\ _e <_ M ) -> ( _e < M <-> ( ( log ` M ) / M ) < ( ( log ` _e ) / _e ) ) )
116 34 112 115 syl2anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( _e < M <-> ( ( log ` M ) / M ) < ( ( log ` _e ) / _e ) ) )
117 111 116 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` M ) / M ) < ( ( log ` _e ) / _e ) )
118 loge
 |-  ( log ` _e ) = 1
119 118 oveq1i
 |-  ( ( log ` _e ) / _e ) = ( 1 / _e )
120 117 119 breqtrdi
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` M ) / M ) < ( 1 / _e ) )
121 7 10 pm3.2i
 |-  ( _e e. RR /\ 0 < _e )
122 121 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( _e e. RR /\ 0 < _e ) )
123 59 nngt0d
 |-  ( ( N e. RR /\ 8 <_ N ) -> 0 < M )
124 34 123 jca
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( M e. RR /\ 0 < M ) )
125 lt2mul2div
 |-  ( ( ( ( log ` M ) e. RR /\ ( _e e. RR /\ 0 < _e ) ) /\ ( 1 e. RR /\ ( M e. RR /\ 0 < M ) ) ) -> ( ( ( log ` M ) x. _e ) < ( 1 x. M ) <-> ( ( log ` M ) / M ) < ( 1 / _e ) ) )
126 98 122 37 124 125 syl22anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` M ) x. _e ) < ( 1 x. M ) <-> ( ( log ` M ) / M ) < ( 1 / _e ) ) )
127 120 126 mpbird
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` M ) x. _e ) < ( 1 x. M ) )
128 34 recnd
 |-  ( ( N e. RR /\ 8 <_ N ) -> M e. CC )
129 128 mulid2d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 1 x. M ) = M )
130 127 129 breqtrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` M ) x. _e ) < M )
131 ltmuldiv
 |-  ( ( ( log ` M ) e. RR /\ M e. RR /\ ( _e e. RR /\ 0 < _e ) ) -> ( ( ( log ` M ) x. _e ) < M <-> ( log ` M ) < ( M / _e ) ) )
132 98 34 122 131 syl3anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` M ) x. _e ) < M <-> ( log ` M ) < ( M / _e ) ) )
133 130 132 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` M ) < ( M / _e ) )
134 98 101 102 133 ltsub2dd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` ( 4 ^ M ) ) - ( M / _e ) ) < ( ( log ` ( 4 ^ M ) ) - ( log ` M ) ) )
135 4 recni
 |-  ( log ` 2 ) e. CC
136 135 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` 2 ) e. CC )
137 13 recni
 |-  ( 1 / ( 2 x. _e ) ) e. CC
138 137 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 1 / ( 2 x. _e ) ) e. CC )
139 70 nnrpd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. M ) e. RR+ )
140 139 rpcnd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. M ) e. CC )
141 136 138 140 subdird
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) x. ( 2 x. M ) ) = ( ( ( log ` 2 ) x. ( 2 x. M ) ) - ( ( 1 / ( 2 x. _e ) ) x. ( 2 x. M ) ) ) )
142 136 140 mulcomd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` 2 ) x. ( 2 x. M ) ) = ( ( 2 x. M ) x. ( log ` 2 ) ) )
143 2z
 |-  2 e. ZZ
144 zmulcl
 |-  ( ( 2 e. ZZ /\ M e. ZZ ) -> ( 2 x. M ) e. ZZ )
145 143 33 144 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. M ) e. ZZ )
146 relogexp
 |-  ( ( 2 e. RR+ /\ ( 2 x. M ) e. ZZ ) -> ( log ` ( 2 ^ ( 2 x. M ) ) ) = ( ( 2 x. M ) x. ( log ` 2 ) ) )
147 2 145 146 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( 2 ^ ( 2 x. M ) ) ) = ( ( 2 x. M ) x. ( log ` 2 ) ) )
148 2cnd
 |-  ( ( N e. RR /\ 8 <_ N ) -> 2 e. CC )
149 59 nnnn0d
 |-  ( ( N e. RR /\ 8 <_ N ) -> M e. NN0 )
150 2nn0
 |-  2 e. NN0
151 150 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 2 e. NN0 )
152 148 149 151 expmuld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 ^ ( 2 x. M ) ) = ( ( 2 ^ 2 ) ^ M ) )
153 sq2
 |-  ( 2 ^ 2 ) = 4
154 153 oveq1i
 |-  ( ( 2 ^ 2 ) ^ M ) = ( 4 ^ M )
155 152 154 eqtrdi
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 ^ ( 2 x. M ) ) = ( 4 ^ M ) )
156 155 fveq2d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( 2 ^ ( 2 x. M ) ) ) = ( log ` ( 4 ^ M ) ) )
157 142 147 156 3eqtr2d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` 2 ) x. ( 2 x. M ) ) = ( log ` ( 4 ^ M ) ) )
158 8 recni
 |-  ( 2 x. _e ) e. CC
159 158 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. _e ) e. CC )
160 12 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. _e ) =/= 0 )
161 140 159 160 divrec2d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( 2 x. M ) / ( 2 x. _e ) ) = ( ( 1 / ( 2 x. _e ) ) x. ( 2 x. M ) ) )
162 7 recni
 |-  _e e. CC
163 162 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> _e e. CC )
164 7 10 gt0ne0ii
 |-  _e =/= 0
165 164 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> _e =/= 0 )
166 15 a1i
 |-  ( ( N e. RR /\ 8 <_ N ) -> 2 =/= 0 )
167 128 163 148 165 166 divcan5d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( 2 x. M ) / ( 2 x. _e ) ) = ( M / _e ) )
168 161 167 eqtr3d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( 1 / ( 2 x. _e ) ) x. ( 2 x. M ) ) = ( M / _e ) )
169 157 168 oveq12d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) x. ( 2 x. M ) ) - ( ( 1 / ( 2 x. _e ) ) x. ( 2 x. M ) ) ) = ( ( log ` ( 4 ^ M ) ) - ( M / _e ) ) )
170 141 169 eqtrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) x. ( 2 x. M ) ) = ( ( log ` ( 4 ^ M ) ) - ( M / _e ) ) )
171 93 94 relogdivd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( ( 4 ^ M ) / M ) ) = ( ( log ` ( 4 ^ M ) ) - ( log ` M ) ) )
172 134 170 171 3brtr4d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) x. ( 2 x. M ) ) < ( log ` ( ( 4 ^ M ) / M ) ) )
173 eqid
 |-  if ( ( 2 x. M ) <_ ( ( 2 x. M ) _C M ) , ( 2 x. M ) , ( ( 2 x. M ) _C M ) ) = if ( ( 2 x. M ) <_ ( ( 2 x. M ) _C M ) , ( 2 x. M ) , ( ( 2 x. M ) _C M ) )
174 173 chebbnd1lem1
 |-  ( M e. ( ZZ>= ` 4 ) -> ( log ` ( ( 4 ^ M ) / M ) ) < ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) )
175 57 174 syl
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( ( 4 ^ M ) / M ) ) < ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) )
176 89 96 97 172 175 lttrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) x. ( 2 x. M ) ) < ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) )
177 83 97 139 ltmuldivd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) x. ( 2 x. M ) ) < ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) <-> ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) < ( ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) / ( 2 x. M ) ) ) )
178 176 177 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) < ( ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) / ( 2 x. M ) ) )
179 86 recnd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ppi ` ( 2 x. M ) ) e. CC )
180 66 rpcnd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( log ` ( 2 x. M ) ) e. CC )
181 139 rpcnne0d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( 2 x. M ) e. CC /\ ( 2 x. M ) =/= 0 ) )
182 divass
 |-  ( ( ( ppi ` ( 2 x. M ) ) e. CC /\ ( log ` ( 2 x. M ) ) e. CC /\ ( ( 2 x. M ) e. CC /\ ( 2 x. M ) =/= 0 ) ) -> ( ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) / ( 2 x. M ) ) = ( ( ppi ` ( 2 x. M ) ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) )
183 179 180 181 182 syl3anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( ppi ` ( 2 x. M ) ) x. ( log ` ( 2 x. M ) ) ) / ( 2 x. M ) ) = ( ( ppi ` ( 2 x. M ) ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) )
184 178 183 breqtrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) < ( ( ppi ` ( 2 x. M ) ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) )
185 flle
 |-  ( ( N / 2 ) e. RR -> ( |_ ` ( N / 2 ) ) <_ ( N / 2 ) )
186 31 185 syl
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( |_ ` ( N / 2 ) ) <_ ( N / 2 ) )
187 1 186 eqbrtrid
 |-  ( ( N e. RR /\ 8 <_ N ) -> M <_ ( N / 2 ) )
188 lemuldiv2
 |-  ( ( M e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. M ) <_ N <-> M <_ ( N / 2 ) ) )
189 34 21 18 48 188 syl112anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( 2 x. M ) <_ N <-> M <_ ( N / 2 ) ) )
190 187 189 mpbird
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. M ) <_ N )
191 ppiwordi
 |-  ( ( ( 2 x. M ) e. RR /\ N e. RR /\ ( 2 x. M ) <_ N ) -> ( ppi ` ( 2 x. M ) ) <_ ( ppi ` N ) )
192 36 21 190 191 syl3anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ppi ` ( 2 x. M ) ) <_ ( ppi ` N ) )
193 66 139 rpdivcld
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) e. RR+ )
194 86 29 193 lemul1d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` ( 2 x. M ) ) <_ ( ppi ` N ) <-> ( ( ppi ` ( 2 x. M ) ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) <_ ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) ) )
195 192 194 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` ( 2 x. M ) ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) <_ ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) )
196 83 87 72 184 195 ltletrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) < ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) )
197 ltdiv1
 |-  ( ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. RR /\ ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) < ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) <-> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) < ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) ) )
198 83 72 18 48 197 syl112anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) < ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) <-> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) < ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) ) )
199 196 198 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) < ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) )
200 1 chebbnd1lem2
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) < ( 2 x. ( ( log ` N ) / N ) ) )
201 remulcl
 |-  ( ( 2 e. RR /\ ( ( log ` N ) / N ) e. RR ) -> ( 2 x. ( ( log ` N ) / N ) ) e. RR )
202 6 81 201 sylancr
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( 2 x. ( ( log ` N ) / N ) ) e. RR )
203 28 nngt0d
 |-  ( ( N e. RR /\ 8 <_ N ) -> 0 < ( ppi ` N ) )
204 ltmul2
 |-  ( ( ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) e. RR /\ ( 2 x. ( ( log ` N ) / N ) ) e. RR /\ ( ( ppi ` N ) e. RR /\ 0 < ( ppi ` N ) ) ) -> ( ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) < ( 2 x. ( ( log ` N ) / N ) ) <-> ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) < ( ( ppi ` N ) x. ( 2 x. ( ( log ` N ) / N ) ) ) ) )
205 71 202 29 203 204 syl112anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) < ( 2 x. ( ( log ` N ) / N ) ) <-> ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) < ( ( ppi ` N ) x. ( 2 x. ( ( log ` N ) / N ) ) ) ) )
206 200 205 mpbid
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) < ( ( ppi ` N ) x. ( 2 x. ( ( log ` N ) / N ) ) ) )
207 29 recnd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ppi ` N ) e. CC )
208 81 recnd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( log ` N ) / N ) e. CC )
209 207 148 208 mul12d
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` N ) x. ( 2 x. ( ( log ` N ) / N ) ) ) = ( 2 x. ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) ) )
210 206 209 breqtrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) < ( 2 x. ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) ) )
211 ltdivmul
 |-  ( ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) e. RR /\ ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) < ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) <-> ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) < ( 2 x. ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) ) ) )
212 72 82 18 48 211 syl112anc
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) < ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) <-> ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) < ( 2 x. ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) ) ) )
213 210 212 mpbird
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( ppi ` N ) x. ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) ) / 2 ) < ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) )
214 17 74 82 199 213 lttrd
 |-  ( ( N e. RR /\ 8 <_ N ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) < ( ( ppi ` N ) x. ( ( log ` N ) / N ) ) )