stirlinglem1 - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > stirlinglem1		Structured version Visualization version GIF version

Theorem stirlinglem1 47223

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 13014	. . . 4 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12737	. . . 4 ⊢ (⊤ → 1 ∈ ℤ)
3		stirlinglem1.4	. . . . . . . . 9 ⊢ 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛))
4		ax-1cn 11268	. . . . . . . . . 10 ⊢ 1 ∈ ℂ
5		divcnv 16034	. . . . . . . . . 10 ⊢ (1 ∈ ℂ → (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0)
6	4, 5	ax-mp 5	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / 𝑛)) ⇝ 0
7	3, 6	eqbrtri 5128	. . . . . . . 8 ⊢ 𝐿 ⇝ 0
8	7	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐿 ⇝ 0)
9		stirlinglem1.3	. . . . . . . . 9 ⊢ 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1)))
10		nnex 12351	. . . . . . . . . 10 ⊢ ℕ ∈ V
11	10	mptex 7236	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))) ∈ V
12	9, 11	eqeltri 2859	. . . . . . . 8 ⊢ 𝐺 ∈ V
13	12	a1i 11	. . . . . . 7 ⊢ (⊤ → 𝐺 ∈ V)
14	3	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐿 = (𝑛 ∈ ℕ ↦ (1 / 𝑛)))
15		simpr 490	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → 𝑛 = 𝑘)
16	15	oveq2d 7443	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / 𝑛) = (1 / 𝑘))
17		id 23	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ)
18		nnrp 13142	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
19	18	rpreccld 13184	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ⁺)
20	14, 16, 17, 19	fvmptd 7009	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) = (1 / 𝑘))
21		nnrecre 12390	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
22	20, 21	eqeltrd 2863	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐿‘𝑘) ∈ ℝ)
23	22	adantl 487	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐿‘𝑘) ∈ ℝ)
24	9	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝐺 = (𝑛 ∈ ℕ ↦ (1 / ((2 · 𝑛) + 1))))
25	15	oveq2d 7443	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (2 · 𝑛) = (2 · 𝑘))
26	25	oveq1d 7442	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((2 · 𝑛) + 1) = ((2 · 𝑘) + 1))
27	26	oveq2d 7443	. . . . . . . . . 10 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 / ((2 · 𝑛) + 1)) = (1 / ((2 · 𝑘) + 1)))
28		2re 12427	. . . . . . . . . . . . . 14 ⊢ 2 ∈ ℝ
29	28	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℝ)
30		nnre 12352	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ)
31	29, 30	remulcld 11349	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℝ)
32		0le2 12455	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 2
33	32	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 2)
34	18	rpge0d 13178	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 0 ≤ 𝑘)
35	29, 30, 33, 34	mulge0d 11903	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (2 · 𝑘))
36	31, 35	ge0p1rpd 13204	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ⁺)
37	36	rpreccld 13184	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ⁺)
38	24, 27, 17, 37	fvmptd 7009	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) = (1 / ((2 · 𝑘) + 1)))
39	37	rpred 13174	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℝ)
40	38, 39	eqeltrd 2863	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ∈ ℝ)
41	40	adantl 487	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℝ)
42		1red 11319	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℝ)
43		0le1 11849	. . . . . . . . . . 11 ⊢ 0 ≤ 1
44	43	a1i 11	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 0 ≤ 1)
45	31, 42	readdcld 11348	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℝ)
46		nncn 12353	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
47	46	mullidd 11337	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) = 𝑘)
48		1lt2 12525	. . . . . . . . . . . . . . 15 ⊢ 1 < 2
49	48	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 1 < 2)
50	42, 29, 18, 49	ltmul1dd 13229	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 · 𝑘) < (2 · 𝑘))
51	47, 50	eqbrtrrd 5131	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 𝑘 < (2 · 𝑘))
52	31	ltp1d 12257	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) < ((2 · 𝑘) + 1))
53	30, 31, 45, 51, 52	lttrd 11481	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 𝑘 < ((2 · 𝑘) + 1))
54	30, 45, 53	ltled 11468	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 𝑘 ≤ ((2 · 𝑘) + 1))
55	18, 36, 42, 44, 54	lediv2ad 13196	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ≤ (1 / 𝑘))
56	55, 38, 20	3brtr4d 5139	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
57	56	adantl 487	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ≤ (𝐿‘𝑘))
58	37	rpge0d 13178	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / ((2 · 𝑘) + 1)))
59	58, 38	breqtrrd 5135	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → 0 ≤ (𝐺‘𝑘))
60	59	adantl 487	. . . . . . 7 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → 0 ≤ (𝐺‘𝑘))
61	1, 2, 8, 13, 23, 41, 57, 60	climsqz2 15821	. . . . . 6 ⊢ (⊤ → 𝐺 ⇝ 0)
62		1cnd 11312	. . . . . 6 ⊢ (⊤ → 1 ∈ ℂ)
63		stirlinglem1.2	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1))))
64	10	mptex 7236	. . . . . . . 8 ⊢ (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))) ∈ V
65	63, 64	eqeltri 2859	. . . . . . 7 ⊢ 𝐹 ∈ V
66	65	a1i 11	. . . . . 6 ⊢ (⊤ → 𝐹 ∈ V)
67	41	recnd 11347	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐺‘𝑘) ∈ ℂ)
68	63	a1i 11	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝐹 = (𝑛 ∈ ℕ ↦ (1 − (1 / ((2 · 𝑛) + 1)))))
69	27	oveq2d 7443	. . . . . . . . 9 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → (1 − (1 / ((2 · 𝑛) + 1))) = (1 − (1 / ((2 · 𝑘) + 1))))
70		1cnd 11312	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → 1 ∈ ℂ)
71		2cnd 12431	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → 2 ∈ ℂ)
72	71, 46	mulcld 11339	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (2 · 𝑘) ∈ ℂ)
73	72, 70	addcld 11338	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ∈ ℂ)
74	36	rpne0d 13179	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → ((2 · 𝑘) + 1) ≠ 0)
75	73, 74	reccld 12096	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) ∈ ℂ)
76	70, 75	subcld 11679	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) ∈ ℂ)
77	68, 69, 17, 76	fvmptd 7009	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (1 / ((2 · 𝑘) + 1))))
78	38	eqcomd 2769	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → (1 / ((2 · 𝑘) + 1)) = (𝐺‘𝑘))
79	78	oveq2d 7443	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 − (1 / ((2 · 𝑘) + 1))) = (1 − (𝐺‘𝑘)))
80	77, 79	eqtrd 2798	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
81	80	adantl 487	. . . . . 6 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) = (1 − (𝐺‘𝑘)))
82	1, 2, 61, 62, 66, 67, 81	climsubc2 15818	. . . . 5 ⊢ (⊤ → 𝐹 ⇝ (1 − 0))
83		1m0e1 12472	. . . . 5 ⊢ (1 − 0) = 1
84	82, 83	breqtrdi 5148	. . . 4 ⊢ (⊤ → 𝐹 ⇝ 1)
85	62	halfcld 12601	. . . 4 ⊢ (⊤ → (1 / 2) ∈ ℂ)
86		stirlinglem1.1	. . . . . 6 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))))
87	10	mptex 7236	. . . . . 6 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) ∈ V
88	86, 87	eqeltri 2859	. . . . 5 ⊢ 𝐻 ∈ V
89	88	a1i 11	. . . 4 ⊢ (⊤ → 𝐻 ∈ V)
90	77, 76	eqeltrd 2863	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
91	90	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
92		nncn 12353	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℂ)
93	92	sqcld 14297	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℂ)
94	93	mullidd 11337	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 · (𝑛↑2)) = (𝑛↑2))
95	94	eqcomd 2769	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (1 · (𝑛↑2)))
96		2cnd 12431	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℂ)
97	96, 92	mulcld 11339	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · 𝑛) ∈ ℂ)
98		1cnd 11312	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → 1 ∈ ℂ)
99	92, 97, 98	adddid 11343	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)))
100	92, 96, 92	mul12d 11529	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛 · 𝑛)))
101	92	sqvald 14296	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (𝑛 · 𝑛))
102	101	eqcomd 2769	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (𝑛 · 𝑛) = (𝑛↑2))
103	102	oveq2d 7443	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 · 𝑛)) = (2 · (𝑛↑2)))
104	100, 103	eqtrd 2798	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · (2 · 𝑛)) = (2 · (𝑛↑2)))
105	92	mulridd 11336	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 · 1) = 𝑛)
106	104, 105	oveq12d 7445	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛 · (2 · 𝑛)) + (𝑛 · 1)) = ((2 · (𝑛↑2)) + 𝑛))
107		2ne0 12459	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ≠ 0
108	107	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 2 ≠ 0)
109	92, 96, 108	divcan2d 12105	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 · (𝑛 / 2)) = 𝑛)
110	109	eqcomd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 = (2 · (𝑛 / 2)))
111	110	oveq2d 7443	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
112	92	halfcld 12601	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℂ)
113	96, 93, 112	adddid 11343	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) + (𝑛 / 2))) = ((2 · (𝑛↑2)) + (2 · (𝑛 / 2))))
114	111, 113	eqtr4d 2801	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((2 · (𝑛↑2)) + 𝑛) = (2 · ((𝑛↑2) + (𝑛 / 2))))
115	99, 106, 114	3eqtrd 2802	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → (𝑛 · ((2 · 𝑛) + 1)) = (2 · ((𝑛↑2) + (𝑛 / 2))))
116	95, 115	oveq12d 7445	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
117	93, 112	addcld 11338	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℂ)
118		nnrp 13142	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 𝑛 ∈ ℝ⁺)
119		2z 12738	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ ℤ
120	119	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → 2 ∈ ℤ)
121	118, 120	rpexpcld 14401	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) ∈ ℝ⁺)
122	118	rphalfcld 13186	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → (𝑛 / 2) ∈ ℝ⁺)
123	121, 122	rpaddcld 13189	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ∈ ℝ⁺)
124	123	rpne0d 13179	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) + (𝑛 / 2)) ≠ 0)
125	98, 96, 93, 117, 108, 124	divmuldivd 12144	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 · (𝑛↑2)) / (2 · ((𝑛↑2) + (𝑛 / 2)))))
126	93, 112	pncand 11680	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) = (𝑛↑2))
127	126	eqcomd 2769	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (𝑛↑2) = (((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)))
128	127	oveq1d 7442	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))))
129	117, 112, 117, 124	divsubdird 12142	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) − (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
130	117, 124	dividd 12101	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) = 1)
131	130	oveq1d 7442	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((((𝑛↑2) + (𝑛 / 2)) / ((𝑛↑2) + (𝑛 / 2))) − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
132	128, 129, 131	3eqtrd 2802	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))))
133		nnne0 12382	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → 𝑛 ≠ 0)
134	96, 92, 133	divcld 12103	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ∈ ℂ)
135	96, 92, 108, 133	divne0d 12119	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (2 / 𝑛) ≠ 0)
136	112, 117, 134, 124, 135	divcan5rd 12130	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))))
137	92, 96, 133, 108	divcan6d 12122	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) · (2 / 𝑛)) = 1)
138	93, 112, 134	adddird 11344	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))))
139	93, 96, 92, 133	div12d 12139	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · ((𝑛↑2) / 𝑛)))
140		1e2m1 12479	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 = (2 − 1)
141	140	oveq2i 7438	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛↑1) = (𝑛↑(2 − 1))
142	92	exp1d 14294	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑1) = 𝑛)
143	92, 133, 120	expm1d 14309	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑛 ∈ ℕ → (𝑛↑(2 − 1)) = ((𝑛↑2) / 𝑛))
144	141, 142, 143	3eqtr3a 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 ∈ ℕ → 𝑛 = ((𝑛↑2) / 𝑛))
145	144	eqcomd 2769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / 𝑛) = 𝑛)
146	145	oveq2d 7443	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ ℕ → (2 · ((𝑛↑2) / 𝑛)) = (2 · 𝑛))
147	139, 146	eqtrd 2798	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) · (2 / 𝑛)) = (2 · 𝑛))
148	147, 137	oveq12d 7445	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) · (2 / 𝑛)) + ((𝑛 / 2) · (2 / 𝑛))) = ((2 · 𝑛) + 1))
149	138, 148	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ ℕ → (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛)) = ((2 · 𝑛) + 1))
150	137, 149	oveq12d 7445	. . . . . . . . . . . . . . 15 ⊢ (𝑛 ∈ ℕ → (((𝑛 / 2) · (2 / 𝑛)) / (((𝑛↑2) + (𝑛 / 2)) · (2 / 𝑛))) = (1 / ((2 · 𝑛) + 1)))
151	136, 150	eqtr3d 2800	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ℕ → ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2))) = (1 / ((2 · 𝑛) + 1)))
152	151	oveq2d 7443	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 − ((𝑛 / 2) / ((𝑛↑2) + (𝑛 / 2)))) = (1 − (1 / ((2 · 𝑛) + 1))))
153	132, 152	eqtrd 2798	. . . . . . . . . . . 12 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2))) = (1 − (1 / ((2 · 𝑛) + 1))))
154	153	oveq2d 7443	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℕ → ((1 / 2) · ((𝑛↑2) / ((𝑛↑2) + (𝑛 / 2)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
155	116, 125, 154	3eqtr2d 2804	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℕ → ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1))) = ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
156	155	mpteq2ia 5202	. . . . . . . . 9 ⊢ (𝑛 ∈ ℕ ↦ ((𝑛↑2) / (𝑛 · ((2 · 𝑛) + 1)))) = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
157	86, 156	eqtri 2786	. . . . . . . 8 ⊢ 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))))
158	157	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → 𝐻 = (𝑛 ∈ ℕ ↦ ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1))))))
159	69	oveq2d 7443	. . . . . . 7 ⊢ ((𝑘 ∈ ℕ ∧ 𝑛 = 𝑘) → ((1 / 2) · (1 − (1 / ((2 · 𝑛) + 1)))) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
160	70	halfcld 12601	. . . . . . . 8 ⊢ (𝑘 ∈ ℕ → (1 / 2) ∈ ℂ)
161	160, 76	mulcld 11339	. . . . . . 7 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))) ∈ ℂ)
162	158, 159, 17, 161	fvmptd 7009	. . . . . 6 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
163	77	oveq2d 7443	. . . . . 6 ⊢ (𝑘 ∈ ℕ → ((1 / 2) · (𝐹‘𝑘)) = ((1 / 2) · (1 − (1 / ((2 · 𝑘) + 1)))))
164	162, 163	eqtr4d 2801	. . . . 5 ⊢ (𝑘 ∈ ℕ → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
165	164	adantl 487	. . . 4 ⊢ ((⊤ ∧ 𝑘 ∈ ℕ) → (𝐻‘𝑘) = ((1 / 2) · (𝐹‘𝑘)))
166	1, 2, 84, 85, 89, 91, 165	climmulc2 15816	. . 3 ⊢ (⊤ → 𝐻 ⇝ ((1 / 2) · 1))
167	166	mptru 1576	. 2 ⊢ 𝐻 ⇝ ((1 / 2) · 1)
168		halfcn 12570	. . 3 ⊢ (1 / 2) ∈ ℂ
169	168	mulridi 11323	. 2 ⊢ ((1 / 2) · 1) = (1 / 2)
170	167, 169	breqtri 5132	1 ⊢ 𝐻 ⇝ (1 / 2)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1569 ⊤wtru 1570 ∈ wcel 2146 ≠ wne 2958 Vcvv 3453 class class class wbr 5105 ↦ cmpt 5188 ‘cfv 6546 (class class class)co 7427 ℂcc 11208 ℝcr 11209 0cc0 11210 1c1 11211 + caddc 11213 · cmul 11215 < clt 11353 ≤ cle 11354 − cmin 11551 / cdiv 11983 ℕcn 12345 2c2 12407 ℤcz 12703 ℝ⁺crp 13130 ↑cexp 14214 ⇝ cli 15663

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1944 ax-6 2001 ax-7 2042 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2196 ax-12 2215 ax-ext 2735 ax-rep 5234 ax-sep 5251 ax-nul 5262 ax-pow 5330 ax-pr 5394 ax-un 7758 ax-cnex 11266 ax-resscn 11267 ax-1cn 11268 ax-icn 11269 ax-addcl 11270 ax-addrcl 11271 ax-mulcl 11272 ax-mulrcl 11273 ax-mulcom 11274 ax-addass 11275 ax-mulass 11276 ax-distr 11277 ax-i2m1 11278 ax-1ne0 11279 ax-1rid 11280 ax-rnegex 11281 ax-rrecex 11282 ax-cnre 11283 ax-pre-lttri 11284 ax-pre-lttrn 11285 ax-pre-ltadd 11286 ax-pre-mulgt0 11287 ax-pre-sup 11288

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2101 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3455 df-sbc 3742 df-csb 3851 df-ss 3900 df-pss 4016 df-dif 4049 df-in 4093 df-un 4153 df-nul 4281 df-if 4485 df-pw 4561 df-sn 4588 df-pr 4590 df-op 4838 df-uni 4870 df-iun 4955 df-br 5106 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5549 df-eprel 5554 df-po 5562 df-so 5563 df-fr 5607 df-we 5609 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6310 df-ord 6371 df-on 6372 df-lim 6373 df-suc 6374 df-iota 6500 df-fun 6548 df-fn 6549 df-f 6550 df-f1 6551 df-fo 6552 df-f1o 6553 df-fv 6554 df-riota 7384 df-ov 7430 df-oprab 7431 df-mpo 7432 df-om 7885 df-2nd 8009 df-frecs 8310 df-wrecs 8341 df-recs 8390 df-rdg 8429 df-er 8728 df-pm 8861 df-en 8985 df-dom 8986 df-sdom 8987 df-sup 9444 df-inf 9445 df-pnf 11355 df-mnf 11356 df-xr 11357 df-ltxr 11358 df-le 11359 df-sub 11553 df-neg 11554 df-div 11984 df-nn 12346 df-2 12415 df-3 12416 df-n0 12617 df-z 12704 df-uz 12976 df-rp 13131 df-fl 13942 df-seq 14155 df-exp 14215 df-cj 15278 df-re 15279 df-im 15280 df-sqrt 15414 df-abs 15415 df-clim 15667 df-rlim 15668

This theorem is used by: stirlinglem15 47237

W3C validator