eulerpart

Description: Euler's theorem on partitions, also known as a special case of Glaisher's theorem. Let P be the set of all partitions of N , represented as multisets of positive integers, which is to say functions from NN to NN0 where the value of the function represents the number of repetitions of an individual element, and the sum of all the elements with repetition equals N . Then the set O of all partitions that only consist of odd numbers and the set D of all partitions which have no repeated elements have the same cardinality. This is Metamath 100 proof #45. (Contributed by Thierry Arnoux, 14-Aug-2018) (Revised by Thierry Arnoux, 1-Sep-2019)

	Ref	Expression
Hypotheses	eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
	eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
	eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
Assertion	eulerpart	$⊢ \|O\| = \|D\|$

Proof

Step	Hyp	Ref	Expression
1		eulerpart.p	$⊢ P = \{f \in ({ℕ_{0}}^{ℕ}) \| (f^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} f (k) k = N)\}$
2		eulerpart.o	$⊢ O = \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\}$
3		eulerpart.d	$⊢ D = \{g \in P \| \forall n \in ℕ g (n) \leq 1\}$
4		eqid	$⊢ \{z \in ℕ \| \neg 2 ∥ z\} = \{z \in ℕ \| \neg 2 ∥ z\}$
5		oveq2	$⊢ a = x \to 2^{b} a = 2^{b} x$
6		oveq2	$⊢ b = y \to 2^{b} = 2^{y}$
7	6	oveq1d	$⊢ b = y \to 2^{b} x = 2^{y} x$
8	5 7	cbvmpov	$⊢ (a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) = (x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x)$
9		oveq1	$⊢ r = m \to r supp \emptyset = m supp \emptyset$
10	9	eleq1d	$⊢ r = m \to (r supp \emptyset \in Fin \leftrightarrow m supp \emptyset \in Fin)$
11	10	cbvrabv	$⊢ \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} = \{m \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| m supp \emptyset \in Fin\}$
12	11	eqcomi	$⊢ \{m \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| m supp \emptyset \in Fin\} = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\}$
13		fveq1	$⊢ t = r \to t (a) = r (a)$
14	13	eleq2d	$⊢ t = r \to (b \in t (a) \leftrightarrow b \in r (a))$
15	14	anbi2d	$⊢ t = r \to ((a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a)) \leftrightarrow (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a)))$
16	15	opabbidv	$⊢ t = r \to \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\} = \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a))\}$
17	16	cbvmptv	$⊢ (t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) = (r \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a))\})$
18		oveq1	$⊢ m = s \to m supp \emptyset = s supp \emptyset$
19	18	eleq1d	$⊢ m = s \to (m supp \emptyset \in Fin \leftrightarrow s supp \emptyset \in Fin)$
20	19	cbvrabv	$⊢ \{m \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| m supp \emptyset \in Fin\} = \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\}$
21	20	eqcomi	$⊢ \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} = \{m \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| m supp \emptyset \in Fin\}$
22		simpl	$⊢ (a = x \land b = y) \to a = x$
23	22	eleq1d	$⊢ (a = x \land b = y) \to (a \in \{z \in ℕ \| \neg 2 ∥ z\} \leftrightarrow x \in \{z \in ℕ \| \neg 2 ∥ z\})$
24		simpr	$⊢ (a = x \land b = y) \to b = y$
25	22	fveq2d	$⊢ (a = x \land b = y) \to r (a) = r (x)$
26	24 25	eleq12d	$⊢ (a = x \land b = y) \to (b \in r (a) \leftrightarrow y \in r (x))$
27	23 26	anbi12d	$⊢ (a = x \land b = y) \to ((a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a)) \leftrightarrow (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x)))$
28	27	cbvopabv	$⊢ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a))\} = \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}$
29	21 28	mpteq12i	$⊢ (r \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a))\}) = (r \in \{m \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| m supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\})$
30	17 29	eqtri	$⊢ (t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) = (r \in \{m \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| m supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\})$
31		cnveq	$⊢ h = f \to h^{-1} = f^{-1}$
32	31	imaeq1d	$⊢ h = f \to h^{-1} [ℕ] = f^{-1} [ℕ]$
33	32	eleq1d	$⊢ h = f \to (h^{-1} [ℕ] \in Fin \leftrightarrow f^{-1} [ℕ] \in Fin)$
34	33	cbvabv	$⊢ \{h \| h^{-1} [ℕ] \in Fin\} = \{f \| f^{-1} [ℕ] \in Fin\}$
35	32	sseq1d	$⊢ h = f \to (h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\} \leftrightarrow f^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\})$
36	35	cbvrabv	$⊢ \{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\}$
37		reseq1	$⊢ o = q \to {o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}} = {q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}$
38	37	coeq2d	$⊢ o = q \to bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}) = bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}})$
39	38	fveq2d	$⊢ o = q \to (r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}})) = (r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))$
40	39	imaeq2d	$⊢ o = q \to (x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))] = (x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]$
41	40	fveq2d	$⊢ o = q \to 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]) = 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])$
42	41	cbvmptv	$⊢ (o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) = (q \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]))$
43	8	eqcomi	$⊢ (x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) = (a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a)$
44	43	imaeq1i	$⊢ (x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))] = (a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]$
45		eqid	$⊢ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\} = \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}$
46	11 45	mpteq12i	$⊢ (r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) = (r \in \{m \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| m supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\})$
47		fveq1	$⊢ r = t \to r (a) = t (a)$
48	47	eleq2d	$⊢ r = t \to (b \in r (a) \leftrightarrow b \in t (a))$
49	48	anbi2d	$⊢ r = t \to ((a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a)) \leftrightarrow (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a)))$
50	49	opabbidv	$⊢ r = t \to \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a))\} = \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}$
51	50	cbvmptv	$⊢ (r \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in r (a))\}) = (t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\})$
52	46 29 51	3eqtr2i	$⊢ (r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) = (t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\})$
53	52	fveq1i	$⊢ (r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}})) = (t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))$
54	53	imaeq2i	$⊢ (a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))] = (a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) [(t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]$
55	44 54	eqtri	$⊢ (x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))] = (a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) [(t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]$
56	55	fveq2i	$⊢ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]) = 𝟙_{ℕ} ((a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) [(t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])$
57	56	mpteq2i	$⊢ (q \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) = (q \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) [(t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]))$
58	42 57	eqtri	$⊢ (o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) = (q \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((a \in \{z \in ℕ \| \neg 2 ∥ z\}, b \in ℕ_{0} ⟼ 2^{b} a) [(t \in \{s \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| s supp \emptyset \in Fin\} ⟼ \{⟨a, b⟩ \| (a \in \{z \in ℕ \| \neg 2 ∥ z\} \land b \in t (a))\}) (bits \circ ({q ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))]))$
59		eqid	$⊢ (f \in (({ℕ_{0}}^{ℕ}) \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ \sum_{k \in ℕ} f (k) k) = (f \in (({ℕ_{0}}^{ℕ}) \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ \sum_{k \in ℕ} f (k) k)$
60	1 2 3 4 8 12 30 34 36 58 59	eulerpartlemn	$⊢ ({(o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) ↾}_{O}) : O \underset{1-1 onto}{⟶} D$
61		ovex	$⊢ {ℕ_{0}}^{ℕ} \in V$
62	61	rabex	$⊢ \{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \in V$
63	62	inex1	$⊢ \{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\} \in V$
64	63	mptex	$⊢ (o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) \in V$
65	64	resex	$⊢ {(o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) ↾}_{O} \in V$
66		f1oeq1	$⊢ g = {(o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) ↾}_{O} \to (g : O \underset{1-1 onto}{⟶} D \leftrightarrow ({(o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) ↾}_{O}) : O \underset{1-1 onto}{⟶} D)$
67	65 66	spcev	$⊢ ({(o \in (\{h \in ({ℕ_{0}}^{ℕ}) \| h^{-1} [ℕ] \subseteq \{z \in ℕ \| \neg 2 ∥ z\}\} \cap \{h \| h^{-1} [ℕ] \in Fin\}) ⟼ 𝟙_{ℕ} ((x \in \{z \in ℕ \| \neg 2 ∥ z\}, y \in ℕ_{0} ⟼ 2^{y} x) [(r \in \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{\{z \in ℕ \| \neg 2 ∥ z\}}) \| r supp \emptyset \in Fin\} ⟼ \{⟨x, y⟩ \| (x \in \{z \in ℕ \| \neg 2 ∥ z\} \land y \in r (x))\}) (bits \circ ({o ↾}_{\{z \in ℕ \| \neg 2 ∥ z\}}))])) ↾}_{O}) : O \underset{1-1 onto}{⟶} D \to \exists g g : O \underset{1-1 onto}{⟶} D$
68		bren	$⊢ O \approx D \leftrightarrow \exists g g : O \underset{1-1 onto}{⟶} D$
69		hasheni	$⊢ O \approx D \to \|O\| = \|D\|$
70	68 69	sylbir	$⊢ \exists g g : O \underset{1-1 onto}{⟶} D \to \|O\| = \|D\|$
71	60 67 70	mp2b	$⊢ \|O\| = \|D\|$

Metamath Proof Explorer

Theorem eulerpart

Proof