Metamath Proof Explorer


Theorem chebbnd1lem2

Description: Lemma for chebbnd1 : Show that log ( N ) / N does not change too much between N and M = |_ ( N / 2 ) . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypothesis chebbnd1lem2.1 M = N 2
Assertion chebbnd1lem2 N 8 N log 2 M 2 M < 2 log N N

Proof

Step Hyp Ref Expression
1 chebbnd1lem2.1 M = N 2
2 2rp 2 +
3 4nn 4
4 4z 4
5 4 a1i N 8 N 4
6 rehalfcl N N 2
7 6 adantr N 8 N N 2
8 7 flcld N 8 N N 2
9 1 8 eqeltrid N 8 N M
10 4t2e8 4 2 = 8
11 simpr N 8 N 8 N
12 10 11 eqbrtrid N 8 N 4 2 N
13 4re 4
14 13 a1i N 8 N 4
15 simpl N 8 N N
16 2re 2
17 16 a1i N 8 N 2
18 2pos 0 < 2
19 18 a1i N 8 N 0 < 2
20 lemuldiv 4 N 2 0 < 2 4 2 N 4 N 2
21 14 15 17 19 20 syl112anc N 8 N 4 2 N 4 N 2
22 12 21 mpbid N 8 N 4 N 2
23 flge N 2 4 4 N 2 4 N 2
24 7 4 23 sylancl N 8 N 4 N 2 4 N 2
25 22 24 mpbid N 8 N 4 N 2
26 25 1 breqtrrdi N 8 N 4 M
27 eluz2 M 4 4 M 4 M
28 5 9 26 27 syl3anbrc N 8 N M 4
29 eluznn 4 M 4 M
30 3 28 29 sylancr N 8 N M
31 30 nnrpd N 8 N M +
32 rpmulcl 2 + M + 2 M +
33 2 31 32 sylancr N 8 N 2 M +
34 33 relogcld N 8 N log 2 M
35 34 33 rerpdivcld N 8 N log 2 M 2 M
36 0red N 8 N 0
37 8re 8
38 37 a1i N 8 N 8
39 8pos 0 < 8
40 39 a1i N 8 N 0 < 8
41 36 38 15 40 11 ltletrd N 8 N 0 < N
42 15 41 elrpd N 8 N N +
43 42 rphalfcld N 8 N N 2 +
44 43 relogcld N 8 N log N 2
45 44 43 rerpdivcld N 8 N log N 2 N 2
46 42 relogcld N 8 N log N
47 46 42 rerpdivcld N 8 N log N N
48 remulcl 2 log N N 2 log N N
49 16 47 48 sylancr N 8 N 2 log N N
50 9 zred N 8 N M
51 peano2re M M + 1
52 50 51 syl N 8 N M + 1
53 remulcl 2 M 2 M
54 16 50 53 sylancr N 8 N 2 M
55 flltp1 N 2 N 2 < N 2 + 1
56 7 55 syl N 8 N N 2 < N 2 + 1
57 1 oveq1i M + 1 = N 2 + 1
58 56 57 breqtrrdi N 8 N N 2 < M + 1
59 1red N 8 N 1
60 30 nnge1d N 8 N 1 M
61 59 50 50 60 leadd2dd N 8 N M + 1 M + M
62 50 recnd N 8 N M
63 62 2timesd N 8 N 2 M = M + M
64 61 63 breqtrrd N 8 N M + 1 2 M
65 7 52 54 58 64 ltletrd N 8 N N 2 < 2 M
66 ere e
67 66 a1i N 8 N e
68 egt2lt3 2 < e e < 3
69 68 simpri e < 3
70 3lt4 3 < 4
71 3re 3
72 66 71 13 lttri e < 3 3 < 4 e < 4
73 69 70 72 mp2an e < 4
74 73 a1i N 8 N e < 4
75 67 14 7 74 22 ltletrd N 8 N e < N 2
76 67 7 75 ltled N 8 N e N 2
77 67 7 54 75 65 lttrd N 8 N e < 2 M
78 67 54 77 ltled N 8 N e 2 M
79 logdivlt N 2 e N 2 2 M e 2 M N 2 < 2 M log 2 M 2 M < log N 2 N 2
80 7 76 54 78 79 syl22anc N 8 N N 2 < 2 M log 2 M 2 M < log N 2 N 2
81 65 80 mpbid N 8 N log 2 M 2 M < log N 2 N 2
82 rphalflt N + N 2 < N
83 42 82 syl N 8 N N 2 < N
84 logltb N 2 + N + N 2 < N log N 2 < log N
85 43 42 84 syl2anc N 8 N N 2 < N log N 2 < log N
86 83 85 mpbid N 8 N log N 2 < log N
87 44 46 43 86 ltdiv1dd N 8 N log N 2 N 2 < log N N 2
88 46 recnd N 8 N log N
89 15 recnd N 8 N N
90 17 recnd N 8 N 2
91 42 rpne0d N 8 N N 0
92 2ne0 2 0
93 92 a1i N 8 N 2 0
94 88 89 90 91 93 divdiv2d N 8 N log N N 2 = log N 2 N
95 88 90 mulcomd N 8 N log N 2 = 2 log N
96 95 oveq1d N 8 N log N 2 N = 2 log N N
97 90 88 89 91 divassd N 8 N 2 log N N = 2 log N N
98 94 96 97 3eqtrd N 8 N log N N 2 = 2 log N N
99 87 98 breqtrd N 8 N log N 2 N 2 < 2 log N N
100 35 45 49 81 99 lttrd N 8 N log 2 M 2 M < 2 log N N