Metamath Proof Explorer


Theorem stirlinglem1

Description: A simple limit of fractions is computed. (Contributed by Glauco Siliprandi, 30-Jun-2017)

Ref Expression
Hypotheses stirlinglem1.1
|- H = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
stirlinglem1.2
|- F = ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) )
stirlinglem1.3
|- G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
stirlinglem1.4
|- L = ( n e. NN |-> ( 1 / n ) )
Assertion stirlinglem1
|- H ~~> ( 1 / 2 )

Proof

Step Hyp Ref Expression
1 stirlinglem1.1
 |-  H = ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) )
2 stirlinglem1.2
 |-  F = ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) )
3 stirlinglem1.3
 |-  G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) )
4 stirlinglem1.4
 |-  L = ( n e. NN |-> ( 1 / n ) )
5 nnuz
 |-  NN = ( ZZ>= ` 1 )
6 1zzd
 |-  ( T. -> 1 e. ZZ )
7 ax-1cn
 |-  1 e. CC
8 divcnv
 |-  ( 1 e. CC -> ( n e. NN |-> ( 1 / n ) ) ~~> 0 )
9 7 8 ax-mp
 |-  ( n e. NN |-> ( 1 / n ) ) ~~> 0
10 4 9 eqbrtri
 |-  L ~~> 0
11 10 a1i
 |-  ( T. -> L ~~> 0 )
12 nnex
 |-  NN e. _V
13 12 mptex
 |-  ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) e. _V
14 3 13 eqeltri
 |-  G e. _V
15 14 a1i
 |-  ( T. -> G e. _V )
16 4 a1i
 |-  ( k e. NN -> L = ( n e. NN |-> ( 1 / n ) ) )
17 simpr
 |-  ( ( k e. NN /\ n = k ) -> n = k )
18 17 oveq2d
 |-  ( ( k e. NN /\ n = k ) -> ( 1 / n ) = ( 1 / k ) )
19 id
 |-  ( k e. NN -> k e. NN )
20 nnrp
 |-  ( k e. NN -> k e. RR+ )
21 20 rpreccld
 |-  ( k e. NN -> ( 1 / k ) e. RR+ )
22 16 18 19 21 fvmptd
 |-  ( k e. NN -> ( L ` k ) = ( 1 / k ) )
23 nnrecre
 |-  ( k e. NN -> ( 1 / k ) e. RR )
24 22 23 eqeltrd
 |-  ( k e. NN -> ( L ` k ) e. RR )
25 24 adantl
 |-  ( ( T. /\ k e. NN ) -> ( L ` k ) e. RR )
26 3 a1i
 |-  ( k e. NN -> G = ( n e. NN |-> ( 1 / ( ( 2 x. n ) + 1 ) ) ) )
27 17 oveq2d
 |-  ( ( k e. NN /\ n = k ) -> ( 2 x. n ) = ( 2 x. k ) )
28 27 oveq1d
 |-  ( ( k e. NN /\ n = k ) -> ( ( 2 x. n ) + 1 ) = ( ( 2 x. k ) + 1 ) )
29 28 oveq2d
 |-  ( ( k e. NN /\ n = k ) -> ( 1 / ( ( 2 x. n ) + 1 ) ) = ( 1 / ( ( 2 x. k ) + 1 ) ) )
30 2re
 |-  2 e. RR
31 30 a1i
 |-  ( k e. NN -> 2 e. RR )
32 nnre
 |-  ( k e. NN -> k e. RR )
33 31 32 remulcld
 |-  ( k e. NN -> ( 2 x. k ) e. RR )
34 0le2
 |-  0 <_ 2
35 34 a1i
 |-  ( k e. NN -> 0 <_ 2 )
36 20 rpge0d
 |-  ( k e. NN -> 0 <_ k )
37 31 32 35 36 mulge0d
 |-  ( k e. NN -> 0 <_ ( 2 x. k ) )
38 33 37 ge0p1rpd
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. RR+ )
39 38 rpreccld
 |-  ( k e. NN -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. RR+ )
