Theorem stirlinglem1

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

	Ref	Expression
Hypotheses	stirlinglem1.1	$$⊢H=\left(n\in \mathbb{N}⟼\frac{n^2}{n\left(2n+1\right)}\right)$$
	stirlinglem1.2	$$⊢F=\left(n\in \mathbb{N}⟼1-\left(\frac{1}{2n+1}\right)\right)$$
	stirlinglem1.3	$$⊢G=\left(n\in \mathbb{N}⟼\frac{1}{2n+1}\right)$$
	stirlinglem1.4	$$⊢L=\left(n\in \mathbb{N}⟼\frac{1}{n}\right)$$
Assertion	stirlinglem1	$$⊢H⇝\left(\frac{1}{2}\right)$$

Proof

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