eulerpartlemb

Description: Lemma for eulerpart . The set of all partitions of N is finite. (Contributed by Mario Carneiro, 26-Jan-2015)

	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))\})$
Assertion	eulerpartlemb	$⊢ P \in Fin$

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		fzfid	$⊢ ⊤ \to (1 \dots N) \in Fin$
9		fzfi	$⊢ (0 \dots N) \in Fin$
10		snfi	$⊢ \{0\} \in Fin$
11	9 10	ifcli	$⊢ if (x \in (1 \dots N), (0 \dots N), \{0\}) \in Fin$
12	11	a1i	$⊢ (⊤ \land x \in ℕ) \to if (x \in (1 \dots N), (0 \dots N), \{0\}) \in Fin$
13		eldifn	$⊢ x \in (ℕ ∖ (1 \dots N)) \to \neg x \in (1 \dots N)$
14	13	adantl	$⊢ (⊤ \land x \in (ℕ ∖ (1 \dots N))) \to \neg x \in (1 \dots N)$
15		iffalse	$⊢ \neg x \in (1 \dots N) \to if (x \in (1 \dots N), (0 \dots N), \{0\}) = \{0\}$
16		eqimss	$⊢ if (x \in (1 \dots N), (0 \dots N), \{0\}) = \{0\} \to if (x \in (1 \dots N), (0 \dots N), \{0\}) \subseteq \{0\}$
17	14 15 16	3syl	$⊢ (⊤ \land x \in (ℕ ∖ (1 \dots N))) \to if (x \in (1 \dots N), (0 \dots N), \{0\}) \subseteq \{0\}$
18	8 12 17	ixpfi2	$⊢ ⊤ \to \underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\}) \in Fin$
19	18	mptru	$⊢ \underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\}) \in Fin$
20	1	eulerpartleme	$⊢ g \in P \leftrightarrow (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N)$
21		ffn	$⊢ g : ℕ ⟶ ℕ_{0} \to g Fn ℕ$
22	21	3ad2ant1	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \to g Fn ℕ$
23		ffvelcdm	$⊢ (g : ℕ ⟶ ℕ_{0} \land x \in ℕ) \to g (x) \in ℕ_{0}$
24	23	3ad2antl1	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) \in ℕ_{0}$
25	24	nn0red	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) \in ℝ$
26		nnre	$⊢ x \in ℕ \to x \in ℝ$
27	26	adantl	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to x \in ℝ$
28	25 27	remulcld	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) x \in ℝ$
29		cnvimass	$⊢ g^{-1} [ℕ] \subseteq dom g$
30		fdm	$⊢ g : ℕ ⟶ ℕ_{0} \to dom g = ℕ$
31	30	adantr	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to dom g = ℕ$
32	29 31	sseqtrid	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to g^{-1} [ℕ] \subseteq ℕ$
33	32	sselda	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in g^{-1} [ℕ]) \to k \in ℕ$
34		ffvelcdm	$⊢ (g : ℕ ⟶ ℕ_{0} \land k \in ℕ) \to g (k) \in ℕ_{0}$
35	34	adantlr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in ℕ) \to g (k) \in ℕ_{0}$
36	33 35	syldan	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in g^{-1} [ℕ]) \to g (k) \in ℕ_{0}$
37	33	nnnn0d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in g^{-1} [ℕ]) \to k \in ℕ_{0}$
38	36 37	nn0mulcld	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in g^{-1} [ℕ]) \to g (k) k \in ℕ_{0}$
39	38	nn0cnd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in g^{-1} [ℕ]) \to g (k) k \in ℂ$
40		simpl	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to g : ℕ ⟶ ℕ_{0}$
41		nnex	$⊢ ℕ \in V$
42		fcdmnn0supp	$⊢ (ℕ \in V \land g : ℕ ⟶ ℕ_{0}) \to g supp 0 = g^{-1} [ℕ]$
43	41 42	mpan	$⊢ g : ℕ ⟶ ℕ_{0} \to g supp 0 = g^{-1} [ℕ]$
44	43	adantr	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to g supp 0 = g^{-1} [ℕ]$
45		eqimss	$⊢ g supp 0 = g^{-1} [ℕ] \to g supp 0 \subseteq g^{-1} [ℕ]$
46	44 45	syl	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to g supp 0 \subseteq g^{-1} [ℕ]$
47	41	a1i	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to ℕ \in V$
48		0nn0	$⊢ 0 \in ℕ_{0}$
49	48	a1i	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to 0 \in ℕ_{0}$
50	40 46 47 49	suppssr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in (ℕ ∖ g^{-1} [ℕ])) \to g (k) = 0$
51	50	oveq1d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in (ℕ ∖ g^{-1} [ℕ])) \to g (k) k = 0 \cdot k$
52		eldifi	$⊢ k \in (ℕ ∖ g^{-1} [ℕ]) \to k \in ℕ$
53	52	adantl	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in (ℕ ∖ g^{-1} [ℕ])) \to k \in ℕ$
54		nncn	$⊢ k \in ℕ \to k \in ℂ$
55		mul02	$⊢ k \in ℂ \to 0 \cdot k = 0$
56	53 54 55	3syl	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in (ℕ ∖ g^{-1} [ℕ])) \to 0 \cdot k = 0$
57	51 56	eqtrd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in (ℕ ∖ g^{-1} [ℕ])) \to g (k) k = 0$
58		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
59	58	eqimssi	$⊢ ℕ \subseteq ℤ_{\geq 1}$
60	59	a1i	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to ℕ \subseteq ℤ_{\geq 1}$
61	32 39 57 60	sumss	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to \sum_{k \in g^{-1} [ℕ]} g (k) k = \sum_{k \in ℕ} g (k) k$
62		simpr	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to g^{-1} [ℕ] \in Fin$
63	62 38	fsumnn0cl	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to \sum_{k \in g^{-1} [ℕ]} g (k) k \in ℕ_{0}$
64	61 63	eqeltrrd	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to \sum_{k \in ℕ} g (k) k \in ℕ_{0}$
65		eleq1	$⊢ \sum_{k \in ℕ} g (k) k = N \to (\sum_{k \in ℕ} g (k) k \in ℕ_{0} \leftrightarrow N \in ℕ_{0})$
66	64 65	syl5ibcom	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to (\sum_{k \in ℕ} g (k) k = N \to N \in ℕ_{0})$
67	66	3impia	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \to N \in ℕ_{0}$
68	67	adantr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to N \in ℕ_{0}$
69	68	nn0red	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to N \in ℝ$
70	24	nn0ge0d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to 0 \leq g (x)$
71		nnge1	$⊢ x \in ℕ \to 1 \leq x$
72	71	adantl	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to 1 \leq x$
73	25 27 70 72	lemulge11d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) \leq g (x) x$
74	62	adantr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land x \in g^{-1} [ℕ])) \to g^{-1} [ℕ] \in Fin$
75	38	nn0red	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in g^{-1} [ℕ]) \to g (k) k \in ℝ$
76	75	adantlr	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land x \in g^{-1} [ℕ])) \land k \in g^{-1} [ℕ]) \to g (k) k \in ℝ$
77	38	nn0ge0d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land k \in g^{-1} [ℕ]) \to 0 \leq g (k) k$
78	77	adantlr	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land x \in g^{-1} [ℕ])) \land k \in g^{-1} [ℕ]) \to 0 \leq g (k) k$
79		fveq2	$⊢ k = x \to g (k) = g (x)$
80		id	$⊢ k = x \to k = x$
81	79 80	oveq12d	$⊢ k = x \to g (k) k = g (x) x$
82		simprr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land x \in g^{-1} [ℕ])) \to x \in g^{-1} [ℕ]$
83	74 76 78 81 82	fsumge1	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land x \in g^{-1} [ℕ])) \to g (x) x \leq \sum_{k \in g^{-1} [ℕ]} g (k) k$
84	83	expr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \to (x \in g^{-1} [ℕ] \to g (x) x \leq \sum_{k \in g^{-1} [ℕ]} g (k) k)$
85		eldif	$⊢ x \in (ℕ ∖ g^{-1} [ℕ]) \leftrightarrow (x \in ℕ \land \neg x \in g^{-1} [ℕ])$
86	57	ralrimiva	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \to \forall k \in (ℕ ∖ g^{-1} [ℕ]) g (k) k = 0$
87	81	eqeq1d	$⊢ k = x \to (g (k) k = 0 \leftrightarrow g (x) x = 0)$
88	87	rspccva	$⊢ (\forall k \in (ℕ ∖ g^{-1} [ℕ]) g (k) k = 0 \land x \in (ℕ ∖ g^{-1} [ℕ])) \to g (x) x = 0$
89	86 88	sylan	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in (ℕ ∖ g^{-1} [ℕ])) \to g (x) x = 0$
90	85 89	sylan2br	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land \neg x \in g^{-1} [ℕ])) \to g (x) x = 0$
91	62	adantr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \to g^{-1} [ℕ] \in Fin$
92	38	adantlr	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \land k \in g^{-1} [ℕ]) \to g (k) k \in ℕ_{0}$
93	92	nn0red	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \land k \in g^{-1} [ℕ]) \to g (k) k \in ℝ$
94	92	nn0ge0d	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \land k \in g^{-1} [ℕ]) \to 0 \leq g (k) k$
95	91 93 94	fsumge0	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \to 0 \leq \sum_{k \in g^{-1} [ℕ]} g (k) k$
96	95	adantrr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land \neg x \in g^{-1} [ℕ])) \to 0 \leq \sum_{k \in g^{-1} [ℕ]} g (k) k$
97	90 96	eqbrtrd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land (x \in ℕ \land \neg x \in g^{-1} [ℕ])) \to g (x) x \leq \sum_{k \in g^{-1} [ℕ]} g (k) k$
98	97	expr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \to (\neg x \in g^{-1} [ℕ] \to g (x) x \leq \sum_{k \in g^{-1} [ℕ]} g (k) k)$
99	84 98	pm2.61d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \to g (x) x \leq \sum_{k \in g^{-1} [ℕ]} g (k) k$
100	61	adantr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \to \sum_{k \in g^{-1} [ℕ]} g (k) k = \sum_{k \in ℕ} g (k) k$
101	99 100	breqtrd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin) \land x \in ℕ) \to g (x) x \leq \sum_{k \in ℕ} g (k) k$
102	101	3adantl3	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) x \leq \sum_{k \in ℕ} g (k) k$
103		simpl3	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to \sum_{k \in ℕ} g (k) k = N$
104	102 103	breqtrd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) x \leq N$
105	25 28 69 73 104	letrd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) \leq N$
106		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
107	24 106	eleqtrdi	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) \in ℤ_{\geq 0}$
108	68	nn0zd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to N \in ℤ$
109		elfz5	$⊢ (g (x) \in ℤ_{\geq 0} \land N \in ℤ) \to (g (x) \in (0 \dots N) \leftrightarrow g (x) \leq N)$
110	107 108 109	syl2anc	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (g (x) \in (0 \dots N) \leftrightarrow g (x) \leq N)$
111	105 110	mpbird	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) \in (0 \dots N)$
112	111	adantr	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \land x \in (1 \dots N)) \to g (x) \in (0 \dots N)$
113		iftrue	$⊢ x \in (1 \dots N) \to if (x \in (1 \dots N), (0 \dots N), \{0\}) = (0 \dots N)$
114	113	adantl	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \land x \in (1 \dots N)) \to if (x \in (1 \dots N), (0 \dots N), \{0\}) = (0 \dots N)$
115	112 114	eleqtrrd	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \land x \in (1 \dots N)) \to g (x) \in if (x \in (1 \dots N), (0 \dots N), \{0\})$
116		nnge1	$⊢ g (x) \in ℕ \to 1 \leq g (x)$
117		nnnn0	$⊢ x \in ℕ \to x \in ℕ_{0}$
118	117	adantl	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to x \in ℕ_{0}$
119	118	nn0ge0d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to 0 \leq x$
120		lemulge12	$⊢ ((x \in ℝ \land g (x) \in ℝ) \land (0 \leq x \land 1 \leq g (x))) \to x \leq g (x) x$
121	120	expr	$⊢ ((x \in ℝ \land g (x) \in ℝ) \land 0 \leq x) \to (1 \leq g (x) \to x \leq g (x) x)$
122	27 25 119 121	syl21anc	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (1 \leq g (x) \to x \leq g (x) x)$
123		letr	$⊢ (x \in ℝ \land g (x) x \in ℝ \land N \in ℝ) \to ((x \leq g (x) x \land g (x) x \leq N) \to x \leq N)$
124	27 28 69 123	syl3anc	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to ((x \leq g (x) x \land g (x) x \leq N) \to x \leq N)$
125	104 124	mpan2d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (x \leq g (x) x \to x \leq N)$
126	122 125	syld	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (1 \leq g (x) \to x \leq N)$
127	116 126	syl5	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (g (x) \in ℕ \to x \leq N)$
128		simpr	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to x \in ℕ$
129	128 58	eleqtrdi	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to x \in ℤ_{\geq 1}$
130		elfz5	$⊢ (x \in ℤ_{\geq 1} \land N \in ℤ) \to (x \in (1 \dots N) \leftrightarrow x \leq N)$
131	129 108 130	syl2anc	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (x \in (1 \dots N) \leftrightarrow x \leq N)$
132	127 131	sylibrd	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (g (x) \in ℕ \to x \in (1 \dots N))$
133	132	con3d	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (\neg x \in (1 \dots N) \to \neg g (x) \in ℕ)$
134		elnn0	$⊢ g (x) \in ℕ_{0} \leftrightarrow (g (x) \in ℕ \lor g (x) = 0)$
135	24 134	sylib	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (g (x) \in ℕ \lor g (x) = 0)$
136	135	ord	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (\neg g (x) \in ℕ \to g (x) = 0)$
137	133 136	syld	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to (\neg x \in (1 \dots N) \to g (x) = 0)$
138	137	imp	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \land \neg x \in (1 \dots N)) \to g (x) = 0$
139		fvex	$⊢ g (x) \in V$
140	139	elsn	$⊢ g (x) \in \{0\} \leftrightarrow g (x) = 0$
141	138 140	sylibr	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \land \neg x \in (1 \dots N)) \to g (x) \in \{0\}$
142	15	adantl	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \land \neg x \in (1 \dots N)) \to if (x \in (1 \dots N), (0 \dots N), \{0\}) = \{0\}$
143	141 142	eleqtrrd	$⊢ (((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \land \neg x \in (1 \dots N)) \to g (x) \in if (x \in (1 \dots N), (0 \dots N), \{0\})$
144	115 143	pm2.61dan	$⊢ ((g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \land x \in ℕ) \to g (x) \in if (x \in (1 \dots N), (0 \dots N), \{0\})$
145	144	ralrimiva	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \to \forall x \in ℕ g (x) \in if (x \in (1 \dots N), (0 \dots N), \{0\})$
146		vex	$⊢ g \in V$
147	146	elixp	$⊢ g \in \underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\}) \leftrightarrow (g Fn ℕ \land \forall x \in ℕ g (x) \in if (x \in (1 \dots N), (0 \dots N), \{0\}))$
148	22 145 147	sylanbrc	$⊢ (g : ℕ ⟶ ℕ_{0} \land g^{-1} [ℕ] \in Fin \land \sum_{k \in ℕ} g (k) k = N) \to g \in \underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\})$
149	20 148	sylbi	$⊢ g \in P \to g \in \underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\})$
150	149	ssriv	$⊢ P \subseteq \underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\})$
151		ssfi	$⊢ (\underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\}) \in Fin \land P \subseteq \underset{x \in ℕ}{⨉} if (x \in (1 \dots N), (0 \dots N), \{0\})) \to P \in Fin$
152	19 150 151	mp2an	$⊢ P \in Fin$

Metamath Proof Explorer

Theorem eulerpartlemb

Proof