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 ‘ 𝑁 ) / 𝑁 ) ) ) |