Metamath Proof Explorer


Theorem chebbnd1lem3

Description: Lemma for chebbnd1 : get a lower bound on ppi ( N ) / ( N / log ( N ) ) that is independent of N . (Contributed by Mario Carneiro, 21-Sep-2014)

Ref Expression
Hypothesis chebbnd1lem2.1 𝑀 = ( ⌊ ‘ ( 𝑁 / 2 ) )
Assertion chebbnd1lem3 ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 chebbnd1lem2.1 𝑀 = ( ⌊ ‘ ( 𝑁 / 2 ) )
2 2rp 2 ∈ ℝ+
3 relogcl ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
4 2 3 ax-mp ( log ‘ 2 ) ∈ ℝ
5 1re 1 ∈ ℝ
6 2re 2 ∈ ℝ
7 ere e ∈ ℝ
8 6 7 remulcli ( 2 · e ) ∈ ℝ
9 2pos 0 < 2
10 epos 0 < e
11 6 7 9 10 mulgt0ii 0 < ( 2 · e )
12 8 11 gt0ne0ii ( 2 · e ) ≠ 0
13 5 8 12 redivcli ( 1 / ( 2 · e ) ) ∈ ℝ
14 4 13 resubcli ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ
15 2ne0 2 ≠ 0
16 14 6 15 redivcli ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) ∈ ℝ
17 16 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) ∈ ℝ )
18 6 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℝ )
19 8re 8 ∈ ℝ
20 19 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 8 ∈ ℝ )
21 simpl ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ∈ ℝ )
22 2lt8 2 < 8
23 6 19 22 ltleii 2 ≤ 8
24 23 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≤ 8 )
25 simpr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 8 ≤ 𝑁 )
26 18 20 21 24 25 letrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≤ 𝑁 )
27 ppinncl ( ( 𝑁 ∈ ℝ ∧ 2 ≤ 𝑁 ) → ( π𝑁 ) ∈ ℕ )
28 26 27 syldan ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π𝑁 ) ∈ ℕ )
29 28 nnred ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π𝑁 ) ∈ ℝ )
30 rehalfcl ( 𝑁 ∈ ℝ → ( 𝑁 / 2 ) ∈ ℝ )
31 30 adantr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑁 / 2 ) ∈ ℝ )
32 31 flcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ∈ ℤ )
33 1 32 eqeltrid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℤ )
34 33 zred ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℝ )
35 remulcl ( ( 2 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 2 · 𝑀 ) ∈ ℝ )
36 6 34 35 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℝ )
37 5 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 ∈ ℝ )
38 1lt2 1 < 2
39 38 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 < 2 )
40 2t1e2 ( 2 · 1 ) = 2
41 4nn 4 ∈ ℕ
42 4z 4 ∈ ℤ
43 42 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ∈ ℤ )
44 4t2e8 ( 4 · 2 ) = 8
45 44 25 eqbrtrid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 · 2 ) ≤ 𝑁 )
46 4re 4 ∈ ℝ
47 46 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ∈ ℝ )
48 9 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 2 )
49 lemuldiv ( ( 4 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 4 · 2 ) ≤ 𝑁 ↔ 4 ≤ ( 𝑁 / 2 ) ) )
50 47 21 18 48 49 syl112anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 4 · 2 ) ≤ 𝑁 ↔ 4 ≤ ( 𝑁 / 2 ) ) )
51 45 50 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ ( 𝑁 / 2 ) )
52 flge ( ( ( 𝑁 / 2 ) ∈ ℝ ∧ 4 ∈ ℤ ) → ( 4 ≤ ( 𝑁 / 2 ) ↔ 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
53 31 42 52 sylancl ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 ≤ ( 𝑁 / 2 ) ↔ 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) ) )
54 51 53 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ ( ⌊ ‘ ( 𝑁 / 2 ) ) )
55 54 1 breqtrrdi ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 4 ≤ 𝑀 )
56 eluz2 ( 𝑀 ∈ ( ℤ ‘ 4 ) ↔ ( 4 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 4 ≤ 𝑀 ) )
57 43 33 55 56 syl3anbrc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ( ℤ ‘ 4 ) )
58 eluznn ( ( 4 ∈ ℕ ∧ 𝑀 ∈ ( ℤ ‘ 4 ) ) → 𝑀 ∈ ℕ )
59 41 57 58 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℕ )
60 59 nnge1d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 ≤ 𝑀 )
61 lemul2 ( ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( 1 ≤ 𝑀 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑀 ) ) )
62 37 34 18 48 61 syl112anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 1 ≤ 𝑀 ↔ ( 2 · 1 ) ≤ ( 2 · 𝑀 ) ) )
63 60 62 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 1 ) ≤ ( 2 · 𝑀 ) )
64 40 63 eqbrtrrid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≤ ( 2 · 𝑀 ) )
65 37 18 36 39 64 ltletrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 1 < ( 2 · 𝑀 ) )
66 36 65 rplogcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 · 𝑀 ) ) ∈ ℝ+ )
67 66 rpred ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 · 𝑀 ) ) ∈ ℝ )
68 2nn 2 ∈ ℕ
69 nnmulcl ( ( 2 ∈ ℕ ∧ 𝑀 ∈ ℕ ) → ( 2 · 𝑀 ) ∈ ℕ )
70 68 59 69 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℕ )
71 67 70 nndivred ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ∈ ℝ )
72 29 71 remulcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ )
73 rehalfcl ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ → ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ∈ ℝ )
74 72 73 syl ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ∈ ℝ )
75 0red ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 ∈ ℝ )
76 8pos 0 < 8
77 76 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 8 )
78 75 20 21 77 25 ltletrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 𝑁 )
79 21 78 elrpd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑁 ∈ ℝ+ )
80 79 relogcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑁 ) ∈ ℝ )
81 80 79 rerpdivcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℝ )
82 29 81 remulcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
83 14 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ )
84 ppinncl ( ( ( 2 · 𝑀 ) ∈ ℝ ∧ 2 ≤ ( 2 · 𝑀 ) ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℕ )
85 36 64 84 syl2anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℕ )
86 85 nnred ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℝ )
87 86 71 remulcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ )
88 remulcl ( ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ ∧ ( 2 · 𝑀 ) ∈ ℝ ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) ∈ ℝ )
89 14 36 88 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) ∈ ℝ )
90 4pos 0 < 4
91 46 90 elrpii 4 ∈ ℝ+
92 rpexpcl ( ( 4 ∈ ℝ+𝑀 ∈ ℤ ) → ( 4 ↑ 𝑀 ) ∈ ℝ+ )
93 91 33 92 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 4 ↑ 𝑀 ) ∈ ℝ+ )
94 59 nnrpd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℝ+ )
95 93 94 rpdivcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 4 ↑ 𝑀 ) / 𝑀 ) ∈ ℝ+ )
96 95 relogcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) ∈ ℝ )
97 86 67 remulcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) ∈ ℝ )
98 94 relogcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑀 ) ∈ ℝ )
99 epr e ∈ ℝ+
100 rerpdivcl ( ( 𝑀 ∈ ℝ ∧ e ∈ ℝ+ ) → ( 𝑀 / e ) ∈ ℝ )
101 34 99 100 sylancl ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑀 / e ) ∈ ℝ )
102 93 relogcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 4 ↑ 𝑀 ) ) ∈ ℝ )
103 7 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ∈ ℝ )
104 egt2lt3 ( 2 < e ∧ e < 3 )
105 104 simpri e < 3
106 3lt4 3 < 4
107 3re 3 ∈ ℝ
108 7 107 46 lttri ( ( e < 3 ∧ 3 < 4 ) → e < 4 )
109 105 106 108 mp2an e < 4
110 109 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e < 4 )
111 103 47 34 110 55 ltletrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e < 𝑀 )
112 103 34 111 ltled ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ≤ 𝑀 )
113 7 leidi e ≤ e
114 logdivlt ( ( ( e ∈ ℝ ∧ e ≤ e ) ∧ ( 𝑀 ∈ ℝ ∧ e ≤ 𝑀 ) ) → ( e < 𝑀 ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) ) )
115 7 113 114 mpanl12 ( ( 𝑀 ∈ ℝ ∧ e ≤ 𝑀 ) → ( e < 𝑀 ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) ) )
116 34 112 115 syl2anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( e < 𝑀 ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) ) )
117 111 116 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) / 𝑀 ) < ( ( log ‘ e ) / e ) )
118 loge ( log ‘ e ) = 1
119 118 oveq1i ( ( log ‘ e ) / e ) = ( 1 / e )
120 117 119 breqtrdi ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) / 𝑀 ) < ( 1 / e ) )
121 7 10 pm3.2i ( e ∈ ℝ ∧ 0 < e )
122 121 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( e ∈ ℝ ∧ 0 < e ) )
123 59 nngt0d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < 𝑀 )
124 34 123 jca ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) )
125 lt2mul2div ( ( ( ( log ‘ 𝑀 ) ∈ ℝ ∧ ( e ∈ ℝ ∧ 0 < e ) ) ∧ ( 1 ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) ) → ( ( ( log ‘ 𝑀 ) · e ) < ( 1 · 𝑀 ) ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( 1 / e ) ) )
126 98 122 37 124 125 syl22anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 𝑀 ) · e ) < ( 1 · 𝑀 ) ↔ ( ( log ‘ 𝑀 ) / 𝑀 ) < ( 1 / e ) ) )
127 120 126 mpbird ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) · e ) < ( 1 · 𝑀 ) )
128 34 recnd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℂ )
129 128 mulid2d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 1 · 𝑀 ) = 𝑀 )
130 127 129 breqtrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑀 ) · e ) < 𝑀 )
131 ltmuldiv ( ( ( log ‘ 𝑀 ) ∈ ℝ ∧ 𝑀 ∈ ℝ ∧ ( e ∈ ℝ ∧ 0 < e ) ) → ( ( ( log ‘ 𝑀 ) · e ) < 𝑀 ↔ ( log ‘ 𝑀 ) < ( 𝑀 / e ) ) )
132 98 34 122 131 syl3anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 𝑀 ) · e ) < 𝑀 ↔ ( log ‘ 𝑀 ) < ( 𝑀 / e ) ) )
133 130 132 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 𝑀 ) < ( 𝑀 / e ) )
134 98 101 102 133 ltsub2dd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( 𝑀 / e ) ) < ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( log ‘ 𝑀 ) ) )
135 4 recni ( log ‘ 2 ) ∈ ℂ
136 135 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ 2 ) ∈ ℂ )
137 13 recni ( 1 / ( 2 · e ) ) ∈ ℂ
138 137 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 1 / ( 2 · e ) ) ∈ ℂ )
139 70 nnrpd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℝ+ )
140 139 rpcnd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℂ )
141 136 138 140 subdird ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) = ( ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) − ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) ) )
142 136 140 mulcomd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) = ( ( 2 · 𝑀 ) · ( log ‘ 2 ) ) )
143 2z 2 ∈ ℤ
144 zmulcl ( ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 2 · 𝑀 ) ∈ ℤ )
145 143 33 144 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ∈ ℤ )
146 relogexp ( ( 2 ∈ ℝ+ ∧ ( 2 · 𝑀 ) ∈ ℤ ) → ( log ‘ ( 2 ↑ ( 2 · 𝑀 ) ) ) = ( ( 2 · 𝑀 ) · ( log ‘ 2 ) ) )
147 2 145 146 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 ↑ ( 2 · 𝑀 ) ) ) = ( ( 2 · 𝑀 ) · ( log ‘ 2 ) ) )
148 2cnd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℂ )
149 59 nnnn0d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ∈ ℕ0 )
150 2nn0 2 ∈ ℕ0
151 150 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ∈ ℕ0 )
152 148 149 151 expmuld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 ↑ ( 2 · 𝑀 ) ) = ( ( 2 ↑ 2 ) ↑ 𝑀 ) )
153 sq2 ( 2 ↑ 2 ) = 4
154 153 oveq1i ( ( 2 ↑ 2 ) ↑ 𝑀 ) = ( 4 ↑ 𝑀 )
155 152 154 eqtrdi ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 ↑ ( 2 · 𝑀 ) ) = ( 4 ↑ 𝑀 ) )
156 155 fveq2d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 ↑ ( 2 · 𝑀 ) ) ) = ( log ‘ ( 4 ↑ 𝑀 ) ) )
157 142 147 156 3eqtr2d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) = ( log ‘ ( 4 ↑ 𝑀 ) ) )
158 8 recni ( 2 · e ) ∈ ℂ
159 158 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · e ) ∈ ℂ )
160 12 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · e ) ≠ 0 )
161 140 159 160 divrec2d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) / ( 2 · e ) ) = ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) )
162 7 recni e ∈ ℂ
163 162 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ∈ ℂ )
164 7 10 gt0ne0ii e ≠ 0
165 164 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → e ≠ 0 )
166 15 a1i ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 2 ≠ 0 )
167 128 163 148 165 166 divcan5d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) / ( 2 · e ) ) = ( 𝑀 / e ) )
168 161 167 eqtr3d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) = ( 𝑀 / e ) )
169 157 168 oveq12d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) · ( 2 · 𝑀 ) ) − ( ( 1 / ( 2 · e ) ) · ( 2 · 𝑀 ) ) ) = ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( 𝑀 / e ) ) )
170 141 169 eqtrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) = ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( 𝑀 / e ) ) )
171 93 94 relogdivd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) = ( ( log ‘ ( 4 ↑ 𝑀 ) ) − ( log ‘ 𝑀 ) ) )
172 134 170 171 3brtr4d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) < ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) )
173 eqid if ( ( 2 · 𝑀 ) ≤ ( ( 2 · 𝑀 ) C 𝑀 ) , ( 2 · 𝑀 ) , ( ( 2 · 𝑀 ) C 𝑀 ) ) = if ( ( 2 · 𝑀 ) ≤ ( ( 2 · 𝑀 ) C 𝑀 ) , ( 2 · 𝑀 ) , ( ( 2 · 𝑀 ) C 𝑀 ) )
174 173 chebbnd1lem1 ( 𝑀 ∈ ( ℤ ‘ 4 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) )
175 57 174 syl ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( ( 4 ↑ 𝑀 ) / 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) )
176 89 96 97 172 175 lttrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) )
177 83 97 139 ltmuldivd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) · ( 2 · 𝑀 ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) ↔ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) ) )
178 176 177 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) )
179 86 recnd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ∈ ℂ )
180 66 rpcnd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( log ‘ ( 2 · 𝑀 ) ) ∈ ℂ )
181 139 rpcnne0d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) ∈ ℂ ∧ ( 2 · 𝑀 ) ≠ 0 ) )
182 divass ( ( ( π ‘ ( 2 · 𝑀 ) ) ∈ ℂ ∧ ( log ‘ ( 2 · 𝑀 ) ) ∈ ℂ ∧ ( ( 2 · 𝑀 ) ∈ ℂ ∧ ( 2 · 𝑀 ) ≠ 0 ) ) → ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) = ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
183 179 180 181 182 syl3anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( π ‘ ( 2 · 𝑀 ) ) · ( log ‘ ( 2 · 𝑀 ) ) ) / ( 2 · 𝑀 ) ) = ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
184 178 183 breqtrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
185 flle ( ( 𝑁 / 2 ) ∈ ℝ → ( ⌊ ‘ ( 𝑁 / 2 ) ) ≤ ( 𝑁 / 2 ) )
186 31 185 syl ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ⌊ ‘ ( 𝑁 / 2 ) ) ≤ ( 𝑁 / 2 ) )
187 1 186 eqbrtrid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 𝑀 ≤ ( 𝑁 / 2 ) )
188 lemuldiv2 ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 2 · 𝑀 ) ≤ 𝑁𝑀 ≤ ( 𝑁 / 2 ) ) )
189 34 21 18 48 188 syl112anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( 2 · 𝑀 ) ≤ 𝑁𝑀 ≤ ( 𝑁 / 2 ) ) )
190 187 189 mpbird ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · 𝑀 ) ≤ 𝑁 )
191 ppiwordi ( ( ( 2 · 𝑀 ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 2 · 𝑀 ) ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ≤ ( π𝑁 ) )
192 36 21 190 191 syl3anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π ‘ ( 2 · 𝑀 ) ) ≤ ( π𝑁 ) )
193 66 139 rpdivcld ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ∈ ℝ+ )
194 86 29 193 lemul1d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) ≤ ( π𝑁 ) ↔ ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ≤ ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ) )
195 192 194 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π ‘ ( 2 · 𝑀 ) ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ≤ ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
196 83 87 72 184 195 ltletrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) )
197 ltdiv1 ( ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ ∧ ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ↔ ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ) )
198 83 72 18 48 197 syl112anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) < ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ↔ ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) ) )
199 196 198 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) )
200 1 chebbnd1lem2 ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )
201 remulcl ( ( 2 ∈ ℝ ∧ ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℝ ) → ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
202 6 81 201 sylancr ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ )
203 28 nngt0d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → 0 < ( π𝑁 ) )
204 ltmul2 ( ( ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ∈ ℝ ∧ ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ ∧ ( ( π𝑁 ) ∈ ℝ ∧ 0 < ( π𝑁 ) ) ) → ( ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( ( π𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
205 71 202 29 203 204 syl112anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) < ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( ( π𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
206 200 205 mpbid ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( ( π𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) )
207 29 recnd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( π𝑁 ) ∈ ℂ )
208 81 recnd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( log ‘ 𝑁 ) / 𝑁 ) ∈ ℂ )
209 207 148 208 mul12d ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π𝑁 ) · ( 2 · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) = ( 2 · ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) )
210 206 209 breqtrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( 2 · ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) )
211 ltdivmul ( ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) ∈ ℝ ∧ ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) < ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( 2 · ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
212 72 82 18 48 211 syl112anc ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) < ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ↔ ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) < ( 2 · ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) ) ) )
213 210 212 mpbird ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( π𝑁 ) · ( ( log ‘ ( 2 · 𝑀 ) ) / ( 2 · 𝑀 ) ) ) / 2 ) < ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )
214 17 74 82 199 213 lttrd ( ( 𝑁 ∈ ℝ ∧ 8 ≤ 𝑁 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( π𝑁 ) · ( ( log ‘ 𝑁 ) / 𝑁 ) ) )