40 26 29 19 39 fvmptd
 |-  ( k e. NN -> ( G ` k ) = ( 1 / ( ( 2 x. k ) + 1 ) ) )
41 39 rpred
 |-  ( k e. NN -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. RR )
42 40 41 eqeltrd
 |-  ( k e. NN -> ( G ` k ) e. RR )
43 42 adantl
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. RR )
44 1red
 |-  ( k e. NN -> 1 e. RR )
45 0le1
 |-  0 <_ 1
46 45 a1i
 |-  ( k e. NN -> 0 <_ 1 )
47 33 44 readdcld
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. RR )
48 nncn
 |-  ( k e. NN -> k e. CC )
49 48 mulid2d
 |-  ( k e. NN -> ( 1 x. k ) = k )
50 1lt2
 |-  1 < 2
51 50 a1i
 |-  ( k e. NN -> 1 < 2 )
52 44 31 20 51 ltmul1dd
 |-  ( k e. NN -> ( 1 x. k ) < ( 2 x. k ) )
53 49 52 eqbrtrrd
 |-  ( k e. NN -> k < ( 2 x. k ) )
54 33 ltp1d
 |-  ( k e. NN -> ( 2 x. k ) < ( ( 2 x. k ) + 1 ) )
55 32 33 47 53 54 lttrd
 |-  ( k e. NN -> k < ( ( 2 x. k ) + 1 ) )
56 32 47 55 ltled
 |-  ( k e. NN -> k <_ ( ( 2 x. k ) + 1 ) )
57 20 38 44 46 56 lediv2ad
 |-  ( k e. NN -> ( 1 / ( ( 2 x. k ) + 1 ) ) <_ ( 1 / k ) )
58 57 40 22 3brtr4d
 |-  ( k e. NN -> ( G ` k ) <_ ( L ` k ) )
59 58 adantl
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) <_ ( L ` k ) )
60 39 rpge0d
 |-  ( k e. NN -> 0 <_ ( 1 / ( ( 2 x. k ) + 1 ) ) )
61 60 40 breqtrrd
 |-  ( k e. NN -> 0 <_ ( G ` k ) )
62 61 adantl
 |-  ( ( T. /\ k e. NN ) -> 0 <_ ( G ` k ) )
63 5 6 11 15 25 43 59 62 climsqz2
 |-  ( T. -> G ~~> 0 )
64 1cnd
 |-  ( T. -> 1 e. CC )
65 12 mptex
 |-  ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) e. _V
66 2 65 eqeltri
 |-  F e. _V
67 66 a1i
 |-  ( T. -> F e. _V )
68 43 recnd
 |-  ( ( T. /\ k e. NN ) -> ( G ` k ) e. CC )
69 2 a1i
 |-  ( k e. NN -> F = ( n e. NN |-> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
70 29 oveq2d
 |-  ( ( k e. NN /\ n = k ) -> ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) = ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) )
71 1cnd
 |-  ( k e. NN -> 1 e. CC )
72 2cnd
 |-  ( k e. NN -> 2 e. CC )
73 72 48 mulcld
 |-  ( k e. NN -> ( 2 x. k ) e. CC )
74 73 71 addcld
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) e. CC )
75 38 rpne0d
 |-  ( k e. NN -> ( ( 2 x. k ) + 1 ) =/= 0 )
76 74 75 reccld
 |-  ( k e. NN -> ( 1 / ( ( 2 x. k ) + 1 ) ) e. CC )
77 71 76 subcld
 |-  ( k e. NN -> ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) e. CC )
78 69 70 19 77 fvmptd
 |-  ( k e. NN -> ( F ` k ) = ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) )
79 40 eqcomd
 |-  ( k e. NN -> ( 1 / ( ( 2 x. k ) + 1 ) ) = ( G ` k ) )
80 79 oveq2d
 |-  ( k e. NN -> ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) = ( 1 - ( G ` k ) ) )
81 78 80 eqtrd
 |-  ( k e. NN -> ( F ` k ) = ( 1 - ( G ` k ) ) )
82 81 adantl
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) = ( 1 - ( G ` k ) ) )
83 5 6 63 64 67 68 82 climsubc2
 |-  ( T. -> F ~~> ( 1 - 0 ) )
