Metamath Proof Explorer

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 ℕ ) ∩ 𝑅 ) → ( 𝑆 ‘ 𝐴 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )