Theorem stirlinglem1 46182

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

Hypotheses

Ref	Expression
stirlinglem1.1	⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
stirlinglem1.2	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
stirlinglem1.3	⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
stirlinglem1.4	⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))

Assertion

Ref	Expression
stirlinglem1	⊢ 𝐻 ⇝ (1 / 2)

Proof of Theorem stirlinglem1

Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nnuz 12775	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12503	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		stirlinglem1.4	. . . . . . . . 9 ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4		ax-1cn 11064	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
5		divcnv 15760	. . . . . . . . . 10 ⊢ (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
7	3, 6	eqbrtri 5110	. . . . . . . 8 ⊢ 𝐿 ⇝ 0
8	7	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐿 ⇝ 0)
9		stirlinglem1.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10		nnex 12131	. . . . . . . . . 10 ⊢ ℕ ∈ V
11	10	mptex 7157	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
12	9, 11	eqeltri 2827	. . . . . . . 8 ⊢ 𝐺 ∈ V
13	12	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐺 ∈ V)
14	3	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
16	15	oveq2d 7362	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17		id 22	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18		nnrp 12902	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
19	18	rpreccld 12944	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
20	14, 16, 17, 19	fvmptd 6936	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) = (1 / 𝑘))
21		nnrecre 12167	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
22	20, 21	eqeltrd 2831	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) ∈ ℝ)
23	22	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿‘𝑘) ∈ ℝ)
24	9	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
25	15	oveq2d 7362	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
26	25	oveq1d 7361	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
27	26	oveq2d 7362	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28		2re 12199	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
29	28	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
30		nnre 12132	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
31	29, 30	remulcld 11142	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32		0le2 12227	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 2
33	32	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 2)
34	18	rpge0d 12938	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 𝑘)
35	29, 30, 33, 34	mulge0d 11694	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
36	31, 35	ge0p1rpd 12964	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ+)
37	36	rpreccld 12944	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
38	24, 27, 17, 37	fvmptd 6936	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (1 / ((2 · 𝑘) + 1)))
39	37	rpred 12934	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
40	38, 39	eqeltrd 2831	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ∈ ℝ)
41	40	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)
42		1red 11113	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
43		0le1 11640	. . . . . . . . . . 11 ⊢ 0 ≤ 1
44	43	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 0 ≤ 1)
45	31, 42	readdcld 11141	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46		nncn 12133	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
47	46	mullidd 11130	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48		1lt2 12291	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 1 < 2)
50	42, 29, 18, 49	ltmul1dd 12989	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
51	47, 50	eqbrtrrd 5113	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
52	31	ltp1d 12052	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
53	30, 31, 45, 51, 52	lttrd 11274	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
54	30, 45, 53	ltled 11261	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
55	18, 36, 42, 44, 54	lediv2ad 12956	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
56	55, 38, 20	3brtr4d 5121	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
57	56	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
58	37	rpge0d 12938	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
59	58, 38	breqtrrd 5117	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 0 ≤ (𝐺‘𝑘))
60	59	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))
61	1, 2, 8, 13, 23, 41, 57, 60	climsqz2 15549	. . . . . 6 ⊢ (⊤ → 𝐺 ⇝ 0)
62		1cnd 11107	. . . . . 6 ⊢ (⊤ → 1 ∈ ℂ)
63		stirlinglem1.2	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
64	10	mptex 7157	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
65	63, 64	eqeltri 2827	. . . . . . 7 ⊢ 𝐹 ∈ V
66	65	a1i 11	. . . . . 6 ⊢ (⊤ → 𝐹 ∈ V)
67	41	recnd 11140	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℂ)
68	63	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
69	27	oveq2d 7362	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70		1cnd 11107	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℂ)
71		2cnd 12203	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
72	71, 46	mulcld 11132	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
73	72, 70	addcld 11131	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
74	36	rpne0d 12939	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
75	73, 74	reccld 11890	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
76	70, 75	subcld 11472	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
77	68, 69, 17, 76	fvmptd 6936	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
78	38	eqcomd 2737	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺‘𝑘))
79	78	oveq2d 7362	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺‘𝑘)))
80	77, 79	eqtrd 2766	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
81	80	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
82	1, 2, 61, 62, 66, 67, 81	climsubc2 15546	. . . . 5 ⊢ (⊤ → 𝐹 ⇝ (1 − 0))
83		1m0e1 12241	. . . . 5 ⊢ (1 − 0) = 1
84	82, 83	breqtrdi 5130	. . . 4 ⊢ (⊤ → 𝐹 ⇝ 1)
85	62	halfcld 12366	. . . 4 ⊢ (⊤ → (1 / 2) ∈ ℂ)
86		stirlinglem1.1	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
87	10	mptex 7157	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
88	86, 87	eqeltri 2827	. . . . 5 ⊢ 𝐻 ∈ V
89	88	a1i 11	. . . 4 ⊢ (⊤ → 𝐻 ∈ V)
90	77, 76	eqeltrd 2831	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
91	90	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
92		nncn 12133	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
93	92	sqcld 14051	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
94	93	mullidd 11130	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
95	94	eqcomd 2737	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96		2cnd 12203	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℂ)
97	96, 92	mulcld 11132	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98		1cnd 11107	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 1 ∈ ℂ)
99	92, 97, 98	adddid 11136	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
100	92, 96, 92	mul12d 11322	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
101	92	sqvald 14050	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102	101	eqcomd 2737	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103	102	oveq2d 7362	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104	100, 103	eqtrd 2766	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
105	92	mulridd 11129	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106	104, 105	oveq12d 7364	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107		2ne0 12229	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 2 ≠ 0)
109	92, 96, 108	divcan2d 11899	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110	109	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111	110	oveq2d 7362	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
112	92	halfcld 12366	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
113	96, 93, 112	adddid 11136	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114	111, 113	eqtr4d 2769	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
115	99, 106, 114	3eqtrd 2770	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
116	95, 115	oveq12d 7364	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
117	93, 112	addcld 11131	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118		nnrp 12902	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
119		2z 12504	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
120	119	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℤ)
121	118, 120	rpexpcld 14154	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ+)
122	118	rphalfcld 12946	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ+)
123	121, 122	rpaddcld 12949	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ+)
124	123	rpne0d 12939	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
125	98, 96, 93, 117, 108, 124	divmuldivd 11938	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
126	93, 112	pncand 11473	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127	126	eqcomd 2737	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128	127	oveq1d 7361	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129	117, 112, 117, 124	divsubdird 11936	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130	117, 124	dividd 11895	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131	130	oveq1d 7361	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132	128, 129, 131	3eqtrd 2770	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133		nnne0 12159	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
134	96, 92, 133	divcld 11897	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
135	96, 92, 108, 133	divne0d 11913	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136	112, 117, 134, 124, 135	divcan5rd 11924	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
137	92, 96, 133, 108	divcan6d 11916	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
138	93, 112, 134	adddird 11137	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
139	93, 96, 92, 133	div12d 11933	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140		1e2m1 12247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 = (2 − 1)
141	140	oveq2i 7357	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛↑1) = (𝑛↑(2 − 1))
142	92	exp1d 14048	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
143	92, 133, 120	expm1d 14063	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144	141, 142, 143	3eqtr3a 2790	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145	144	eqcomd 2737	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146	145	oveq2d 7362	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147	139, 146	eqtrd 2766	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148	147, 137	oveq12d 7364	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149	138, 148	eqtrd 2766	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150	137, 149	oveq12d 7364	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151	136, 150	eqtr3d 2768	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152	151	oveq2d 7362	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153	132, 152	eqtrd 2766	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154	153	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155	116, 125, 154	3eqtr2d 2772	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156	155	mpteq2ia 5184	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
157	86, 156	eqtri 2754	. . . . . . . 8 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158	157	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
159	69	oveq2d 7362	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
160	70	halfcld 12366	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161	160, 76	mulcld 11132	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162	158, 159, 17, 161	fvmptd 6936	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
163	77	oveq2d 7362	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (𝐹‘𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164	162, 163	eqtr4d 2769	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
165	164	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
166	1, 2, 84, 85, 89, 91, 165	climmulc2 15544	. . 3 ⊢ (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167	166	mptru 1548	. 2 ⊢ 𝐻 ⇝ ((1 / 2) · 1)
168		halfcn 12335	. . 3 ⊢ (1 / 2) ∈ ℂ
169	168	mulridi 11116	. 2 ⊢ ((1 / 2) · 1) = (1 / 2)
170	167, 169	breqtri 5114	1 ⊢ 𝐻 ⇝ (1 / 2)

Syntax hints:   ∧ wa 395   = wceq 1541  ⊤wtru 1542   ∈ wcel 2111   ≠ wne 2928  Vcvv 3436   class class class wbr 5089   ↦ cmpt 5170  ‘cfv 6481  (class class class)co 7346  ℂcc 11004  ℝcr 11005  0cc0 11006  1c1 11007   + caddc 11009   · cmul 11011   < clt 11146   ≤ cle 11147   − cmin 11344   / cdiv 11774  ℕcn 12125  2c2 12180  ℤcz 12468  ℝ⁺crp 12890  ↑cexp 13968   ⇝ cli 15391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-cnex 11062  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083  ax-pre-sup 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-tr 5197  df-id 5509  df-eprel 5514  df-po 5522  df-so 5523  df-fr 5567  df-we 5569  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-pred 6248  df-ord 6309  df-on 6310  df-lim 6311  df-suc 6312  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-om 7797  df-2nd 7922  df-frecs 8211  df-wrecs 8242  df-recs 8291  df-rdg 8329  df-er 8622  df-pm 8753  df-en 8870  df-dom 8871  df-sdom 8872  df-sup 9326  df-inf 9327  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-div 11775  df-nn 12126  df-2 12188  df-3 12189  df-n0 12382  df-z 12469  df-uz 12733  df-rp 12891  df-fl 13696  df-seq 13909  df-exp 13969  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-clim 15395  df-rlim 15396

This theorem is referenced by:  stirlinglem15  46196