Metamath Proof Explorer

Theorem eulerpartlemv

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

Ref Expression
Hypothesis eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
Assertion eulerpartlemv ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2 1 eulerpartleme ⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
3 cnvimass ⊢ ( ◡ 𝐴 “ ℕ ) ⊆ dom 𝐴
4 fdm ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → dom 𝐴 = ℕ )
5 3 4 sseqtrid ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → ( ◡ 𝐴 “ ℕ ) ⊆ ℕ )
6 simpl ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝐴 : ℕ ⟶ ℕ0 )
7 5 sselda ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑘 ∈ ℕ )
8 6 7 ffvelcdmd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
9 7 nnnn0d ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → 𝑘 ∈ ℕ0 )
10 8 9 nn0mulcld ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℕ0 )
11 10 nn0cnd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) ∈ ℂ )
12 simpr ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) )
13 12 eldifad ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ℕ )
14 12 eldifbd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) )
15 simpl ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝐴 : ℕ ⟶ ℕ0 )
16 ffn ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → 𝐴 Fn ℕ )
17 elpreima ⊢ ( 𝐴 Fn ℕ → ( 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ) )
18 15 16 17 3syl ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ) )
19 14 18 mtbid ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
20 imnan ⊢ ( ( 𝑘 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) ↔ ¬ ( 𝑘 ∈ ℕ ∧ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
21 19 20 sylibr ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝑘 ∈ ℕ → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ ) )
22 13 21 mpd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ )
23 15 13 ffvelcdmd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 )
24 elnn0 ⊢ ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ0 ↔ ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) )
25 23 24 sylib ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) )
26 orel1 ⊢ ( ¬ ( 𝐴 ‘ 𝑘 ) ∈ ℕ → ( ( ( 𝐴 ‘ 𝑘 ) ∈ ℕ ∨ ( 𝐴 ‘ 𝑘 ) = 0 ) → ( 𝐴 ‘ 𝑘 ) = 0 ) )
27 22 25 26 sylc ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 𝐴 ‘ 𝑘 ) = 0 )
28 27 oveq1d ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = ( 0 · 𝑘 ) )
29 13 nncnd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → 𝑘 ∈ ℂ )
30 29 mul02d ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( 0 · 𝑘 ) = 0 )
31 28 30 eqtrd ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ 𝑘 ∈ ( ℕ ∖ ( ◡ 𝐴 “ ℕ ) ) ) → ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 0 )
32 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
33 32 eqimssi ⊢ ℕ ⊆ ( ℤ≥ ‘ 1 )
34 33 a1i ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → ℕ ⊆ ( ℤ≥ ‘ 1 ) )
35 5 11 31 34 sumss ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
36 35 eqcomd ⊢ ( 𝐴 : ℕ ⟶ ℕ0 → Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
37 36 adantr ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) → Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
38 37 eqeq1d ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) → ( Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ↔ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
39 38 pm5.32i ⊢ ( ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
40 df-3an ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
41 df-3an ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
42 39 40 41 3bitr4i ⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
43 2 42 bitri ⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ( ◡ 𝐴 “ ℕ ) ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )