eulerpartlemf

Description: Lemma for eulerpart : Odd partitions are zero for even numbers. (Contributed by Thierry Arnoux, 9-Sep-2017)

	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\}$
Assertion	eulerpartlemf	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to A (t) = 0$

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		eldif	$⊢ t \in (ℕ ∖ J) \leftrightarrow (t \in ℕ \land \neg t \in J)$
11		breq2	$⊢ z = t \to (2 ∥ z \leftrightarrow 2 ∥ t)$
12	11	notbid	$⊢ z = t \to (\neg 2 ∥ z \leftrightarrow \neg 2 ∥ t)$
13	12 4	elrab2	$⊢ t \in J \leftrightarrow (t \in ℕ \land \neg 2 ∥ t)$
14	13	simplbi2	$⊢ t \in ℕ \to (\neg 2 ∥ t \to t \in J)$
15	14	con1d	$⊢ t \in ℕ \to (\neg t \in J \to 2 ∥ t)$
16	15	imp	$⊢ (t \in ℕ \land \neg t \in J) \to 2 ∥ t$
17	10 16	sylbi	$⊢ t \in (ℕ ∖ J) \to 2 ∥ t$
18	17	adantl	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to 2 ∥ t$
19	18	adantr	$⊢ ((A \in (T \cap R) \land t \in (ℕ ∖ J)) \land A (t) \in ℕ) \to 2 ∥ t$
20		simpll	$⊢ ((A \in (T \cap R) \land t \in (ℕ ∖ J)) \land A (t) \in ℕ) \to A \in (T \cap R)$
21		eldifi	$⊢ t \in (ℕ ∖ J) \to t \in ℕ$
22	1 2 3 4 5 6 7 8 9	eulerpartlemt0	$⊢ A \in (T \cap R) \leftrightarrow (A \in ({ℕ_{0}}^{ℕ}) \land A^{-1} [ℕ] \in Fin \land A^{-1} [ℕ] \subseteq J)$
23	22	simp1bi	$⊢ A \in (T \cap R) \to A \in ({ℕ_{0}}^{ℕ})$
24		elmapi	$⊢ A \in ({ℕ_{0}}^{ℕ}) \to A : ℕ ⟶ ℕ_{0}$
25	23 24	syl	$⊢ A \in (T \cap R) \to A : ℕ ⟶ ℕ_{0}$
26		ffn	$⊢ A : ℕ ⟶ ℕ_{0} \to A Fn ℕ$
27		elpreima	$⊢ A Fn ℕ \to (t \in A^{-1} [ℕ] \leftrightarrow (t \in ℕ \land A (t) \in ℕ))$
28	25 26 27	3syl	$⊢ A \in (T \cap R) \to (t \in A^{-1} [ℕ] \leftrightarrow (t \in ℕ \land A (t) \in ℕ))$
29	28	baibd	$⊢ (A \in (T \cap R) \land t \in ℕ) \to (t \in A^{-1} [ℕ] \leftrightarrow A (t) \in ℕ)$
30	21 29	sylan2	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to (t \in A^{-1} [ℕ] \leftrightarrow A (t) \in ℕ)$
31	30	biimpar	$⊢ ((A \in (T \cap R) \land t \in (ℕ ∖ J)) \land A (t) \in ℕ) \to t \in A^{-1} [ℕ]$
32	22	simp3bi	$⊢ A \in (T \cap R) \to A^{-1} [ℕ] \subseteq J$
33	32	sselda	$⊢ (A \in (T \cap R) \land t \in A^{-1} [ℕ]) \to t \in J$
34	13	simprbi	$⊢ t \in J \to \neg 2 ∥ t$
35	33 34	syl	$⊢ (A \in (T \cap R) \land t \in A^{-1} [ℕ]) \to \neg 2 ∥ t$
36	20 31 35	syl2anc	$⊢ ((A \in (T \cap R) \land t \in (ℕ ∖ J)) \land A (t) \in ℕ) \to \neg 2 ∥ t$
37	19 36	pm2.65da	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to \neg A (t) \in ℕ$
38	25	adantr	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to A : ℕ ⟶ ℕ_{0}$
39	21	adantl	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to t \in ℕ$
40	38 39	ffvelcdmd	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to A (t) \in ℕ_{0}$
41		elnn0	$⊢ A (t) \in ℕ_{0} \leftrightarrow (A (t) \in ℕ \lor A (t) = 0)$
42	40 41	sylib	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to (A (t) \in ℕ \lor A (t) = 0)$
43		orel1	$⊢ \neg A (t) \in ℕ \to ((A (t) \in ℕ \lor A (t) = 0) \to A (t) = 0)$
44	37 42 43	sylc	$⊢ (A \in (T \cap R) \land t \in (ℕ ∖ J)) \to A (t) = 0$

Metamath Proof Explorer

Theorem eulerpartlemf

Proof