sticksstones22

Description: Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones22.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones22.2	$⊢ φ \to S \in Fin$
	sticksstones22.3	$⊢ φ \to S \neq \emptyset$
	sticksstones22.4	$⊢ A = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}$
Assertion	sticksstones22	$⊢ φ \to \|A\| = (\binom{N + \|S\|}{\|S\|})$

Proof

Step	Hyp	Ref	Expression
1		sticksstones22.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones22.2	$⊢ φ \to S \in Fin$
3		sticksstones22.3	$⊢ φ \to S \neq \emptyset$
4		sticksstones22.4	$⊢ A = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}$
5	4	a1i	$⊢ φ \to A = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}$
6	5	fveq2d	$⊢ φ \to \|A\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}\|$
7		breq2	$⊢ x = 0 \to (\sum_{i \in S} f (i) \leq x \leftrightarrow \sum_{i \in S} f (i) \leq 0)$
8	7	anbi2d	$⊢ x = 0 \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x) \leftrightarrow (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0))$
9	8	abbidv	$⊢ x = 0 \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)\}$
10	9	fveq2d	$⊢ x = 0 \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)\}\|$
11		oveq1	$⊢ x = 0 \to x + \|S\| = 0 + \|S\|$
12	11	oveq1d	$⊢ x = 0 \to (\binom{x + \|S\|}{\|S\|}) = (\binom{0 + \|S\|}{\|S\|})$
13	10 12	eqeq12d	$⊢ x = 0 \to (\|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = (\binom{x + \|S\|}{\|S\|}) \leftrightarrow \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)\}\| = (\binom{0 + \|S\|}{\|S\|}))$
14		breq2	$⊢ x = y \to (\sum_{i \in S} f (i) \leq x \leftrightarrow \sum_{i \in S} f (i) \leq y)$
15	14	anbi2d	$⊢ x = y \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x) \leftrightarrow (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y))$
16	15	abbidv	$⊢ x = y \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}$
17	16	fveq2d	$⊢ x = y \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\|$
18		oveq1	$⊢ x = y \to x + \|S\| = y + \|S\|$
19	18	oveq1d	$⊢ x = y \to (\binom{x + \|S\|}{\|S\|}) = (\binom{y + \|S\|}{\|S\|})$
20	17 19	eqeq12d	$⊢ x = y \to (\|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = (\binom{x + \|S\|}{\|S\|}) \leftrightarrow \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|}))$
21		breq2	$⊢ x = y + 1 \to (\sum_{i \in S} f (i) \leq x \leftrightarrow \sum_{i \in S} f (i) \leq y + 1)$
22	21	anbi2d	$⊢ x = y + 1 \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x) \leftrightarrow (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1))$
23	22	abbidv	$⊢ x = y + 1 \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\}$
24	23	fveq2d	$⊢ x = y + 1 \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\}\|$
25		oveq1	$⊢ x = y + 1 \to x + \|S\| = y + 1 + \|S\|$
26	25	oveq1d	$⊢ x = y + 1 \to (\binom{x + \|S\|}{\|S\|}) = (\binom{y + 1 + \|S\|}{\|S\|})$
27	24 26	eqeq12d	$⊢ x = y + 1 \to (\|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = (\binom{x + \|S\|}{\|S\|}) \leftrightarrow \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\}\| = (\binom{y + 1 + \|S\|}{\|S\|}))$
28		breq2	$⊢ x = N \to (\sum_{i \in S} f (i) \leq x \leftrightarrow \sum_{i \in S} f (i) \leq N)$
29	28	anbi2d	$⊢ x = N \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x) \leftrightarrow (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N))$
30	29	abbidv	$⊢ x = N \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}$
31	30	fveq2d	$⊢ x = N \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}\|$
32		oveq1	$⊢ x = N \to x + \|S\| = N + \|S\|$
33	32	oveq1d	$⊢ x = N \to (\binom{x + \|S\|}{\|S\|}) = (\binom{N + \|S\|}{\|S\|})$
34	31 33	eqeq12d	$⊢ x = N \to (\|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq x)\}\| = (\binom{x + \|S\|}{\|S\|}) \leftrightarrow \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}\| = (\binom{N + \|S\|}{\|S\|}))$
35		simprl	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to f : S ⟶ ℕ_{0}$
36		simprr	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to \sum_{i \in S} f (i) \leq 0$
37	2	adantr	$⊢ (φ \land f : S ⟶ ℕ_{0}) \to S \in Fin$
38		simpr	$⊢ (φ \land f : S ⟶ ℕ_{0}) \to f : S ⟶ ℕ_{0}$
39	38	ffvelrnda	$⊢ ((φ \land f : S ⟶ ℕ_{0}) \land i \in S) \to f (i) \in ℕ_{0}$
40	37 39	fsumnn0cl	$⊢ (φ \land f : S ⟶ ℕ_{0}) \to \sum_{i \in S} f (i) \in ℕ_{0}$
41	35 40	syldan	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to \sum_{i \in S} f (i) \in ℕ_{0}$
42	41	nn0ge0d	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to 0 \leq \sum_{i \in S} f (i)$
43		0red	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to 0 \in ℝ$
44	41	nn0red	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to \sum_{i \in S} f (i) \in ℝ$
45	43 44	lenltd	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to (0 \leq \sum_{i \in S} f (i) \leftrightarrow \neg \sum_{i \in S} f (i) < 0)$
46	42 45	mpbid	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to \neg \sum_{i \in S} f (i) < 0$
47	36 46	jca	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to (\sum_{i \in S} f (i) \leq 0 \land \neg \sum_{i \in S} f (i) < 0)$
48	44 43	eqleltd	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to (\sum_{i \in S} f (i) = 0 \leftrightarrow (\sum_{i \in S} f (i) \leq 0 \land \neg \sum_{i \in S} f (i) < 0))$
49	47 48	mpbird	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to \sum_{i \in S} f (i) = 0$
50	35 49	jca	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)$
51	50	ex	$⊢ φ \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0))$
52		simprl	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)) \to f : S ⟶ ℕ_{0}$
53		simprr	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)) \to \sum_{i \in S} f (i) = 0$
54		0red	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)) \to 0 \in ℝ$
55	54	leidd	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)) \to 0 \leq 0$
56	53 55	eqbrtrd	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)) \to \sum_{i \in S} f (i) \leq 0$
57	52 56	jca	$⊢ (φ \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)$
58	57	ex	$⊢ φ \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0))$
59	51 58	impbid	$⊢ φ \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0) \leftrightarrow (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0))$
60	59	abbidv	$⊢ φ \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)\}$
61	60	fveq2d	$⊢ φ \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)\}\|$
62		0nn0	$⊢ 0 \in ℕ_{0}$
63	62	a1i	$⊢ φ \to 0 \in ℕ_{0}$
64		eqid	$⊢ \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)\}$
65	63 2 3 64	sticksstones21	$⊢ φ \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)\}\| = (\binom{0 + \|S\| - 1}{\|S\| - 1})$
66		hashnncl	$⊢ S \in Fin \to (\|S\| \in ℕ \leftrightarrow S \neq \emptyset)$
67	2 66	syl	$⊢ φ \to (\|S\| \in ℕ \leftrightarrow S \neq \emptyset)$
68	67	bicomd	$⊢ φ \to (S \neq \emptyset \leftrightarrow \|S\| \in ℕ)$
69	68	biimpd	$⊢ φ \to (S \neq \emptyset \to \|S\| \in ℕ)$
70	3 69	mpd	$⊢ φ \to \|S\| \in ℕ$
71	70	nncnd	$⊢ φ \to \|S\| \in ℂ$
72		1cnd	$⊢ φ \to 1 \in ℂ$
73	71 72	subcld	$⊢ φ \to \|S\| - 1 \in ℂ$
74	73	addid2d	$⊢ φ \to 0 + \|S\| - 1 = \|S\| - 1$
75	74	oveq1d	$⊢ φ \to (\binom{0 + \|S\| - 1}{\|S\| - 1}) = (\binom{\|S\| - 1}{\|S\| - 1})$
76		nnm1nn0	$⊢ \|S\| \in ℕ \to \|S\| - 1 \in ℕ_{0}$
77	70 76	syl	$⊢ φ \to \|S\| - 1 \in ℕ_{0}$
78		bcnn	$⊢ \|S\| - 1 \in ℕ_{0} \to (\binom{\|S\| - 1}{\|S\| - 1}) = 1$
79	77 78	syl	$⊢ φ \to (\binom{\|S\| - 1}{\|S\| - 1}) = 1$
80	75 79	eqtrd	$⊢ φ \to (\binom{0 + \|S\| - 1}{\|S\| - 1}) = 1$
81		eqidd	$⊢ φ \to 1 = 1$
82	70	nnnn0d	$⊢ φ \to \|S\| \in ℕ_{0}$
83		bcnn	$⊢ \|S\| \in ℕ_{0} \to (\binom{\|S\|}{\|S\|}) = 1$
84	82 83	syl	$⊢ φ \to (\binom{\|S\|}{\|S\|}) = 1$
85	84	eqcomd	$⊢ φ \to 1 = (\binom{\|S\|}{\|S\|})$
86	71	addid2d	$⊢ φ \to 0 + \|S\| = \|S\|$
87	86	eqcomd	$⊢ φ \to \|S\| = 0 + \|S\|$
88	87	oveq1d	$⊢ φ \to (\binom{\|S\|}{\|S\|}) = (\binom{0 + \|S\|}{\|S\|})$
89	85 88	eqtrd	$⊢ φ \to 1 = (\binom{0 + \|S\|}{\|S\|})$
90	80 81 89	3eqtrd	$⊢ φ \to (\binom{0 + \|S\| - 1}{\|S\| - 1}) = (\binom{0 + \|S\|}{\|S\|})$
91	65 90	eqtrd	$⊢ φ \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = 0)\}\| = (\binom{0 + \|S\|}{\|S\|})$
92	61 91	eqtrd	$⊢ φ \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq 0)\}\| = (\binom{0 + \|S\|}{\|S\|})$
93		simprl	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to f : S ⟶ ℕ_{0}$
94		simprr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to \sum_{i \in S} f (i) \leq y + 1$
95	2	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to S \in Fin$
96		simpr	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to f : S ⟶ ℕ_{0}$
97	96	ffvelrnda	$⊢ (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land i \in S) \to f (i) \in ℕ_{0}$
98	95 97	fsumnn0cl	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to \sum_{i \in S} f (i) \in ℕ_{0}$
99	93 98	syldan	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to \sum_{i \in S} f (i) \in ℕ_{0}$
100	99	nn0red	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to \sum_{i \in S} f (i) \in ℝ$
101		nn0re	$⊢ y \in ℕ_{0} \to y \in ℝ$
102	101	adantl	$⊢ (φ \land y \in ℕ_{0}) \to y \in ℝ$
103	102	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to y \in ℝ$
104		1red	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to 1 \in ℝ$
105	103 104	readdcld	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to y + 1 \in ℝ$
106	100 105	leloed	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to (\sum_{i \in S} f (i) \leq y + 1 \leftrightarrow (\sum_{i \in S} f (i) < y + 1 \lor \sum_{i \in S} f (i) = y + 1))$
107	94 106	mpbid	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to (\sum_{i \in S} f (i) < y + 1 \lor \sum_{i \in S} f (i) = y + 1)$
108	99	nn0zd	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to \sum_{i \in S} f (i) \in ℤ$
109		nn0z	$⊢ y \in ℕ_{0} \to y \in ℤ$
110	109	adantl	$⊢ (φ \land y \in ℕ_{0}) \to y \in ℤ$
111	110	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to y \in ℤ$
112		zleltp1	$⊢ (\sum_{i \in S} f (i) \in ℤ \land y \in ℤ) \to (\sum_{i \in S} f (i) \leq y \leftrightarrow \sum_{i \in S} f (i) < y + 1)$
113	112	bicomd	$⊢ (\sum_{i \in S} f (i) \in ℤ \land y \in ℤ) \to (\sum_{i \in S} f (i) < y + 1 \leftrightarrow \sum_{i \in S} f (i) \leq y)$
114	108 111 113	syl2anc	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to (\sum_{i \in S} f (i) < y + 1 \leftrightarrow \sum_{i \in S} f (i) \leq y)$
115	114	orbi1d	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to ((\sum_{i \in S} f (i) < y + 1 \lor \sum_{i \in S} f (i) = y + 1) \leftrightarrow (\sum_{i \in S} f (i) \leq y \lor \sum_{i \in S} f (i) = y + 1))$
116	107 115	mpbid	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to (\sum_{i \in S} f (i) \leq y \lor \sum_{i \in S} f (i) = y + 1)$
117	93 116	jca	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to (f : S ⟶ ℕ_{0} \land (\sum_{i \in S} f (i) \leq y \lor \sum_{i \in S} f (i) = y + 1))$
118		andi	$⊢ (f : S ⟶ ℕ_{0} \land (\sum_{i \in S} f (i) \leq y \lor \sum_{i \in S} f (i) = y + 1)) \leftrightarrow ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))$
119	118	bicomi	$⊢ ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \leftrightarrow (f : S ⟶ ℕ_{0} \land (\sum_{i \in S} f (i) \leq y \lor \sum_{i \in S} f (i) = y + 1))$
120	117 119	sylibr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))$
121	120	ex	$⊢ (φ \land y \in ℕ_{0}) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)))$
122		simprl	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to f : S ⟶ ℕ_{0}$
123	122 98	syldan	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \in ℕ_{0}$
124	123	nn0red	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \in ℝ$
125	102	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to y \in ℝ$
126		1red	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to 1 \in ℝ$
127	125 126	readdcld	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to y + 1 \in ℝ$
128		simprr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \leq y$
129	125	lep1d	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to y \leq y + 1$
130	124 125 127 128 129	letrd	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \leq y + 1$
131	122 130	jca	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)$
132	131	ex	$⊢ (φ \land y \in ℕ_{0}) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1))$
133		simprl	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to f : S ⟶ ℕ_{0}$
134		simprr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to \sum_{i \in S} f (i) = y + 1$
135	102	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to y \in ℝ$
136		1red	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to 1 \in ℝ$
137	135 136	readdcld	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to y + 1 \in ℝ$
138	137	leidd	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to y + 1 \leq y + 1$
139	134 138	eqbrtrd	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to \sum_{i \in S} f (i) \leq y + 1$
140	133 139	jca	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)$
141	140	ex	$⊢ (φ \land y \in ℕ_{0}) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1))$
142	132 141	jaod	$⊢ (φ \land y \in ℕ_{0}) \to (((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1))$
143	121 142	impbid	$⊢ (φ \land y \in ℕ_{0}) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1) \leftrightarrow ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)))$
144	143	abbidv	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\} = \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\}$
145		unab	$⊢ \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\}$
146	145	a1i	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\}$
147	146	eqcomd	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \lor (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}$
148	144 147	eqtrd	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}$
149	148	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}$
150	149	fveq2d	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\|$
151	2	adantr	$⊢ (φ \land y \in ℕ_{0}) \to S \in Fin$
152		fzfid	$⊢ (φ \land y \in ℕ_{0}) \to (0 \dots y) \in Fin$
153	151 152	jca	$⊢ (φ \land y \in ℕ_{0}) \to (S \in Fin \land (0 \dots y) \in Fin)$
154		xpfi	$⊢ (S \in Fin \land (0 \dots y) \in Fin) \to S \times (0 \dots y) \in Fin$
155	153 154	syl	$⊢ (φ \land y \in ℕ_{0}) \to S \times (0 \dots y) \in Fin$
156		pwfi	$⊢ S \times (0 \dots y) \in Fin \leftrightarrow 𝒫 (S \times (0 \dots y)) \in Fin$
157	155 156	sylib	$⊢ (φ \land y \in ℕ_{0}) \to 𝒫 (S \times (0 \dots y)) \in Fin$
158		fsetsspwxp	$⊢ \{f \| f : S ⟶ (0 \dots y)\} \subseteq 𝒫 (S \times (0 \dots y))$
159	158	a1i	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| f : S ⟶ (0 \dots y)\} \subseteq 𝒫 (S \times (0 \dots y))$
160	157 159	ssfid	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| f : S ⟶ (0 \dots y)\} \in Fin$
161		ffn	$⊢ f : S ⟶ ℕ_{0} \to f Fn S$
162	122 161	syl	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to f Fn S$
163		0zd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to 0 \in ℤ$
164	110	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to y \in ℤ$
165	164	adantr	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to y \in ℤ$
166	122	ffvelrnda	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) \in ℕ_{0}$
167	166	nn0zd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) \in ℤ$
168	166	nn0ge0d	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to 0 \leq f (s)$
169	128	ad2antrr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to \sum_{i \in S} f (i) \leq y$
170	125	ad2antrr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to y \in ℝ$
171	166	nn0red	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) \in ℝ$
172	171	adantr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to f (s) \in ℝ$
173	124	adantr	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to \sum_{i \in S} f (i) \in ℝ$
174	173	adantr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to \sum_{i \in S} f (i) \in ℝ$
175		simpr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to y < f (s)$
176		simplll	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to φ$
177		simpllr	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to y \in ℕ_{0}$
178		simplrl	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f : S ⟶ ℕ_{0}$
179	176 177 178	jca31	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0})$
180		difssd	$⊢ φ \to S ∖ \{s\} \subseteq S$
181	2 180	ssfid	$⊢ φ \to S ∖ \{s\} \in Fin$
182	181	adantr	$⊢ (φ \land y \in ℕ_{0}) \to S ∖ \{s\} \in Fin$
183	182	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to S ∖ \{s\} \in Fin$
184		eldifi	$⊢ i \in (S ∖ \{s\}) \to i \in S$
185	184	adantl	$⊢ (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land i \in (S ∖ \{s\})) \to i \in S$
186	97	adantlr	$⊢ ((((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land i \in (S ∖ \{s\})) \land i \in S) \to f (i) \in ℕ_{0}$
187	185 186	mpdan	$⊢ (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land i \in (S ∖ \{s\})) \to f (i) \in ℕ_{0}$
188	183 187	fsumnn0cl	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℕ_{0}$
189	179 188	syl	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℕ_{0}$
190	189	nn0ge0d	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to 0 \leq \sum_{i \in S ∖ \{s\}} f (i)$
191		difssd	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to S ∖ \{s\} \subseteq S$
192	95 191	ssfid	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to S ∖ \{s\} \in Fin$
193	192 187	fsumnn0cl	$⊢ ((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℕ_{0}$
194	179 193	syl	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℕ_{0}$
195	194	nn0red	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℝ$
196	171 195	addge01d	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to (0 \leq \sum_{i \in S ∖ \{s\}} f (i) \leftrightarrow f (s) \leq f (s) + \sum_{i \in S ∖ \{s\}} f (i))$
197	190 196	mpbid	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) \leq f (s) + \sum_{i \in S ∖ \{s\}} f (i)$
198		simpr	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to s \in S$
199	179 198	jca	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land s \in S)$
200		nfv	$⊢ Ⅎ i (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land s \in S)$
201		nfcv	$⊢ \underline{Ⅎ} i f (s)$
202	95	adantr	$⊢ (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land s \in S) \to S \in Fin$
203	97	adantlr	$⊢ ((((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land s \in S) \land i \in S) \to f (i) \in ℕ_{0}$
204	203	nn0cnd	$⊢ ((((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land s \in S) \land i \in S) \to f (i) \in ℂ$
205		simpr	$⊢ (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land s \in S) \to s \in S$
206		fveq2	$⊢ i = s \to f (i) = f (s)$
207	200 201 202 204 205 206	fsumsplit1	$⊢ (((φ \land y \in ℕ_{0}) \land f : S ⟶ ℕ_{0}) \land s \in S) \to \sum_{i \in S} f (i) = f (s) + \sum_{i \in S ∖ \{s\}} f (i)$
208	199 207	syl	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to \sum_{i \in S} f (i) = f (s) + \sum_{i \in S ∖ \{s\}} f (i)$
209	208	eqcomd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) + \sum_{i \in S ∖ \{s\}} f (i) = \sum_{i \in S} f (i)$
210	197 209	breqtrd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) \leq \sum_{i \in S} f (i)$
211	210	adantr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to f (s) \leq \sum_{i \in S} f (i)$
212	170 172 174 175 211	ltletrd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to y < \sum_{i \in S} f (i)$
213	170 174	ltnled	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to (y < \sum_{i \in S} f (i) \leftrightarrow \neg \sum_{i \in S} f (i) \leq y)$
214	212 213	mpbid	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to \neg \sum_{i \in S} f (i) \leq y$
215	169 214	pm2.21dd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \land y < f (s)) \to \neg y < f (s)$
216	215	pm2.01da	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to \neg y < f (s)$
217	177 101	syl	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to y \in ℝ$
218	171 217	lenltd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to (f (s) \leq y \leftrightarrow \neg y < f (s))$
219	216 218	mpbird	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) \leq y$
220	163 165 167 168 219	elfzd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \land s \in S) \to f (s) \in (0 \dots y)$
221	220	ralrimiva	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \forall s \in S f (s) \in (0 \dots y)$
222	162 221	jca	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to (f Fn S \land \forall s \in S f (s) \in (0 \dots y))$
223		ffnfv	$⊢ f : S ⟶ (0 \dots y) \leftrightarrow (f Fn S \land \forall s \in S f (s) \in (0 \dots y))$
224	222 223	sylibr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to f : S ⟶ (0 \dots y)$
225	224	ex	$⊢ (φ \land y \in ℕ_{0}) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \to f : S ⟶ (0 \dots y))$
226	225	ss2abdv	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \subseteq \{f \| f : S ⟶ (0 \dots y)\}$
227	160 226	ssfid	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \in Fin$
228	227	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \in Fin$
229		fzfid	$⊢ (φ \land y \in ℕ_{0}) \to (0 \dots y + 1) \in Fin$
230	151 229	jca	$⊢ (φ \land y \in ℕ_{0}) \to (S \in Fin \land (0 \dots y + 1) \in Fin)$
231		xpfi	$⊢ (S \in Fin \land (0 \dots y + 1) \in Fin) \to S \times (0 \dots y + 1) \in Fin$
232	230 231	syl	$⊢ (φ \land y \in ℕ_{0}) \to S \times (0 \dots y + 1) \in Fin$
233		pwfi	$⊢ S \times (0 \dots y + 1) \in Fin \leftrightarrow 𝒫 (S \times (0 \dots y + 1)) \in Fin$
234	232 233	sylib	$⊢ (φ \land y \in ℕ_{0}) \to 𝒫 (S \times (0 \dots y + 1)) \in Fin$
235		fsetsspwxp	$⊢ \{f \| f : S ⟶ (0 \dots y + 1)\} \subseteq 𝒫 (S \times (0 \dots y + 1))$
236	235	a1i	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| f : S ⟶ (0 \dots y + 1)\} \subseteq 𝒫 (S \times (0 \dots y + 1))$
237	234 236	ssfid	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| f : S ⟶ (0 \dots y + 1)\} \in Fin$
238	161	ad2antrl	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to f Fn S$
239		0zd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to 0 \in ℤ$
240		simpllr	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to y \in ℕ_{0}$
241	240	nn0zd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to y \in ℤ$
242	241	peano2zd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to y + 1 \in ℤ$
243	133	ffvelrnda	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to f (s) \in ℕ_{0}$
244	243	nn0zd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to f (s) \in ℤ$
245	243	nn0ge0d	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to 0 \leq f (s)$
246	134	ad2antrr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to \sum_{i \in S} f (i) = y + 1$
247	137	ad2antrr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to y + 1 \in ℝ$
248	133	ad2antrr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to f : S ⟶ ℕ_{0}$
249		simplr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to s \in S$
250	248 249	ffvelrnd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to f (s) \in ℕ_{0}$
251	250	nn0red	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to f (s) \in ℝ$
252	246 247	eqeltrd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to \sum_{i \in S} f (i) \in ℝ$
253		simpr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to y + 1 < f (s)$
254	133 188	syldan	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℕ_{0}$
255	254	adantr	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℕ_{0}$
256	255	adantr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℕ_{0}$
257	256	nn0ge0d	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to 0 \leq \sum_{i \in S ∖ \{s\}} f (i)$
258	256	nn0red	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to \sum_{i \in S ∖ \{s\}} f (i) \in ℝ$
259	251 258	addge01d	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to (0 \leq \sum_{i \in S ∖ \{s\}} f (i) \leftrightarrow f (s) \leq f (s) + \sum_{i \in S ∖ \{s\}} f (i))$
260	257 259	mpbid	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to f (s) \leq f (s) + \sum_{i \in S ∖ \{s\}} f (i)$
261	133 207	syldanl	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to \sum_{i \in S} f (i) = f (s) + \sum_{i \in S ∖ \{s\}} f (i)$
262	261	adantr	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to \sum_{i \in S} f (i) = f (s) + \sum_{i \in S ∖ \{s\}} f (i)$
263	262	eqcomd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to f (s) + \sum_{i \in S ∖ \{s\}} f (i) = \sum_{i \in S} f (i)$
264	260 263	breqtrd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to f (s) \leq \sum_{i \in S} f (i)$
265	247 251 252 253 264	ltletrd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to y + 1 < \sum_{i \in S} f (i)$
266	247 265	ltned	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to y + 1 \neq \sum_{i \in S} f (i)$
267	266	necomd	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to \sum_{i \in S} f (i) \neq y + 1$
268	246 267	pm2.21ddne	$⊢ ((((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \land y + 1 < f (s)) \to \neg y + 1 < f (s)$
269	268	pm2.01da	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to \neg y + 1 < f (s)$
270	243	nn0red	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to f (s) \in ℝ$
271	137	adantr	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to y + 1 \in ℝ$
272	270 271	lenltd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to (f (s) \leq y + 1 \leftrightarrow \neg y + 1 < f (s))$
273	269 272	mpbird	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to f (s) \leq y + 1$
274	239 242 244 245 273	elfzd	$⊢ (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \land s \in S) \to f (s) \in (0 \dots y + 1)$
275	274	ralrimiva	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to \forall s \in S f (s) \in (0 \dots y + 1)$
276	238 275	jca	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to (f Fn S \land \forall s \in S f (s) \in (0 \dots y + 1))$
277		ffnfv	$⊢ f : S ⟶ (0 \dots y + 1) \leftrightarrow (f Fn S \land \forall s \in S f (s) \in (0 \dots y + 1))$
278	276 277	sylibr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)) \to f : S ⟶ (0 \dots y + 1)$
279	278	ex	$⊢ (φ \land y \in ℕ_{0}) \to ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1) \to f : S ⟶ (0 \dots y + 1))$
280	279	ss2abdv	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} \subseteq \{f \| f : S ⟶ (0 \dots y + 1)\}$
281	237 280	ssfid	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} \in Fin$
282	281	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} \in Fin$
283		inab	$⊢ \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cap \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\}$
284	283	a1i	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cap \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\}$
285	98	adantrr	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \in ℕ_{0}$
286	285	nn0zd	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \in ℤ$
287	286	zred	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \in ℝ$
288	125	ltp1d	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to y < y + 1$
289	287 125 127 128 288	lelttrd	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) < y + 1$
290	287 289	ltned	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \sum_{i \in S} f (i) \neq y + 1$
291	290	neneqd	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \neg \sum_{i \in S} f (i) = y + 1$
292	291	intnand	$⊢ ((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \neg (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)$
293		nan	$⊢ ((φ \land y \in ℕ_{0}) \to \neg ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))) \leftrightarrow (((φ \land y \in ℕ_{0}) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)) \to \neg (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))$
294	292 293	mpbir	$⊢ (φ \land y \in ℕ_{0}) \to \neg ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))$
295	294	alrimiv	$⊢ (φ \land y \in ℕ_{0}) \to \forall f \neg ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))$
296		ab0	$⊢ \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\} = \emptyset \leftrightarrow \forall f \neg ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))$
297	295 296	sylibr	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| ((f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y) \land (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1))\} = \emptyset$
298	284 297	eqtrd	$⊢ (φ \land y \in ℕ_{0}) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cap \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \emptyset$
299	298	adantr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cap \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \emptyset$
300		hashun	$⊢ (\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \in Fin \land \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} \in Fin \land \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cap \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \emptyset) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| + \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\|$
301	228 282 299 300	syl3anc	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\| = \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| + \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\|$
302		simpr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})$
303		simplr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to y \in ℕ_{0}$
304		1nn0	$⊢ 1 \in ℕ_{0}$
305	304	a1i	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to 1 \in ℕ_{0}$
306	303 305	nn0addcld	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to y + 1 \in ℕ_{0}$
307	2	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to S \in Fin$
308	3	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to S \neq \emptyset$
309		eqid	$⊢ \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\} = \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}$
310	306 307 308 309	sticksstones21	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\| = (\binom{y + 1 + (\|S\| - 1)}{\|S\| - 1})$
311	302 310	oveq12d	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| + \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\| = (\binom{y + \|S\|}{\|S\|}) + (\binom{y + 1 + (\|S\| - 1)}{\|S\| - 1})$
312	303	nn0cnd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to y \in ℂ$
313		1cnd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to 1 \in ℂ$
314	71	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|S\| \in ℂ$
315	312 313 314	ppncand	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to y + 1 + (\|S\| - 1) = y + \|S\|$
316	315	oveq1d	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to (\binom{y + 1 + (\|S\| - 1)}{\|S\| - 1}) = (\binom{y + \|S\|}{\|S\| - 1})$
317	316	oveq2d	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to (\binom{y + \|S\|}{\|S\|}) + (\binom{y + 1 + (\|S\| - 1)}{\|S\| - 1}) = (\binom{y + \|S\|}{\|S\|}) + (\binom{y + \|S\|}{\|S\| - 1})$
318	82	ad2antrr	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|S\| \in ℕ_{0}$
319	303 318	nn0addcld	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to y + \|S\| \in ℕ_{0}$
320	318	nn0zd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|S\| \in ℤ$
321		bcpasc	$⊢ (y + \|S\| \in ℕ_{0} \land \|S\| \in ℤ) \to (\binom{y + \|S\|}{\|S\|}) + (\binom{y + \|S\|}{\|S\| - 1}) = (\binom{y + \|S\| + 1}{\|S\|})$
322	319 320 321	syl2anc	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to (\binom{y + \|S\|}{\|S\|}) + (\binom{y + \|S\|}{\|S\| - 1}) = (\binom{y + \|S\| + 1}{\|S\|})$
323	317 322	eqtrd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to (\binom{y + \|S\|}{\|S\|}) + (\binom{y + 1 + (\|S\| - 1)}{\|S\| - 1}) = (\binom{y + \|S\| + 1}{\|S\|})$
324	312 314 313	add32d	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to y + \|S\| + 1 = y + 1 + \|S\|$
325	324	oveq1d	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to (\binom{y + \|S\| + 1}{\|S\|}) = (\binom{y + 1 + \|S\|}{\|S\|})$
326	323 325	eqtrd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to (\binom{y + \|S\|}{\|S\|}) + (\binom{y + 1 + (\|S\| - 1)}{\|S\| - 1}) = (\binom{y + 1 + \|S\|}{\|S\|})$
327	311 326	eqtrd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| + \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\| = (\binom{y + 1 + \|S\|}{\|S\|})$
328	301 327	eqtrd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\} \cup \{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) = y + 1)\}\| = (\binom{y + 1 + \|S\|}{\|S\|})$
329	150 328	eqtrd	$⊢ ((φ \land y \in ℕ_{0}) \land \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y)\}\| = (\binom{y + \|S\|}{\|S\|})) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq y + 1)\}\| = (\binom{y + 1 + \|S\|}{\|S\|})$
330	13 20 27 34 92 329	nn0indd	$⊢ (φ \land N \in ℕ_{0}) \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}\| = (\binom{N + \|S\|}{\|S\|})$
331	1 330	mpdan	$⊢ φ \to \|\{f \| (f : S ⟶ ℕ_{0} \land \sum_{i \in S} f (i) \leq N)\}\| = (\binom{N + \|S\|}{\|S\|})$
332	6 331	eqtrd	$⊢ φ \to \|A\| = (\binom{N + \|S\|}{\|S\|})$

Metamath Proof Explorer

Theorem sticksstones22

Proof