Metamath Proof Explorer

Theorem eulerpartleme

Description: Lemma for eulerpart . (Contributed by Mario Carneiro, 26-Jan-2015)

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

Proof

Step Hyp Ref Expression
1 eulerpart.p ⊢ P = f ∈ ℕ 0 ℕ | f -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ f ⁡ k ⁢ k = N
2 nn0ex ⊢ ℕ 0 ∈ V
3 nnex ⊢ ℕ ∈ V
4 2 3 elmap ⊢ A ∈ ℕ 0 ℕ ↔ A : ℕ ⟶ ℕ 0
5 4 anbi1i ⊢ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N ↔ A : ℕ ⟶ ℕ 0 ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N
6 cnveq ⊢ f = A → f -1 = A -1
7 6 imaeq1d ⊢ f = A → f -1 ℕ = A -1 ℕ
8 7 eleq1d ⊢ f = A → f -1 ℕ ∈ Fin ↔ A -1 ℕ ∈ Fin
9 fveq1 ⊢ f = A → f ⁡ k = A ⁡ k
10 9 oveq1d ⊢ f = A → f ⁡ k ⁢ k = A ⁡ k ⁢ k
11 10 sumeq2sdv ⊢ f = A → ∑ k ∈ ℕ f ⁡ k ⁢ k = ∑ k ∈ ℕ A ⁡ k ⁢ k
12 11 eqeq1d ⊢ f = A → ∑ k ∈ ℕ f ⁡ k ⁢ k = N ↔ ∑ k ∈ ℕ A ⁡ k ⁢ k = N
13 8 12 anbi12d ⊢ f = A → f -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ f ⁡ k ⁢ k = N ↔ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N
14 13 1 elrab2 ⊢ A ∈ P ↔ A ∈ ℕ 0 ℕ ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N
15 3anass ⊢ A : ℕ ⟶ ℕ 0 ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N ↔ A : ℕ ⟶ ℕ 0 ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N
16 5 14 15 3bitr4i ⊢ A ∈ P ↔ A : ℕ ⟶ ℕ 0 ∧ A -1 ℕ ∈ Fin ∧ ∑ k ∈ ℕ A ⁡ k ⁢ k = N