Theorem stirlinglem1 46502

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 12827	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12558	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		stirlinglem1.4	. . . . . . . . 9 ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4		ax-1cn 11096	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
5		divcnv 15818	. . . . . . . . . 10 ⊢ (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
7	3, 6	eqbrtri 5106	. . . . . . . 8 ⊢ 𝐿 ⇝ 0
8	7	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐿 ⇝ 0)
9		stirlinglem1.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10		nnex 12180	. . . . . . . . . 10 ⊢ ℕ ∈ V
11	10	mptex 7178	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
12	9, 11	eqeltri 2832	. . . . . . . 8 ⊢ 𝐺 ∈ V
13	12	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐺 ∈ V)
14	3	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
16	15	oveq2d 7383	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17		id 22	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18		nnrp 12954	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
19	18	rpreccld 12996	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
20	14, 16, 17, 19	fvmptd 6955	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) = (1 / 𝑘))
21		nnrecre 12219	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
22	20, 21	eqeltrd 2836	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) ∈ ℝ)
23	22	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿‘𝑘) ∈ ℝ)
24	9	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
25	15	oveq2d 7383	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
26	25	oveq1d 7382	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
27	26	oveq2d 7383	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28		2re 12255	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
29	28	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
30		nnre 12181	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
31	29, 30	remulcld 11175	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32		0le2 12283	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 2
33	32	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 2)
34	18	rpge0d 12990	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 𝑘)
35	29, 30, 33, 34	mulge0d 11727	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
36	31, 35	ge0p1rpd 13016	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ+)
37	36	rpreccld 12996	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
38	24, 27, 17, 37	fvmptd 6955	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (1 / ((2 · 𝑘) + 1)))
39	37	rpred 12986	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
40	38, 39	eqeltrd 2836	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ∈ ℝ)
41	40	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)
42		1red 11145	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
43		0le1 11673	. . . . . . . . . . 11 ⊢ 0 ≤ 1
44	43	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 0 ≤ 1)
45	31, 42	readdcld 11174	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46		nncn 12182	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
47	46	mullidd 11163	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48		1lt2 12347	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 1 < 2)
50	42, 29, 18, 49	ltmul1dd 13041	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
51	47, 50	eqbrtrrd 5109	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
52	31	ltp1d 12086	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
53	30, 31, 45, 51, 52	lttrd 11307	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
54	30, 45, 53	ltled 11294	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
55	18, 36, 42, 44, 54	lediv2ad 13008	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
56	55, 38, 20	3brtr4d 5117	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
57	56	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
58	37	rpge0d 12990	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
59	58, 38	breqtrrd 5113	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 0 ≤ (𝐺‘𝑘))
60	59	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))
61	1, 2, 8, 13, 23, 41, 57, 60	climsqz2 15604	. . . . . 6 ⊢ (⊤ → 𝐺 ⇝ 0)
62		1cnd 11139	. . . . . 6 ⊢ (⊤ → 1 ∈ ℂ)
63		stirlinglem1.2	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
64	10	mptex 7178	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
65	63, 64	eqeltri 2832	. . . . . . 7 ⊢ 𝐹 ∈ V
66	65	a1i 11	. . . . . 6 ⊢ (⊤ → 𝐹 ∈ V)
67	41	recnd 11173	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℂ)
68	63	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
69	27	oveq2d 7383	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70		1cnd 11139	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℂ)
71		2cnd 12259	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
72	71, 46	mulcld 11165	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
73	72, 70	addcld 11164	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
74	36	rpne0d 12991	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
75	73, 74	reccld 11924	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
76	70, 75	subcld 11505	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
77	68, 69, 17, 76	fvmptd 6955	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
78	38	eqcomd 2742	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺‘𝑘))
79	78	oveq2d 7383	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺‘𝑘)))
80	77, 79	eqtrd 2771	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
81	80	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
82	1, 2, 61, 62, 66, 67, 81	climsubc2 15601	. . . . 5 ⊢ (⊤ → 𝐹 ⇝ (1 − 0))
83		1m0e1 12297	. . . . 5 ⊢ (1 − 0) = 1
84	82, 83	breqtrdi 5126	. . . 4 ⊢ (⊤ → 𝐹 ⇝ 1)
85	62	halfcld 12422	. . . 4 ⊢ (⊤ → (1 / 2) ∈ ℂ)
86		stirlinglem1.1	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
87	10	mptex 7178	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
88	86, 87	eqeltri 2832	. . . . 5 ⊢ 𝐻 ∈ V
89	88	a1i 11	. . . 4 ⊢ (⊤ → 𝐻 ∈ V)
90	77, 76	eqeltrd 2836	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
91	90	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
92		nncn 12182	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
93	92	sqcld 14106	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
94	93	mullidd 11163	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
95	94	eqcomd 2742	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96		2cnd 12259	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℂ)
97	96, 92	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98		1cnd 11139	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 1 ∈ ℂ)
99	92, 97, 98	adddid 11169	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
100	92, 96, 92	mul12d 11355	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
101	92	sqvald 14105	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102	101	eqcomd 2742	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103	102	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104	100, 103	eqtrd 2771	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
105	92	mulridd 11162	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106	104, 105	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107		2ne0 12285	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 2 ≠ 0)
109	92, 96, 108	divcan2d 11933	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110	109	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111	110	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
112	92	halfcld 12422	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
113	96, 93, 112	adddid 11169	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114	111, 113	eqtr4d 2774	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
115	99, 106, 114	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
116	95, 115	oveq12d 7385	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
117	93, 112	addcld 11164	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118		nnrp 12954	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
119		2z 12559	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
120	119	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℤ)
121	118, 120	rpexpcld 14209	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ+)
122	118	rphalfcld 12998	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ+)
123	121, 122	rpaddcld 13001	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ+)
124	123	rpne0d 12991	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
125	98, 96, 93, 117, 108, 124	divmuldivd 11972	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
126	93, 112	pncand 11506	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127	126	eqcomd 2742	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128	127	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129	117, 112, 117, 124	divsubdird 11970	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130	117, 124	dividd 11929	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131	130	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132	128, 129, 131	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133		nnne0 12211	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
134	96, 92, 133	divcld 11931	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
135	96, 92, 108, 133	divne0d 11947	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136	112, 117, 134, 124, 135	divcan5rd 11958	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
137	92, 96, 133, 108	divcan6d 11950	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
138	93, 112, 134	adddird 11170	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
139	93, 96, 92, 133	div12d 11967	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140		1e2m1 12303	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 = (2 − 1)
141	140	oveq2i 7378	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛↑1) = (𝑛↑(2 − 1))
142	92	exp1d 14103	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
143	92, 133, 120	expm1d 14118	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144	141, 142, 143	3eqtr3a 2795	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145	144	eqcomd 2742	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146	145	oveq2d 7383	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147	139, 146	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148	147, 137	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149	138, 148	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150	137, 149	oveq12d 7385	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151	136, 150	eqtr3d 2773	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152	151	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153	132, 152	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154	153	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155	116, 125, 154	3eqtr2d 2777	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156	155	mpteq2ia 5180	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
157	86, 156	eqtri 2759	. . . . . . . 8 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158	157	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
159	69	oveq2d 7383	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
160	70	halfcld 12422	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161	160, 76	mulcld 11165	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162	158, 159, 17, 161	fvmptd 6955	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
163	77	oveq2d 7383	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (𝐹‘𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164	162, 163	eqtr4d 2774	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
165	164	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
166	1, 2, 84, 85, 89, 91, 165	climmulc2 15599	. . 3 ⊢ (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167	166	mptru 1549	. 2 ⊢ 𝐻 ⇝ ((1 / 2) · 1)
168		halfcn 12391	. . 3 ⊢ (1 / 2) ∈ ℂ
169	168	mulridi 11149	. 2 ⊢ ((1 / 2) · 1) = (1 / 2)
170	167, 169	breqtri 5110	1 ⊢ 𝐻 ⇝ (1 / 2)

Syntax hints:   ∧ wa 395   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ≠ wne 2932  Vcvv 3429   class class class wbr 5085   ↦ cmpt 5166  ‘cfv 6498  (class class class)co 7367  ℂcc 11036  ℝcr 11037  0cc0 11038  1c1 11039   + caddc 11041   · cmul 11043   < clt 11179   ≤ cle 11180   − cmin 11377   / cdiv 11807  ℕcn 12174  2c2 12236  ℤcz 12524  ℝ⁺crp 12942  ↑cexp 14023   ⇝ cli 15446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-cnex 11094  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115  ax-pre-sup 11116

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-er 8643  df-pm 8776  df-en 8894  df-dom 8895  df-sdom 8896  df-sup 9355  df-inf 9356  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-div 11808  df-nn 12175  df-2 12244  df-3 12245  df-n0 12438  df-z 12525  df-uz 12789  df-rp 12943  df-fl 13751  df-seq 13964  df-exp 14024  df-cj 15061  df-re 15062  df-im 15063  df-sqrt 15197  df-abs 15198  df-clim 15450  df-rlim 15451

This theorem is referenced by:  stirlinglem15  46516