sticksstones10

Description: Establish mapping between strictly monotone functions and functions that sum to a fixed non-negative integer. (Contributed by metakunt, 6-Oct-2024)

	Ref	Expression
Hypotheses	sticksstones10.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones10.2	$⊢ φ \to K \in ℕ$
	sticksstones10.3	$⊢ G = (b \in B ⟼ if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))))$
	sticksstones10.4	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
	sticksstones10.5	$⊢ B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
Assertion	sticksstones10	$⊢ φ \to G : B ⟶ A$

Proof

Step	Hyp	Ref	Expression
1		sticksstones10.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones10.2	$⊢ φ \to K \in ℕ$
3		sticksstones10.3	$⊢ G = (b \in B ⟼ if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))))$
4		sticksstones10.4	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
5		sticksstones10.5	$⊢ B = \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
6	2	nnne0d	$⊢ φ \to K \neq 0$
7	6	adantr	$⊢ (φ \land b \in B) \to K \neq 0$
8	7	neneqd	$⊢ (φ \land b \in B) \to \neg K = 0$
9	8	iffalsed	$⊢ (φ \land b \in B) \to if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))) = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))$
10	9	eqcomd	$⊢ (φ \land b \in B) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) = if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))))$
11		eleq1	$⊢ N + K - b (K) = if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) \to (N + K - b (K) \in ℕ_{0} \leftrightarrow if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) \in ℕ_{0})$
12		eleq1	$⊢ if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) = if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) \to (if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) \in ℕ_{0} \leftrightarrow if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) \in ℕ_{0})$
13	1	nn0zd	$⊢ φ \to N \in ℤ$
14	13	adantr	$⊢ (φ \land b \in B) \to N \in ℤ$
15	2	nnzd	$⊢ φ \to K \in ℤ$
16	15	adantr	$⊢ (φ \land b \in B) \to K \in ℤ$
17	14 16	zaddcld	$⊢ (φ \land b \in B) \to N + K \in ℤ$
18	5	eleq2i	$⊢ b \in B \leftrightarrow b \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\}$
19		vex	$⊢ b \in V$
20		feq1	$⊢ f = b \to (f : (1 \dots K) ⟶ (1 \dots N + K) \leftrightarrow b : (1 \dots K) ⟶ (1 \dots N + K))$
21		fveq1	$⊢ f = b \to f (x) = b (x)$
22		fveq1	$⊢ f = b \to f (y) = b (y)$
23	21 22	breq12d	$⊢ f = b \to (f (x) < f (y) \leftrightarrow b (x) < b (y))$
24	23	imbi2d	$⊢ f = b \to ((x < y \to f (x) < f (y)) \leftrightarrow (x < y \to b (x) < b (y)))$
25	24	2ralbidv	$⊢ f = b \to (\forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)) \leftrightarrow \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y)))$
26	20 25	anbi12d	$⊢ f = b \to ((f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y))) \leftrightarrow (b : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y))))$
27	19 26	elab	$⊢ b \in \{f \| (f : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to f (x) < f (y)))\} \leftrightarrow (b : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y)))$
28	18 27	bitri	$⊢ b \in B \leftrightarrow (b : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y)))$
29	28	bilani	$⊢ (φ \land b \in B) \to (b : (1 \dots K) ⟶ (1 \dots N + K) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y)))$
30	29	simpld	$⊢ (φ \land b \in B) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
31		1zzd	$⊢ (φ \land b \in B) \to 1 \in ℤ$
32	2	nnge1d	$⊢ φ \to 1 \leq K$
33	32	adantr	$⊢ (φ \land b \in B) \to 1 \leq K$
34	16	zred	$⊢ (φ \land b \in B) \to K \in ℝ$
35	34	leidd	$⊢ (φ \land b \in B) \to K \leq K$
36	31 16 16 33 35	elfzd	$⊢ (φ \land b \in B) \to K \in (1 \dots K)$
37	30 36	ffvelcdmd	$⊢ (φ \land b \in B) \to b (K) \in (1 \dots N + K)$
38		elfznn	$⊢ b (K) \in (1 \dots N + K) \to b (K) \in ℕ$
39	37 38	syl	$⊢ (φ \land b \in B) \to b (K) \in ℕ$
40	39	nnzd	$⊢ (φ \land b \in B) \to b (K) \in ℤ$
41	17 40	zsubcld	$⊢ (φ \land b \in B) \to N + K - b (K) \in ℤ$
42	39	nnred	$⊢ (φ \land b \in B) \to b (K) \in ℝ$
43	42	recnd	$⊢ (φ \land b \in B) \to b (K) \in ℂ$
44	43	addridd	$⊢ (φ \land b \in B) \to b (K) + 0 = b (K)$
45		elfzle2	$⊢ b (K) \in (1 \dots N + K) \to b (K) \leq N + K$
46	37 45	syl	$⊢ (φ \land b \in B) \to b (K) \leq N + K$
47	44 46	eqbrtrd	$⊢ (φ \land b \in B) \to b (K) + 0 \leq N + K$
48		0red	$⊢ (φ \land b \in B) \to 0 \in ℝ$
49	17	zred	$⊢ (φ \land b \in B) \to N + K \in ℝ$
50	42 48 49	leaddsub2d	$⊢ (φ \land b \in B) \to (b (K) + 0 \leq N + K \leftrightarrow 0 \leq N + K - b (K))$
51	47 50	mpbid	$⊢ (φ \land b \in B) \to 0 \leq N + K - b (K)$
52	41 51	jca	$⊢ (φ \land b \in B) \to (N + K - b (K) \in ℤ \land 0 \leq N + K - b (K))$
53		elnn0z	$⊢ N + K - b (K) \in ℕ_{0} \leftrightarrow (N + K - b (K) \in ℤ \land 0 \leq N + K - b (K))$
54	52 53	sylibr	$⊢ (φ \land b \in B) \to N + K - b (K) \in ℕ_{0}$
55	54	adantr	$⊢ ((φ \land b \in B) \land k \in (1 \dots K + 1)) \to N + K - b (K) \in ℕ_{0}$
56	55	3impa	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to N + K - b (K) \in ℕ_{0}$
57	56	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land k = K + 1) \to N + K - b (K) \in ℕ_{0}$
58		eleq1	$⊢ b (1) - 1 = if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) \to (b (1) - 1 \in ℕ_{0} \leftrightarrow if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) \in ℕ_{0})$
59		eleq1	$⊢ b (k) - b (k - 1) - 1 = if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) \to (b (k) - b (k - 1) - 1 \in ℕ_{0} \leftrightarrow if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) \in ℕ_{0})$
60		1red	$⊢ (φ \land b \in B) \to 1 \in ℝ$
61	60	leidd	$⊢ (φ \land b \in B) \to 1 \leq 1$
62	31 16 31 61 33	elfzd	$⊢ (φ \land b \in B) \to 1 \in (1 \dots K)$
63	30 62	ffvelcdmd	$⊢ (φ \land b \in B) \to b (1) \in (1 \dots N + K)$
64		elfznn	$⊢ b (1) \in (1 \dots N + K) \to b (1) \in ℕ$
65	64	nnzd	$⊢ b (1) \in (1 \dots N + K) \to b (1) \in ℤ$
66	63 65	syl	$⊢ (φ \land b \in B) \to b (1) \in ℤ$
67	66 31	zsubcld	$⊢ (φ \land b \in B) \to b (1) - 1 \in ℤ$
68		1cnd	$⊢ (φ \land b \in B) \to 1 \in ℂ$
69	68	addridd	$⊢ (φ \land b \in B) \to 1 + 0 = 1$
70		elfzle1	$⊢ b (1) \in (1 \dots N + K) \to 1 \leq b (1)$
71	63 70	syl	$⊢ (φ \land b \in B) \to 1 \leq b (1)$
72	69 71	eqbrtrd	$⊢ (φ \land b \in B) \to 1 + 0 \leq b (1)$
73	66	zred	$⊢ (φ \land b \in B) \to b (1) \in ℝ$
74	60 48 73	leaddsub2d	$⊢ (φ \land b \in B) \to (1 + 0 \leq b (1) \leftrightarrow 0 \leq b (1) - 1)$
75	72 74	mpbid	$⊢ (φ \land b \in B) \to 0 \leq b (1) - 1$
76	67 75	jca	$⊢ (φ \land b \in B) \to (b (1) - 1 \in ℤ \land 0 \leq b (1) - 1)$
77		elnn0z	$⊢ b (1) - 1 \in ℕ_{0} \leftrightarrow (b (1) - 1 \in ℤ \land 0 \leq b (1) - 1)$
78	76 77	sylibr	$⊢ (φ \land b \in B) \to b (1) - 1 \in ℕ_{0}$
79	78	adantr	$⊢ ((φ \land b \in B) \land k \in (1 \dots K + 1)) \to b (1) - 1 \in ℕ_{0}$
80	79	3impa	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to b (1) - 1 \in ℕ_{0}$
81	80	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to b (1) - 1 \in ℕ_{0}$
82	81	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land k = 1) \to b (1) - 1 \in ℕ_{0}$
83	30	3adant3	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
84	83	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
85		1zzd	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to 1 \in ℤ$
86	16	3adant3	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to K \in ℤ$
87	86	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K \in ℤ$
88		simp3	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to k \in (1 \dots K + 1)$
89		elfznn	$⊢ k \in (1 \dots K + 1) \to k \in ℕ$
90	88 89	syl	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to k \in ℕ$
91	90	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℕ$
92	91	nnzd	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℤ$
93	91	nnge1d	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to 1 \leq k$
94		elfzle2	$⊢ k \in (1 \dots K + 1) \to k \leq K + 1$
95	88 94	syl	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to k \leq K + 1$
96	95	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \leq K + 1$
97		neqne	$⊢ \neg k = K + 1 \to k \neq K + 1$
98	97	adantl	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \neq K + 1$
99	98	necomd	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \neq k$
100	96 99	jca	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (k \leq K + 1 \land K + 1 \neq k)$
101	91	nnred	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℝ$
102	87	zred	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K \in ℝ$
103		1red	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to 1 \in ℝ$
104	102 103	readdcld	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \in ℝ$
105	101 104	ltlend	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (k < K + 1 \leftrightarrow (k \leq K + 1 \land K + 1 \neq k))$
106	100 105	mpbird	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k < K + 1$
107	90	nnzd	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to k \in ℤ$
108		zleltp1	$⊢ (k \in ℤ \land K \in ℤ) \to (k \leq K \leftrightarrow k < K + 1)$
109	107 86 108	syl2anc	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to (k \leq K \leftrightarrow k < K + 1)$
110	109	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (k \leq K \leftrightarrow k < K + 1)$
111	106 110	mpbird	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \leq K$
112	85 87 92 93 111	elfzd	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in (1 \dots K)$
113	84 112	ffvelcdmd	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to b (k) \in (1 \dots N + K)$
114		elfznn	$⊢ b (k) \in (1 \dots N + K) \to b (k) \in ℕ$
115	113 114	syl	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to b (k) \in ℕ$
116	115	nnzd	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to b (k) \in ℤ$
117	116	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k) \in ℤ$
118	84	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
119		1zzd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \in ℤ$
120	87	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to K \in ℤ$
121	92	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in ℤ$
122	121 119	zsubcld	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - 1 \in ℤ$
123	93	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \leq k$
124		neqne	$⊢ \neg k = 1 \to k \neq 1$
125	124	adantl	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \neq 1$
126	123 125	jca	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (1 \leq k \land k \neq 1)$
127	103	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \in ℝ$
128	101	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in ℝ$
129	127 128	ltlend	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (1 < k \leftrightarrow (1 \leq k \land k \neq 1))$
130	126 129	mpbird	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 < k$
131	119 121	zltlem1d	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (1 < k \leftrightarrow 1 \leq k - 1)$
132	130 131	mpbid	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \leq k - 1$
133	90	nnred	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to k \in ℝ$
134	60	3adant3	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to 1 \in ℝ$
135	34	3adant3	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to K \in ℝ$
136		lesubadd	$⊢ (k \in ℝ \land 1 \in ℝ \land K \in ℝ) \to (k - 1 \leq K \leftrightarrow k \leq K + 1)$
137	133 134 135 136	syl3anc	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to (k - 1 \leq K \leftrightarrow k \leq K + 1)$
138	95 137	mpbird	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to k - 1 \leq K$
139	138	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k - 1 \leq K$
140	139	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - 1 \leq K$
141	119 120 122 132 140	elfzd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
142	118 141	ffvelcdmd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) \in (1 \dots N + K)$
143		elfznn	$⊢ b (k - 1) \in (1 \dots N + K) \to b (k - 1) \in ℕ$
144	142 143	syl	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) \in ℕ$
145	144	nnzd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) \in ℤ$
146	117 145	zsubcld	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k) - b (k - 1) \in ℤ$
147	146 119	zsubcld	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k) - b (k - 1) - 1 \in ℤ$
148		0p1e1	$⊢ 0 + 1 = 1$
149	148	a1i	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 0 + 1 = 1$
150		1cnd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \in ℂ$
151	150	subidd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 - 1 = 0$
152	145	zred	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) \in ℝ$
153	152	recnd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) \in ℂ$
154	153	addridd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) + 0 = b (k - 1)$
155	128	ltm1d	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - 1 < k$
156	112	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in (1 \dots K)$
157	141 156	jca	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (k - 1 \in (1 \dots K) \land k \in (1 \dots K))$
158	29	simprd	$⊢ (φ \land b \in B) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y))$
159	158	3adant3	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y))$
160	159	adantr	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y))$
161	160	adantr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y))$
162		breq1	$⊢ x = k - 1 \to (x < y \leftrightarrow k - 1 < y)$
163		fveq2	$⊢ x = k - 1 \to b (x) = b (k - 1)$
164	163	breq1d	$⊢ x = k - 1 \to (b (x) < b (y) \leftrightarrow b (k - 1) < b (y))$
165	162 164	imbi12d	$⊢ x = k - 1 \to ((x < y \to b (x) < b (y)) \leftrightarrow (k - 1 < y \to b (k - 1) < b (y)))$
166		breq2	$⊢ y = k \to (k - 1 < y \leftrightarrow k - 1 < k)$
167		fveq2	$⊢ y = k \to b (y) = b (k)$
168	167	breq2d	$⊢ y = k \to (b (k - 1) < b (y) \leftrightarrow b (k - 1) < b (k))$
169	166 168	imbi12d	$⊢ y = k \to ((k - 1 < y \to b (k - 1) < b (y)) \leftrightarrow (k - 1 < k \to b (k - 1) < b (k)))$
170	165 169	rspc2va	$⊢ ((k - 1 \in (1 \dots K) \land k \in (1 \dots K)) \land \forall x \in (1 \dots K) \forall y \in (1 \dots K) (x < y \to b (x) < b (y))) \to (k - 1 < k \to b (k - 1) < b (k))$
171	157 161 170	syl2anc	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (k - 1 < k \to b (k - 1) < b (k))$
172	155 171	mpd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) < b (k)$
173	154 172	eqbrtrd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k - 1) + 0 < b (k)$
174		0red	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 0 \in ℝ$
175	117	zred	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k) \in ℝ$
176	152 174 175	ltaddsub2d	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (b (k - 1) + 0 < b (k) \leftrightarrow 0 < b (k) - b (k - 1))$
177	173 176	mpbid	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 0 < b (k) - b (k - 1)$
178	151 177	eqbrtrd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 - 1 < b (k) - b (k - 1)$
179		zlem1lt	$⊢ (1 \in ℤ \land b (k) - b (k - 1) \in ℤ) \to (1 \leq b (k) - b (k - 1) \leftrightarrow 1 - 1 < b (k) - b (k - 1))$
180	119 146 179	syl2anc	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (1 \leq b (k) - b (k - 1) \leftrightarrow 1 - 1 < b (k) - b (k - 1))$
181	178 180	mpbird	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \leq b (k) - b (k - 1)$
182	149 181	eqbrtrd	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 0 + 1 \leq b (k) - b (k - 1)$
183	146	zred	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k) - b (k - 1) \in ℝ$
184		leaddsub	$⊢ (0 \in ℝ \land 1 \in ℝ \land b (k) - b (k - 1) \in ℝ) \to (0 + 1 \leq b (k) - b (k - 1) \leftrightarrow 0 \leq b (k) - b (k - 1) - 1)$
185	174 127 183 184	syl3anc	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (0 + 1 \leq b (k) - b (k - 1) \leftrightarrow 0 \leq b (k) - b (k - 1) - 1)$
186	182 185	mpbid	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 0 \leq b (k) - b (k - 1) - 1$
187	147 186	jca	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (b (k) - b (k - 1) - 1 \in ℤ \land 0 \leq b (k) - b (k - 1) - 1)$
188		elnn0z	$⊢ b (k) - b (k - 1) - 1 \in ℕ_{0} \leftrightarrow (b (k) - b (k - 1) - 1 \in ℤ \land 0 \leq b (k) - b (k - 1) - 1)$
189	187 188	sylibr	$⊢ (((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to b (k) - b (k - 1) - 1 \in ℕ_{0}$
190	58 59 82 189	ifbothda	$⊢ ((φ \land b \in B \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) \in ℕ_{0}$
191	11 12 57 190	ifbothda	$⊢ (φ \land b \in B \land k \in (1 \dots K + 1)) \to if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) \in ℕ_{0}$
192	191	3expa	$⊢ ((φ \land b \in B) \land k \in (1 \dots K + 1)) \to if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) \in ℕ_{0}$
193	192	fmpttd	$⊢ (φ \land b \in B) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) : (1 \dots K + 1) ⟶ ℕ_{0}$
194		eqidd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))$
195		simpr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to k = i$
196	195	eqeq1d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to (k = K + 1 \leftrightarrow i = K + 1)$
197	195	eqeq1d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to (k = 1 \leftrightarrow i = 1)$
198	195	fveq2d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to b (k) = b (i)$
199	195	fvoveq1d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to b (k - 1) = b (i - 1)$
200	198 199	oveq12d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to b (k) - b (k - 1) = b (i) - b (i - 1)$
201	200	oveq1d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to b (k) - b (k - 1) - 1 = b (i) - b (i - 1) - 1$
202	197 201	ifbieq2d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) = if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)$
203	196 202	ifbieq2d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K + 1)) \land k = i) \to if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) = if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1))$
204		simpr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to i \in (1 \dots K + 1)$
205		ovexd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to N + K - b (K) \in V$
206		ovexd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to b (1) - 1 \in V$
207		ovexd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to b (i) - b (i - 1) - 1 \in V$
208	206 207	ifcld	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \in V$
209	205 208	ifcld	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \in V$
210	194 203 204 209	fvmptd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i) = if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1))$
211	210	sumeq2dv	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K + 1} (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i) = \sum_{i = 1}^{K + 1} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1))$
212	2	adantr	$⊢ (φ \land b \in B) \to K \in ℕ$
213		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
214	212 213	eleqtrdi	$⊢ (φ \land b \in B) \to K \in ℤ_{\geq 1}$
215		eleq1	$⊢ N + K - b (K) = if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \to (N + K - b (K) \in ℤ \leftrightarrow if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \in ℤ)$
216		eleq1	$⊢ if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) = if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \to (if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \in ℤ \leftrightarrow if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \in ℤ)$
217	14	3adant3	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to N \in ℤ$
218	217	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land i = K + 1) \to N \in ℤ$
219	16	3adant3	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to K \in ℤ$
220	219	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land i = K + 1) \to K \in ℤ$
221	218 220	zaddcld	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land i = K + 1) \to N + K \in ℤ$
222	39	3adant3	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to b (K) \in ℕ$
223	222	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land i = K + 1) \to b (K) \in ℕ$
224	223	nnzd	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land i = K + 1) \to b (K) \in ℤ$
225	221 224	zsubcld	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land i = K + 1) \to N + K - b (K) \in ℤ$
226		eleq1	$⊢ b (1) - 1 = if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \to (b (1) - 1 \in ℤ \leftrightarrow if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \in ℤ)$
227		eleq1	$⊢ b (i) - b (i - 1) - 1 = if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \to (b (i) - b (i - 1) - 1 \in ℤ \leftrightarrow if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \in ℤ)$
228	66	3adant3	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to b (1) \in ℤ$
229	228	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to b (1) \in ℤ$
230	229	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land i = 1) \to b (1) \in ℤ$
231		1zzd	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land i = 1) \to 1 \in ℤ$
232	230 231	zsubcld	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land i = 1) \to b (1) - 1 \in ℤ$
233	30	3adant3	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
234	233	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
235	234	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
236		1zzd	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to 1 \in ℤ$
237	219	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to K \in ℤ$
238		elfznn	$⊢ i \in (1 \dots K + 1) \to i \in ℕ$
239	238	adantl	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to i \in ℕ$
240	239	3impa	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to i \in ℕ$
241	240	nnzd	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to i \in ℤ$
242	241	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to i \in ℤ$
243	240	nnge1d	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to 1 \leq i$
244	243	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to 1 \leq i$
245		simp3	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to i \in (1 \dots K + 1)$
246		elfzle2	$⊢ i \in (1 \dots K + 1) \to i \leq K + 1$
247	245 246	syl	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to i \leq K + 1$
248	247	adantr	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to i \leq K + 1$
249		neqne	$⊢ \neg i = K + 1 \to i \neq K + 1$
250	249	adantl	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to i \neq K + 1$
251	250	necomd	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to K + 1 \neq i$
252	248 251	jca	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to (i \leq K + 1 \land K + 1 \neq i)$
253	242	zred	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to i \in ℝ$
254	237	zred	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to K \in ℝ$
255		1red	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to 1 \in ℝ$
256	254 255	readdcld	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to K + 1 \in ℝ$
257	253 256	ltlend	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to (i < K + 1 \leftrightarrow (i \leq K + 1 \land K + 1 \neq i))$
258	252 257	mpbird	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to i < K + 1$
259		zleltp1	$⊢ (i \in ℤ \land K \in ℤ) \to (i \leq K \leftrightarrow i < K + 1)$
260	242 237 259	syl2anc	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to (i \leq K \leftrightarrow i < K + 1)$
261	258 260	mpbird	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to i \leq K$
262	236 237 242 244 261	elfzd	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to i \in (1 \dots K)$
263	262	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i \in (1 \dots K)$
264	235 263	ffvelcdmd	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i) \in (1 \dots N + K)$
265		elfznn	$⊢ b (i) \in (1 \dots N + K) \to b (i) \in ℕ$
266	264 265	syl	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i) \in ℕ$
267	266	nnzd	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i) \in ℤ$
268		1zzd	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to 1 \in ℤ$
269	237	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to K \in ℤ$
270	242	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i \in ℤ$
271	270 268	zsubcld	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i - 1 \in ℤ$
272	244	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to 1 \leq i$
273		neqne	$⊢ \neg i = 1 \to i \neq 1$
274	273	adantl	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i \neq 1$
275	272 274	jca	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to (1 \leq i \land i \neq 1)$
276		1red	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to 1 \in ℝ$
277	270	zred	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i \in ℝ$
278	276 277	ltlend	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to (1 < i \leftrightarrow (1 \leq i \land i \neq 1))$
279	275 278	mpbird	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to 1 < i$
280		zltp1le	$⊢ (1 \in ℤ \land i \in ℤ) \to (1 < i \leftrightarrow 1 + 1 \leq i)$
281	268 270 280	syl2anc	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to (1 < i \leftrightarrow 1 + 1 \leq i)$
282	279 281	mpbid	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to 1 + 1 \leq i$
283		leaddsub	$⊢ (1 \in ℝ \land 1 \in ℝ \land i \in ℝ) \to (1 + 1 \leq i \leftrightarrow 1 \leq i - 1)$
284	276 276 277 283	syl3anc	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to (1 + 1 \leq i \leftrightarrow 1 \leq i - 1)$
285	282 284	mpbid	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to 1 \leq i - 1$
286	248	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i \leq K + 1$
287	254	adantr	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to K \in ℝ$
288		lesubadd	$⊢ (i \in ℝ \land 1 \in ℝ \land K \in ℝ) \to (i - 1 \leq K \leftrightarrow i \leq K + 1)$
289	277 276 287 288	syl3anc	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to (i - 1 \leq K \leftrightarrow i \leq K + 1)$
290	286 289	mpbird	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i - 1 \leq K$
291	268 269 271 285 290	elfzd	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to i - 1 \in (1 \dots K)$
292	235 291	ffvelcdmd	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i - 1) \in (1 \dots N + K)$
293		elfznn	$⊢ b (i - 1) \in (1 \dots N + K) \to b (i - 1) \in ℕ$
294	292 293	syl	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i - 1) \in ℕ$
295	294	nnzd	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i - 1) \in ℤ$
296	267 295	zsubcld	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i) - b (i - 1) \in ℤ$
297	296 268	zsubcld	$⊢ (((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \land \neg i = 1) \to b (i) - b (i - 1) - 1 \in ℤ$
298	226 227 232 297	ifbothda	$⊢ ((φ \land b \in B \land i \in (1 \dots K + 1)) \land \neg i = K + 1) \to if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \in ℤ$
299	215 216 225 298	ifbothda	$⊢ (φ \land b \in B \land i \in (1 \dots K + 1)) \to if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \in ℤ$
300	299	3expa	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \in ℤ$
301	300	zcnd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K + 1)) \to if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) \in ℂ$
302		eqeq1	$⊢ i = K + 1 \to (i = K + 1 \leftrightarrow K + 1 = K + 1)$
303		eqeq1	$⊢ i = K + 1 \to (i = 1 \leftrightarrow K + 1 = 1)$
304		fveq2	$⊢ i = K + 1 \to b (i) = b (K + 1)$
305		fvoveq1	$⊢ i = K + 1 \to b (i - 1) = b (K + 1 - 1)$
306	304 305	oveq12d	$⊢ i = K + 1 \to b (i) - b (i - 1) = b (K + 1) - b (K + 1 - 1)$
307	306	oveq1d	$⊢ i = K + 1 \to b (i) - b (i - 1) - 1 = b (K + 1) - b (K + 1 - 1) - 1$
308	303 307	ifbieq2d	$⊢ i = K + 1 \to if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) = if (K + 1 = 1, b (1) - 1, b (K + 1) - b (K + 1 - 1) - 1)$
309	302 308	ifbieq2d	$⊢ i = K + 1 \to if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) = if (K + 1 = K + 1, N + K - b (K), if (K + 1 = 1, b (1) - 1, b (K + 1) - b (K + 1 - 1) - 1))$
310	214 301 309	fsump1	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K + 1} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) = \sum_{i = 1}^{K} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) + if (K + 1 = K + 1, N + K - b (K), if (K + 1 = 1, b (1) - 1, b (K + 1) - b (K + 1 - 1) - 1))$
311		eqidd	$⊢ (φ \land b \in B) \to K + 1 = K + 1$
312	311	iftrued	$⊢ (φ \land b \in B) \to if (K + 1 = K + 1, N + K - b (K), if (K + 1 = 1, b (1) - 1, b (K + 1) - b (K + 1 - 1) - 1)) = N + K - b (K)$
313	312	oveq2d	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) + if (K + 1 = K + 1, N + K - b (K), if (K + 1 = 1, b (1) - 1, b (K + 1) - b (K + 1 - 1) - 1)) = \sum_{i = 1}^{K} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) + (N + K) - b (K)$
314		elfznn	$⊢ i \in (1 \dots K) \to i \in ℕ$
315	314	adantl	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \in ℕ$
316	315	nnred	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \in ℝ$
317	34	adantr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to K \in ℝ$
318		1red	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to 1 \in ℝ$
319	317 318	readdcld	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to K + 1 \in ℝ$
320		elfzle2	$⊢ i \in (1 \dots K) \to i \leq K$
321	320	adantl	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \leq K$
322	317	ltp1d	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to K < K + 1$
323	316 317 319 321 322	lelttrd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i < K + 1$
324	316 323	ltned	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \neq K + 1$
325	324	neneqd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to \neg i = K + 1$
326	325	iffalsed	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) = if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)$
327	326	sumeq2dv	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) = \sum_{i = 1}^{K} if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)$
328	327	oveq1d	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) + (N + K) - b (K) = \sum_{i = 1}^{K} if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) + (N + K) - b (K)$
329		eqeq1	$⊢ b (1) - 1 = if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \to (b (1) - 1 = if (i = 1, b (1), b (i) - b (i - 1)) - 1 \leftrightarrow if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) = if (i = 1, b (1), b (i) - b (i - 1)) - 1)$
330		eqeq1	$⊢ b (i) - b (i - 1) - 1 = if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) \to (b (i) - b (i - 1) - 1 = if (i = 1, b (1), b (i) - b (i - 1)) - 1 \leftrightarrow if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) = if (i = 1, b (1), b (i) - b (i - 1)) - 1)$
331		eqidd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to b (1) - 1 = b (1) - 1$
332		simpr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to i = 1$
333	332	iftrued	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to if (i = 1, b (1), b (i) - b (i - 1)) = b (1)$
334	333	eqcomd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to b (1) = if (i = 1, b (1), b (i) - b (i - 1))$
335	334	oveq1d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to b (1) - 1 = if (i = 1, b (1), b (i) - b (i - 1)) - 1$
336	331 335	eqtrd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to b (1) - 1 = if (i = 1, b (1), b (i) - b (i - 1)) - 1$
337		eqidd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i) - b (i - 1) - 1 = b (i) - b (i - 1) - 1$
338		simpr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to \neg i = 1$
339	338	iffalsed	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to if (i = 1, b (1), b (i) - b (i - 1)) = b (i) - b (i - 1)$
340	339	oveq1d	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to if (i = 1, b (1), b (i) - b (i - 1)) - 1 = b (i) - b (i - 1) - 1$
341	340	eqcomd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i) - b (i - 1) - 1 = if (i = 1, b (1), b (i) - b (i - 1)) - 1$
342	337 341	eqtrd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i) - b (i - 1) - 1 = if (i = 1, b (1), b (i) - b (i - 1)) - 1$
343	329 330 336 342	ifbothda	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) = if (i = 1, b (1), b (i) - b (i - 1)) - 1$
344	343	sumeq2dv	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) = \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1)$
345	344	oveq1d	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) + (N + K) - b (K) = \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) + (N + K) - b (K)$
346		fzfid	$⊢ (φ \land b \in B) \to (1 \dots K) \in Fin$
347		eleq1	$⊢ b (1) = if (i = 1, b (1), b (i) - b (i - 1)) \to (b (1) \in ℤ \leftrightarrow if (i = 1, b (1), b (i) - b (i - 1)) \in ℤ)$
348		eleq1	$⊢ b (i) - b (i - 1) = if (i = 1, b (1), b (i) - b (i - 1)) \to (b (i) - b (i - 1) \in ℤ \leftrightarrow if (i = 1, b (1), b (i) - b (i - 1)) \in ℤ)$
349	66	ad2antrr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to b (1) \in ℤ$
350	30	adantr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
351		simpr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \in (1 \dots K)$
352	350 351	ffvelcdmd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to b (i) \in (1 \dots N + K)$
353	265	nnzd	$⊢ b (i) \in (1 \dots N + K) \to b (i) \in ℤ$
354	352 353	syl	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to b (i) \in ℤ$
355	354	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i) \in ℤ$
356	350	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
357		1zzd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \in ℤ$
358	16	ad2antrr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to K \in ℤ$
359	315	nnzd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \in ℤ$
360	359	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i \in ℤ$
361	360 357	zsubcld	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i - 1 \in ℤ$
362	315	nnge1d	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to 1 \leq i$
363	362	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \leq i$
364	338 273	syl	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i \neq 1$
365	363 364	jca	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to (1 \leq i \land i \neq 1)$
366	318	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \in ℝ$
367	316	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i \in ℝ$
368	366 367	ltlend	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to (1 < i \leftrightarrow (1 \leq i \land i \neq 1))$
369	365 368	mpbird	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 < i$
370		zltlem1	$⊢ (1 \in ℤ \land i \in ℤ) \to (1 < i \leftrightarrow 1 \leq i - 1)$
371	357 360 370	syl2anc	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to (1 < i \leftrightarrow 1 \leq i - 1)$
372	369 371	mpbid	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \leq i - 1$
373	316 318	resubcld	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i - 1 \in ℝ$
374	316	lem1d	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i - 1 \leq i$
375	373 316 317 374 321	letrd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i - 1 \leq K$
376	375	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i - 1 \leq K$
377	357 358 361 372 376	elfzd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i - 1 \in (1 \dots K)$
378	356 377	ffvelcdmd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i - 1) \in (1 \dots N + K)$
379	378 293	syl	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i - 1) \in ℕ$
380	379	nnzd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i - 1) \in ℤ$
381	355 380	zsubcld	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i) - b (i - 1) \in ℤ$
382	347 348 349 381	ifbothda	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to if (i = 1, b (1), b (i) - b (i - 1)) \in ℤ$
383	382	zcnd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to if (i = 1, b (1), b (i) - b (i - 1)) \in ℂ$
384	68	adantr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to 1 \in ℂ$
385	346 383 384	fsumsub	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = \sum_{i = 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) - \sum_{i = 1}^{K} 1$
386		id	$⊢ i = 1 \to i = 1$
387	386	iftrued	$⊢ i = 1 \to if (i = 1, b (1), b (i) - b (i - 1)) = b (1)$
388	214 383 387	fsum1p	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) = b (1) + \sum_{i = 1 + 1}^{K} if (i = 1, b (1), b (i) - b (i - 1))$
389	60	adantr	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 \in ℝ$
390		elfzle1	$⊢ i \in (1 + 1 \dots K) \to 1 + 1 \leq i$
391	390	adantl	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 + 1 \leq i$
392	31	adantr	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 \in ℤ$
393		elfzelz	$⊢ i \in (1 + 1 \dots K) \to i \in ℤ$
394	393	adantl	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to i \in ℤ$
395	392 394 280	syl2anc	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to (1 < i \leftrightarrow 1 + 1 \leq i)$
396	391 395	mpbird	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 < i$
397	389 396	ltned	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 \neq i$
398	397	necomd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to i \neq 1$
399	398	neneqd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to \neg i = 1$
400	399	iffalsed	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to if (i = 1, b (1), b (i) - b (i - 1)) = b (i) - b (i - 1)$
401	400	sumeq2dv	$⊢ (φ \land b \in B) \to \sum_{i = 1 + 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) = \sum_{i = 1 + 1}^{K} (b (i) - b (i - 1))$
402	401	oveq2d	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) = b (1) + \sum_{i = 1 + 1}^{K} (b (i) - b (i - 1))$
403	34	recnd	$⊢ (φ \land b \in B) \to K \in ℂ$
404	403 68	npcand	$⊢ (φ \land b \in B) \to K - 1 + 1 = K$
405	404	eqcomd	$⊢ (φ \land b \in B) \to K = K - 1 + 1$
406	405	oveq2d	$⊢ (φ \land b \in B) \to (1 + 1 \dots K) = (1 + 1 \dots K - 1 + 1)$
407	406	sumeq1d	$⊢ (φ \land b \in B) \to \sum_{i = 1 + 1}^{K} (b (i) - b (i - 1)) = \sum_{i = 1 + 1}^{K - 1 + 1} (b (i) - b (i - 1))$
408	407	oveq2d	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K} (b (i) - b (i - 1)) = b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i) - b (i - 1))$
409		elfzelz	$⊢ i \in (1 + 1 \dots K - 1 + 1) \to i \in ℤ$
410	409	adantl	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i \in ℤ$
411	410	zcnd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i \in ℂ$
412		1cnd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to 1 \in ℂ$
413	411 412	npcand	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i - 1 + 1 = i$
414	413	eqcomd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i = i - 1 + 1$
415	414	fveq2d	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to b (i) = b (i - 1 + 1)$
416		eqidd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to b (i - 1) = b (i - 1)$
417	415 416	oveq12d	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to b (i) - b (i - 1) = b (i - 1 + 1) - b (i - 1)$
418	417	sumeq2dv	$⊢ (φ \land b \in B) \to \sum_{i = 1 + 1}^{K - 1 + 1} (b (i) - b (i - 1)) = \sum_{i = 1 + 1}^{K - 1 + 1} (b (i - 1 + 1) - b (i - 1))$
419	418	oveq2d	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i) - b (i - 1)) = b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i - 1 + 1) - b (i - 1))$
420	16 31	zsubcld	$⊢ (φ \land b \in B) \to K - 1 \in ℤ$
421	30	adantr	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
422		1zzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \in ℤ$
423	16	adantr	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K \in ℤ$
424		elfznn	$⊢ s \in (1 \dots K - 1) \to s \in ℕ$
425	424	adantl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in ℕ$
426	425	nnzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in ℤ$
427	426	peano2zd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \in ℤ$
428		1red	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \in ℝ$
429	425	nnred	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in ℝ$
430	429 428	readdcld	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \in ℝ$
431	425	nnge1d	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \leq s$
432	429	lep1d	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \leq s + 1$
433	428 429 430 431 432	letrd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \leq s + 1$
434		elfzle2	$⊢ s \in (1 \dots K - 1) \to s \leq K - 1$
435	434	adantl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \leq K - 1$
436	34	adantr	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K \in ℝ$
437		leaddsub	$⊢ (s \in ℝ \land 1 \in ℝ \land K \in ℝ) \to (s + 1 \leq K \leftrightarrow s \leq K - 1)$
438	429 428 436 437	syl3anc	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to (s + 1 \leq K \leftrightarrow s \leq K - 1)$
439	435 438	mpbird	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \leq K$
440	422 423 427 433 439	elfzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \in (1 \dots K)$
441	421 440	ffvelcdmd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) \in (1 \dots N + K)$
442		elfznn	$⊢ b (s + 1) \in (1 \dots N + K) \to b (s + 1) \in ℕ$
443	441 442	syl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) \in ℕ$
444	443	nnzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) \in ℤ$
445	436 428	resubcld	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K - 1 \in ℝ$
446	436	lem1d	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K - 1 \leq K$
447	429 445 436 435 446	letrd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \leq K$
448	422 423 426 431 447	elfzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in (1 \dots K)$
449	421 448	ffvelcdmd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s) \in (1 \dots N + K)$
450		elfznn	$⊢ b (s) \in (1 \dots N + K) \to b (s) \in ℕ$
451	450	nnzd	$⊢ b (s) \in (1 \dots N + K) \to b (s) \in ℤ$
452	449 451	syl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s) \in ℤ$
453	444 452	zsubcld	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) - b (s) \in ℤ$
454	453	zcnd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) - b (s) \in ℂ$
455		fvoveq1	$⊢ s = i - 1 \to b (s + 1) = b (i - 1 + 1)$
456		fveq2	$⊢ s = i - 1 \to b (s) = b (i - 1)$
457	455 456	oveq12d	$⊢ s = i - 1 \to b (s + 1) - b (s) = b (i - 1 + 1) - b (i - 1)$
458	31 31 420 454 457	fsumshft	$⊢ (φ \land b \in B) \to \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = \sum_{i = 1 + 1}^{K - 1 + 1} (b (i - 1 + 1) - b (i - 1))$
459	458	oveq2d	$⊢ (φ \land b \in B) \to b (1) + \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i - 1 + 1) - b (i - 1))$
460	459	eqcomd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i - 1 + 1) - b (i - 1)) = b (1) + \sum_{s = 1}^{K - 1} (b (s + 1) - b (s))$
461		fvoveq1	$⊢ s = i \to b (s + 1) = b (i + 1)$
462		fveq2	$⊢ s = i \to b (s) = b (i)$
463	461 462	oveq12d	$⊢ s = i \to b (s + 1) - b (s) = b (i + 1) - b (i)$
464		nfcv	$⊢ \underline{Ⅎ} i (b (s + 1) - b (s))$
465		nfcv	$⊢ \underline{Ⅎ} s (b (i + 1) - b (i))$
466	463 464 465	cbvsum	$⊢ \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = \sum_{i = 1}^{K - 1} (b (i + 1) - b (i))$
467	466	a1i	$⊢ (φ \land b \in B) \to \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = \sum_{i = 1}^{K - 1} (b (i + 1) - b (i))$
468	467	oveq2d	$⊢ (φ \land b \in B) \to b (1) + \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = b (1) + \sum_{i = 1}^{K - 1} (b (i + 1) - b (i))$
469		fveq2	$⊢ w = i \to b (w) = b (i)$
470		fveq2	$⊢ w = i + 1 \to b (w) = b (i + 1)$
471		fveq2	$⊢ w = 1 \to b (w) = b (1)$
472		fveq2	$⊢ w = K - 1 + 1 \to b (w) = b (K - 1 + 1)$
473	404 214	eqeltrd	$⊢ (φ \land b \in B) \to K - 1 + 1 \in ℤ_{\geq 1}$
474	30	adantr	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
475		1zzd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to 1 \in ℤ$
476	16	adantr	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to K \in ℤ$
477		elfzelz	$⊢ w \in (1 \dots K - 1 + 1) \to w \in ℤ$
478	477	adantl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \in ℤ$
479		elfzle1	$⊢ w \in (1 \dots K - 1 + 1) \to 1 \leq w$
480	479	adantl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to 1 \leq w$
481		elfzle2	$⊢ w \in (1 \dots K - 1 + 1) \to w \leq K - 1 + 1$
482	481	adantl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \leq K - 1 + 1$
483	404	adantr	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to K - 1 + 1 = K$
484	482 483	breqtrd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \leq K$
485	475 476 478 480 484	elfzd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \in (1 \dots K)$
486	474 485	ffvelcdmd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to b (w) \in (1 \dots N + K)$
487		elfznn	$⊢ b (w) \in (1 \dots N + K) \to b (w) \in ℕ$
488	487	nncnd	$⊢ b (w) \in (1 \dots N + K) \to b (w) \in ℂ$
489	486 488	syl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to b (w) \in ℂ$
490	469 470 471 472 420 473 489	telfsum2	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K - 1} (b (i + 1) - b (i)) = b (K - 1 + 1) - b (1)$
491	490	oveq2d	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1}^{K - 1} (b (i + 1) - b (i)) = b (1) + b (K - 1 + 1) - b (1)$
492	73	recnd	$⊢ (φ \land b \in B) \to b (1) \in ℂ$
493	39	nncnd	$⊢ (φ \land b \in B) \to b (K) \in ℂ$
494	404	fveq2d	$⊢ (φ \land b \in B) \to b (K - 1 + 1) = b (K)$
495	494	eleq1d	$⊢ (φ \land b \in B) \to (b (K - 1 + 1) \in ℂ \leftrightarrow b (K) \in ℂ)$
496	493 495	mpbird	$⊢ (φ \land b \in B) \to b (K - 1 + 1) \in ℂ$
497	492 496	pncan3d	$⊢ (φ \land b \in B) \to b (1) + b (K - 1 + 1) - b (1) = b (K - 1 + 1)$
498	497 494	eqtrd	$⊢ (φ \land b \in B) \to b (1) + b (K - 1 + 1) - b (1) = b (K)$
499	491 498	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1}^{K - 1} (b (i + 1) - b (i)) = b (K)$
500	468 499	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = b (K)$
501	460 500	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i - 1 + 1) - b (i - 1)) = b (K)$
502	419 501	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i) - b (i - 1)) = b (K)$
503	408 502	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K} (b (i) - b (i - 1)) = b (K)$
504	402 503	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) = b (K)$
505	388 504	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) = b (K)$
506		fsumconst	$⊢ ((1 \dots K) \in Fin \land 1 \in ℂ) \to \sum_{i = 1}^{K} 1 = \|(1 \dots K)\| \cdot 1$
507	346 68 506	syl2anc	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} 1 = \|(1 \dots K)\| \cdot 1$
508	212	nnnn0d	$⊢ (φ \land b \in B) \to K \in ℕ_{0}$
509		hashfz1	$⊢ K \in ℕ_{0} \to \|(1 \dots K)\| = K$
510	508 509	syl	$⊢ (φ \land b \in B) \to \|(1 \dots K)\| = K$
511	510	oveq1d	$⊢ (φ \land b \in B) \to \|(1 \dots K)\| \cdot 1 = K \cdot 1$
512	403	mulridd	$⊢ (φ \land b \in B) \to K \cdot 1 = K$
513	511 512	eqtrd	$⊢ (φ \land b \in B) \to \|(1 \dots K)\| \cdot 1 = K$
514	507 513	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} 1 = K$
515	505 514	oveq12d	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) - \sum_{i = 1}^{K} 1 = b (K) - K$
516	385 515	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = b (K) - K$
517	43	addlidd	$⊢ (φ \land b \in B) \to 0 + b (K) = b (K)$
518	517	eqcomd	$⊢ (φ \land b \in B) \to b (K) = 0 + b (K)$
519	518	oveq1d	$⊢ (φ \land b \in B) \to b (K) - K = 0 + b (K) - K$
520	516 519	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = 0 + b (K) - K$
521		0cnd	$⊢ (φ \land b \in B) \to 0 \in ℂ$
522	521 403 43	subsub3d	$⊢ (φ \land b \in B) \to 0 - (K - b (K)) = 0 + b (K) - K$
523	522	eqcomd	$⊢ (φ \land b \in B) \to 0 + b (K) - K = 0 - (K - b (K))$
524	520 523	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = 0 - (K - b (K))$
525	14	zcnd	$⊢ (φ \land b \in B) \to N \in ℂ$
526	525	subidd	$⊢ (φ \land b \in B) \to N - N = 0$
527	526	eqcomd	$⊢ (φ \land b \in B) \to 0 = N - N$
528	527	oveq1d	$⊢ (φ \land b \in B) \to 0 - (K - b (K)) = N - N - (K - b (K))$
529	524 528	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = N - N - (K - b (K))$
530	403 43	subcld	$⊢ (φ \land b \in B) \to K - b (K) \in ℂ$
531	525 525 530	subsub4d	$⊢ (φ \land b \in B) \to N - N - (K - b (K)) = N - (N + K - b (K))$
532	529 531	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = N - (N + K - b (K))$
533	525 403 43	addsubassd	$⊢ (φ \land b \in B) \to N + K - b (K) = N + K - b (K)$
534	533	eqcomd	$⊢ (φ \land b \in B) \to N + K - b (K) = N + K - b (K)$
535	534	oveq2d	$⊢ (φ \land b \in B) \to N - (N + K - b (K)) = N - (N + K - b (K))$
536	532 535	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = N - (N + K - b (K))$
537		1zzd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to 1 \in ℤ$
538	382 537	zsubcld	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to if (i = 1, b (1), b (i) - b (i - 1)) - 1 \in ℤ$
539	346 538	fsumzcl	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) \in ℤ$
540	539	zcnd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) \in ℂ$
541	54	nn0cnd	$⊢ (φ \land b \in B) \to N + K - b (K) \in ℂ$
542	540 541 525	addlsub	$⊢ (φ \land b \in B) \to (\sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) + (N + K) - b (K) = N \leftrightarrow \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = N - (N + K - b (K)))$
543	536 542	mpbird	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) + (N + K) - b (K) = N$
544	345 543	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1) + (N + K) - b (K) = N$
545	328 544	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) + (N + K) - b (K) = N$
546	313 545	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) + if (K + 1 = K + 1, N + K - b (K), if (K + 1 = 1, b (1) - 1, b (K + 1) - b (K + 1 - 1) - 1)) = N$
547	310 546	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K + 1} if (i = K + 1, N + K - b (K), if (i = 1, b (1) - 1, b (i) - b (i - 1) - 1)) = N$
548	211 547	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K + 1} (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i) = N$
549	193 548	jca	$⊢ (φ \land b \in B) \to ((k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i) = N)$
550		ovex	$⊢ (1 \dots K + 1) \in V$
551	550	mptex	$⊢ (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \in V$
552		feq1	$⊢ g = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \to (g : (1 \dots K + 1) ⟶ ℕ_{0} \leftrightarrow (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) : (1 \dots K + 1) ⟶ ℕ_{0})$
553		simpl	$⊢ (g = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \land i \in (1 \dots K + 1)) \to g = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))$
554	553	fveq1d	$⊢ (g = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \land i \in (1 \dots K + 1)) \to g (i) = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i)$
555	554	sumeq2dv	$⊢ g = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \to \sum_{i = 1}^{K + 1} g (i) = \sum_{i = 1}^{K + 1} (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i)$
556	555	eqeq1d	$⊢ g = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \to (\sum_{i = 1}^{K + 1} g (i) = N \leftrightarrow \sum_{i = 1}^{K + 1} (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i) = N)$
557	552 556	anbi12d	$⊢ g = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \to ((g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N) \leftrightarrow ((k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i) = N))$
558	551 557	elab	$⊢ (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow ((k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) (i) = N)$
559	549 558	sylibr	$⊢ (φ \land b \in B) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
560	4	a1i	$⊢ (φ \land b \in B) \to A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
561	559 560	eleqtrrd	$⊢ (φ \land b \in B) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1))) \in A$
562	10 561	eqeltrrd	$⊢ (φ \land b \in B) \to if (K = 0, \{⟨1, N⟩\}, (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)))) \in A$
563	562 3	fmptd	$⊢ φ \to G : B ⟶ A$

Metamath Proof Explorer

Theorem sticksstones10

Proof