Theorem eulerpartleme

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

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

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2		nn0ex	⊢ ℕ0 ∈ V
3		nnex	⊢ ℕ ∈ V
4	2 3	elmap	⊢ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ↔ 𝐴 : ℕ ⟶ ℕ0 )
5	4	anbi1i	⊢ ( ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ) ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ) )
6		cnveq	⊢ ( 𝑓 = 𝐴 → ◡ 𝑓 = ◡ 𝐴 )
7	6	imaeq1d	⊢ ( 𝑓 = 𝐴 → ( ◡ 𝑓 “ ℕ ) = ( ◡ 𝐴 “ ℕ ) )
8	7	eleq1d	⊢ ( 𝑓 = 𝐴 → ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ↔ ( ◡ 𝐴 “ ℕ ) ∈ Fin ) )
9		fveq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 ‘ 𝑘 ) = ( 𝐴 ‘ 𝑘 ) )
10	9	oveq1d	⊢ ( 𝑓 = 𝐴 → ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
11	10	sumeq2sdv	⊢ ( 𝑓 = 𝐴 → Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) )
12	11	eqeq1d	⊢ ( 𝑓 = 𝐴 → ( Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ↔ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )
13	8 12	anbi12d	⊢ ( 𝑓 = 𝐴 → ( ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ) )
14	13 1	elrab2	⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 ∈ ( ℕ0 ↑m ℕ ) ∧ ( ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ) )
15		3anass	⊢ ( ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) ) )
16	5 14 15	3bitr4i	⊢ ( 𝐴 ∈ 𝑃 ↔ ( 𝐴 : ℕ ⟶ ℕ0 ∧ ( ◡ 𝐴 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝐴 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) )