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 e. RR /\ 8 <_ N ) -> ( ( log ` ( 2 x. M ) ) / ( 2 x. M ) ) < ( 2 x. ( ( log ` N ) / N ) ) )

Proof

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