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 )