Theorem eulerpartlemsv3

Description: Lemma for eulerpart . Value of the sum of a finite partition A (Contributed by Thierry Arnoux, 19-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	eulerpartlemsv3	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(A\right)=\sum _{k=1}^{S\left(A\right)}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	1 2	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$$
4		fzssuz	$$⊢\left(1\dots S\left(A\right)\right)\subseteq {\mathbb{Z}}_{\ge 1}$$
5		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
6	4 5	sseqtrri	$$⊢\left(1\dots S\left(A\right)\right)\subseteq \mathbb{N}$$
7	6	a1i	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \left(1\dots S\left(A\right)\right)\subseteq \mathbb{N}$$
8	1 2	eulerpartlemelr	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \left(A:\mathbb{N}⟶{\mathbb{N}}_0\wedge A^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right)$$
9	8	simpld	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
10	9	adantr	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(1\dots S\left(A\right)\right)\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
11	7	sselda	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(1\dots S\left(A\right)\right)\right)\to k\in \mathbb{N}$$
12	10 11	ffvelcdmd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(1\dots S\left(A\right)\right)\right)\to A\left(k\right)\in {\mathbb{N}}_0$$
13	12	nn0cnd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(1\dots S\left(A\right)\right)\right)\to A\left(k\right)\in ℂ$$
14	11	nncnd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(1\dots S\left(A\right)\right)\right)\to k\in ℂ$$
15	13 14	mulcld	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(1\dots S\left(A\right)\right)\right)\to A\left(k\right)k\in ℂ$$
16	1 2	eulerpartlems	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge t\in {\mathbb{Z}}_{\ge \left(S\left(A\right)+1\right)}\right)\to A\left(t\right)=0$$
17	16	ralrimiva	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \forall t\in {\mathbb{Z}}_{\ge \left(S\left(A\right)+1\right)}A\left(t\right)=0$$
18		fveqeq2	$$⊢k=t\to \left(A\left(k\right)=0\leftrightarrow A\left(t\right)=0\right)$$
19	18	cbvralvw	$$⊢\forall k\in {\mathbb{Z}}_{\ge \left(S\left(A\right)+1\right)}A\left(k\right)=0\leftrightarrow \forall t\in {\mathbb{Z}}_{\ge \left(S\left(A\right)+1\right)}A\left(t\right)=0$$
20	17 19	sylibr	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \forall k\in {\mathbb{Z}}_{\ge \left(S\left(A\right)+1\right)}A\left(k\right)=0$$
21	1 2	eulerpartlemsf	$$⊢S:\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R⟶{\mathbb{N}}_0$$
22	21	ffvelcdmi	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(A\right)\in {\mathbb{N}}_0$$
23		nndiffz1	$$⊢S\left(A\right)\in {\mathbb{N}}_0\to \mathbb{N}\setminus \left(1\dots S\left(A\right)\right)={\mathbb{Z}}_{\ge \left(S\left(A\right)+1\right)}$$
24	22 23	syl	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \mathbb{N}\setminus \left(1\dots S\left(A\right)\right)={\mathbb{Z}}_{\ge \left(S\left(A\right)+1\right)}$$
25	20 24	raleqtrrdv	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \forall k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)A\left(k\right)=0$$
26	25	r19.21bi	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)\right)\to A\left(k\right)=0$$
27	26	oveq1d	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)\right)\to A\left(k\right)k=0\cdot k$$
28		simpr	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)\right)\to k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)$$
29	28	eldifad	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)\right)\to k\in \mathbb{N}$$
30	29	nncnd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)\right)\to k\in ℂ$$
31	30	mul02d	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)\right)\to 0\cdot k=0$$
32	27 31	eqtrd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus \left(1\dots S\left(A\right)\right)\right)\right)\to A\left(k\right)k=0$$
33	5	eqimssi	$$⊢\mathbb{N}\subseteq {\mathbb{Z}}_{\ge 1}$$
34	33	a1i	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \mathbb{N}\subseteq {\mathbb{Z}}_{\ge 1}$$
35	7 15 32 34	sumss	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \sum _{k=1}^{S\left(A\right)}A\left(k\right)k=\sum _{k\in \mathbb{N}}A\left(k\right)k$$
36	3 35	eqtr4d	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(A\right)=\sum _{k=1}^{S\left(A\right)}A\left(k\right)k$$