Theorem eulerpartlemsv3

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	eulerpartlemsv3	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpartlems.r	⊢ 𝑅 = { 𝑓 ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
2		eulerpartlems.s	⊢ 𝑆 = ( 𝑓 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ↦ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) )
3	1 2	eulerpartlemsv1	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
4		fzssuz	⊢ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ⊆ ( ℤ≥ ‘ 1 )
5		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
6	4 5	sseqtrri	⊢ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ⊆ ℕ
7	6	a1i	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ⊆ ℕ )
8	1 2	eulerpartlemelr	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) )
9	8	simpld	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → 𝐴 : ℕ ⟶ ℕ0 )
10	9	adantr	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 𝐴 : ℕ ⟶ ℕ0 )
11	7	sselda	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 𝑘 ∈ ℕ )
12	10 11	ffvelcdmd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
13	12	nn0cnd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℂ )
14	11	nncnd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → 𝑘 ∈ ℂ )
15	13 14	mulcld	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℂ )
16	1 2	eulerpartlems	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ) → ( 𝐴 ‘ 𝑡 ) = 0 )
17	16	ralrimiva	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ∀ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ( 𝐴 ‘ 𝑡 ) = 0 )
18		fveqeq2	⊢ ( 𝑘 = 𝑡 → ( ( 𝐴 ‘ 𝑘 ) = 0 ↔ ( 𝐴 ‘ 𝑡 ) = 0 ) )
19	18	cbvralvw	⊢ ( ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ( 𝐴 ‘ 𝑘 ) = 0 ↔ ∀ 𝑡 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ( 𝐴 ‘ 𝑡 ) = 0 )
20	17 19	sylibr	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ( 𝐴 ‘ 𝑘 ) = 0 )
21	1 2	eulerpartlemsf	⊢ 𝑆 : ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ⟶ ℕ0
22	21	ffvelcdmi	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 )
23		nndiffz1	⊢ ( ( 𝑆 ‘ 𝐴 ) ∈ ℕ0 → ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) = ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) )
24	22 23	syl	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) = ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) )
25	24	raleqdv	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( ∀ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ( 𝐴 ‘ 𝑘 ) = 0 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ ( ( 𝑆 ‘ 𝐴 ) + 1 ) ) ( 𝐴 ‘ 𝑘 ) = 0 ) )
26	20 25	mpbird	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ∀ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ( 𝐴 ‘ 𝑘 ) = 0 )
27	26	r19.21bi	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
28	27	oveq1d	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = ( 0 · 𝑘 ) )
29		simpr	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) )
30	29	eldifad	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝑘 ∈ ℕ )
31	30	nncnd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → 𝑘 ∈ ℂ )
32	31	mul02d	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( 0 · 𝑘 ) = 0 )
33	28 32	eqtrd	⊢ ( ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) ∧ 𝑘 ∈ ( ℕ ∖ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 0 )
34	5	eqimssi	⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
35	34	a1i	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ℕ ⊆ ( ℤ≥ ‘ 1 ) )
36	7 15 33 35	sumss	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
37	3 36	eqtr4d	⊢ ( 𝐴 ∈ ( ( ℕ0 ↑m ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( 1 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )