Metamath Proof Explorer

Theorem stirlinglem11

Description: B is decreasing. (Contributed by Glauco Siliprandi, 29-Jun-2017)

Ref Expression
Hypotheses stirlinglem11.1 ⊢A=n∈ℕ⟼n!2⁢n⁢nen
stirlinglem11.2 ⊢B=n∈ℕ⟼log⁡A⁡n
stirlinglem11.3 ⊢K=k∈ℕ⟼12⁢k+1⁢12⋅ N+12⁢k
Assertion stirlinglem11 ⊢N∈ℕ→B⁡N+1<B⁡N

Proof

Step Hyp Ref Expression
1 stirlinglem11.1 ⊢A=n∈ℕ⟼n!2⁢n⁢nen
2 stirlinglem11.2 ⊢B=n∈ℕ⟼log⁡A⁡n
3 stirlinglem11.3 ⊢K=k∈ℕ⟼12⁢k+1⁢12⋅ N+12⁢k
4 0red ⊢N∈ℕ→0∈ℝ
5 3 a1i ⊢N∈ℕ→K=k∈ℕ⟼12⁢k+1⁢12⋅ N+12⁢k
6 simpr ⊢N∈ℕ∧k=1→k=1
7 6 oveq2d ⊢N∈ℕ∧k=1→2⁢k=2⋅1
8 7 oveq1d ⊢N∈ℕ∧k=1→2⁢k+1=2⋅1+1
9 8 oveq2d ⊢N∈ℕ∧k=1→12⁢k+1=12⋅1+1
10 7 oveq2d ⊢N∈ℕ∧k=1→12⋅ N+12⁢k=12⋅ N+12⋅1
11 9 10 oveq12d ⊢N∈ℕ∧k=1→12⁢k+1⁢12⋅ N+12⁢k=12⋅1+1⁢12⋅ N+12⋅1
12 1nn ⊢1∈ℕ
13 12 a1i ⊢N∈ℕ→1∈ℕ
14 2cnd ⊢N∈ℕ→2∈ℂ
15 1cnd ⊢N∈ℕ→1∈ℂ
16 14 15 mulcld ⊢N∈ℕ→2⋅1∈ℂ
17 16 15 addcld ⊢N∈ℕ→2⋅1+1∈ℂ
18 2t1e2 ⊢2⋅1=2
19 18 oveq1i ⊢2⋅1+1=2+1
20 2p1e3 ⊢2+1=3
21 19 20 eqtri ⊢2⋅1+1=3
22 3ne0 ⊢3≠0
23 21 22 eqnetri ⊢2⋅1+1≠0
24 23 a1i ⊢N∈ℕ→2⋅1+1≠0
25 17 24 reccld ⊢N∈ℕ→12⋅1+1∈ℂ
26 nncn ⊢N∈ℕ→N∈ℂ
27 14 26 mulcld ⊢N∈ℕ→2⋅ N∈ℂ
28 27 15 addcld ⊢N∈ℕ→2⋅ N+1∈ℂ
29 1red ⊢N∈ℕ→1∈ℝ
30 2re ⊢2∈ℝ
31 30 a1i ⊢N∈ℕ→2∈ℝ
32 nnre ⊢N∈ℕ→N∈ℝ
33 31 32 remulcld ⊢N∈ℕ→2⋅ N∈ℝ
34 33 29 readdcld ⊢N∈ℕ→2⋅ N+1∈ℝ
35 0lt1 ⊢0<1
36 35 a1i ⊢N∈ℕ→0<1
37 2rp ⊢2∈ℝ+
38 37 a1i ⊢N∈ℕ→2∈ℝ+
39 nnrp ⊢N∈ℕ→N∈ℝ+
40 38 39 rpmulcld ⊢N∈ℕ→2⋅ N∈ℝ+
41 29 40 ltaddrp2d ⊢N∈ℕ→1<2⋅ N+1
42 4 29 34 36 41 lttrd ⊢N∈ℕ→0<2⋅ N+1
43 42 gt0ne0d ⊢N∈ℕ→2⋅ N+1≠0
44 28 43 reccld ⊢N∈ℕ→12⋅ N+1∈ℂ
45 2nn0 ⊢2∈ℕ0
46 45 a1i ⊢N∈ℕ→2∈ℕ0
47 1nn0 ⊢1∈ℕ0
48 47 a1i ⊢N∈ℕ→1∈ℕ0
49 46 48 nn0mulcld ⊢N∈ℕ→2⋅1∈ℕ0
50 44 49 expcld ⊢N∈ℕ→12⋅ N+12⋅1∈ℂ
51 25 50 mulcld ⊢N∈ℕ→12⋅1+1⁢12⋅ N+12⋅1∈ℂ
52 5 11 13 51 fvmptd ⊢N∈ℕ→K⁡1=12⋅1+1⁢12⋅ N+12⋅1
53 1re ⊢1∈ℝ
54 30 53 remulcli ⊢2⋅1∈ℝ
55 54 53 readdcli ⊢2⋅1+1∈ℝ
56 55 23 rereccli ⊢12⋅1+1∈ℝ
57 56 a1i ⊢N∈ℕ→12⋅1+1∈ℝ
58 34 43 rereccld ⊢N∈ℕ→12⋅ N+1∈ℝ
59 58 49 reexpcld ⊢N∈ℕ→12⋅ N+12⋅1∈ℝ
60 57 59 remulcld ⊢N∈ℕ→12⋅1+1⁢12⋅ N+12⋅1∈ℝ
61 52 60 eqeltrd ⊢N∈ℕ→K⁡1∈ℝ
62 1 stirlinglem2 ⊢N∈ℕ→A⁡N∈ℝ+
63 62 relogcld ⊢N∈ℕ→log⁡A⁡N∈ℝ
64 nfcv ⊢Ⅎ_nN
65 nfcv ⊢Ⅎ_nlog
66 nfmpt1 ⊢Ⅎ_nn∈ℕ⟼n!2⁢n⁢nen
67 1 66 nfcxfr ⊢Ⅎ_nA
68 67 64 nffv ⊢Ⅎ_nA⁡N
69 65 68 nffv ⊢Ⅎ_nlog⁡A⁡N
70 2fveq3 ⊢n=N→log⁡A⁡n=log⁡A⁡N
71 64 69 70 2 fvmptf ⊢N∈ℕ∧log⁡A⁡N∈ℝ→B⁡N=log⁡A⁡N
72 63 71 mpdan ⊢N∈ℕ→B⁡N=log⁡A⁡N
73 72 63 eqeltrd ⊢N∈ℕ→B⁡N∈ℝ
74 peano2nn ⊢N∈ℕ→N+1∈ℕ
75 1 stirlinglem2 ⊢N+1∈ℕ→A⁡N+1∈ℝ+
76 74 75 syl ⊢N∈ℕ→A⁡N+1∈ℝ+
77 76 relogcld ⊢N∈ℕ→log⁡A⁡N+1∈ℝ
78 nfcv ⊢Ⅎ_nN+1
79 67 78 nffv ⊢Ⅎ_nA⁡N+1
80 65 79 nffv ⊢Ⅎ_nlog⁡A⁡N+1
81 2fveq3 ⊢n=N+1→log⁡A⁡n=log⁡A⁡N+1
82 78 80 81 2 fvmptf ⊢N+1∈ℕ∧log⁡A⁡N+1∈ℝ→B⁡N+1=log⁡A⁡N+1
83 74 77 82 syl2anc ⊢N∈ℕ→B⁡N+1=log⁡A⁡N+1
84 83 77 eqeltrd ⊢N∈ℕ→B⁡N+1∈ℝ
85 73 84 resubcld ⊢N∈ℕ→B⁡N−B⁡N+1∈ℝ
86 31 29 remulcld ⊢N∈ℕ→2⋅1∈ℝ
87 0le2 ⊢0≤2
88 87 a1i ⊢N∈ℕ→0≤2
89 0le1 ⊢0≤1
90 89 a1i ⊢N∈ℕ→0≤1
91 31 29 88 90 mulge0d ⊢N∈ℕ→0≤2⋅1
92 86 91 ge0p1rpd ⊢N∈ℕ→2⋅1+1∈ℝ+
93 92 rpreccld ⊢N∈ℕ→12⋅1+1∈ℝ+
94 39 rpge0d ⊢N∈ℕ→0≤N
95 31 32 88 94 mulge0d ⊢N∈ℕ→0≤2⋅ N
96 33 95 ge0p1rpd ⊢N∈ℕ→2⋅ N+1∈ℝ+
97 96 rpreccld ⊢N∈ℕ→12⋅ N+1∈ℝ+
98 2z ⊢2∈ℤ
99 98 a1i ⊢N∈ℕ→2∈ℤ
100 1z ⊢1∈ℤ
101 100 a1i ⊢N∈ℕ→1∈ℤ
102 99 101 zmulcld ⊢N∈ℕ→2⋅1∈ℤ
103 97 102 rpexpcld ⊢N∈ℕ→12⋅ N+12⋅1∈ℝ+
104 93 103 rpmulcld ⊢N∈ℕ→12⋅1+1⁢12⋅ N+12⋅1∈ℝ+
105 52 104 eqeltrd ⊢N∈ℕ→K⁡1∈ℝ+
106 105 rpgt0d ⊢N∈ℕ→0<K⁡1
107 85 61 resubcld ⊢N∈ℕ→B⁡N-B⁡N+1-K⁡1∈ℝ
108 eqid ⊢ℤ≥1+1=ℤ≥1+1
109 101 peano2zd ⊢N∈ℕ→1+1∈ℤ
110 nnuz ⊢ℕ=ℤ≥1
111 3 a1i ⊢N∈ℕ∧j∈ℕ→K=k∈ℕ⟼12⁢k+1⁢12⋅ N+12⁢k
112 oveq2 ⊢k=j→2⁢k=2⁢j
113 112 oveq1d ⊢k=j→2⁢k+1=2⁢j+1
114 113 oveq2d ⊢k=j→12⁢k+1=12⁢j+1
115 112 oveq2d ⊢k=j→12⋅ N+12⁢k=12⋅ N+12⁢j
116 114 115 oveq12d ⊢k=j→12⁢k+1⁢12⋅ N+12⁢k=12⁢j+1⁢12⋅ N+12⁢j
117 116 adantl ⊢N∈ℕ∧j∈ℕ∧k=j→12⁢k+1⁢12⋅ N+12⁢k=12⁢j+1⁢12⋅ N+12⁢j
118 simpr ⊢N∈ℕ∧j∈ℕ→j∈ℕ
119 2cnd ⊢N∈ℕ∧j∈ℕ→2∈ℂ
120 nncn ⊢j∈ℕ→j∈ℂ
121 120 adantl ⊢N∈ℕ∧j∈ℕ→j∈ℂ
122 119 121 mulcld ⊢N∈ℕ∧j∈ℕ→2⁢j∈ℂ
123 1cnd ⊢N∈ℕ∧j∈ℕ→1∈ℂ
124 122 123 addcld ⊢N∈ℕ∧j∈ℕ→2⁢j+1∈ℂ
125 0red ⊢N∈ℕ∧j∈ℕ→0∈ℝ
126 1red ⊢N∈ℕ∧j∈ℕ→1∈ℝ
127 30 a1i ⊢N∈ℕ∧j∈ℕ→2∈ℝ
128 nnre ⊢j∈ℕ→j∈ℝ
129 128 adantl ⊢N∈ℕ∧j∈ℕ→j∈ℝ
130 127 129 remulcld ⊢N∈ℕ∧j∈ℕ→2⁢j∈ℝ
131 130 126 readdcld ⊢N∈ℕ∧j∈ℕ→2⁢j+1∈ℝ
132 35 a1i ⊢N∈ℕ∧j∈ℕ→0<1
133 37 a1i ⊢N∈ℕ∧j∈ℕ→2∈ℝ+
134 nnrp ⊢j∈ℕ→j∈ℝ+
135 134 adantl ⊢N∈ℕ∧j∈ℕ→j∈ℝ+
136 133 135 rpmulcld ⊢N∈ℕ∧j∈ℕ→2⁢j∈ℝ+
137 126 136 ltaddrp2d ⊢N∈ℕ∧j∈ℕ→1<2⁢j+1
138 125 126 131 132 137 lttrd ⊢N∈ℕ∧j∈ℕ→0<2⁢j+1
139 138 gt0ne0d ⊢N∈ℕ∧j∈ℕ→2⁢j+1≠0
140 124 139 reccld ⊢N∈ℕ∧j∈ℕ→12⁢j+1∈ℂ
141 26 adantr ⊢N∈ℕ∧j∈ℕ→N∈ℂ
142 119 141 mulcld ⊢N∈ℕ∧j∈ℕ→2⋅ N∈ℂ
143 142 123 addcld ⊢N∈ℕ∧j∈ℕ→2⋅ N+1∈ℂ
144 43 adantr ⊢N∈ℕ∧j∈ℕ→2⋅ N+1≠0
145 143 144 reccld ⊢N∈ℕ∧j∈ℕ→12⋅ N+1∈ℂ
146 45 a1i ⊢N∈ℕ∧j∈ℕ→2∈ℕ0
147 nnnn0 ⊢j∈ℕ→j∈ℕ0
148 147 adantl ⊢N∈ℕ∧j∈ℕ→j∈ℕ0
149 146 148 nn0mulcld ⊢N∈ℕ∧j∈ℕ→2⁢j∈ℕ0
150 145 149 expcld ⊢N∈ℕ∧j∈ℕ→12⋅ N+12⁢j∈ℂ
151 140 150 mulcld ⊢N∈ℕ∧j∈ℕ→12⁢j+1⁢12⋅ N+12⁢j∈ℂ
152 111 117 118 151 fvmptd ⊢N∈ℕ∧j∈ℕ→K⁡j=12⁢j+1⁢12⋅ N+12⁢j
153 0red ⊢j∈ℕ→0∈ℝ
154 1red ⊢j∈ℕ→1∈ℝ
155 30 a1i ⊢j∈ℕ→2∈ℝ
156 155 128 remulcld ⊢j∈ℕ→2⁢j∈ℝ
157 156 154 readdcld ⊢j∈ℕ→2⁢j+1∈ℝ
158 35 a1i ⊢j∈ℕ→0<1
159 37 a1i ⊢j∈ℕ→2∈ℝ+
160 159 134 rpmulcld ⊢j∈ℕ→2⁢j∈ℝ+
161 154 160 ltaddrp2d ⊢j∈ℕ→1<2⁢j+1
162 153 154 157 158 161 lttrd ⊢j∈ℕ→0<2⁢j+1
163 162 gt0ne0d ⊢j∈ℕ→2⁢j+1≠0
164 163 adantl ⊢N∈ℕ∧j∈ℕ→2⁢j+1≠0
165 124 164 reccld ⊢N∈ℕ∧j∈ℕ→12⁢j+1∈ℂ
166 165 150 mulcld ⊢N∈ℕ∧j∈ℕ→12⁢j+1⁢12⋅ N+12⁢j∈ℂ
167 152 166 eqeltrd ⊢N∈ℕ∧j∈ℕ→K⁡j∈ℂ
168 eqid ⊢n∈ℕ⟼1+2⁢n2⁢log⁡n+1n−1=n∈ℕ⟼1+2⁢n2⁢log⁡n+1n−1
169 1 2 168 3 stirlinglem9 ⊢N∈ℕ→seq1+K⇝B⁡N−B⁡N+1
170 110 13 167 169 clim2ser ⊢N∈ℕ→seq1+1+K⇝B⁡N-B⁡N+1-seq1+K⁡1
171 peano2nn ⊢1∈ℕ→1+1∈ℕ
172 uznnssnn ⊢1+1∈ℕ→ℤ≥1+1⊆ℕ
173 12 171 172 mp2b ⊢ℤ≥1+1⊆ℕ
174 173 a1i ⊢N∈ℕ→ℤ≥1+1⊆ℕ
175 174 sseld ⊢N∈ℕ→j∈ℤ≥1+1→j∈ℕ
176 175 imdistani ⊢N∈ℕ∧j∈ℤ≥1+1→N∈ℕ∧j∈ℕ
177 176 152 syl ⊢N∈ℕ∧j∈ℤ≥1+1→K⁡j=12⁢j+1⁢12⋅ N+12⁢j
178 30 a1i ⊢j∈ℤ≥1+1→2∈ℝ
179 eluzelre ⊢j∈ℤ≥1+1→j∈ℝ
180 178 179 remulcld ⊢j∈ℤ≥1+1→2⁢j∈ℝ
181 1red ⊢j∈ℤ≥1+1→1∈ℝ
182 180 181 readdcld ⊢j∈ℤ≥1+1→2⁢j+1∈ℝ
183 173 sseli ⊢j∈ℤ≥1+1→j∈ℕ
184 183 163 syl ⊢j∈ℤ≥1+1→2⁢j+1≠0
185 182 184 rereccld ⊢j∈ℤ≥1+1→12⁢j+1∈ℝ
186 185 adantl ⊢N∈ℕ∧j∈ℤ≥1+1→12⁢j+1∈ℝ
187 34 adantr ⊢N∈ℕ∧j∈ℤ≥1+1→2⋅ N+1∈ℝ
188 43 adantr ⊢N∈ℕ∧j∈ℤ≥1+1→2⋅ N+1≠0
189 187 188 rereccld ⊢N∈ℕ∧j∈ℤ≥1+1→12⋅ N+1∈ℝ
190 176 149 syl ⊢N∈ℕ∧j∈ℤ≥1+1→2⁢j∈ℕ0
191 189 190 reexpcld ⊢N∈ℕ∧j∈ℤ≥1+1→12⋅ N+12⁢j∈ℝ
192 186 191 remulcld ⊢N∈ℕ∧j∈ℤ≥1+1→12⁢j+1⁢12⋅ N+12⁢j∈ℝ
193 177 192 eqeltrd ⊢N∈ℕ∧j∈ℤ≥1+1→K⁡j∈ℝ
194 1red ⊢N∈ℕ∧j∈ℤ≥1+1→1∈ℝ
195 30 a1i ⊢N∈ℕ∧j∈ℤ≥1+1→2∈ℝ
196 176 129 syl ⊢N∈ℕ∧j∈ℤ≥1+1→j∈ℝ
197 195 196 remulcld ⊢N∈ℕ∧j∈ℤ≥1+1→2⁢j∈ℝ
198 87 a1i ⊢N∈ℕ∧j∈ℤ≥1+1→0≤2
199 0red ⊢j∈ℤ≥1+1→0∈ℝ
200 87 a1i ⊢j∈ℤ≥1+1→0≤2
201 1p1e2 ⊢1+1=2
202 eluzle ⊢j∈ℤ≥1+1→1+1≤j
203 201 202 eqbrtrrid ⊢j∈ℤ≥1+1→2≤j
204 199 178 179 200 203 letrd ⊢j∈ℤ≥1+1→0≤j
205 204 adantl ⊢N∈ℕ∧j∈ℤ≥1+1→0≤j
206 195 196 198 205 mulge0d ⊢N∈ℕ∧j∈ℤ≥1+1→0≤2⁢j
207 197 206 ge0p1rpd ⊢N∈ℕ∧j∈ℤ≥1+1→2⁢j+1∈ℝ+
208 89 a1i ⊢N∈ℕ∧j∈ℤ≥1+1→0≤1
209 194 207 208 divge0d ⊢N∈ℕ∧j∈ℤ≥1+1→0≤12⁢j+1
210 32 adantr ⊢N∈ℕ∧j∈ℤ≥1+1→N∈ℝ
211 195 210 remulcld ⊢N∈ℕ∧j∈ℤ≥1+1→2⋅ N∈ℝ
212 94 adantr ⊢N∈ℕ∧j∈ℤ≥1+1→0≤N
213 195 210 198 212 mulge0d ⊢N∈ℕ∧j∈ℤ≥1+1→0≤2⋅ N
214 211 213 ge0p1rpd ⊢N∈ℕ∧j∈ℤ≥1+1→2⋅ N+1∈ℝ+
215 194 214 208 divge0d ⊢N∈ℕ∧j∈ℤ≥1+1→0≤12⋅ N+1
216 189 190 215 expge0d ⊢N∈ℕ∧j∈ℤ≥1+1→0≤12⋅ N+12⁢j
217 186 191 209 216 mulge0d ⊢N∈ℕ∧j∈ℤ≥1+1→0≤12⁢j+1⁢12⋅ N+12⁢j
218 217 177 breqtrrd ⊢N∈ℕ∧j∈ℤ≥1+1→0≤K⁡j
219 108 109 170 193 218 iserge0 ⊢N∈ℕ→0≤B⁡N-B⁡N+1-seq1+K⁡1
220 seq1 ⊢1∈ℤ→seq1+K⁡1=K⁡1
221 100 220 mp1i ⊢N∈ℕ→seq1+K⁡1=K⁡1
222 221 oveq2d ⊢N∈ℕ→B⁡N-B⁡N+1-seq1+K⁡1=B⁡N-B⁡N+1-K⁡1
223 219 222 breqtrd ⊢N∈ℕ→0≤B⁡N-B⁡N+1-K⁡1
224 4 107 61 223 leadd1dd ⊢N∈ℕ→0+K⁡1≤B⁡N−B⁡N+1-K⁡1+K⁡1
225 52 51 eqeltrd ⊢N∈ℕ→K⁡1∈ℂ
226 225 addlidd ⊢N∈ℕ→0+K⁡1=K⁡1
227 73 recnd ⊢N∈ℕ→B⁡N∈ℂ
228 84 recnd ⊢N∈ℕ→B⁡N+1∈ℂ
229 227 228 subcld ⊢N∈ℕ→B⁡N−B⁡N+1∈ℂ
230 229 225 npcand ⊢N∈ℕ→B⁡N−B⁡N+1-K⁡1+K⁡1=B⁡N−B⁡N+1
231 224 226 230 3brtr3d ⊢N∈ℕ→K⁡1≤B⁡N−B⁡N+1
232 4 61 85 106 231 ltletrd ⊢N∈ℕ→0<B⁡N−B⁡N+1
233 84 73 posdifd ⊢N∈ℕ→B⁡N+1<B⁡N↔0<B⁡N−B⁡N+1
234 232 233 mpbird ⊢N∈ℕ→B⁡N+1<B⁡N