Theorem 0sgm

Description: The value of the sum-of-divisors function, usually denoted σ₀(n). (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	0sgm	$$⊢A\in \mathbb{N}\to 0\sigma A=\left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|$$

Proof

Step	Hyp	Ref	Expression
1		0z	$$⊢0\in \mathbb{Z}$$
2		sgmval2	$$⊢\left(0\in \mathbb{Z}\wedge A\in \mathbb{N}\right)\to 0\sigma A=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel A\right\}}{k}^0$$
3	1 2	mpan	$$⊢A\in \mathbb{N}\to 0\sigma A=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel A\right\}}{k}^0$$
4		elrabi	$$⊢k\in \left\{p\in \mathbb{N}|p\parallel A\right\}\to k\in \mathbb{N}$$
5	4	nncnd	$$⊢k\in \left\{p\in \mathbb{N}|p\parallel A\right\}\to k\in ℂ$$
6	5	exp0d	$$⊢k\in \left\{p\in \mathbb{N}|p\parallel A\right\}\to k^0=1$$
7	6	sumeq2i	$$⊢\sum _{k\in \left\{p\in \mathbb{N}|p\parallel A\right\}}{k}^0=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel A\right\}}1$$
8		fzfid	$$⊢A\in \mathbb{N}\to \left(1\dots A\right)\in \mathrm{Fin}$$
9		dvdsssfz1	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{N}|p\parallel A\right\}\subseteq \left(1\dots A\right)$$
10	8 9	ssfid	$$⊢A\in \mathbb{N}\to \left\{p\in \mathbb{N}|p\parallel A\right\}\in \mathrm{Fin}$$
11		ax-1cn	$$⊢1\in ℂ$$
12		fsumconst	$$⊢\left(\left\{p\in \mathbb{N}|p\parallel A\right\}\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel A\right\}}1=\left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|\cdot 1$$
13	10 11 12	sylancl	$$⊢A\in \mathbb{N}\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel A\right\}}1=\left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|\cdot 1$$
14	7 13	eqtrid	$$⊢A\in \mathbb{N}\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel A\right\}}{k}^0=\left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|\cdot 1$$
15		hashcl	$$⊢\left\{p\in \mathbb{N}|p\parallel A\right\}\in \mathrm{Fin}\to \left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|\in {\mathbb{N}}_0$$
16	10 15	syl	$$⊢A\in \mathbb{N}\to \left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|\in {\mathbb{N}}_0$$
17	16	nn0cnd	$$⊢A\in \mathbb{N}\to \left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|\in ℂ$$
18	17	mulridd	$$⊢A\in \mathbb{N}\to \left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|\cdot 1=\left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|$$
19	3 14 18	3eqtrd	$$⊢A\in \mathbb{N}\to 0\sigma A=\left|\left\{p\in \mathbb{N}|p\parallel A\right\}\right|$$