Metamath Proof Explorer


Theorem eulerpartlemsf

Description: Lemma for eulerpart . (Contributed by Thierry Arnoux, 8-Aug-2018)

Ref Expression
Hypotheses eulerpartlems.r 𝑅 = { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin }
eulerpartlems.s 𝑆 = ( 𝑓 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) )
Assertion eulerpartlemsf 𝑆 : ( ( ℕ0m ℕ ) ∩ 𝑅 ) ⟶ ℕ0

Proof

Step Hyp Ref Expression
1 eulerpartlems.r 𝑅 = { 𝑓 ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 eulerpartlems.s 𝑆 = ( 𝑓 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) )
3 simpl ( ( 𝑔 = 𝑓𝑘 ∈ ℕ ) → 𝑔 = 𝑓 )
4 3 fveq1d ( ( 𝑔 = 𝑓𝑘 ∈ ℕ ) → ( 𝑔𝑘 ) = ( 𝑓𝑘 ) )
5 4 oveq1d ( ( 𝑔 = 𝑓𝑘 ∈ ℕ ) → ( ( 𝑔𝑘 ) · 𝑘 ) = ( ( 𝑓𝑘 ) · 𝑘 ) )
6 5 sumeq2dv ( 𝑔 = 𝑓 → Σ 𝑘 ∈ ℕ ( ( 𝑔𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) )
7 6 eleq1d ( 𝑔 = 𝑓 → ( Σ 𝑘 ∈ ℕ ( ( 𝑔𝑘 ) · 𝑘 ) ∈ ℕ0 ↔ Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) ∈ ℕ0 ) )
8 1 2 eulerpartlemsv2 ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑆𝑔 ) = Σ 𝑘 ∈ ( 𝑔 “ ℕ ) ( ( 𝑔𝑘 ) · 𝑘 ) )
9 1 2 eulerpartlemsv1 ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑆𝑔 ) = Σ 𝑘 ∈ ℕ ( ( 𝑔𝑘 ) · 𝑘 ) )
10 8 9 eqtr3d ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ( 𝑔 “ ℕ ) ( ( 𝑔𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝑔𝑘 ) · 𝑘 ) )
11 1 2 eulerpartlemelr ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑔 : ℕ ⟶ ℕ0 ∧ ( 𝑔 “ ℕ ) ∈ Fin ) )
12 11 simprd ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑔 “ ℕ ) ∈ Fin )
13 11 simpld ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → 𝑔 : ℕ ⟶ ℕ0 )
14 13 adantr ( ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 𝑔 “ ℕ ) ) → 𝑔 : ℕ ⟶ ℕ0 )
15 cnvimass ( 𝑔 “ ℕ ) ⊆ dom 𝑔
16 15 13 fssdm ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → ( 𝑔 “ ℕ ) ⊆ ℕ )
17 16 sselda ( ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 𝑔 “ ℕ ) ) → 𝑘 ∈ ℕ )
18 14 17 ffvelrnd ( ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 𝑔 “ ℕ ) ) → ( 𝑔𝑘 ) ∈ ℕ0 )
19 17 nnnn0d ( ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 𝑔 “ ℕ ) ) → 𝑘 ∈ ℕ0 )
20 18 19 nn0mulcld ( ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 𝑔 “ ℕ ) ) → ( ( 𝑔𝑘 ) · 𝑘 ) ∈ ℕ0 )
21 12 20 fsumnn0cl ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ( 𝑔 “ ℕ ) ( ( 𝑔𝑘 ) · 𝑘 ) ∈ ℕ0 )
22 10 21 eqeltrrd ( 𝑔 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ℕ ( ( 𝑔𝑘 ) · 𝑘 ) ∈ ℕ0 )
23 7 22 vtoclga ( 𝑓 ∈ ( ( ℕ0m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ℕ ( ( 𝑓𝑘 ) · 𝑘 ) ∈ ℕ0 )
24 2 23 fmpti 𝑆 : ( ( ℕ0m ℕ ) ∩ 𝑅 ) ⟶ ℕ0