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

Metamath Proof Explorer

Theorem sticksstones10

Proof