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