Theorem eulerpartlemsv1

Description: Lemma for eulerpart . Value of the sum of a partition A . (Contributed by Thierry Arnoux, 26-Aug-2018)

	Ref	Expression
Hypotheses	eulerpartlems.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
	eulerpartlems.s	$$⊢S=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
Assertion	eulerpartlemsv1	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(A\right)=\sum _{k\in \mathbb{N}}A\left(k\right)k$$

Proof

Step	Hyp	Ref	Expression
1		eulerpartlems.r	$$⊢R=\left\{f|f^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
2		eulerpartlems.s	$$⊢S=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
3	2	a1i	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S=\left(f\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)⟼\sum _{k\in \mathbb{N}}f\left(k\right)k\right)$$
4		simplr	$$⊢\left(\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge f=A\right)\wedge k\in \mathbb{N}\right)\to f=A$$
5	4	fveq1d	$$⊢\left(\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge f=A\right)\wedge k\in \mathbb{N}\right)\to f\left(k\right)=A\left(k\right)$$
6	5	oveq1d	$$⊢\left(\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge f=A\right)\wedge k\in \mathbb{N}\right)\to f\left(k\right)k=A\left(k\right)k$$
7	6	sumeq2dv	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge f=A\right)\to \sum _{k\in \mathbb{N}}f\left(k\right)k=\sum _{k\in \mathbb{N}}A\left(k\right)k$$
8		id	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)$$
9		sumex	$$⊢\sum _{k\in \mathbb{N}}A\left(k\right)k\in \mathrm{V}$$
10	9	a1i	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \sum _{k\in \mathbb{N}}A\left(k\right)k\in \mathrm{V}$$
11	3 7 8 10	fvmptd	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(A\right)=\sum _{k\in \mathbb{N}}A\left(k\right)k$$