Metamath Proof Explorer

Theorem eulerpartlemv

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

Ref Expression
Hypothesis eulerpart.p ⊢ P = f ∈ ℕ 0 ℕ | f -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ f ⁡ k ⁢ k = N
Assertion eulerpartlemv ⊢ A ∈ P ↔ A : ℕ ⟶ ℕ 0 ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ A -1 ℕ A ⁡ k ⁢ k = N

Proof

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