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	14	zcnd	$⊢ (φ \land b \in B) \to N \in ℂ$
347	54	nn0cnd	$⊢ (φ \land b \in B) \to N + K - b (K) \in ℂ$
348		fzfid	$⊢ (φ \land b \in B) \to (1 \dots K) \in Fin$
349		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 ℤ)$
350		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 ℤ)$
351	66	ad2antrr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land i = 1) \to b (1) \in ℤ$
352	30	adantr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
353		simpr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \in (1 \dots K)$
354	352 353	ffvelcdmd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to b (i) \in (1 \dots N + K)$
355	265	nnzd	$⊢ b (i) \in (1 \dots N + K) \to b (i) \in ℤ$
356	354 355	syl	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to b (i) \in ℤ$
357	356	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i) \in ℤ$
358	352	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
359		1zzd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \in ℤ$
360	16	ad2antrr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to K \in ℤ$
361	315	nnzd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i \in ℤ$
362	361	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i \in ℤ$
363	362 359	zsubcld	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i - 1 \in ℤ$
364	315	nnge1d	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to 1 \leq i$
365	364	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \leq i$
366	338 273	syl	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i \neq 1$
367	365 366	jca	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to (1 \leq i \land i \neq 1)$
368	318	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \in ℝ$
369	316	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i \in ℝ$
370	368 369	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))$
371	367 370	mpbird	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 < i$
372		zltlem1	$⊢ (1 \in ℤ \land i \in ℤ) \to (1 < i \leftrightarrow 1 \leq i - 1)$
373	359 362 372	syl2anc	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to (1 < i \leftrightarrow 1 \leq i - 1)$
374	371 373	mpbid	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to 1 \leq i - 1$
375	316 318	resubcld	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i - 1 \in ℝ$
376	316	lem1d	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i - 1 \leq i$
377	375 316 317 376 321	letrd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to i - 1 \leq K$
378	377	adantr	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i - 1 \leq K$
379	359 360 363 374 378	elfzd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to i - 1 \in (1 \dots K)$
380	358 379	ffvelcdmd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i - 1) \in (1 \dots N + K)$
381	380 293	syl	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i - 1) \in ℕ$
382	381	nnzd	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i - 1) \in ℤ$
383	357 382	zsubcld	$⊢ (((φ \land b \in B) \land i \in (1 \dots K)) \land \neg i = 1) \to b (i) - b (i - 1) \in ℤ$
384	349 350 351 383	ifbothda	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to if (i = 1, b (1), b (i) - b (i - 1)) \in ℤ$
385	384	zcnd	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to if (i = 1, b (1), b (i) - b (i - 1)) \in ℂ$
386	68	adantr	$⊢ ((φ \land b \in B) \land i \in (1 \dots K)) \to 1 \in ℂ$
387	348 385 386	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$
388		id	$⊢ i = 1 \to i = 1$
389	388	iftrued	$⊢ i = 1 \to if (i = 1, b (1), b (i) - b (i - 1)) = b (1)$
390	214 385 389	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))$
391	60	adantr	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 \in ℝ$
392		elfzle1	$⊢ i \in (1 + 1 \dots K) \to 1 + 1 \leq i$
393	392	adantl	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 + 1 \leq i$
394	31	adantr	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 \in ℤ$
395		elfzelz	$⊢ i \in (1 + 1 \dots K) \to i \in ℤ$
396	395	adantl	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to i \in ℤ$
397	394 396 280	syl2anc	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to (1 < i \leftrightarrow 1 + 1 \leq i)$
398	393 397	mpbird	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 < i$
399	391 398	ltned	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to 1 \neq i$
400	399	necomd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to i \neq 1$
401	400	neneqd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K)) \to \neg i = 1$
402	401	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)$
403	402	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))$
404	403	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))$
405	34	recnd	$⊢ (φ \land b \in B) \to K \in ℂ$
406	405 68	npcand	$⊢ (φ \land b \in B) \to K - 1 + 1 = K$
407	406	eqcomd	$⊢ (φ \land b \in B) \to K = K - 1 + 1$
408	407	oveq2d	$⊢ (φ \land b \in B) \to (1 + 1 \dots K) = (1 + 1 \dots K - 1 + 1)$
409	408	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))$
410	409	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))$
411		elfzelz	$⊢ i \in (1 + 1 \dots K - 1 + 1) \to i \in ℤ$
412	411	adantl	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i \in ℤ$
413	412	zcnd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i \in ℂ$
414		1cnd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to 1 \in ℂ$
415	413 414	npcand	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i - 1 + 1 = i$
416	415	eqcomd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to i = i - 1 + 1$
417	416	fveq2d	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to b (i) = b (i - 1 + 1)$
418		eqidd	$⊢ ((φ \land b \in B) \land i \in (1 + 1 \dots K - 1 + 1)) \to b (i - 1) = b (i - 1)$
419	417 418	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)$
420	419	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))$
421	420	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))$
422	16 31	zsubcld	$⊢ (φ \land b \in B) \to K - 1 \in ℤ$
423	30	adantr	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
424		1zzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \in ℤ$
425	16	adantr	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K \in ℤ$
426		elfznn	$⊢ s \in (1 \dots K - 1) \to s \in ℕ$
427	426	adantl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in ℕ$
428	427	nnzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in ℤ$
429	428	peano2zd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \in ℤ$
430		1red	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \in ℝ$
431	427	nnred	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in ℝ$
432	431 430	readdcld	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \in ℝ$
433	427	nnge1d	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \leq s$
434	431	lep1d	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \leq s + 1$
435	430 431 432 433 434	letrd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to 1 \leq s + 1$
436		elfzle2	$⊢ s \in (1 \dots K - 1) \to s \leq K - 1$
437	436	adantl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \leq K - 1$
438	34	adantr	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K \in ℝ$
439		leaddsub	$⊢ (s \in ℝ \land 1 \in ℝ \land K \in ℝ) \to (s + 1 \leq K \leftrightarrow s \leq K - 1)$
440	431 430 438 439	syl3anc	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to (s + 1 \leq K \leftrightarrow s \leq K - 1)$
441	437 440	mpbird	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \leq K$
442	424 425 429 435 441	elfzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s + 1 \in (1 \dots K)$
443	423 442	ffvelcdmd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) \in (1 \dots N + K)$
444		elfznn	$⊢ b (s + 1) \in (1 \dots N + K) \to b (s + 1) \in ℕ$
445	443 444	syl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) \in ℕ$
446	445	nnzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) \in ℤ$
447	438 430	resubcld	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K - 1 \in ℝ$
448	438	lem1d	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to K - 1 \leq K$
449	431 447 438 437 448	letrd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \leq K$
450	424 425 428 433 449	elfzd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to s \in (1 \dots K)$
451	423 450	ffvelcdmd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s) \in (1 \dots N + K)$
452		elfznn	$⊢ b (s) \in (1 \dots N + K) \to b (s) \in ℕ$
453	452	nnzd	$⊢ b (s) \in (1 \dots N + K) \to b (s) \in ℤ$
454	451 453	syl	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s) \in ℤ$
455	446 454	zsubcld	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) - b (s) \in ℤ$
456	455	zcnd	$⊢ ((φ \land b \in B) \land s \in (1 \dots K - 1)) \to b (s + 1) - b (s) \in ℂ$
457		fvoveq1	$⊢ s = i - 1 \to b (s + 1) = b (i - 1 + 1)$
458		fveq2	$⊢ s = i - 1 \to b (s) = b (i - 1)$
459	457 458	oveq12d	$⊢ s = i - 1 \to b (s + 1) - b (s) = b (i - 1 + 1) - b (i - 1)$
460	31 31 422 456 459	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))$
461	460	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))$
462	461	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))$
463		fvoveq1	$⊢ s = i \to b (s + 1) = b (i + 1)$
464		fveq2	$⊢ s = i \to b (s) = b (i)$
465	463 464	oveq12d	$⊢ s = i \to b (s + 1) - b (s) = b (i + 1) - b (i)$
466		nfcv	$⊢ \underline{Ⅎ} i (b (s + 1) - b (s))$
467		nfcv	$⊢ \underline{Ⅎ} s (b (i + 1) - b (i))$
468	465 466 467	cbvsum	$⊢ \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = \sum_{i = 1}^{K - 1} (b (i + 1) - b (i))$
469	468	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))$
470	469	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))$
471		fveq2	$⊢ w = i \to b (w) = b (i)$
472		fveq2	$⊢ w = i + 1 \to b (w) = b (i + 1)$
473		fveq2	$⊢ w = 1 \to b (w) = b (1)$
474		fveq2	$⊢ w = K - 1 + 1 \to b (w) = b (K - 1 + 1)$
475	406 214	eqeltrd	$⊢ (φ \land b \in B) \to K - 1 + 1 \in ℤ_{\geq 1}$
476	30	adantr	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to b : (1 \dots K) ⟶ (1 \dots N + K)$
477		1zzd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to 1 \in ℤ$
478	16	adantr	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to K \in ℤ$
479		elfzelz	$⊢ w \in (1 \dots K - 1 + 1) \to w \in ℤ$
480	479	adantl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \in ℤ$
481		elfzle1	$⊢ w \in (1 \dots K - 1 + 1) \to 1 \leq w$
482	481	adantl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to 1 \leq w$
483		elfzle2	$⊢ w \in (1 \dots K - 1 + 1) \to w \leq K - 1 + 1$
484	483	adantl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \leq K - 1 + 1$
485	406	adantr	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to K - 1 + 1 = K$
486	484 485	breqtrd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \leq K$
487	477 478 480 482 486	elfzd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to w \in (1 \dots K)$
488	476 487	ffvelcdmd	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to b (w) \in (1 \dots N + K)$
489		elfznn	$⊢ b (w) \in (1 \dots N + K) \to b (w) \in ℕ$
490	489	nncnd	$⊢ b (w) \in (1 \dots N + K) \to b (w) \in ℂ$
491	488 490	syl	$⊢ ((φ \land b \in B) \land w \in (1 \dots K - 1 + 1)) \to b (w) \in ℂ$
492	471 472 473 474 422 475 491	telfsum2	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K - 1} (b (i + 1) - b (i)) = b (K - 1 + 1) - b (1)$
493	492	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)$
494	73	recnd	$⊢ (φ \land b \in B) \to b (1) \in ℂ$
495	39	nncnd	$⊢ (φ \land b \in B) \to b (K) \in ℂ$
496	406	fveq2d	$⊢ (φ \land b \in B) \to b (K - 1 + 1) = b (K)$
497	496	eleq1d	$⊢ (φ \land b \in B) \to (b (K - 1 + 1) \in ℂ \leftrightarrow b (K) \in ℂ)$
498	495 497	mpbird	$⊢ (φ \land b \in B) \to b (K - 1 + 1) \in ℂ$
499	494 498	pncan3d	$⊢ (φ \land b \in B) \to b (1) + b (K - 1 + 1) - b (1) = b (K - 1 + 1)$
500	499 496	eqtrd	$⊢ (φ \land b \in B) \to b (1) + b (K - 1 + 1) - b (1) = b (K)$
501	493 500	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1}^{K - 1} (b (i + 1) - b (i)) = b (K)$
502	470 501	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{s = 1}^{K - 1} (b (s + 1) - b (s)) = b (K)$
503	462 502	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i - 1 + 1) - b (i - 1)) = b (K)$
504	421 503	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K - 1 + 1} (b (i) - b (i - 1)) = b (K)$
505	410 504	eqtrd	$⊢ (φ \land b \in B) \to b (1) + \sum_{i = 1 + 1}^{K} (b (i) - b (i - 1)) = b (K)$
506	404 505	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)$
507	390 506	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} if (i = 1, b (1), b (i) - b (i - 1)) = b (K)$
508		fsumconst	$⊢ ((1 \dots K) \in Fin \land 1 \in ℂ) \to \sum_{i = 1}^{K} 1 = \|(1 \dots K)\| \cdot 1$
509	348 68 508	syl2anc	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} 1 = \|(1 \dots K)\| \cdot 1$
510	212	nnnn0d	$⊢ (φ \land b \in B) \to K \in ℕ_{0}$
511		hashfz1	$⊢ K \in ℕ_{0} \to \|(1 \dots K)\| = K$
512	510 511	syl	$⊢ (φ \land b \in B) \to \|(1 \dots K)\| = K$
513	512	oveq1d	$⊢ (φ \land b \in B) \to \|(1 \dots K)\| \cdot 1 = K \cdot 1$
514	405	mulridd	$⊢ (φ \land b \in B) \to K \cdot 1 = K$
515	513 514	eqtrd	$⊢ (φ \land b \in B) \to \|(1 \dots K)\| \cdot 1 = K$
516	509 515	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} 1 = K$
517	507 516	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$
518	387 517	eqtrd	$⊢ (φ \land b \in B) \to \sum_{i = 1}^{K} (if (i = 1, b (1), b (i) - b (i - 1)) - 1) = b (K) - K$
519	43	addlidd	$⊢ (φ \land b \in B) \to 0 + b (K) = b (K)$
520	519	eqcomd	$⊢ (φ \land b \in B) \to b (K) = 0 + b (K)$
521	520	oveq1d	$⊢ (φ \land b \in B) \to b (K) - K = 0 + b (K) - K$
522	518 521	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$
523		0cnd	$⊢ (φ \land b \in B) \to 0 \in ℂ$
524	523 405 43	subsub3d	$⊢ (φ \land b \in B) \to 0 - (K - b (K)) = 0 + b (K) - K$
525	524	eqcomd	$⊢ (φ \land b \in B) \to 0 + b (K) - K = 0 - (K - b (K))$
526	522 525	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))$
527	346	subidd	$⊢ (φ \land b \in B) \to N - N = 0$
528	527	eqcomd	$⊢ (φ \land b \in B) \to 0 = N - N$
529	528	oveq1d	$⊢ (φ \land b \in B) \to 0 - (K - b (K)) = N - N - (K - b (K))$
530	526 529	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))$
531	405 43	subcld	$⊢ (φ \land b \in B) \to K - b (K) \in ℂ$
532	346 346 531	subsub4d	$⊢ (φ \land b \in B) \to N - N - (K - b (K)) = N - (N + K - b (K))$
533	530 532	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))$
534	346 405 43	addsubassd	$⊢ (φ \land b \in B) \to N + K - b (K) = N + K - b (K)$
535	534	eqcomd	$⊢ (φ \land b \in B) \to N + K - b (K) = N + K - b (K)$
536	535	oveq2d	$⊢ (φ \land b \in B) \to N - (N + K - b (K)) = N - (N + K - b (K))$
537	533 536	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))$
538	346 347 537	mvrrsubd	$⊢ (φ \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$
539	345 538	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$
540	328 539	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$
541	313 540	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$
542	310 541	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$
543	211 542	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$
544	193 543	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)$
545		ovex	$⊢ (1 \dots K + 1) \in V$
546	545	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$
547		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})$
548		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)))$
549	548	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)$
550	549	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)$
551	550	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)$
552	547 551	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))$
553	546 552	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)$
554	544 553	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)\}$
555	4	a1i	$⊢ (φ \land b \in B) \to A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
556	554 555	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$
557	10 556	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$
558	557 3	fmptd	$⊢ φ \to G : B ⟶ A$

Metamath Proof Explorer

Theorem sticksstones10

Proof