stirlinglem6 - Mathbox for Glauco Siliprandi

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

Theorem stirlinglem6 43132

Description: A series that converges to log (N+1)/N. (Contributed by Glauco Siliprandi, 29-Jun-2017.)

**Hypothesis**
Ref	Expression
stirlinglem6.1	⊢ 𝐻 = (𝑗 ∈ ℕ₀ ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))

**Assertion**
Ref	Expression
stirlinglem6	⊢ (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))

Distinct variable group: 𝑗,𝑁 Allowed substitution hint: 𝐻(𝑗)

**Proof of Theorem stirlinglem6**
Step	Hyp	Ref	Expression
1		eqid 2758	. . 3 ⊢ (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ ((-1↑(𝑗 − 1)) · (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗)))
2		eqid 2758	. . 3 ⊢ (𝑗 ∈ ℕ ↦ (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗)) = (𝑗 ∈ ℕ ↦ (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗))
3		eqid 2758	. . 3 ⊢ (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗)) + (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗))) = (𝑗 ∈ ℕ ↦ (((-1↑(𝑗 − 1)) · (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗)) + (((1 / ((2 · 𝑁) + 1))↑𝑗) / 𝑗)))
4		stirlinglem6.1	. . 3 ⊢ 𝐻 = (𝑗 ∈ ℕ₀ ↦ (2 · ((1 / ((2 · 𝑗) + 1)) · ((1 / ((2 · 𝑁) + 1))↑((2 · 𝑗) + 1)))))
5		eqid 2758	. . 3 ⊢ (𝑗 ∈ ℕ₀ ↦ ((2 · 𝑗) + 1)) = (𝑗 ∈ ℕ₀ ↦ ((2 · 𝑗) + 1))
6		2re 11761	. . . . . . 7 ⊢ 2 ∈ ℝ
7	6	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℝ)
8		nnre 11694	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
9	7, 8	remulcld 10722	. . . . 5 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ)
10		0le2 11789	. . . . . . 7 ⊢ 0 ≤ 2
11	10	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 0 ≤ 2)
12		0red 10695	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 0 ∈ ℝ)
13		nngt0 11718	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 0 < 𝑁)
14	12, 8, 13	ltled 10839	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 0 ≤ 𝑁)
15	7, 8, 11, 14	mulge0d 11268	. . . . 5 ⊢ (𝑁 ∈ ℕ → 0 ≤ (2 · 𝑁))
16	9, 15	ge0p1rpd 12515	. . . 4 ⊢ (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℝ⁺)
17	16	rpreccld 12495	. . 3 ⊢ (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) ∈ ℝ⁺)
18		1red 10693	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ)
19	18	renegcld 11118	. . . . 5 ⊢ (𝑁 ∈ ℕ → -1 ∈ ℝ)
20	17	rpred 12485	. . . . 5 ⊢ (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) ∈ ℝ)
21		neg1lt0 11804	. . . . . 6 ⊢ -1 < 0
22	21	a1i 11	. . . . 5 ⊢ (𝑁 ∈ ℕ → -1 < 0)
23	17	rpgt0d 12488	. . . . 5 ⊢ (𝑁 ∈ ℕ → 0 < (1 / ((2 · 𝑁) + 1)))
24	19, 12, 20, 22, 23	lttrd 10852	. . . 4 ⊢ (𝑁 ∈ ℕ → -1 < (1 / ((2 · 𝑁) + 1)))
25		1rp 12447	. . . . . 6 ⊢ 1 ∈ ℝ⁺
26	25	a1i 11	. . . . 5 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℝ⁺)
27		1cnd 10687	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
28	27	div1d 11459	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (1 / 1) = 1)
29		2rp 12448	. . . . . . . . 9 ⊢ 2 ∈ ℝ⁺
30	29	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℝ⁺)
31		nnrp 12454	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ⁺)
32	30, 31	rpmulcld 12501	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℝ⁺)
33	18, 32	ltaddrp2d 12519	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 1 < ((2 · 𝑁) + 1))
34	28, 33	eqbrtrd 5058	. . . . 5 ⊢ (𝑁 ∈ ℕ → (1 / 1) < ((2 · 𝑁) + 1))
35	26, 16, 34	ltrec1d 12505	. . . 4 ⊢ (𝑁 ∈ ℕ → (1 / ((2 · 𝑁) + 1)) < 1)
36	20, 18	absltd 14850	. . . 4 ⊢ (𝑁 ∈ ℕ → ((abs‘(1 / ((2 · 𝑁) + 1))) < 1 ↔ (-1 < (1 / ((2 · 𝑁) + 1)) ∧ (1 / ((2 · 𝑁) + 1)) < 1)))
37	24, 35, 36	mpbir2and 712	. . 3 ⊢ (𝑁 ∈ ℕ → (abs‘(1 / ((2 · 𝑁) + 1))) < 1)
38	1, 2, 3, 4, 5, 17, 37	stirlinglem5 43131	. 2 ⊢ (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((1 + (1 / ((2 · 𝑁) + 1))) / (1 − (1 / ((2 · 𝑁) + 1))))))
39		2cnd 11765	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 2 ∈ ℂ)
40		nncn 11695	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
41	39, 40	mulcld 10712	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) ∈ ℂ)
42	41, 27	addcld 10711	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℂ)
43	9, 18	readdcld 10721	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ∈ ℝ)
44		2pos 11790	. . . . . . . . . . . 12 ⊢ 0 < 2
45	44	a1i 11	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → 0 < 2)
46	7, 8, 45, 13	mulgt0d 10846	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 0 < (2 · 𝑁))
47	9	ltp1d 11621	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) < ((2 · 𝑁) + 1))
48	12, 9, 43, 46, 47	lttrd 10852	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → 0 < ((2 · 𝑁) + 1))
49	48	gt0ne0d 11255	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((2 · 𝑁) + 1) ≠ 0)
50	42, 49	dividd 11465	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) = 1)
51	50	eqcomd 2764	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 1 = (((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)))
52	51	oveq1d 7171	. . . . 5 ⊢ (𝑁 ∈ ℕ → (1 + (1 / ((2 · 𝑁) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) + (1 / ((2 · 𝑁) + 1))))
53	51	oveq1d 7171	. . . . 5 ⊢ (𝑁 ∈ ℕ → (1 − (1 / ((2 · 𝑁) + 1))) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) − (1 / ((2 · 𝑁) + 1))))
54	52, 53	oveq12d 7174	. . . 4 ⊢ (𝑁 ∈ ℕ → ((1 + (1 / ((2 · 𝑁) + 1))) / (1 − (1 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) + (1 / ((2 · 𝑁) + 1))) / ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) − (1 / ((2 · 𝑁) + 1)))))
55	42, 27, 42, 49	divdird 11505	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) + 1) / ((2 · 𝑁) + 1)) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) + (1 / ((2 · 𝑁) + 1))))
56	55	eqcomd 2764	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) + (1 / ((2 · 𝑁) + 1))) = ((((2 · 𝑁) + 1) + 1) / ((2 · 𝑁) + 1)))
57	42, 27, 42, 49	divsubdird 11506	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) − 1) / ((2 · 𝑁) + 1)) = ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) − (1 / ((2 · 𝑁) + 1))))
58	57	eqcomd 2764	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) − (1 / ((2 · 𝑁) + 1))) = ((((2 · 𝑁) + 1) − 1) / ((2 · 𝑁) + 1)))
59	56, 58	oveq12d 7174	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) + (1 / ((2 · 𝑁) + 1))) / ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) − (1 / ((2 · 𝑁) + 1)))) = (((((2 · 𝑁) + 1) + 1) / ((2 · 𝑁) + 1)) / ((((2 · 𝑁) + 1) − 1) / ((2 · 𝑁) + 1))))
60	41, 27, 27	addassd 10714	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) + 1) = ((2 · 𝑁) + (1 + 1)))
61		1p1e2 11812	. . . . . . . . . 10 ⊢ (1 + 1) = 2
62	61	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (1 + 1) = 2)
63	62	oveq2d 7172	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((2 · 𝑁) + (1 + 1)) = ((2 · 𝑁) + 2))
64	39	mulid1d 10709	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (2 · 1) = 2)
65	64	eqcomd 2764	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → 2 = (2 · 1))
66	65	oveq2d 7172	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((2 · 𝑁) + 2) = ((2 · 𝑁) + (2 · 1)))
67	39, 40, 27	adddid 10716	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (2 · (𝑁 + 1)) = ((2 · 𝑁) + (2 · 1)))
68	66, 67	eqtr4d 2796	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((2 · 𝑁) + 2) = (2 · (𝑁 + 1)))
69	60, 63, 68	3eqtrd 2797	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) + 1) = (2 · (𝑁 + 1)))
70	69	oveq1d 7171	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) + 1) / ((2 · 𝑁) + 1)) = ((2 · (𝑁 + 1)) / ((2 · 𝑁) + 1)))
71	41, 27	pncand 11049	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (((2 · 𝑁) + 1) − 1) = (2 · 𝑁))
72	71	oveq1d 7171	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((((2 · 𝑁) + 1) − 1) / ((2 · 𝑁) + 1)) = ((2 · 𝑁) / ((2 · 𝑁) + 1)))
73	70, 72	oveq12d 7174	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) + 1) / ((2 · 𝑁) + 1)) / ((((2 · 𝑁) + 1) − 1) / ((2 · 𝑁) + 1))) = (((2 · (𝑁 + 1)) / ((2 · 𝑁) + 1)) / ((2 · 𝑁) / ((2 · 𝑁) + 1))))
74	59, 73	eqtrd 2793	. . . 4 ⊢ (𝑁 ∈ ℕ → (((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) + (1 / ((2 · 𝑁) + 1))) / ((((2 · 𝑁) + 1) / ((2 · 𝑁) + 1)) − (1 / ((2 · 𝑁) + 1)))) = (((2 · (𝑁 + 1)) / ((2 · 𝑁) + 1)) / ((2 · 𝑁) / ((2 · 𝑁) + 1))))
75	40, 27	addcld 10711	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℂ)
76	39, 75	mulcld 10712	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (2 · (𝑁 + 1)) ∈ ℂ)
77	46	gt0ne0d 11255	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (2 · 𝑁) ≠ 0)
78	76, 41, 42, 77, 49	divcan7d 11495	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((2 · (𝑁 + 1)) / ((2 · 𝑁) + 1)) / ((2 · 𝑁) / ((2 · 𝑁) + 1))) = ((2 · (𝑁 + 1)) / (2 · 𝑁)))
79	45	gt0ne0d 11255	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 2 ≠ 0)
80	13	gt0ne0d 11255	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ≠ 0)
81	39, 39, 75, 40, 79, 80	divmuldivd 11508	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((2 / 2) · ((𝑁 + 1) / 𝑁)) = ((2 · (𝑁 + 1)) / (2 · 𝑁)))
82	81	eqcomd 2764	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((2 · (𝑁 + 1)) / (2 · 𝑁)) = ((2 / 2) · ((𝑁 + 1) / 𝑁)))
83	39, 79	dividd 11465	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (2 / 2) = 1)
84	83	oveq1d 7171	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((2 / 2) · ((𝑁 + 1) / 𝑁)) = (1 · ((𝑁 + 1) / 𝑁)))
85	75, 40, 80	divcld 11467	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) / 𝑁) ∈ ℂ)
86	85	mulid2d 10710	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (1 · ((𝑁 + 1) / 𝑁)) = ((𝑁 + 1) / 𝑁))
87	84, 86	eqtrd 2793	. . . . 5 ⊢ (𝑁 ∈ ℕ → ((2 / 2) · ((𝑁 + 1) / 𝑁)) = ((𝑁 + 1) / 𝑁))
88	78, 82, 87	3eqtrd 2797	. . . 4 ⊢ (𝑁 ∈ ℕ → (((2 · (𝑁 + 1)) / ((2 · 𝑁) + 1)) / ((2 · 𝑁) / ((2 · 𝑁) + 1))) = ((𝑁 + 1) / 𝑁))
89	54, 74, 88	3eqtrd 2797	. . 3 ⊢ (𝑁 ∈ ℕ → ((1 + (1 / ((2 · 𝑁) + 1))) / (1 − (1 / ((2 · 𝑁) + 1)))) = ((𝑁 + 1) / 𝑁))
90	89	fveq2d 6667	. 2 ⊢ (𝑁 ∈ ℕ → (log‘((1 + (1 / ((2 · 𝑁) + 1))) / (1 − (1 / ((2 · 𝑁) + 1))))) = (log‘((𝑁 + 1) / 𝑁)))
91	38, 90	breqtrd 5062	1 ⊢ (𝑁 ∈ ℕ → seq0( + , 𝐻) ⇝ (log‘((𝑁 + 1) / 𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1538 ∈ wcel 2111 class class class wbr 5036 ↦ cmpt 5116 ‘cfv 6340 (class class class)co 7156 ℝcr 10587 0cc0 10588 1c1 10589 + caddc 10591 · cmul 10593 < clt 10726 ≤ cle 10727 − cmin 10921 -cneg 10922 / cdiv 11348 ℕcn 11687 2c2 11742 ℕ₀cn0 11947 ℝ⁺crp 12443 seqcseq 13431 ↑cexp 13492 abscabs 14654 ⇝ cli 14902 logclog 25259

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 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5160 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465 ax-inf2 9150 ax-cnex 10644 ax-resscn 10645 ax-1cn 10646 ax-icn 10647 ax-addcl 10648 ax-addrcl 10649 ax-mulcl 10650 ax-mulrcl 10651 ax-mulcom 10652 ax-addass 10653 ax-mulass 10654 ax-distr 10655 ax-i2m1 10656 ax-1ne0 10657 ax-1rid 10658 ax-rnegex 10659 ax-rrecex 10660 ax-cnre 10661 ax-pre-lttri 10662 ax-pre-lttrn 10663 ax-pre-ltadd 10664 ax-pre-mulgt0 10665 ax-pre-sup 10666 ax-addf 10667 ax-mulf 10668

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-nel 3056 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-iin 4889 df-br 5037 df-opab 5099 df-mpt 5117 df-tr 5143 df-id 5434 df-eprel 5439 df-po 5447 df-so 5448 df-fr 5487 df-se 5488 df-we 5489 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-ord 6177 df-on 6178 df-lim 6179 df-suc 6180 df-iota 6299 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-isom 6349 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-of 7411 df-om 7586 df-1st 7699 df-2nd 7700 df-supp 7842 df-wrecs 7963 df-recs 8024 df-rdg 8062 df-1o 8118 df-2o 8119 df-oadd 8122 df-er 8305 df-map 8424 df-pm 8425 df-ixp 8493 df-en 8541 df-dom 8542 df-sdom 8543 df-fin 8544 df-fsupp 8880 df-fi 8921 df-sup 8952 df-inf 8953 df-oi 9020 df-card 9414 df-pnf 10728 df-mnf 10729 df-xr 10730 df-ltxr 10731 df-le 10732 df-sub 10923 df-neg 10924 df-div 11349 df-nn 11688 df-2 11750 df-3 11751 df-4 11752 df-5 11753 df-6 11754 df-7 11755 df-8 11756 df-9 11757 df-n0 11948 df-xnn0 12020 df-z 12034 df-dec 12151 df-uz 12296 df-q 12402 df-rp 12444 df-xneg 12561 df-xadd 12562 df-xmul 12563 df-ioo 12796 df-ioc 12797 df-ico 12798 df-icc 12799 df-fz 12953 df-fzo 13096 df-fl 13224 df-mod 13300 df-seq 13432 df-exp 13493 df-fac 13697 df-bc 13726 df-hash 13754 df-shft 14487 df-cj 14519 df-re 14520 df-im 14521 df-sqrt 14655 df-abs 14656 df-limsup 14889 df-clim 14906 df-rlim 14907 df-sum 15104 df-ef 15482 df-sin 15484 df-cos 15485 df-tan 15486 df-pi 15487 df-dvds 15669 df-struct 16557 df-ndx 16558 df-slot 16559 df-base 16561 df-sets 16562 df-ress 16563 df-plusg 16650 df-mulr 16651 df-starv 16652 df-sca 16653 df-vsca 16654 df-ip 16655 df-tset 16656 df-ple 16657 df-ds 16659 df-unif 16660 df-hom 16661 df-cco 16662 df-rest 16768 df-topn 16769 df-0g 16787 df-gsum 16788 df-topgen 16789 df-pt 16790 df-prds 16793 df-xrs 16847 df-qtop 16852 df-imas 16853 df-xps 16855 df-mre 16929 df-mrc 16930 df-acs 16932 df-mgm 17932 df-sgrp 17981 df-mnd 17992 df-submnd 18037 df-mulg 18306 df-cntz 18528 df-cmn 18989 df-psmet 20172 df-xmet 20173 df-met 20174 df-bl 20175 df-mopn 20176 df-fbas 20177 df-fg 20178 df-cnfld 20181 df-top 21608 df-topon 21625 df-topsp 21647 df-bases 21660 df-cld 21733 df-ntr 21734 df-cls 21735 df-nei 21812 df-lp 21850 df-perf 21851 df-cn 21941 df-cnp 21942 df-haus 22029 df-cmp 22101 df-tx 22276 df-hmeo 22469 df-fil 22560 df-fm 22652 df-flim 22653 df-flf 22654 df-xms 23036 df-ms 23037 df-tms 23038 df-cncf 23593 df-limc 24579 df-dv 24580 df-ulm 25085 df-log 25261

This theorem is referenced by: stirlinglem7 43133

W3C validator