84 1m0e1
 |-  ( 1 - 0 ) = 1
85 83 84 breqtrdi
 |-  ( T. -> F ~~> 1 )
86 64 halfcld
 |-  ( T. -> ( 1 / 2 ) e. CC )
87 12 mptex
 |-  ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) e. _V
88 1 87 eqeltri
 |-  H e. _V
89 88 a1i
 |-  ( T. -> H e. _V )
90 78 77 eqeltrd
 |-  ( k e. NN -> ( F ` k ) e. CC )
91 90 adantl
 |-  ( ( T. /\ k e. NN ) -> ( F ` k ) e. CC )
92 nncn
 |-  ( n e. NN -> n e. CC )
93 92 sqcld
 |-  ( n e. NN -> ( n ^ 2 ) e. CC )
94 93 mulid2d
 |-  ( n e. NN -> ( 1 x. ( n ^ 2 ) ) = ( n ^ 2 ) )
95 94 eqcomd
 |-  ( n e. NN -> ( n ^ 2 ) = ( 1 x. ( n ^ 2 ) ) )
96 2cnd
 |-  ( n e. NN -> 2 e. CC )
97 96 92 mulcld
 |-  ( n e. NN -> ( 2 x. n ) e. CC )
98 1cnd
 |-  ( n e. NN -> 1 e. CC )
99 92 97 98 adddid
 |-  ( n e. NN -> ( n x. ( ( 2 x. n ) + 1 ) ) = ( ( n x. ( 2 x. n ) ) + ( n x. 1 ) ) )
100 92 96 92 mul12d
 |-  ( n e. NN -> ( n x. ( 2 x. n ) ) = ( 2 x. ( n x. n ) ) )
101 92 sqvald
 |-  ( n e. NN -> ( n ^ 2 ) = ( n x. n ) )
102 101 eqcomd
 |-  ( n e. NN -> ( n x. n ) = ( n ^ 2 ) )
103 102 oveq2d
 |-  ( n e. NN -> ( 2 x. ( n x. n ) ) = ( 2 x. ( n ^ 2 ) ) )
104 100 103 eqtrd
 |-  ( n e. NN -> ( n x. ( 2 x. n ) ) = ( 2 x. ( n ^ 2 ) ) )
105 92 mulid1d
 |-  ( n e. NN -> ( n x. 1 ) = n )
106 104 105 oveq12d
 |-  ( n e. NN -> ( ( n x. ( 2 x. n ) ) + ( n x. 1 ) ) = ( ( 2 x. ( n ^ 2 ) ) + n ) )
107 2ne0
 |-  2 =/= 0
108 107 a1i
 |-  ( n e. NN -> 2 =/= 0 )
109 92 96 108 divcan2d
 |-  ( n e. NN -> ( 2 x. ( n / 2 ) ) = n )
110 109 eqcomd
 |-  ( n e. NN -> n = ( 2 x. ( n / 2 ) ) )
111 110 oveq2d
 |-  ( n e. NN -> ( ( 2 x. ( n ^ 2 ) ) + n ) = ( ( 2 x. ( n ^ 2 ) ) + ( 2 x. ( n / 2 ) ) ) )
112 92 halfcld
 |-  ( n e. NN -> ( n / 2 ) e. CC )
113 96 93 112 adddid
 |-  ( n e. NN -> ( 2 x. ( ( n ^ 2 ) + ( n / 2 ) ) ) = ( ( 2 x. ( n ^ 2 ) ) + ( 2 x. ( n / 2 ) ) ) )
114 111 113 eqtr4d
 |-  ( n e. NN -> ( ( 2 x. ( n ^ 2 ) ) + n ) = ( 2 x. ( ( n ^ 2 ) + ( n / 2 ) ) ) )
115 99 106 114 3eqtrd
 |-  ( n e. NN -> ( n x. ( ( 2 x. n ) + 1 ) ) = ( 2 x. ( ( n ^ 2 ) + ( n / 2 ) ) ) )
116 95 115 oveq12d
 |-  ( n e. NN -> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) = ( ( 1 x. ( n ^ 2 ) ) / ( 2 x. ( ( n ^ 2 ) + ( n / 2 ) ) ) ) )
