Theorem eulerpartlemsv2

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	eulerpartlemsv2	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(A\right)=\sum _{k\in A^{-1}\left[\mathbb{N}\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		cnvimass	$$⊢A^{-1}\left[\mathbb{N}\right]\subseteq \mathrm{dom}A$$
5	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)$$
6	5	simpld	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
7	4 6	fssdm	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to A^{-1}\left[\mathbb{N}\right]\subseteq \mathbb{N}$$
8	6	adantr	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in A^{-1}\left[\mathbb{N}\right]\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
9	7	sselda	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in A^{-1}\left[\mathbb{N}\right]\right)\to k\in \mathbb{N}$$
10	8 9	ffvelrnd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in A^{-1}\left[\mathbb{N}\right]\right)\to A\left(k\right)\in {\mathbb{N}}_0$$
11	9	nnnn0d	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in A^{-1}\left[\mathbb{N}\right]\right)\to k\in {\mathbb{N}}_0$$
12	10 11	nn0mulcld	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in A^{-1}\left[\mathbb{N}\right]\right)\to A\left(k\right)k\in {\mathbb{N}}_0$$
13	12	nn0cnd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in A^{-1}\left[\mathbb{N}\right]\right)\to A\left(k\right)k\in ℂ$$
14		simpr	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)$$
15	14	eldifad	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to k\in \mathbb{N}$$
16	14	eldifbd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to \neg k\in A^{-1}\left[\mathbb{N}\right]$$
17	6	adantr	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to A:\mathbb{N}⟶{\mathbb{N}}_0$$
18		ffn	$$⊢A:\mathbb{N}⟶{\mathbb{N}}_0\to AFn\mathbb{N}$$
19		elpreima	$$⊢AFn\mathbb{N}\to \left(k\in A^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(k\in \mathbb{N}\wedge A\left(k\right)\in \mathbb{N}\right)\right)$$
20	17 18 19	3syl	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to \left(k\in A^{-1}\left[\mathbb{N}\right]\leftrightarrow \left(k\in \mathbb{N}\wedge A\left(k\right)\in \mathbb{N}\right)\right)$$
21	16 20	mtbid	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to \neg \left(k\in \mathbb{N}\wedge A\left(k\right)\in \mathbb{N}\right)$$
22		imnan	$$⊢\left(k\in \mathbb{N}\to \neg A\left(k\right)\in \mathbb{N}\right)\leftrightarrow \neg \left(k\in \mathbb{N}\wedge A\left(k\right)\in \mathbb{N}\right)$$
23	21 22	sylibr	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to \left(k\in \mathbb{N}\to \neg A\left(k\right)\in \mathbb{N}\right)$$
24	15 23	mpd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to \neg A\left(k\right)\in \mathbb{N}$$
25	17 15	ffvelrnd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to A\left(k\right)\in {\mathbb{N}}_0$$
26		elnn0	$$⊢A\left(k\right)\in {\mathbb{N}}_0\leftrightarrow \left(A\left(k\right)\in \mathbb{N}\vee A\left(k\right)=0\right)$$
27	25 26	sylib	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to \left(A\left(k\right)\in \mathbb{N}\vee A\left(k\right)=0\right)$$
28		orel1	$$⊢\neg A\left(k\right)\in \mathbb{N}\to \left(\left(A\left(k\right)\in \mathbb{N}\vee A\left(k\right)=0\right)\to A\left(k\right)=0\right)$$
29	24 27 28	sylc	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to A\left(k\right)=0$$
30	29	oveq1d	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to A\left(k\right)k=0\cdot k$$
31	15	nncnd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to k\in ℂ$$
32	31	mul02d	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to 0\cdot k=0$$
33	30 32	eqtrd	$$⊢\left(A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\wedge k\in \left(\mathbb{N}\setminus A^{-1}\left[\mathbb{N}\right]\right)\right)\to A\left(k\right)k=0$$
34		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
35	34	eqimssi	$$⊢\mathbb{N}\subseteq {\mathbb{Z}}_{\ge 1}$$
36	35	a1i	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \mathbb{N}\subseteq {\mathbb{Z}}_{\ge 1}$$
37	7 13 33 36	sumss	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to \sum _{k\in A^{-1}\left[\mathbb{N}\right]}A\left(k\right)k=\sum _{k\in \mathbb{N}}A\left(k\right)k$$
38	3 37	eqtr4d	$$⊢A\in \left(\left({{\mathbb{N}}_0}^{\mathbb{N}}\right)\cap R\right)\to S\left(A\right)=\sum _{k\in A^{-1}\left[\mathbb{N}\right]}A\left(k\right)k$$