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 ⊢ 𝑀 = ( ⌊ ‘ ( 𝑁 / 2 ) )
Assertion chebbnd1lem2 ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )

Proof

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