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 ) ) )