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=N2
Assertion chebbnd1lem2 N8Nlog2 M2 M<2logNN

Proof

Step Hyp Ref Expression
1 chebbnd1lem2.1 M=N2
2 2rp 2+
3 4nn 4
4 4z 4
5 4 a1i N8N4
6 rehalfcl NN2
7 6 adantr N8NN2
8 7 flcld N8NN2
9 1 8 eqeltrid N8NM
10 4t2e8 42=8
11 simpr N8N8N
12 10 11 eqbrtrid N8N42N
13 4re 4
14 13 a1i N8N4
15 simpl N8NN
16 2re 2
17 16 a1i N8N2
18 2pos 0<2
19 18 a1i N8N0<2
20 lemuldiv 4N20<242N4N2
21 14 15 17 19 20 syl112anc N8N42N4N2
22 12 21 mpbid N8N4N2
23 flge N244N24N2
24 7 4 23 sylancl N8N4N24N2
25 22 24 mpbid N8N4N2
26 25 1 breqtrrdi N8N4M
27 eluz2 M44M4M
28 5 9 26 27 syl3anbrc N8NM4
29 eluznn 4M4M
30 3 28 29 sylancr N8NM
31 30 nnrpd N8NM+
32 rpmulcl 2+M+2 M+
33 2 31 32 sylancr N8N2 M+
34 33 relogcld N8Nlog2 M
35 34 33 rerpdivcld N8Nlog2 M2 M
36 0red N8N0
37 8re 8
38 37 a1i N8N8
39 8pos 0<8
40 39 a1i N8N0<8
41 36 38 15 40 11 ltletrd N8N0<N
42 15 41 elrpd N8NN+
43 42 rphalfcld N8NN2+
44 43 relogcld N8NlogN2
45 44 43 rerpdivcld N8NlogN2N2
46 42 relogcld N8NlogN
47 46 42 rerpdivcld N8NlogNN
48 remulcl 2logNN2logNN
49 16 47 48 sylancr N8N2logNN
50 9 zred N8NM
51 peano2re MM+1
52 50 51 syl N8NM+1
53 remulcl 2M2 M
54 16 50 53 sylancr N8N2 M
55 flltp1 N2N2<N2+1
56 7 55 syl N8NN2<N2+1
57 1 oveq1i M+1=N2+1
58 56 57 breqtrrdi N8NN2<M+1
59 1red N8N1
60 30 nnge1d N8N1M
61 59 50 50 60 leadd2dd N8NM+1M+M
62 50 recnd N8NM
63 62 2timesd N8N2 M=M+M
64 61 63 breqtrrd N8NM+12 M
65 7 52 54 58 64 ltletrd N8NN2<2 M
66 ere e
67 66 a1i N8Ne
68 egt2lt3 2<ee<3
69 68 simpri e<3
70 3lt4 3<4
71 3re 3
72 66 71 13 lttri e<33<4e<4
73 69 70 72 mp2an e<4
74 73 a1i N8Ne<4
75 67 14 7 74 22 ltletrd N8Ne<N2
76 67 7 75 ltled N8NeN2
77 67 7 54 75 65 lttrd N8Ne<2 M
78 67 54 77 ltled N8Ne2 M
79 logdivlt N2eN22 Me2 MN2<2 Mlog2 M2 M<logN2N2
80 7 76 54 78 79 syl22anc N8NN2<2 Mlog2 M2 M<logN2N2
81 65 80 mpbid N8Nlog2 M2 M<logN2N2
82 rphalflt N+N2<N
83 42 82 syl N8NN2<N
84 logltb N2+N+N2<NlogN2<logN
85 43 42 84 syl2anc N8NN2<NlogN2<logN
86 83 85 mpbid N8NlogN2<logN
87 44 46 43 86 ltdiv1dd N8NlogN2N2<logNN2
88 46 recnd N8NlogN
89 15 recnd N8NN
90 17 recnd N8N2
91 42 rpne0d N8NN0
92 2ne0 20
93 92 a1i N8N20
94 88 89 90 91 93 divdiv2d N8NlogNN2=logN2N
95 88 90 mulcomd N8NlogN2=2logN
96 95 oveq1d N8NlogN2N=2logNN
97 90 88 89 91 divassd N8N2logNN=2logNN
98 94 96 97 3eqtrd N8NlogNN2=2logNN
99 87 98 breqtrd N8NlogN2N2<2logNN
100 35 45 49 81 99 lttrd N8Nlog2 M2 M<2logNN