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	⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	eulerpartlems.s	⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
Assertion	eulerpartlemsv2	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpartlems.r	⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		eulerpartlems.s	⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
3	1 2	eulerpartlemsv1	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
4		cnvimass	⊢ ( ◡ 𝐴 “ ℕ ) ⊆ dom 𝐴
5	1 2	eulerpartlemelr	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) )
6	5	simpld	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
7	4 6	fssdm	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ◡ 𝐴 “ ℕ ) ⊆ ℕ )
8	6	adantr	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝐴 : ℕ ⟶ ℕ0 )
9	7	sselda	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑘 ∈ ℕ )
10	8 9	ffvelcdmd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
11	9	nnnn0d	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑘 ∈ ℕ0 )
12	10 11	nn0mulcld	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 )
13	12	nn0cnd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℂ )
14		simpr	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) )
15	14	eldifad	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ℕ )
16	14	eldifbd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) )
17	6	adantr	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝐴 : ℕ ⟶ ℕ0 )
18		ffn	⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 𝐴 Fn ℕ )
19		elpreima	⊢ ( 𝐴 Fn ℕ → ( 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ) )
20	17 18 19	3syl	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ) )
21	16 20	mtbid	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
22		imnan	⊢ ( ( 𝑘 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ↔ ¬ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
23	21 22	sylibr	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝑘 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
24	15 23	mpd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ )
25	17 15	ffvelcdmd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
26		elnn0	⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 ↔ ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) )
27	25 26	sylib	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) )
28		orel1	⊢ ( ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ → ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
29	24 27 28	sylc	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
30	29	oveq1d	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = ( 0 · 𝑘 ) )
31	15	nncnd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ℂ )
32	31	mul02d	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 0 · 𝑘 ) = 0 )
33	30 32	eqtrd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 0 )
34		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
35	34	eqimssi	⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
36	35	a1i	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ℕ ⊆ ( ℤ≥ ‘ 1 ) )
37	7 13 33 36	sumss	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
38	3 37	eqtr4d	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )