Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( 𝐴 ∈ ( ( ℕ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 ffvelrni ⊢ ( 𝐴 ∈ ( ( ℕ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 ... ( 𝑆 ‘ 𝐴 ) ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )