Theorem sgmnncl

Description: Closure of the divisor function. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	sgmnncl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A\sigma B\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢A\in {\mathbb{N}}_0\to A\in \mathbb{Z}$$
2		sgmval2	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{N}\right)\to A\sigma B=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A$$
3	1 2	sylan	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A\sigma B=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A$$
4		fzfid	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left(1\dots B\right)\in \mathrm{Fin}$$
5		dvdsssfz1	$$⊢B\in \mathbb{N}\to \left\{p\in \mathbb{N}|p\parallel B\right\}\subseteq \left(1\dots B\right)$$
6	5	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left\{p\in \mathbb{N}|p\parallel B\right\}\subseteq \left(1\dots B\right)$$
7	4 6	ssfid	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left\{p\in \mathbb{N}|p\parallel B\right\}\in \mathrm{Fin}$$
8		elrabi	$$⊢k\in \left\{p\in \mathbb{N}|p\parallel B\right\}\to k\in \mathbb{N}$$
9		simpl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A\in {\mathbb{N}}_0$$
10		nnexpcl	$$⊢\left(k\in \mathbb{N}\wedge A\in {\mathbb{N}}_0\right)\to k^A\in \mathbb{N}$$
11	8 9 10	syl2anr	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\wedge k\in \left\{p\in \mathbb{N}|p\parallel B\right\}\right)\to k^A\in \mathbb{N}$$
12	11	nnzd	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\wedge k\in \left\{p\in \mathbb{N}|p\parallel B\right\}\right)\to k^A\in \mathbb{Z}$$
13	7 12	fsumzcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A\in \mathbb{Z}$$
14		nnz	$$⊢B\in \mathbb{N}\to B\in \mathbb{Z}$$
15		iddvds	$$⊢B\in \mathbb{Z}\to B\parallel B$$
16	14 15	syl	$$⊢B\in \mathbb{N}\to B\parallel B$$
17		breq1	$$⊢p=B\to \left(p\parallel B\leftrightarrow B\parallel B\right)$$
18	17	rspcev	$$⊢\left(B\in \mathbb{N}\wedge B\parallel B\right)\to \exists p\in \mathbb{N}p\parallel B$$
19	16 18	mpdan	$$⊢B\in \mathbb{N}\to \exists p\in \mathbb{N}p\parallel B$$
20		rabn0	$$⊢\left\{p\in \mathbb{N}|p\parallel B\right\}\ne \varnothing \leftrightarrow \exists p\in \mathbb{N}p\parallel B$$
21	19 20	sylibr	$$⊢B\in \mathbb{N}\to \left\{p\in \mathbb{N}|p\parallel B\right\}\ne \varnothing$$
22	21	adantl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \left\{p\in \mathbb{N}|p\parallel B\right\}\ne \varnothing$$
23	11	nnrpd	$$⊢\left(\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\wedge k\in \left\{p\in \mathbb{N}|p\parallel B\right\}\right)\to k^A\in {ℝ}^{+}$$
24	7 22 23	fsumrpcl	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A\in {ℝ}^{+}$$
25	24	rpgt0d	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to 0<\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A$$
26		elnnz	$$⊢\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A\in \mathbb{N}\leftrightarrow \left(\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A\in \mathbb{Z}\wedge 0<\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A\right)$$
27	13 25 26	sylanbrc	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A\in \mathbb{N}$$
28	3 27	eqeltrd	$$⊢\left(A\in {\mathbb{N}}_0\wedge B\in \mathbb{N}\right)\to A\sigma B\in \mathbb{N}$$