eulerpartlemn

	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\}$
	eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
	eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
	eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
	eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
	eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
	eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
	eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
	eulerpart.s	$⊢ S = (f \in (({ℕ_{0}}^{ℕ}) \cap R) ⟼ \sum_{k \in ℕ} f (k) k)$
Assertion	eulerpartlemn	$⊢ ({G ↾}_{O}) : O \underset{1-1 onto}{⟶} 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		eulerpart.j	$⊢ J = \{z \in ℕ \| \neg 2 ∥ z\}$
5		eulerpart.f	$⊢ F = (x \in J, y \in ℕ_{0} ⟼ 2^{y} x)$
6		eulerpart.h	$⊢ H = \{r \in ({(𝒫 ℕ_{0} \cap Fin)}^{J}) \| r supp \emptyset \in Fin\}$
7		eulerpart.m	$⊢ M = (r \in H ⟼ \{⟨x, y⟩ \| (x \in J \land y \in r (x))\})$
8		eulerpart.r	$⊢ R = \{f \| f^{-1} [ℕ] \in Fin\}$
9		eulerpart.t	$⊢ T = \{f \in ({ℕ_{0}}^{ℕ}) \| f^{-1} [ℕ] \subseteq J\}$
10		eulerpart.g	$⊢ G = (o \in (T \cap R) ⟼ 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
11		eulerpart.s	$⊢ S = (f \in (({ℕ_{0}}^{ℕ}) \cap R) ⟼ \sum_{k \in ℕ} f (k) k)$
12		simpl	$⊢ (o = q \land k \in ℕ) \to o = q$
13	12	fveq1d	$⊢ (o = q \land k \in ℕ) \to o (k) = q (k)$
14	13	oveq1d	$⊢ (o = q \land k \in ℕ) \to o (k) k = q (k) k$
15	14	sumeq2dv	$⊢ o = q \to \sum_{k \in ℕ} o (k) k = \sum_{k \in ℕ} q (k) k$
16	15	eqeq1d	$⊢ o = q \to (\sum_{k \in ℕ} o (k) k = N \leftrightarrow \sum_{k \in ℕ} q (k) k = N)$
17	16	cbvrabv	$⊢ \{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\} = \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}$
18	17	a1i	$⊢ o = q \to \{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\} = \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}$
19	18	reseq2d	$⊢ o = q \to {G ↾}_{\{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\}} = {G ↾}_{\{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}}$
20		eqidd	$⊢ o = q \to \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\} = \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}$
21	19 18 20	f1oeq123d	$⊢ o = q \to (({G ↾}_{\{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\}}) : \{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\} \underset{1-1 onto}{⟶} \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\} \leftrightarrow ({G ↾}_{\{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}}) : \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\} \underset{1-1 onto}{⟶} \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\})$
22	21	imbi2d	$⊢ o = q \to ((⊤ \to ({G ↾}_{\{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\}}) : \{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\} \underset{1-1 onto}{⟶} \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}) \leftrightarrow (⊤ \to ({G ↾}_{\{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}}) : \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\} \underset{1-1 onto}{⟶} \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}))$
23	1 2 3 4 5 6 7 8 9 10	eulerpartgbij	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
24	23	a1i	$⊢ ⊤ \to G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R$
25		fveq2	$⊢ q = o \to G (q) = G (o)$
26		reseq1	$⊢ q = o \to {q ↾}_{J} = {o ↾}_{J}$
27	26	coeq2d	$⊢ q = o \to bits \circ ({q ↾}_{J}) = bits \circ ({o ↾}_{J})$
28	27	fveq2d	$⊢ q = o \to M (bits \circ ({q ↾}_{J})) = M (bits \circ ({o ↾}_{J}))$
29	28	imaeq2d	$⊢ q = o \to F [M (bits \circ ({q ↾}_{J}))] = F [M (bits \circ ({o ↾}_{J}))]$
30	29	fveq2d	$⊢ q = o \to 𝟙_{ℕ} (F [M (bits \circ ({q ↾}_{J}))]) = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])$
31	25 30	eqeq12d	$⊢ q = o \to (G (q) = 𝟙_{ℕ} (F [M (bits \circ ({q ↾}_{J}))]) \leftrightarrow G (o) = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))]))$
32	1 2 3 4 5 6 7 8 9 10	eulerpartlemgv	$⊢ q \in (T \cap R) \to G (q) = 𝟙_{ℕ} (F [M (bits \circ ({q ↾}_{J}))])$
33	31 32	vtoclga	$⊢ o \in (T \cap R) \to G (o) = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])$
34	33	3ad2ant2	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to G (o) = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])$
35		simp3	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])$
36	34 35	eqtr4d	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to G (o) = d$
37	36	fveq1d	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to G (o) (k) = d (k)$
38	37	oveq1d	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to G (o) (k) k = d (k) k$
39	38	sumeq2sdv	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to \sum_{k \in ℕ} G (o) (k) k = \sum_{k \in ℕ} d (k) k$
40	25	fveq2d	$⊢ q = o \to S (G (q)) = S (G (o))$
41		fveq2	$⊢ q = o \to S (q) = S (o)$
42	40 41	eqeq12d	$⊢ q = o \to (S (G (q)) = S (q) \leftrightarrow S (G (o)) = S (o))$
43	1 2 3 4 5 6 7 8 9 10 11	eulerpartlemgs2	$⊢ q \in (T \cap R) \to S (G (q)) = S (q)$
44	42 43	vtoclga	$⊢ o \in (T \cap R) \to S (G (o)) = S (o)$
45		nn0ex	$⊢ ℕ_{0} \in V$
46		0nn0	$⊢ 0 \in ℕ_{0}$
47		1nn0	$⊢ 1 \in ℕ_{0}$
48		prssi	$⊢ (0 \in ℕ_{0} \land 1 \in ℕ_{0}) \to \{0, 1\} \subseteq ℕ_{0}$
49	46 47 48	mp2an	$⊢ \{0, 1\} \subseteq ℕ_{0}$
50		mapss	$⊢ (ℕ_{0} \in V \land \{0, 1\} \subseteq ℕ_{0}) \to {\{0, 1\}}^{ℕ} \subseteq {ℕ_{0}}^{ℕ}$
51	45 49 50	mp2an	$⊢ {\{0, 1\}}^{ℕ} \subseteq {ℕ_{0}}^{ℕ}$
52		ssrin	$⊢ {\{0, 1\}}^{ℕ} \subseteq {ℕ_{0}}^{ℕ} \to ({\{0, 1\}}^{ℕ}) \cap R \subseteq ({ℕ_{0}}^{ℕ}) \cap R$
53	51 52	ax-mp	$⊢ ({\{0, 1\}}^{ℕ}) \cap R \subseteq ({ℕ_{0}}^{ℕ}) \cap R$
54		f1of	$⊢ G : T \cap R \underset{1-1 onto}{⟶} ({\{0, 1\}}^{ℕ}) \cap R \to G : T \cap R ⟶ ({\{0, 1\}}^{ℕ}) \cap R$
55	23 54	ax-mp	$⊢ G : T \cap R ⟶ ({\{0, 1\}}^{ℕ}) \cap R$
56	55	ffvelrni	$⊢ o \in (T \cap R) \to G (o) \in (({\{0, 1\}}^{ℕ}) \cap R)$
57	53 56	sseldi	$⊢ o \in (T \cap R) \to G (o) \in (({ℕ_{0}}^{ℕ}) \cap R)$
58	8 11	eulerpartlemsv1	$⊢ G (o) \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (G (o)) = \sum_{k \in ℕ} G (o) (k) k$
59	57 58	syl	$⊢ o \in (T \cap R) \to S (G (o)) = \sum_{k \in ℕ} G (o) (k) k$
60	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$⊢ o \in (T \cap R) \leftrightarrow (o \in ({ℕ_{0}}^{ℕ}) \land o^{-1} [ℕ] \in Fin \land o^{-1} [ℕ] \subseteq J)$
61	60	simp1bi	$⊢ o \in (T \cap R) \to o \in ({ℕ_{0}}^{ℕ})$
62		inss2	$⊢ T \cap R \subseteq R$
63	62	sseli	$⊢ o \in (T \cap R) \to o \in R$
64	61 63	elind	$⊢ o \in (T \cap R) \to o \in (({ℕ_{0}}^{ℕ}) \cap R)$
65	8 11	eulerpartlemsv1	$⊢ o \in (({ℕ_{0}}^{ℕ}) \cap R) \to S (o) = \sum_{k \in ℕ} o (k) k$
66	64 65	syl	$⊢ o \in (T \cap R) \to S (o) = \sum_{k \in ℕ} o (k) k$
67	44 59 66	3eqtr3d	$⊢ o \in (T \cap R) \to \sum_{k \in ℕ} G (o) (k) k = \sum_{k \in ℕ} o (k) k$
68	67	3ad2ant2	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to \sum_{k \in ℕ} G (o) (k) k = \sum_{k \in ℕ} o (k) k$
69	39 68	eqtr3d	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to \sum_{k \in ℕ} d (k) k = \sum_{k \in ℕ} o (k) k$
70	69	eqeq1d	$⊢ (⊤ \land o \in (T \cap R) \land d = 𝟙_{ℕ} (F [M (bits \circ ({o ↾}_{J}))])) \to (\sum_{k \in ℕ} d (k) k = N \leftrightarrow \sum_{k \in ℕ} o (k) k = N)$
71	10 24 70	f1oresrab	$⊢ ⊤ \to ({G ↾}_{\{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\}}) : \{o \in (T \cap R) \| \sum_{k \in ℕ} o (k) k = N\} \underset{1-1 onto}{⟶} \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}$
72	22 71	chvarvv	$⊢ ⊤ \to ({G ↾}_{\{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}}) : \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\} \underset{1-1 onto}{⟶} \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}$
73		cnveq	$⊢ g = q \to g^{-1} = q^{-1}$
74	73	imaeq1d	$⊢ g = q \to g^{-1} [ℕ] = q^{-1} [ℕ]$
75	74	raleqdv	$⊢ g = q \to (\forall n \in g^{-1} [ℕ] \neg 2 ∥ n \leftrightarrow \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
76	75	cbvrabv	$⊢ \{g \in P \| \forall n \in g^{-1} [ℕ] \neg 2 ∥ n\} = \{q \in P \| \forall n \in q^{-1} [ℕ] \neg 2 ∥ n\}$
77		nfrab1	$⊢ \underline{Ⅎ} q \{q \in P \| \forall n \in q^{-1} [ℕ] \neg 2 ∥ n\}$
78		nfrab1	$⊢ \underline{Ⅎ} q \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}$
79		df-3an	$⊢ (q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} q (k) k = N) \leftrightarrow ((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \sum_{k \in ℕ} q (k) k = N)$
80	79	anbi1i	$⊢ ((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} q (k) k = N) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n) \leftrightarrow (((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \sum_{k \in ℕ} q (k) k = N) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
81	1	eulerpartleme	$⊢ q \in P \leftrightarrow (q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} q (k) k = N)$
82	81	anbi1i	$⊢ (q \in P \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n) \leftrightarrow ((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} q (k) k = N) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
83		an32	$⊢ (((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n) \land \sum_{k \in ℕ} q (k) k = N) \leftrightarrow (((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \sum_{k \in ℕ} q (k) k = N) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
84	80 82 83	3bitr4i	$⊢ (q \in P \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n) \leftrightarrow (((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n) \land \sum_{k \in ℕ} q (k) k = N)$
85	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$⊢ q \in (T \cap R) \leftrightarrow (q \in ({ℕ_{0}}^{ℕ}) \land q^{-1} [ℕ] \in Fin \land q^{-1} [ℕ] \subseteq J)$
86		nnex	$⊢ ℕ \in V$
87	45 86	elmap	$⊢ q \in ({ℕ_{0}}^{ℕ}) \leftrightarrow q : ℕ ⟶ ℕ_{0}$
88	87	3anbi1i	$⊢ (q \in ({ℕ_{0}}^{ℕ}) \land q^{-1} [ℕ] \in Fin \land q^{-1} [ℕ] \subseteq J) \leftrightarrow (q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin \land q^{-1} [ℕ] \subseteq J)$
89	85 88	bitri	$⊢ q \in (T \cap R) \leftrightarrow (q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin \land q^{-1} [ℕ] \subseteq J)$
90		df-3an	$⊢ (q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin \land q^{-1} [ℕ] \subseteq J) \leftrightarrow ((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land q^{-1} [ℕ] \subseteq J)$
91		cnvimass	$⊢ q^{-1} [ℕ] \subseteq dom q$
92		fdm	$⊢ q : ℕ ⟶ ℕ_{0} \to dom q = ℕ$
93	91 92	sseqtrid	$⊢ q : ℕ ⟶ ℕ_{0} \to q^{-1} [ℕ] \subseteq ℕ$
94		dfss3	$⊢ q^{-1} [ℕ] \subseteq ℕ \leftrightarrow \forall n \in q^{-1} [ℕ] n \in ℕ$
95	93 94	sylib	$⊢ q : ℕ ⟶ ℕ_{0} \to \forall n \in q^{-1} [ℕ] n \in ℕ$
96	95	biantrurd	$⊢ q : ℕ ⟶ ℕ_{0} \to (\forall n \in q^{-1} [ℕ] \neg 2 ∥ n \leftrightarrow (\forall n \in q^{-1} [ℕ] n \in ℕ \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n))$
97		dfss3	$⊢ q^{-1} [ℕ] \subseteq J \leftrightarrow \forall n \in q^{-1} [ℕ] n \in J$
98		breq2	$⊢ z = n \to (2 ∥ z \leftrightarrow 2 ∥ n)$
99	98	notbid	$⊢ z = n \to (\neg 2 ∥ z \leftrightarrow \neg 2 ∥ n)$
100	99 4	elrab2	$⊢ n \in J \leftrightarrow (n \in ℕ \land \neg 2 ∥ n)$
101	100	ralbii	$⊢ \forall n \in q^{-1} [ℕ] n \in J \leftrightarrow \forall n \in q^{-1} [ℕ] (n \in ℕ \land \neg 2 ∥ n)$
102		r19.26	$⊢ \forall n \in q^{-1} [ℕ] (n \in ℕ \land \neg 2 ∥ n) \leftrightarrow (\forall n \in q^{-1} [ℕ] n \in ℕ \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
103	97 101 102	3bitri	$⊢ q^{-1} [ℕ] \subseteq J \leftrightarrow (\forall n \in q^{-1} [ℕ] n \in ℕ \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
104	96 103	syl6rbbr	$⊢ q : ℕ ⟶ ℕ_{0} \to (q^{-1} [ℕ] \subseteq J \leftrightarrow \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
105	104	adantr	$⊢ (q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \to (q^{-1} [ℕ] \subseteq J \leftrightarrow \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
106	105	pm5.32i	$⊢ ((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land q^{-1} [ℕ] \subseteq J) \leftrightarrow ((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
107	89 90 106	3bitri	$⊢ q \in (T \cap R) \leftrightarrow ((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
108	107	anbi1i	$⊢ (q \in (T \cap R) \land \sum_{k \in ℕ} q (k) k = N) \leftrightarrow (((q : ℕ ⟶ ℕ_{0} \land q^{-1} [ℕ] \in Fin) \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n) \land \sum_{k \in ℕ} q (k) k = N)$
109	84 108	bitr4i	$⊢ (q \in P \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n) \leftrightarrow (q \in (T \cap R) \land \sum_{k \in ℕ} q (k) k = N)$
110		rabid	$⊢ q \in \{q \in P \| \forall n \in q^{-1} [ℕ] \neg 2 ∥ n\} \leftrightarrow (q \in P \land \forall n \in q^{-1} [ℕ] \neg 2 ∥ n)$
111		rabid	$⊢ q \in \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\} \leftrightarrow (q \in (T \cap R) \land \sum_{k \in ℕ} q (k) k = N)$
112	109 110 111	3bitr4i	$⊢ q \in \{q \in P \| \forall n \in q^{-1} [ℕ] \neg 2 ∥ n\} \leftrightarrow q \in \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}$
113	77 78 112	eqri	$⊢ \{q \in P \| \forall n \in q^{-1} [ℕ] \neg 2 ∥ n\} = \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}$
114	2 76 113	3eqtri	$⊢ O = \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}$
115	114	reseq2i	$⊢ {G ↾}_{O} = {G ↾}_{\{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}}$
116	115	a1i	$⊢ ⊤ \to {G ↾}_{O} = {G ↾}_{\{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}}$
117	114	a1i	$⊢ ⊤ \to O = \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}$
118		nfcv	$⊢ \underline{Ⅎ} d D$
119		nfrab1	$⊢ \underline{Ⅎ} d \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}$
120		fnima	$⊢ d Fn ℕ \to d [ℕ] = ran d$
121	120	sseq1d	$⊢ d Fn ℕ \to (d [ℕ] \subseteq \{0, 1\} \leftrightarrow ran d \subseteq \{0, 1\})$
122	121	anbi2d	$⊢ d Fn ℕ \to ((ran d \subseteq ℕ_{0} \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow (ran d \subseteq ℕ_{0} \land ran d \subseteq \{0, 1\}))$
123		sstr	$⊢ (ran d \subseteq \{0, 1\} \land \{0, 1\} \subseteq ℕ_{0}) \to ran d \subseteq ℕ_{0}$
124	49 123	mpan2	$⊢ ran d \subseteq \{0, 1\} \to ran d \subseteq ℕ_{0}$
125	124	pm4.71ri	$⊢ ran d \subseteq \{0, 1\} \leftrightarrow (ran d \subseteq ℕ_{0} \land ran d \subseteq \{0, 1\})$
126	122 125	syl6bbr	$⊢ d Fn ℕ \to ((ran d \subseteq ℕ_{0} \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow ran d \subseteq \{0, 1\})$
127	126	pm5.32i	$⊢ (d Fn ℕ \land (ran d \subseteq ℕ_{0} \land d [ℕ] \subseteq \{0, 1\})) \leftrightarrow (d Fn ℕ \land ran d \subseteq \{0, 1\})$
128		anass	$⊢ ((d Fn ℕ \land ran d \subseteq ℕ_{0}) \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow (d Fn ℕ \land (ran d \subseteq ℕ_{0} \land d [ℕ] \subseteq \{0, 1\}))$
129		df-f	$⊢ d : ℕ ⟶ \{0, 1\} \leftrightarrow (d Fn ℕ \land ran d \subseteq \{0, 1\})$
130	127 128 129	3bitr4ri	$⊢ d : ℕ ⟶ \{0, 1\} \leftrightarrow ((d Fn ℕ \land ran d \subseteq ℕ_{0}) \land d [ℕ] \subseteq \{0, 1\})$
131		prex	$⊢ \{0, 1\} \in V$
132	131 86	elmap	$⊢ d \in ({\{0, 1\}}^{ℕ}) \leftrightarrow d : ℕ ⟶ \{0, 1\}$
133		df-f	$⊢ d : ℕ ⟶ ℕ_{0} \leftrightarrow (d Fn ℕ \land ran d \subseteq ℕ_{0})$
134	133	anbi1i	$⊢ (d : ℕ ⟶ ℕ_{0} \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow ((d Fn ℕ \land ran d \subseteq ℕ_{0}) \land d [ℕ] \subseteq \{0, 1\})$
135	130 132 134	3bitr4i	$⊢ d \in ({\{0, 1\}}^{ℕ}) \leftrightarrow (d : ℕ ⟶ ℕ_{0} \land d [ℕ] \subseteq \{0, 1\})$
136		vex	$⊢ d \in V$
137		cnveq	$⊢ f = d \to f^{-1} = d^{-1}$
138	137	imaeq1d	$⊢ f = d \to f^{-1} [ℕ] = d^{-1} [ℕ]$
139	138	eleq1d	$⊢ f = d \to (f^{-1} [ℕ] \in Fin \leftrightarrow d^{-1} [ℕ] \in Fin)$
140	136 139 8	elab2	$⊢ d \in R \leftrightarrow d^{-1} [ℕ] \in Fin$
141	135 140	anbi12i	$⊢ (d \in ({\{0, 1\}}^{ℕ}) \land d \in R) \leftrightarrow ((d : ℕ ⟶ ℕ_{0} \land d [ℕ] \subseteq \{0, 1\}) \land d^{-1} [ℕ] \in Fin)$
142		elin	$⊢ d \in (({\{0, 1\}}^{ℕ}) \cap R) \leftrightarrow (d \in ({\{0, 1\}}^{ℕ}) \land d \in R)$
143		an32	$⊢ ((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow ((d : ℕ ⟶ ℕ_{0} \land d [ℕ] \subseteq \{0, 1\}) \land d^{-1} [ℕ] \in Fin)$
144	141 142 143	3bitr4i	$⊢ d \in (({\{0, 1\}}^{ℕ}) \cap R) \leftrightarrow ((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land d [ℕ] \subseteq \{0, 1\})$
145	144	anbi1i	$⊢ (d \in (({\{0, 1\}}^{ℕ}) \cap R) \land \sum_{k \in ℕ} d (k) k = N) \leftrightarrow (((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land d [ℕ] \subseteq \{0, 1\}) \land \sum_{k \in ℕ} d (k) k = N)$
146	1	eulerpartleme	$⊢ d \in P \leftrightarrow (d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} d (k) k = N)$
147	146	anbi1i	$⊢ (d \in P \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow ((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} d (k) k = N) \land d [ℕ] \subseteq \{0, 1\})$
148		df-3an	$⊢ (d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} d (k) k = N) \leftrightarrow ((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land \sum_{k \in ℕ} d (k) k = N)$
149	148	anbi1i	$⊢ ((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} d (k) k = N) \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow (((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land \sum_{k \in ℕ} d (k) k = N) \land d [ℕ] \subseteq \{0, 1\})$
150		an32	$⊢ (((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land \sum_{k \in ℕ} d (k) k = N) \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow (((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land d [ℕ] \subseteq \{0, 1\}) \land \sum_{k \in ℕ} d (k) k = N)$
151	147 149 150	3bitri	$⊢ (d \in P \land d [ℕ] \subseteq \{0, 1\}) \leftrightarrow (((d : ℕ ⟶ ℕ_{0} \land d^{-1} [ℕ] \in Fin) \land d [ℕ] \subseteq \{0, 1\}) \land \sum_{k \in ℕ} d (k) k = N)$
152	145 151	bitr4i	$⊢ (d \in (({\{0, 1\}}^{ℕ}) \cap R) \land \sum_{k \in ℕ} d (k) k = N) \leftrightarrow (d \in P \land d [ℕ] \subseteq \{0, 1\})$
153		rabid	$⊢ d \in \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\} \leftrightarrow (d \in (({\{0, 1\}}^{ℕ}) \cap R) \land \sum_{k \in ℕ} d (k) k = N)$
154	1 2 3	eulerpartlemd	$⊢ d \in D \leftrightarrow (d \in P \land d [ℕ] \subseteq \{0, 1\})$
155	152 153 154	3bitr4ri	$⊢ d \in D \leftrightarrow d \in \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}$
156	118 119 155	eqri	$⊢ D = \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}$
157	156	a1i	$⊢ ⊤ \to D = \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\}$
158	116 117 157	f1oeq123d	$⊢ ⊤ \to (({G ↾}_{O}) : O \underset{1-1 onto}{⟶} D \leftrightarrow ({G ↾}_{\{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\}}) : \{q \in (T \cap R) \| \sum_{k \in ℕ} q (k) k = N\} \underset{1-1 onto}{⟶} \{d \in (({\{0, 1\}}^{ℕ}) \cap R) \| \sum_{k \in ℕ} d (k) k = N\})$
159	72 158	mpbird	$⊢ ⊤ \to ({G ↾}_{O}) : O \underset{1-1 onto}{⟶} D$
160	159	mptru	$⊢ ({G ↾}_{O}) : O \underset{1-1 onto}{⟶} D$

Metamath Proof Explorer

Theorem eulerpartlemn

Proof