Theorem sgmval

Description: The value of the divisor function. (Contributed by Mario Carneiro, 22-Sep-2014) (Revised by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	sgmval	$$⊢\left(A\in ℂ\wedge B\in \mathbb{N}\right)\to A\sigma B=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(x=A\wedge n=B\right)\to n=B$$
2	1	breq2d	$$⊢\left(x=A\wedge n=B\right)\to \left(p\parallel n\leftrightarrow p\parallel B\right)$$
3	2	rabbidv	$$⊢\left(x=A\wedge n=B\right)\to \left\{p\in \mathbb{N}|p\parallel n\right\}=\left\{p\in \mathbb{N}|p\parallel B\right\}$$
4		simpll	$$⊢\left(\left(x=A\wedge n=B\right)\wedge k\in \left\{p\in \mathbb{N}|p\parallel n\right\}\right)\to x=A$$
5	4	oveq2d	$$⊢\left(\left(x=A\wedge n=B\right)\wedge k\in \left\{p\in \mathbb{N}|p\parallel n\right\}\right)\to k^x=k^A$$
6	3 5	sumeq12dv	$$⊢\left(x=A\wedge n=B\right)\to \sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A$$
7		df-sgm	$$⊢\sigma =\left(x\in ℂ,n\in \mathbb{N}⟼\sum _{k\in \left\{p\in \mathbb{N}|p\parallel n\right\}}{k}^x\right)$$
8		sumex	$$⊢\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A\in \mathrm{V}$$
9	6 7 8	ovmpoa	$$⊢\left(A\in ℂ\wedge B\in \mathbb{N}\right)\to A\sigma B=\sum _{k\in \left\{p\in \mathbb{N}|p\parallel B\right\}}{k}^A$$