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	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
	eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
	eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
Assertion	eulerpartlemo	|- ( A e. O <-> ( A e. P /\ A. n e. ( `' A " NN ) -. 2 || n ) )

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2		eulerpart.o	|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3		eulerpart.d	|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4		cnveq	|- ( g = A -> `' g = `' A )
5	4	imaeq1d	|- ( g = A -> ( `' g " NN ) = ( `' A " NN ) )
6	5	raleqdv	|- ( g = A -> ( A. n e. ( `' g " NN ) -. 2 || n <-> A. n e. ( `' A " NN ) -. 2 || n ) )
7	6 2	elrab2	|- ( A e. O <-> ( A e. P /\ A. n e. ( `' A " NN ) -. 2 || n ) )