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 mullidd ⊢ ( ( 𝑁 ∈ ℝ ∧ 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 ‘ 𝑁 ) / 𝑁 ) ) )