Theorem stirlinglem1 46260

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 12788	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 12520	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		stirlinglem1.4	. . . . . . . . 9 ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4		ax-1cn 11082	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
5		divcnv 15774	. . . . . . . . . 10 ⊢ (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
7	3, 6	eqbrtri 5117	. . . . . . . 8 ⊢ 𝐿 ⇝ 0
8	7	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐿 ⇝ 0)
9		stirlinglem1.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10		nnex 12149	. . . . . . . . . 10 ⊢ ℕ ∈ V
11	10	mptex 7167	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
12	9, 11	eqeltri 2830	. . . . . . . 8 ⊢ 𝐺 ∈ V
13	12	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐺 ∈ V)
14	3	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15		simpr 484	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
16	15	oveq2d 7372	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17		id 22	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18		nnrp 12915	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
19	18	rpreccld 12957	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
20	14, 16, 17, 19	fvmptd 6946	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) = (1 / 𝑘))
21		nnrecre 12185	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
22	20, 21	eqeltrd 2834	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) ∈ ℝ)
23	22	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿‘𝑘) ∈ ℝ)
24	9	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
25	15	oveq2d 7372	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
26	25	oveq1d 7371	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
27	26	oveq2d 7372	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28		2re 12217	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
29	28	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
30		nnre 12150	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
31	29, 30	remulcld 11160	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32		0le2 12245	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 2
33	32	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 2)
34	18	rpge0d 12951	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 𝑘)
35	29, 30, 33, 34	mulge0d 11712	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
36	31, 35	ge0p1rpd 12977	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ+)
37	36	rpreccld 12957	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
38	24, 27, 17, 37	fvmptd 6946	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (1 / ((2 · 𝑘) + 1)))
39	37	rpred 12947	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
40	38, 39	eqeltrd 2834	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ∈ ℝ)
41	40	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)
42		1red 11131	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
43		0le1 11658	. . . . . . . . . . 11 ⊢ 0 ≤ 1
44	43	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 0 ≤ 1)
45	31, 42	readdcld 11159	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46		nncn 12151	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
47	46	mullidd 11148	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48		1lt2 12309	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 1 < 2)
50	42, 29, 18, 49	ltmul1dd 13002	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
51	47, 50	eqbrtrrd 5120	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
52	31	ltp1d 12070	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
53	30, 31, 45, 51, 52	lttrd 11292	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
54	30, 45, 53	ltled 11279	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
55	18, 36, 42, 44, 54	lediv2ad 12969	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
56	55, 38, 20	3brtr4d 5128	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
57	56	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
58	37	rpge0d 12951	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
59	58, 38	breqtrrd 5124	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 0 ≤ (𝐺‘𝑘))
60	59	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))
61	1, 2, 8, 13, 23, 41, 57, 60	climsqz2 15563	. . . . . 6 ⊢ (⊤ → 𝐺 ⇝ 0)
62		1cnd 11125	. . . . . 6 ⊢ (⊤ → 1 ∈ ℂ)
63		stirlinglem1.2	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
64	10	mptex 7167	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
65	63, 64	eqeltri 2830	. . . . . . 7 ⊢ 𝐹 ∈ V
66	65	a1i 11	. . . . . 6 ⊢ (⊤ → 𝐹 ∈ V)
67	41	recnd 11158	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℂ)
68	63	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
69	27	oveq2d 7372	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70		1cnd 11125	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℂ)
71		2cnd 12221	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
72	71, 46	mulcld 11150	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
73	72, 70	addcld 11149	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
74	36	rpne0d 12952	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
75	73, 74	reccld 11908	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
76	70, 75	subcld 11490	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
77	68, 69, 17, 76	fvmptd 6946	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
78	38	eqcomd 2740	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺‘𝑘))
79	78	oveq2d 7372	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺‘𝑘)))
80	77, 79	eqtrd 2769	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
81	80	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
82	1, 2, 61, 62, 66, 67, 81	climsubc2 15560	. . . . 5 ⊢ (⊤ → 𝐹 ⇝ (1 − 0))
83		1m0e1 12259	. . . . 5 ⊢ (1 − 0) = 1
84	82, 83	breqtrdi 5137	. . . 4 ⊢ (⊤ → 𝐹 ⇝ 1)
85	62	halfcld 12384	. . . 4 ⊢ (⊤ → (1 / 2) ∈ ℂ)
86		stirlinglem1.1	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
87	10	mptex 7167	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
88	86, 87	eqeltri 2830	. . . . 5 ⊢ 𝐻 ∈ V
89	88	a1i 11	. . . 4 ⊢ (⊤ → 𝐻 ∈ V)
90	77, 76	eqeltrd 2834	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
91	90	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
92		nncn 12151	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
93	92	sqcld 14065	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
94	93	mullidd 11148	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
95	94	eqcomd 2740	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96		2cnd 12221	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℂ)
97	96, 92	mulcld 11150	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98		1cnd 11125	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 1 ∈ ℂ)
99	92, 97, 98	adddid 11154	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
100	92, 96, 92	mul12d 11340	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
101	92	sqvald 14064	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102	101	eqcomd 2740	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103	102	oveq2d 7372	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104	100, 103	eqtrd 2769	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
105	92	mulridd 11147	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106	104, 105	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107		2ne0 12247	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 2 ≠ 0)
109	92, 96, 108	divcan2d 11917	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110	109	eqcomd 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111	110	oveq2d 7372	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
112	92	halfcld 12384	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
113	96, 93, 112	adddid 11154	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114	111, 113	eqtr4d 2772	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
115	99, 106, 114	3eqtrd 2773	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
116	95, 115	oveq12d 7374	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
117	93, 112	addcld 11149	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118		nnrp 12915	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
119		2z 12521	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
120	119	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℤ)
121	118, 120	rpexpcld 14168	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ+)
122	118	rphalfcld 12959	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ+)
123	121, 122	rpaddcld 12962	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ+)
124	123	rpne0d 12952	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
125	98, 96, 93, 117, 108, 124	divmuldivd 11956	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
126	93, 112	pncand 11491	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127	126	eqcomd 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128	127	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129	117, 112, 117, 124	divsubdird 11954	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130	117, 124	dividd 11913	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131	130	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132	128, 129, 131	3eqtrd 2773	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133		nnne0 12177	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
134	96, 92, 133	divcld 11915	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
135	96, 92, 108, 133	divne0d 11931	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136	112, 117, 134, 124, 135	divcan5rd 11942	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
137	92, 96, 133, 108	divcan6d 11934	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
138	93, 112, 134	adddird 11155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
139	93, 96, 92, 133	div12d 11951	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140		1e2m1 12265	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 = (2 − 1)
141	140	oveq2i 7367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛↑1) = (𝑛↑(2 − 1))
142	92	exp1d 14062	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
143	92, 133, 120	expm1d 14077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144	141, 142, 143	3eqtr3a 2793	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145	144	eqcomd 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146	145	oveq2d 7372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147	139, 146	eqtrd 2769	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148	147, 137	oveq12d 7374	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149	138, 148	eqtrd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150	137, 149	oveq12d 7374	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151	136, 150	eqtr3d 2771	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152	151	oveq2d 7372	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153	132, 152	eqtrd 2769	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154	153	oveq2d 7372	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155	116, 125, 154	3eqtr2d 2775	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156	155	mpteq2ia 5191	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
157	86, 156	eqtri 2757	. . . . . . . 8 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158	157	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
159	69	oveq2d 7372	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
160	70	halfcld 12384	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161	160, 76	mulcld 11150	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162	158, 159, 17, 161	fvmptd 6946	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
163	77	oveq2d 7372	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (𝐹‘𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164	162, 163	eqtr4d 2772	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
165	164	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
166	1, 2, 84, 85, 89, 91, 165	climmulc2 15558	. . 3 ⊢ (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167	166	mptru 1548	. 2 ⊢ 𝐻 ⇝ ((1 / 2) · 1)
168		halfcn 12353	. . 3 ⊢ (1 / 2) ∈ ℂ
169	168	mulridi 11134	. 2 ⊢ ((1 / 2) · 1) = (1 / 2)
170	167, 169	breqtri 5121	1 ⊢ 𝐻 ⇝ (1 / 2)

Syntax hints:   ∧ wa 395   = wceq 1541  ⊤wtru 1542   ∈ wcel 2113   ≠ wne 2930  Vcvv 3438   class class class wbr 5096   ↦ cmpt 5177  ‘cfv 6490  (class class class)co 7356  ℂcc 11022  ℝcr 11023  0cc0 11024  1c1 11025   + caddc 11027   · cmul 11029   < clt 11164   ≤ cle 11165   − cmin 11362   / cdiv 11792  ℕcn 12143  2c2 12198  ℤcz 12486  ℝ⁺crp 12903  ↑cexp 13982   ⇝ cli 15405

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 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101  ax-pre-sup 11102

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-pm 8764  df-en 8882  df-dom 8883  df-sdom 8884  df-sup 9343  df-inf 9344  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-div 11793  df-nn 12144  df-2 12206  df-3 12207  df-n0 12400  df-z 12487  df-uz 12750  df-rp 12904  df-fl 13710  df-seq 13923  df-exp 13983  df-cj 15020  df-re 15021  df-im 15022  df-sqrt 15156  df-abs 15157  df-clim 15409  df-rlim 15410

This theorem is referenced by:  stirlinglem15  46274