# Metamath Proof Explorer

## 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[ℕ\right]\in \mathrm{Fin}\right\}$
eulerpartlems.s ${⊢}{S}=\left({f}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)⟼\sum _{{k}\in ℕ}{f}\left({k}\right){k}\right)$
Assertion eulerpartlemsv2 ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to {S}\left({A}\right)=\sum _{{k}\in {{A}}^{-1}\left[ℕ\right]}{A}\left({k}\right){k}$

### Proof

Step Hyp Ref Expression
1 eulerpartlems.r ${⊢}{R}=\left\{{f}|{{f}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right\}$
2 eulerpartlems.s ${⊢}{S}=\left({f}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)⟼\sum _{{k}\in ℕ}{f}\left({k}\right){k}\right)$
3 1 2 eulerpartlemsv1 ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to {S}\left({A}\right)=\sum _{{k}\in ℕ}{A}\left({k}\right){k}$
4 cnvimass ${⊢}{{A}}^{-1}\left[ℕ\right]\subseteq \mathrm{dom}{A}$
5 1 2 eulerpartlemelr ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to \left({A}:ℕ⟶{ℕ}_{0}\wedge {{A}}^{-1}\left[ℕ\right]\in \mathrm{Fin}\right)$
6 5 simpld ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to {A}:ℕ⟶{ℕ}_{0}$
7 4 6 fssdm ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to {{A}}^{-1}\left[ℕ\right]\subseteq ℕ$
8 6 adantr ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in {{A}}^{-1}\left[ℕ\right]\right)\to {A}:ℕ⟶{ℕ}_{0}$
9 7 sselda ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in {{A}}^{-1}\left[ℕ\right]\right)\to {k}\in ℕ$
10 8 9 ffvelrnd ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in {{A}}^{-1}\left[ℕ\right]\right)\to {A}\left({k}\right)\in {ℕ}_{0}$
11 9 nnnn0d ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in {{A}}^{-1}\left[ℕ\right]\right)\to {k}\in {ℕ}_{0}$
12 10 11 nn0mulcld ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in {{A}}^{-1}\left[ℕ\right]\right)\to {A}\left({k}\right){k}\in {ℕ}_{0}$
13 12 nn0cnd ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in {{A}}^{-1}\left[ℕ\right]\right)\to {A}\left({k}\right){k}\in ℂ$
14 simpr ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)$
15 14 eldifad ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {k}\in ℕ$
16 14 eldifbd ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to ¬{k}\in {{A}}^{-1}\left[ℕ\right]$
17 6 adantr ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {A}:ℕ⟶{ℕ}_{0}$
18 ffn ${⊢}{A}:ℕ⟶{ℕ}_{0}\to {A}Fnℕ$
19 elpreima ${⊢}{A}Fnℕ\to \left({k}\in {{A}}^{-1}\left[ℕ\right]↔\left({k}\in ℕ\wedge {A}\left({k}\right)\in ℕ\right)\right)$
20 17 18 19 3syl ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to \left({k}\in {{A}}^{-1}\left[ℕ\right]↔\left({k}\in ℕ\wedge {A}\left({k}\right)\in ℕ\right)\right)$
21 16 20 mtbid ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to ¬\left({k}\in ℕ\wedge {A}\left({k}\right)\in ℕ\right)$
22 imnan ${⊢}\left({k}\in ℕ\to ¬{A}\left({k}\right)\in ℕ\right)↔¬\left({k}\in ℕ\wedge {A}\left({k}\right)\in ℕ\right)$
23 21 22 sylibr ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to \left({k}\in ℕ\to ¬{A}\left({k}\right)\in ℕ\right)$
24 15 23 mpd ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to ¬{A}\left({k}\right)\in ℕ$
25 17 15 ffvelrnd ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {A}\left({k}\right)\in {ℕ}_{0}$
26 elnn0 ${⊢}{A}\left({k}\right)\in {ℕ}_{0}↔\left({A}\left({k}\right)\in ℕ\vee {A}\left({k}\right)=0\right)$
27 25 26 sylib ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to \left({A}\left({k}\right)\in ℕ\vee {A}\left({k}\right)=0\right)$
28 orel1 ${⊢}¬{A}\left({k}\right)\in ℕ\to \left(\left({A}\left({k}\right)\in ℕ\vee {A}\left({k}\right)=0\right)\to {A}\left({k}\right)=0\right)$
29 24 27 28 sylc ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {A}\left({k}\right)=0$
30 29 oveq1d ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {A}\left({k}\right){k}=0\cdot {k}$
31 15 nncnd ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {k}\in ℂ$
32 31 mul02d ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to 0\cdot {k}=0$
33 30 32 eqtrd ${⊢}\left({A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\wedge {k}\in \left(ℕ\setminus {{A}}^{-1}\left[ℕ\right]\right)\right)\to {A}\left({k}\right){k}=0$
34 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
35 34 eqimssi ${⊢}ℕ\subseteq {ℤ}_{\ge 1}$
36 35 a1i ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to ℕ\subseteq {ℤ}_{\ge 1}$
37 7 13 33 36 sumss ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to \sum _{{k}\in {{A}}^{-1}\left[ℕ\right]}{A}\left({k}\right){k}=\sum _{{k}\in ℕ}{A}\left({k}\right){k}$
38 3 37 eqtr4d ${⊢}{A}\in \left(\left({{ℕ}_{0}}^{ℕ}\right)\cap {R}\right)\to {S}\left({A}\right)=\sum _{{k}\in {{A}}^{-1}\left[ℕ\right]}{A}\left({k}\right){k}$