117 93 112 addcld
 |-  ( n e. NN -> ( ( n ^ 2 ) + ( n / 2 ) ) e. CC )
118 nnrp
 |-  ( n e. NN -> n e. RR+ )
119 2z
 |-  2 e. ZZ
120 119 a1i
 |-  ( n e. NN -> 2 e. ZZ )
121 118 120 rpexpcld
 |-  ( n e. NN -> ( n ^ 2 ) e. RR+ )
122 118 rphalfcld
 |-  ( n e. NN -> ( n / 2 ) e. RR+ )
123 121 122 rpaddcld
 |-  ( n e. NN -> ( ( n ^ 2 ) + ( n / 2 ) ) e. RR+ )
124 123 rpne0d
 |-  ( n e. NN -> ( ( n ^ 2 ) + ( n / 2 ) ) =/= 0 )
125 98 96 93 117 108 124 divmuldivd
 |-  ( n e. NN -> ( ( 1 / 2 ) x. ( ( n ^ 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) ) = ( ( 1 x. ( n ^ 2 ) ) / ( 2 x. ( ( n ^ 2 ) + ( n / 2 ) ) ) ) )
126 93 112 pncand
 |-  ( n e. NN -> ( ( ( n ^ 2 ) + ( n / 2 ) ) - ( n / 2 ) ) = ( n ^ 2 ) )
127 126 eqcomd
 |-  ( n e. NN -> ( n ^ 2 ) = ( ( ( n ^ 2 ) + ( n / 2 ) ) - ( n / 2 ) ) )
128 127 oveq1d
 |-  ( n e. NN -> ( ( n ^ 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) = ( ( ( ( n ^ 2 ) + ( n / 2 ) ) - ( n / 2 ) ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) )
129 117 112 117 124 divsubdird
 |-  ( n e. NN -> ( ( ( ( n ^ 2 ) + ( n / 2 ) ) - ( n / 2 ) ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) = ( ( ( ( n ^ 2 ) + ( n / 2 ) ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) - ( ( n / 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) ) )
130 117 124 dividd
 |-  ( n e. NN -> ( ( ( n ^ 2 ) + ( n / 2 ) ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) = 1 )
131 130 oveq1d
 |-  ( n e. NN -> ( ( ( ( n ^ 2 ) + ( n / 2 ) ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) - ( ( n / 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) ) = ( 1 - ( ( n / 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) ) )
132 128 129 131 3eqtrd
 |-  ( n e. NN -> ( ( n ^ 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) = ( 1 - ( ( n / 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) ) )
133 nnne0
 |-  ( n e. NN -> n =/= 0 )
134 96 92 133 divcld
 |-  ( n e. NN -> ( 2 / n ) e. CC )
135 96 92 108 133 divne0d
 |-  ( n e. NN -> ( 2 / n ) =/= 0 )
136 112 117 134 124 135 divcan5rd
 |-  ( n e. NN -> ( ( ( n / 2 ) x. ( 2 / n ) ) / ( ( ( n ^ 2 ) + ( n / 2 ) ) x. ( 2 / n ) ) ) = ( ( n / 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) )
137 92 96 133 108 divcan6d
 |-  ( n e. NN -> ( ( n / 2 ) x. ( 2 / n ) ) = 1 )
138 93 112 134 adddird
 |-  ( n e. NN -> ( ( ( n ^ 2 ) + ( n / 2 ) ) x. ( 2 / n ) ) = ( ( ( n ^ 2 ) x. ( 2 / n ) ) + ( ( n / 2 ) x. ( 2 / n ) ) ) )
139 93 96 92 133 div12d
 |-  ( n e. NN -> ( ( n ^ 2 ) x. ( 2 / n ) ) = ( 2 x. ( ( n ^ 2 ) / n ) ) )
140 1e2m1
 |-  1 = ( 2 - 1 )
141 140 oveq2i
 |-  ( n ^ 1 ) = ( n ^ ( 2 - 1 ) )
142 92 exp1d
 |-  ( n e. NN -> ( n ^ 1 ) = n )
143 92 133 120 expm1d
 |-  ( n e. NN -> ( n ^ ( 2 - 1 ) ) = ( ( n ^ 2 ) / n ) )
144 141 142 143 3eqtr3a
 |-  ( n e. NN -> n = ( ( n ^ 2 ) / n ) )
145 144 eqcomd
 |-  ( n e. NN -> ( ( n ^ 2 ) / n ) = n )
146 145 oveq2d
 |-  ( n e. NN -> ( 2 x. ( ( n ^ 2 ) / n ) ) = ( 2 x. n ) )
147 139 146 eqtrd
 |-  ( n e. NN -> ( ( n ^ 2 ) x. ( 2 / n ) ) = ( 2 x. n ) )
148 147 137 oveq12d
 |-  ( n e. NN -> ( ( ( n ^ 2 ) x. ( 2 / n ) ) + ( ( n / 2 ) x. ( 2 / n ) ) ) = ( ( 2 x. n ) + 1 ) )
149 138 148 eqtrd
 |-  ( n e. NN -> ( ( ( n ^ 2 ) + ( n / 2 ) ) x. ( 2 / n ) ) = ( ( 2 x. n ) + 1 ) )
150 137 149 oveq12d
 |-  ( n e. NN -> ( ( ( n / 2 ) x. ( 2 / n ) ) / ( ( ( n ^ 2 ) + ( n / 2 ) ) x. ( 2 / n ) ) ) = ( 1 / ( ( 2 x. n ) + 1 ) ) )
151 136 150 eqtr3d
 |-  ( n e. NN -> ( ( n / 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) = ( 1 / ( ( 2 x. n ) + 1 ) ) )
152 151 oveq2d
 |-  ( n e. NN -> ( 1 - ( ( n / 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) ) = ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) )
153 132 152 eqtrd
 |-  ( n e. NN -> ( ( n ^ 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) = ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) )
154 153 oveq2d
 |-  ( n e. NN -> ( ( 1 / 2 ) x. ( ( n ^ 2 ) / ( ( n ^ 2 ) + ( n / 2 ) ) ) ) = ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
155 116 125 154 3eqtr2d
 |-  ( n e. NN -> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) = ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
156 155 mpteq2ia
 |-  ( n e. NN |-> ( ( n ^ 2 ) / ( n x. ( ( 2 x. n ) + 1 ) ) ) ) = ( n e. NN |-> ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
157 1 156 eqtri
 |-  H = ( n e. NN |-> ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) )
158 157 a1i
 |-  ( k e. NN -> H = ( n e. NN |-> ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) ) )
159 70 oveq2d
 |-  ( ( k e. NN /\ n = k ) -> ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. n ) + 1 ) ) ) ) = ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) )
160 71 halfcld
 |-  ( k e. NN -> ( 1 / 2 ) e. CC )
161 160 77 mulcld
 |-  ( k e. NN -> ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) e. CC )
162 158 159 19 161 fvmptd
 |-  ( k e. NN -> ( H ` k ) = ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) )
163 78 oveq2d
 |-  ( k e. NN -> ( ( 1 / 2 ) x. ( F ` k ) ) = ( ( 1 / 2 ) x. ( 1 - ( 1 / ( ( 2 x. k ) + 1 ) ) ) ) )
164 162 163 eqtr4d
 |-  ( k e. NN -> ( H ` k ) = ( ( 1 / 2 ) x. ( F ` k ) ) )
165 164 adantl
 |-  ( ( T. /\ k e. NN ) -> ( H ` k ) = ( ( 1 / 2 ) x. ( F ` k ) ) )
166 5 6 85 86 89 91 165 climmulc2
 |-  ( T. -> H ~~> ( ( 1 / 2 ) x. 1 ) )
167 166 mptru
 |-  H ~~> ( ( 1 / 2 ) x. 1 )
168 halfcn
 |-  ( 1 / 2 ) e. CC
169 168 mulid1i
 |-  ( ( 1 / 2 ) x. 1 ) = ( 1 / 2 )
170 167 169 breqtri
 |-  H ~~> ( 1 / 2 )