Theorem stirlinglem1 38967

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 11599	. . . 4 ⊢ ℕ = (ℤ≥‘1)
2		1zzd 11285	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		stirlinglem1.4	. . . . . . . . 9 ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4		ax-1cn 9873	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
5		divcnv 14424	. . . . . . . . . 10 ⊢ (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
7	3, 6	eqbrtri 4604	. . . . . . . 8 ⊢ 𝐿 ⇝ 0
8	7	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐿 ⇝ 0)
9		stirlinglem1.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10		nnex 10903	. . . . . . . . . 10 ⊢ ℕ ∈ V
11	10	mptex 6390	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
12	9, 11	eqeltri 2684	. . . . . . . 8 ⊢ 𝐺 ∈ V
13	12	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐺 ∈ V)
14	3	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15		simpr 476	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
16	15	oveq2d 6565	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17		id 22	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18		nnrp 11718	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ+)
19	18	rpreccld 11758	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ+)
20	14, 16, 17, 19	fvmptd 6197	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) = (1 / 𝑘))
21		nnrecre 10934	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
22	20, 21	eqeltrd 2688	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) ∈ ℝ)
23	22	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿‘𝑘) ∈ ℝ)
24	9	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
25	15	oveq2d 6565	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
26	25	oveq1d 6564	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
27	26	oveq2d 6565	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28		2re 10967	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
29	28	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
30		nnre 10904	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
31	29, 30	remulcld 9949	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32		0le2 10988	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 2
33	32	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 2)
34	18	rpge0d 11752	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 𝑘)
35	29, 30, 33, 34	mulge0d 10483	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
36	31, 35	ge0p1rpd 11778	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ+)
37	36	rpreccld 11758	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ+)
38	24, 27, 17, 37	fvmptd 6197	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (1 / ((2 · 𝑘) + 1)))
39	37	rpred 11748	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
40	38, 39	eqeltrd 2688	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ∈ ℝ)
41	40	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)
42		1red 9934	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
43		0le1 10430	. . . . . . . . . . 11 ⊢ 0 ≤ 1
44	43	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 0 ≤ 1)
45	31, 42	readdcld 9948	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46		nncn 10905	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
47	46	mulid2d 9937	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48		1lt2 11071	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 1 < 2)
50	42, 29, 18, 49	ltmul1dd 11803	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
51	47, 50	eqbrtrrd 4607	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
52	31	ltp1d 10833	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
53	30, 31, 45, 51, 52	lttrd 10077	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
54	30, 45, 53	ltled 10064	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
55	18, 36, 42, 44, 54	lediv2ad 11770	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
56	55, 38, 20	3brtr4d 4615	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
57	56	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
58	37	rpge0d 11752	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
59	58, 38	breqtrrd 4611	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 0 ≤ (𝐺‘𝑘))
60	59	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))
61	1, 2, 8, 13, 23, 41, 57, 60	climsqz2 14220	. . . . . 6 ⊢ (⊤ → 𝐺 ⇝ 0)
62		1cnd 9935	. . . . . 6 ⊢ (⊤ → 1 ∈ ℂ)
63		stirlinglem1.2	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
64	10	mptex 6390	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
65	63, 64	eqeltri 2684	. . . . . . 7 ⊢ 𝐹 ∈ V
66	65	a1i 11	. . . . . 6 ⊢ (⊤ → 𝐹 ∈ V)
67	41	recnd 9947	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℂ)
68	63	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
69	27	oveq2d 6565	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70		1cnd 9935	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℂ)
71		2cnd 10970	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
72	71, 46	mulcld 9939	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
73	72, 70	addcld 9938	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
74	36	rpne0d 11753	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
75	73, 74	reccld 10673	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
76	70, 75	subcld 10271	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
77	68, 69, 17, 76	fvmptd 6197	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
78	38	eqcomd 2616	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺‘𝑘))
79	78	oveq2d 6565	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺‘𝑘)))
80	77, 79	eqtrd 2644	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
81	80	adantl 481	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
82	1, 2, 61, 62, 66, 67, 81	climsubc2 14217	. . . . 5 ⊢ (⊤ → 𝐹 ⇝ (1 − 0))
83		1m0e1 11008	. . . . 5 ⊢ (1 − 0) = 1
84	82, 83	syl6breq 4624	. . . 4 ⊢ (⊤ → 𝐹 ⇝ 1)
85	62	halfcld 11154	. . . 4 ⊢ (⊤ → (1 / 2) ∈ ℂ)
86		stirlinglem1.1	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
87	10	mptex 6390	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
88	86, 87	eqeltri 2684	. . . . 5 ⊢ 𝐻 ∈ V
89	88	a1i 11	. . . 4 ⊢ (⊤ → 𝐻 ∈ V)
90	77, 76	eqeltrd 2688	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
91	90	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
92		nncn 10905	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
93	92	sqcld 12868	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
94	93	mulid2d 9937	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
95	94	eqcomd 2616	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96		2cnd 10970	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℂ)
97	96, 92	mulcld 9939	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98		1cnd 9935	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 1 ∈ ℂ)
99	92, 97, 98	adddid 9943	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
100	92, 96, 92	mul12d 10124	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
101	92	sqvald 12867	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102	101	eqcomd 2616	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103	102	oveq2d 6565	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104	100, 103	eqtrd 2644	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
105	92	mulid1d 9936	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106	104, 105	oveq12d 6567	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107		2ne0 10990	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 2 ≠ 0)
109	92, 96, 108	divcan2d 10682	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110	109	eqcomd 2616	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111	110	oveq2d 6565	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
112	92	halfcld 11154	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
113	96, 93, 112	adddid 9943	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114	111, 113	eqtr4d 2647	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
115	99, 106, 114	3eqtrd 2648	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
116	95, 115	oveq12d 6567	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
117	93, 112	addcld 9938	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118		nnrp 11718	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ+)
119		2z 11286	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
120	119	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℤ)
121	118, 120	rpexpcld 12894	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ+)
122	118	rphalfcld 11760	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ+)
123	121, 122	rpaddcld 11763	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ+)
124	123	rpne0d 11753	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
125	98, 96, 93, 117, 108, 124	divmuldivd 10721	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
126	93, 112	pncand 10272	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127	126	eqcomd 2616	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128	127	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129	117, 112, 117, 124	divsubdird 10719	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130	117, 124	dividd 10678	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131	130	oveq1d 6564	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132	128, 129, 131	3eqtrd 2648	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133		nnne0 10930	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
134	96, 92, 133	divcld 10680	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
135	96, 92, 108, 133	divne0d 10696	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136	112, 117, 134, 124, 135	divcan5rd 10707	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
137	92, 96, 133, 108	divcan6d 10699	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
138	93, 112, 134	adddird 9944	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
139	93, 96, 92, 133	div12d 10716	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140		1e2m1 11013	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 = (2 − 1)
141	140	oveq2i 6560	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛↑1) = (𝑛↑(2 − 1))
142	92	exp1d 12865	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
143	92, 133, 120	expm1d 12880	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144	141, 142, 143	3eqtr3a 2668	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145	144	eqcomd 2616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146	145	oveq2d 6565	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147	139, 146	eqtrd 2644	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148	147, 137	oveq12d 6567	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149	138, 148	eqtrd 2644	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150	137, 149	oveq12d 6567	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151	136, 150	eqtr3d 2646	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152	151	oveq2d 6565	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153	132, 152	eqtrd 2644	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154	153	oveq2d 6565	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155	116, 125, 154	3eqtr2d 2650	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156	155	mpteq2ia 4668	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
157	86, 156	eqtri 2632	. . . . . . . 8 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158	157	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
159	69	oveq2d 6565	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
160	70	halfcld 11154	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161	160, 76	mulcld 9939	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162	158, 159, 17, 161	fvmptd 6197	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
163	77	oveq2d 6565	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (𝐹‘𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164	162, 163	eqtr4d 2647	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
165	164	adantl 481	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
166	1, 2, 84, 85, 89, 91, 165	climmulc2 14215	. . 3 ⊢ (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167	166	trud 1484	. 2 ⊢ 𝐻 ⇝ ((1 / 2) · 1)
168		halfcn 11124	. . 3 ⊢ (1 / 2) ∈ ℂ
169	168	mulid1i 9921	. 2 ⊢ ((1 / 2) · 1) = (1 / 2)
170	167, 169	breqtri 4608	1 ⊢ 𝐻 ⇝ (1 / 2)

Syntax hints:   ∧ wa 383   = wceq 1475  ⊤wtru 1476   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   class class class wbr 4583   ↦ cmpt 4643  ‘cfv 5804  (class class class)co 6549  ℂcc 9813  ℝcr 9814  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820   < clt 9953   ≤ cle 9954   − cmin 10145   / cdiv 10563  ℕcn 10897  2c2 10947  ℤcz 11254  ℝ⁺crp 11708  ↑cexp 12722   ⇝ cli 14063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-rp 11709  df-fl 12455  df-seq 12664  df-exp 12723  df-cj 13687  df-re 13688  df-im 13689  df-sqrt 13823  df-abs 13824  df-clim 14067  df-rlim 14068

This theorem is referenced by:  stirlinglem15  38981