Theorem eulerpartlemo

Description: Lemma for eulerpart : O is the set of odd partitions of N . (Contributed by Thierry Arnoux, 10-Aug-2017)

	Ref	Expression
Hypotheses	eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
	eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
	eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
Assertion	eulerpartlemo	⊢ ( 𝐴 ∈ 𝑂 ↔ ( 𝐴 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ¬ 2 ∥ 𝑛 ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	⊢ 𝑃 = { 𝑓 ∈ ( ℕ0 ↑m ℕ ) ∣ ( ( ◡ 𝑓 “ ℕ ) ∈ Fin ∧ Σ 𝑘 ∈ ℕ ( ( 𝑓 ‘ 𝑘 ) · 𝑘 ) = 𝑁 ) }
2		eulerpart.o	⊢ 𝑂 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 }
3		eulerpart.d	⊢ 𝐷 = { 𝑔 ∈ 𝑃 ∣ ∀ 𝑛 ∈ ℕ ( 𝑔 ‘ 𝑛 ) ≤ 1 }
4		cnveq	⊢ ( 𝑔 = 𝐴 → ◡ 𝑔 = ◡ 𝐴 )
5	4	imaeq1d	⊢ ( 𝑔 = 𝐴 → ( ◡ 𝑔 “ ℕ ) = ( ◡ 𝐴 “ ℕ ) )
6	5	raleqdv	⊢ ( 𝑔 = 𝐴 → ( ∀ 𝑛 ∈ ( ◡ 𝑔 “ ℕ ) ¬ 2 ∥ 𝑛 ↔ ∀ 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ¬ 2 ∥ 𝑛 ) )
7	6 2	elrab2	⊢ ( 𝐴 ∈ 𝑂 ↔ ( 𝐴 ∈ 𝑃 ∧ ∀ 𝑛 ∈ ( ◡ 𝐴 “ ℕ ) ¬ 2 ∥ 𝑛 ) )