Theorem eulerpartlemsf

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

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

Proof

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