sticksstones12

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

	Ref	Expression
Hypotheses	sticksstones12.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones12.2	$⊢ φ \to K \in ℕ$
	sticksstones12.3	$⊢ F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
	sticksstones12.4	$⊢ 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)))))$
	sticksstones12.5	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
	sticksstones12.6	$⊢ 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	sticksstones12	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		sticksstones12.1	$⊢ φ \to N \in ℕ_{0}$
2		sticksstones12.2	$⊢ φ \to K \in ℕ$
3		sticksstones12.3	$⊢ F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
4		sticksstones12.4	$⊢ 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)))))$
5		sticksstones12.5	$⊢ A = \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
6		sticksstones12.6	$⊢ 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)))\}$
7	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
8	1 7 3 5 6	sticksstones8	$⊢ φ \to F : A ⟶ B$
9	1 2 4 5 6	sticksstones10	$⊢ φ \to G : B ⟶ A$
10	4	a1i	$⊢ φ \to 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)))))$
11		0red	$⊢ φ \to 0 \in ℝ$
12	2	nngt0d	$⊢ φ \to 0 < K$
13	11 12	ltned	$⊢ φ \to 0 \neq K$
14	13	necomd	$⊢ φ \to K \neq 0$
15	14	neneqd	$⊢ φ \to \neg K = 0$
16	15	iffalsed	$⊢ φ \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)))$
17	16	adantr	$⊢ (φ \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)))$
18	17	mpteq2dva	$⊢ φ \to (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))))) = (b \in B ⟼ (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))))$
19	10 18	eqtrd	$⊢ φ \to G = (b \in B ⟼ (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))))$
20	19	adantr	$⊢ (φ \land c \in A) \to G = (b \in B ⟼ (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))))$
21		fveq1	$⊢ b = F (c) \to b (K) = F (c) (K)$
22	21	oveq2d	$⊢ b = F (c) \to N + K - b (K) = N + K - F (c) (K)$
23		fveq1	$⊢ b = F (c) \to b (1) = F (c) (1)$
24	23	oveq1d	$⊢ b = F (c) \to b (1) - 1 = F (c) (1) - 1$
25		fveq1	$⊢ b = F (c) \to b (k) = F (c) (k)$
26		fveq1	$⊢ b = F (c) \to b (k - 1) = F (c) (k - 1)$
27	25 26	oveq12d	$⊢ b = F (c) \to b (k) - b (k - 1) = F (c) (k) - F (c) (k - 1)$
28	27	oveq1d	$⊢ b = F (c) \to b (k) - b (k - 1) - 1 = F (c) (k) - F (c) (k - 1) - 1$
29	24 28	ifeq12d	$⊢ b = F (c) \to if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1) = if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1)$
30	22 29	ifeq12d	$⊢ b = F (c) \to if (k = K + 1, N + K - b (K), if (k = 1, b (1) - 1, b (k) - b (k - 1) - 1)) = if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1))$
31	30	adantr	$⊢ (b = F (c) \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)) = if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1))$
32	31	mpteq2dva	$⊢ b = F (c) \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 - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1)))$
33	32	adantl	$⊢ ((φ \land c \in A) \land b = F (c)) \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 - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1)))$
34	8	ffvelcdmda	$⊢ (φ \land c \in A) \to F (c) \in B$
35		fzfid	$⊢ (φ \land c \in A) \to (1 \dots K + 1) \in Fin$
36	35	mptexd	$⊢ (φ \land c \in A) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1))) \in V$
37	20 33 34 36	fvmptd	$⊢ (φ \land c \in A) \to G (F (c)) = (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1)))$
38	3	a1i	$⊢ (φ \land c \in A) \to F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
39		simpllr	$⊢ ((((φ \land c \in A) \land a = c) \land j \in (1 \dots K)) \land l \in (1 \dots j)) \to a = c$
40	39	fveq1d	$⊢ ((((φ \land c \in A) \land a = c) \land j \in (1 \dots K)) \land l \in (1 \dots j)) \to a (l) = c (l)$
41	40	sumeq2dv	$⊢ (((φ \land c \in A) \land a = c) \land j \in (1 \dots K)) \to \sum_{l = 1}^{j} a (l) = \sum_{l = 1}^{j} c (l)$
42	41	oveq2d	$⊢ (((φ \land c \in A) \land a = c) \land j \in (1 \dots K)) \to j + \sum_{l = 1}^{j} a (l) = j + \sum_{l = 1}^{j} c (l)$
43	42	mpteq2dva	$⊢ ((φ \land c \in A) \land a = c) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l))$
44		simpr	$⊢ (φ \land c \in A) \to c \in A$
45		fzfid	$⊢ (φ \land c \in A) \to (1 \dots K) \in Fin$
46	45	mptexd	$⊢ (φ \land c \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) \in V$
47	38 43 44 46	fvmptd	$⊢ (φ \land c \in A) \to F (c) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l))$
48		simpr	$⊢ ((φ \land c \in A) \land j = K) \to j = K$
49	48	oveq2d	$⊢ ((φ \land c \in A) \land j = K) \to (1 \dots j) = (1 \dots K)$
50	49	sumeq1d	$⊢ ((φ \land c \in A) \land j = K) \to \sum_{l = 1}^{j} c (l) = \sum_{l = 1}^{K} c (l)$
51	48 50	oveq12d	$⊢ ((φ \land c \in A) \land j = K) \to j + \sum_{l = 1}^{j} c (l) = K + \sum_{l = 1}^{K} c (l)$
52		1zzd	$⊢ φ \to 1 \in ℤ$
53	7	nn0zd	$⊢ φ \to K \in ℤ$
54	2	nnge1d	$⊢ φ \to 1 \leq K$
55	2	nnred	$⊢ φ \to K \in ℝ$
56	55	leidd	$⊢ φ \to K \leq K$
57	52 53 53 54 56	elfzd	$⊢ φ \to K \in (1 \dots K)$
58	57	adantr	$⊢ (φ \land c \in A) \to K \in (1 \dots K)$
59		ovexd	$⊢ (φ \land c \in A) \to K + \sum_{l = 1}^{K} c (l) \in V$
60	47 51 58 59	fvmptd	$⊢ (φ \land c \in A) \to F (c) (K) = K + \sum_{l = 1}^{K} c (l)$
61	60	oveq2d	$⊢ (φ \land c \in A) \to N + K - F (c) (K) = N + K - (K + \sum_{l = 1}^{K} c (l))$
62	1	nn0cnd	$⊢ φ \to N \in ℂ$
63	62	adantr	$⊢ (φ \land c \in A) \to N \in ℂ$
64	55	recnd	$⊢ φ \to K \in ℂ$
65	64	adantr	$⊢ (φ \land c \in A) \to K \in ℂ$
66	63 65	addcomd	$⊢ (φ \land c \in A) \to N + K = K + N$
67	66	oveq1d	$⊢ (φ \land c \in A) \to N + K - (K + \sum_{l = 1}^{K} c (l)) = K + N - (K + \sum_{l = 1}^{K} c (l))$
68		1zzd	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to 1 \in ℤ$
69	53	ad2antrr	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to K \in ℤ$
70	69	peano2zd	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to K + 1 \in ℤ$
71		elfzelz	$⊢ l \in (1 \dots K) \to l \in ℤ$
72	71	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to l \in ℤ$
73		elfzle1	$⊢ l \in (1 \dots K) \to 1 \leq l$
74	73	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to 1 \leq l$
75	72	zred	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to l \in ℝ$
76	55	ad2antrr	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to K \in ℝ$
77	70	zred	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to K + 1 \in ℝ$
78		elfzle2	$⊢ l \in (1 \dots K) \to l \leq K$
79	78	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to l \leq K$
80	76	lep1d	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to K \leq K + 1$
81	75 76 77 79 80	letrd	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to l \leq K + 1$
82	68 70 72 74 81	elfzd	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to l \in (1 \dots K + 1)$
83	5	eleq2i	$⊢ c \in A \leftrightarrow c \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
84	83	biimpi	$⊢ c \in A \to c \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
85	84	adantl	$⊢ (φ \land c \in A) \to c \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\}$
86		vex	$⊢ c \in V$
87		feq1	$⊢ g = c \to (g : (1 \dots K + 1) ⟶ ℕ_{0} \leftrightarrow c : (1 \dots K + 1) ⟶ ℕ_{0})$
88		simpl	$⊢ (g = c \land i \in (1 \dots K + 1)) \to g = c$
89	88	fveq1d	$⊢ (g = c \land i \in (1 \dots K + 1)) \to g (i) = c (i)$
90	89	sumeq2dv	$⊢ g = c \to \sum_{i = 1}^{K + 1} g (i) = \sum_{i = 1}^{K + 1} c (i)$
91	90	eqeq1d	$⊢ g = c \to (\sum_{i = 1}^{K + 1} g (i) = N \leftrightarrow \sum_{i = 1}^{K + 1} c (i) = N)$
92	87 91	anbi12d	$⊢ g = c \to ((g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N) \leftrightarrow (c : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} c (i) = N))$
93	86 92	elab	$⊢ c \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (c : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} c (i) = N)$
94	93	a1i	$⊢ (φ \land c \in A) \to (c \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \leftrightarrow (c : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} c (i) = N))$
95	94	biimpd	$⊢ (φ \land c \in A) \to (c \in \{g \| (g : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} g (i) = N)\} \to (c : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} c (i) = N))$
96	85 95	mpd	$⊢ (φ \land c \in A) \to (c : (1 \dots K + 1) ⟶ ℕ_{0} \land \sum_{i = 1}^{K + 1} c (i) = N)$
97	96	simpld	$⊢ (φ \land c \in A) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
98	97	adantr	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
99	98	ffvelcdmda	$⊢ (((φ \land c \in A) \land l \in (1 \dots K)) \land l \in (1 \dots K + 1)) \to c (l) \in ℕ_{0}$
100	82 99	mpdan	$⊢ ((φ \land c \in A) \land l \in (1 \dots K)) \to c (l) \in ℕ_{0}$
101	45 100	fsumnn0cl	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K} c (l) \in ℕ_{0}$
102	101	nn0cnd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K} c (l) \in ℂ$
103	65 63 102	pnpcand	$⊢ (φ \land c \in A) \to K + N - (K + \sum_{l = 1}^{K} c (l)) = N - \sum_{l = 1}^{K} c (l)$
104		eqid	$⊢ 1 = 1$
105		1p0e1	$⊢ 1 + 0 = 1$
106	104 105	eqtr4i	$⊢ 1 = 1 + 0$
107	106	a1i	$⊢ φ \to 1 = 1 + 0$
108		1red	$⊢ φ \to 1 \in ℝ$
109		0le1	$⊢ 0 \leq 1$
110	109	a1i	$⊢ φ \to 0 \leq 1$
111	108 11 55 108 54 110	le2addd	$⊢ φ \to 1 + 0 \leq K + 1$
112	107 111	eqbrtrd	$⊢ φ \to 1 \leq K + 1$
113	53	peano2zd	$⊢ φ \to K + 1 \in ℤ$
114		eluz	$⊢ (1 \in ℤ \land K + 1 \in ℤ) \to (K + 1 \in ℤ_{\geq 1} \leftrightarrow 1 \leq K + 1)$
115	52 113 114	syl2anc	$⊢ φ \to (K + 1 \in ℤ_{\geq 1} \leftrightarrow 1 \leq K + 1)$
116	112 115	mpbird	$⊢ φ \to K + 1 \in ℤ_{\geq 1}$
117	116	adantr	$⊢ (φ \land c \in A) \to K + 1 \in ℤ_{\geq 1}$
118	97	ffvelcdmda	$⊢ ((φ \land c \in A) \land l \in (1 \dots K + 1)) \to c (l) \in ℕ_{0}$
119	118	nn0cnd	$⊢ ((φ \land c \in A) \land l \in (1 \dots K + 1)) \to c (l) \in ℂ$
120		fveq2	$⊢ l = K + 1 \to c (l) = c (K + 1)$
121	117 119 120	fsumm1	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1} c (l) = \sum_{l = 1}^{K + 1 - 1} c (l) + c (K + 1)$
122		1cnd	$⊢ (φ \land c \in A) \to 1 \in ℂ$
123	65 122	pncand	$⊢ (φ \land c \in A) \to K + 1 - 1 = K$
124	123	oveq2d	$⊢ (φ \land c \in A) \to (1 \dots K + 1 - 1) = (1 \dots K)$
125	124	sumeq1d	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1 - 1} c (l) = \sum_{l = 1}^{K} c (l)$
126	125	oveq1d	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1 - 1} c (l) + c (K + 1) = \sum_{l = 1}^{K} c (l) + c (K + 1)$
127	121 126	eqtrd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1} c (l) = \sum_{l = 1}^{K} c (l) + c (K + 1)$
128	127	eqcomd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K} c (l) + c (K + 1) = \sum_{l = 1}^{K + 1} c (l)$
129		fveq2	$⊢ l = i \to c (l) = c (i)$
130		nfcv	$⊢ \underline{Ⅎ} i (1 \dots K + 1)$
131		nfcv	$⊢ \underline{Ⅎ} l (1 \dots K + 1)$
132		nfcv	$⊢ \underline{Ⅎ} i c (l)$
133		nfcv	$⊢ \underline{Ⅎ} l c (i)$
134	129 130 131 132 133	cbvsum	$⊢ \sum_{l = 1}^{K + 1} c (l) = \sum_{i = 1}^{K + 1} c (i)$
135	134	a1i	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1} c (l) = \sum_{i = 1}^{K + 1} c (i)$
136	96	simprd	$⊢ (φ \land c \in A) \to \sum_{i = 1}^{K + 1} c (i) = N$
137	135 136	eqtrd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1} c (l) = N$
138	128 137	eqtrd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K} c (l) + c (K + 1) = N$
139		1zzd	$⊢ (φ \land c \in A) \to 1 \in ℤ$
140	53	adantr	$⊢ (φ \land c \in A) \to K \in ℤ$
141	140	peano2zd	$⊢ (φ \land c \in A) \to K + 1 \in ℤ$
142		1e0p1	$⊢ 1 = 0 + 1$
143	142	a1i	$⊢ (φ \land c \in A) \to 1 = 0 + 1$
144		0red	$⊢ (φ \land c \in A) \to 0 \in ℝ$
145	55	adantr	$⊢ (φ \land c \in A) \to K \in ℝ$
146		1red	$⊢ (φ \land c \in A) \to 1 \in ℝ$
147	11 55 12	ltled	$⊢ φ \to 0 \leq K$
148	147	adantr	$⊢ (φ \land c \in A) \to 0 \leq K$
149	144 145 146 148	leadd1dd	$⊢ (φ \land c \in A) \to 0 + 1 \leq K + 1$
150	143 149	eqbrtrd	$⊢ (φ \land c \in A) \to 1 \leq K + 1$
151	55 55 108 56	leadd1dd	$⊢ φ \to K + 1 \leq K + 1$
152	151	adantr	$⊢ (φ \land c \in A) \to K + 1 \leq K + 1$
153	139 141 141 150 152	elfzd	$⊢ (φ \land c \in A) \to K + 1 \in (1 \dots K + 1)$
154	97 153	ffvelcdmd	$⊢ (φ \land c \in A) \to c (K + 1) \in ℕ_{0}$
155	154	nn0cnd	$⊢ (φ \land c \in A) \to c (K + 1) \in ℂ$
156	63 102 155	subaddd	$⊢ (φ \land c \in A) \to (N - \sum_{l = 1}^{K} c (l) = c (K + 1) \leftrightarrow \sum_{l = 1}^{K} c (l) + c (K + 1) = N)$
157	138 156	mpbird	$⊢ (φ \land c \in A) \to N - \sum_{l = 1}^{K} c (l) = c (K + 1)$
158	103 157	eqtrd	$⊢ (φ \land c \in A) \to K + N - (K + \sum_{l = 1}^{K} c (l)) = c (K + 1)$
159	67 158	eqtrd	$⊢ (φ \land c \in A) \to N + K - (K + \sum_{l = 1}^{K} c (l)) = c (K + 1)$
160	61 159	eqtrd	$⊢ (φ \land c \in A) \to N + K - F (c) (K) = c (K + 1)$
161	160	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to N + K - F (c) (K) = c (K + 1)$
162	161	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to N + K - F (c) (K) = c (K + 1)$
163		simpr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to k = K + 1$
164	163	fveq2d	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to c (k) = c (K + 1)$
165	164	eqcomd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to c (K + 1) = c (k)$
166	162 165	eqtrd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to N + K - F (c) (K) = c (k)$
167	47	fveq1d	$⊢ (φ \land c \in A) \to F (c) (1) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1)$
168	167	oveq1d	$⊢ (φ \land c \in A) \to F (c) (1) - 1 = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1) - 1$
169		eqidd	$⊢ (φ \land c \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l))$
170		simpr	$⊢ ((φ \land c \in A) \land j = 1) \to j = 1$
171	170	oveq2d	$⊢ ((φ \land c \in A) \land j = 1) \to (1 \dots j) = (1 \dots 1)$
172	171	sumeq1d	$⊢ ((φ \land c \in A) \land j = 1) \to \sum_{l = 1}^{j} c (l) = \sum_{l = 1}^{1} c (l)$
173	170 172	oveq12d	$⊢ ((φ \land c \in A) \land j = 1) \to j + \sum_{l = 1}^{j} c (l) = 1 + \sum_{l = 1}^{1} c (l)$
174	146	leidd	$⊢ (φ \land c \in A) \to 1 \leq 1$
175	54	adantr	$⊢ (φ \land c \in A) \to 1 \leq K$
176	139 140 139 174 175	elfzd	$⊢ (φ \land c \in A) \to 1 \in (1 \dots K)$
177		ovexd	$⊢ (φ \land c \in A) \to 1 + \sum_{l = 1}^{1} c (l) \in V$
178	169 173 176 177	fvmptd	$⊢ (φ \land c \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1) = 1 + \sum_{l = 1}^{1} c (l)$
179	178	oveq1d	$⊢ (φ \land c \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1) - 1 = 1 + \sum_{l = 1}^{1} c (l) - 1$
180		fzfid	$⊢ (φ \land c \in A) \to (1 \dots 1) \in Fin$
181		1zzd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 \in ℤ$
182	140	adantr	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to K \in ℤ$
183	182	peano2zd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to K + 1 \in ℤ$
184		elfzelz	$⊢ l \in (1 \dots 1) \to l \in ℤ$
185	184	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \in ℤ$
186		elfzle1	$⊢ l \in (1 \dots 1) \to 1 \leq l$
187	186	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 \leq l$
188	185	zred	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \in ℝ$
189		0red	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 0 \in ℝ$
190		1red	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 \in ℝ$
191	189 190	readdcld	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 0 + 1 \in ℝ$
192	183	zred	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to K + 1 \in ℝ$
193		elfzle2	$⊢ l \in (1 \dots 1) \to l \leq 1$
194	193	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \leq 1$
195	142	a1i	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 = 0 + 1$
196	194 195	breqtrd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \leq 0 + 1$
197	149	adantr	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 0 + 1 \leq K + 1$
198	188 191 192 196 197	letrd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \leq K + 1$
199	181 183 185 187 198	elfzd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \in (1 \dots K + 1)$
200	118	adantlr	$⊢ (((φ \land c \in A) \land l \in (1 \dots 1)) \land l \in (1 \dots K + 1)) \to c (l) \in ℕ_{0}$
201	199 200	mpdan	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to c (l) \in ℕ_{0}$
202	180 201	fsumnn0cl	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{1} c (l) \in ℕ_{0}$
203	202	nn0cnd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{1} c (l) \in ℂ$
204	122 203	pncan2d	$⊢ (φ \land c \in A) \to 1 + \sum_{l = 1}^{1} c (l) - 1 = \sum_{l = 1}^{1} c (l)$
205	139 141 139 174 150	elfzd	$⊢ (φ \land c \in A) \to 1 \in (1 \dots K + 1)$
206	97 205	ffvelcdmd	$⊢ (φ \land c \in A) \to c (1) \in ℕ_{0}$
207	206	nn0cnd	$⊢ (φ \land c \in A) \to c (1) \in ℂ$
208		fveq2	$⊢ l = 1 \to c (l) = c (1)$
209	208	fsum1	$⊢ (1 \in ℤ \land c (1) \in ℂ) \to \sum_{l = 1}^{1} c (l) = c (1)$
210	139 207 209	syl2anc	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{1} c (l) = c (1)$
211	204 210	eqtrd	$⊢ (φ \land c \in A) \to 1 + \sum_{l = 1}^{1} c (l) - 1 = c (1)$
212	179 211	eqtrd	$⊢ (φ \land c \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1) - 1 = c (1)$
213	168 212	eqtrd	$⊢ (φ \land c \in A) \to F (c) (1) - 1 = c (1)$
214	213	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to F (c) (1) - 1 = c (1)$
215	214	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to F (c) (1) - 1 = c (1)$
216	215	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land k = 1) \to F (c) (1) - 1 = c (1)$
217		simpr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land k = 1) \to k = 1$
218	217	fveq2d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land k = 1) \to c (k) = c (1)$
219	218	eqcomd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land k = 1) \to c (1) = c (k)$
220	216 219	eqtrd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land k = 1) \to F (c) (1) - 1 = c (k)$
221	3	a1i	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to F = (a \in A ⟼ (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)))$
222		simpllr	$⊢ ((((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land a = c) \land j \in (1 \dots K)) \land l \in (1 \dots j)) \to a = c$
223	222	fveq1d	$⊢ ((((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land a = c) \land j \in (1 \dots K)) \land l \in (1 \dots j)) \to a (l) = c (l)$
224	223	sumeq2dv	$⊢ (((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land a = c) \land j \in (1 \dots K)) \to \sum_{l = 1}^{j} a (l) = \sum_{l = 1}^{j} c (l)$
225	224	oveq2d	$⊢ (((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land a = c) \land j \in (1 \dots K)) \to j + \sum_{l = 1}^{j} a (l) = j + \sum_{l = 1}^{j} c (l)$
226	225	mpteq2dva	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land a = c) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} a (l)) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l))$
227		simpll2	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to c \in A$
228		fzfid	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (1 \dots K) \in Fin$
229	228	mptexd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) \in V$
230	221 226 227 229	fvmptd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to F (c) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l))$
231	230	fveq1d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to F (c) (k) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k)$
232	230	fveq1d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to F (c) (k - 1) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k - 1)$
233	231 232	oveq12d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to F (c) (k) - F (c) (k - 1) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k) - (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k - 1)$
234	233	oveq1d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to F (c) (k) - F (c) (k - 1) - 1 = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k) - (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k - 1) - 1$
235		eqidd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l))$
236		simpr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k) \to j = k$
237	236	oveq2d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k) \to (1 \dots j) = (1 \dots k)$
238	237	sumeq1d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k) \to \sum_{l = 1}^{j} c (l) = \sum_{l = 1}^{k} c (l)$
239	236 238	oveq12d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k) \to j + \sum_{l = 1}^{j} c (l) = k + \sum_{l = 1}^{k} c (l)$
240		1zzd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \in ℤ$
241	140	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to K \in ℤ$
242	241	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K \in ℤ$
243	242	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to K \in ℤ$
244		elfznn	$⊢ k \in (1 \dots K + 1) \to k \in ℕ$
245	244	3ad2ant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in ℕ$
246	245	nnzd	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in ℤ$
247	246	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℤ$
248	247	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in ℤ$
249	245	nnge1d	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to 1 \leq k$
250	249	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to 1 \leq k$
251	250	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \leq k$
252		simpl3	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in (1 \dots K + 1)$
253		1zzd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to 1 \in ℤ$
254	242	peano2zd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \in ℤ$
255		elfz	$⊢ (k \in ℤ \land 1 \in ℤ \land K + 1 \in ℤ) \to (k \in (1 \dots K + 1) \leftrightarrow (1 \leq k \land k \leq K + 1))$
256	247 253 254 255	syl3anc	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (k \in (1 \dots K + 1) \leftrightarrow (1 \leq k \land k \leq K + 1))$
257	256	biimpd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (k \in (1 \dots K + 1) \to (1 \leq k \land k \leq K + 1))$
258	252 257	mpd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (1 \leq k \land k \leq K + 1)$
259	258	simprd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \leq K + 1$
260		neqne	$⊢ \neg k = K + 1 \to k \neq K + 1$
261	260	adantl	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \neq K + 1$
262	261	necomd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \neq k$
263	259 262	jca	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (k \leq K + 1 \land K + 1 \neq k)$
264	247	zred	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℝ$
265	254	zred	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \in ℝ$
266	264 265	ltlend	$⊢ ((φ \land c \in A \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))$
267	263 266	mpbird	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k < K + 1$
268		zleltp1	$⊢ (k \in ℤ \land K \in ℤ) \to (k \leq K \leftrightarrow k < K + 1)$
269	247 242 268	syl2anc	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to (k \leq K \leftrightarrow k < K + 1)$
270	267 269	mpbird	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \leq K$
271	270	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \leq K$
272	240 243 248 251 271	elfzd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in (1 \dots K)$
273		ovexd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k + \sum_{l = 1}^{k} c (l) \in V$
274	235 239 272 273	fvmptd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k) = k + \sum_{l = 1}^{k} c (l)$
275		simpr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k - 1) \to j = k - 1$
276	275	oveq2d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k - 1) \to (1 \dots j) = (1 \dots k - 1)$
277	276	sumeq1d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k - 1) \to \sum_{l = 1}^{j} c (l) = \sum_{l = 1}^{k - 1} c (l)$
278	275 277	oveq12d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land j = k - 1) \to j + \sum_{l = 1}^{j} c (l) = k - 1 + \sum_{l = 1}^{k - 1} c (l)$
279		1zzd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℤ$
280	53	ad2antrr	$⊢ ((φ \land k \in (1 \dots K + 1)) \land \neg k = 1) \to K \in ℤ$
281	280	3impa	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \in ℤ$
282	244	nnzd	$⊢ k \in (1 \dots K + 1) \to k \in ℤ$
283	282	adantl	$⊢ (φ \land k \in (1 \dots K + 1)) \to k \in ℤ$
284	283	adantr	$⊢ ((φ \land k \in (1 \dots K + 1)) \land \neg k = 1) \to k \in ℤ$
285	284	3impa	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \in ℤ$
286	285 279	zsubcld	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \in ℤ$
287		neqne	$⊢ \neg k = 1 \to k \neq 1$
288	287	3ad2ant3	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \neq 1$
289	108	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℝ$
290	285	zred	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \in ℝ$
291		simp2	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \in (1 \dots K + 1)$
292		elfzle1	$⊢ k \in (1 \dots K + 1) \to 1 \leq k$
293	291 292	syl	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \leq k$
294	289 290 293	leltned	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to (1 < k \leftrightarrow k \neq 1)$
295	288 294	mpbird	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 < k$
296	279 285	zltp1led	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to (1 < k \leftrightarrow 1 + 1 \leq k)$
297	295 296	mpbid	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 + 1 \leq k$
298		leaddsub	$⊢ (1 \in ℝ \land 1 \in ℝ \land k \in ℝ) \to (1 + 1 \leq k \leftrightarrow 1 \leq k - 1)$
299	289 289 290 298	syl3anc	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to (1 + 1 \leq k \leftrightarrow 1 \leq k - 1)$
300	297 299	mpbid	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \leq k - 1$
301	286	zred	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \in ℝ$
302	55	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \in ℝ$
303		1red	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℝ$
304	302 303	readdcld	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 \in ℝ$
305	304 303	resubcld	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 - 1 \in ℝ$
306		elfzle2	$⊢ k \in (1 \dots K + 1) \to k \leq K + 1$
307	306	3ad2ant2	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \leq K + 1$
308	290 304 303 307	lesub1dd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \leq K + 1 - 1$
309	64	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \in ℂ$
310		1cnd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℂ$
311	309 310	pncand	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 - 1 = K$
312	56	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \leq K$
313	311 312	eqbrtrd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 - 1 \leq K$
314	301 305 302 308 313	letrd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \leq K$
315	279 281 286 300 314	elfzd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
316	315	3expa	$⊢ ((φ \land k \in (1 \dots K + 1)) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
317	316	3adantl2	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
318	317	adantlr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
319		ovexd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - 1 + \sum_{l = 1}^{k - 1} c (l) \in V$
320	235 278 318 319	fvmptd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k - 1) = k - 1 + \sum_{l = 1}^{k - 1} c (l)$
321	274 320	oveq12d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k) - (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k - 1) = k + \sum_{l = 1}^{k} c (l) - (k - 1 + \sum_{l = 1}^{k - 1} c (l))$
322	321	oveq1d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k) - (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k - 1) - 1 = (k + \sum_{l = 1}^{k} c (l)) - (k - 1 + \sum_{l = 1}^{k - 1} c (l)) - 1$
323	248	zcnd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in ℂ$
324		fzfid	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (1 \dots k) \in Fin$
325		1zzd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to 1 \in ℤ$
326	243	adantr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to K \in ℤ$
327	326	peano2zd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to K + 1 \in ℤ$
328		elfznn	$⊢ l \in (1 \dots k) \to l \in ℕ$
329	328	adantl	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to l \in ℕ$
330	329	nnzd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to l \in ℤ$
331	329	nnge1d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to 1 \leq l$
332	329	nnred	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to l \in ℝ$
333	264	ad2antrr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to k \in ℝ$
334	265	ad2antrr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to K + 1 \in ℝ$
335		elfzle2	$⊢ l \in (1 \dots k) \to l \leq k$
336	335	adantl	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to l \leq k$
337	259	ad2antrr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to k \leq K + 1$
338	332 333 334 336 337	letrd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to l \leq K + 1$
339	325 327 330 331 338	elfzd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to l \in (1 \dots K + 1)$
340	97	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
341	340	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
342	341	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
343	342	adantr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
344	343	ffvelcdmda	$⊢ (((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \land l \in (1 \dots K + 1)) \to c (l) \in ℕ_{0}$
345	339 344	mpdan	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to c (l) \in ℕ_{0}$
346	324 345	fsumnn0cl	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k} c (l) \in ℕ_{0}$
347	346	nn0cnd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k} c (l) \in ℂ$
348		1cnd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \in ℂ$
349	323 348	subcld	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - 1 \in ℂ$
350		fzfid	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (1 \dots k - 1) \in Fin$
351		1zzd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to 1 \in ℤ$
352	243	adantr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to K \in ℤ$
353	352	peano2zd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to K + 1 \in ℤ$
354		elfznn	$⊢ l \in (1 \dots k - 1) \to l \in ℕ$
355	354	adantl	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to l \in ℕ$
356	355	nnzd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to l \in ℤ$
357	355	nnge1d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to 1 \leq l$
358	355	nnred	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to l \in ℝ$
359	264	ad2antrr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to k \in ℝ$
360		1red	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to 1 \in ℝ$
361	359 360	resubcld	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to k - 1 \in ℝ$
362	265	ad2antrr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to K + 1 \in ℝ$
363		elfzle2	$⊢ l \in (1 \dots k - 1) \to l \leq k - 1$
364	363	adantl	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to l \leq k - 1$
365	359	lem1d	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to k - 1 \leq k$
366	259	ad2antrr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to k \leq K + 1$
367	361 359 362 365 366	letrd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to k - 1 \leq K + 1$
368	358 361 362 364 367	letrd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to l \leq K + 1$
369	351 353 356 357 368	elfzd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to l \in (1 \dots K + 1)$
370	342	adantr	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
371	370	ffvelcdmda	$⊢ (((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \land l \in (1 \dots K + 1)) \to c (l) \in ℕ_{0}$
372	369 371	mpdan	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k - 1)) \to c (l) \in ℕ_{0}$
373	350 372	fsumnn0cl	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k - 1} c (l) \in ℕ_{0}$
374	373	nn0cnd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k - 1} c (l) \in ℂ$
375	323 347 349 374	addsub4d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k + \sum_{l = 1}^{k} c (l) - (k - 1 + \sum_{l = 1}^{k - 1} c (l)) = (k - (k - 1)) + \sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)$
376	375	oveq1d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (k + \sum_{l = 1}^{k} c (l)) - (k - 1 + \sum_{l = 1}^{k - 1} c (l)) - 1 = (k - (k - 1)) + (\sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)) - 1$
377	323 348	nncand	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k - (k - 1) = 1$
378	377	oveq1d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (k - (k - 1)) + \sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l) = 1 + \sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)$
379	378	oveq1d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (k - (k - 1)) + (\sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)) - 1 = 1 + (\sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)) - 1$
380	347 374	subcld	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l) \in ℂ$
381	348 380	pncan2d	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 + (\sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)) - 1 = \sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)$
382	139	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to 1 \in ℤ$
383	382 246 249	3jca	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to (1 \in ℤ \land k \in ℤ \land 1 \leq k)$
384		eluz2	$⊢ k \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land k \in ℤ \land 1 \leq k)$
385	383 384	sylibr	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in ℤ_{\geq 1}$
386	385	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℤ_{\geq 1}$
387	386	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in ℤ_{\geq 1}$
388	345	nn0cnd	$⊢ ((((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \land l \in (1 \dots k)) \to c (l) \in ℂ$
389		fveq2	$⊢ l = k \to c (l) = c (k)$
390	387 388 389	fsumm1	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k} c (l) = \sum_{l = 1}^{k - 1} c (l) + c (k)$
391	390	eqcomd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k - 1} c (l) + c (k) = \sum_{l = 1}^{k} c (l)$
392		simp3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in (1 \dots K + 1)$
393	340 392	ffvelcdmd	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to c (k) \in ℕ_{0}$
394	393	nn0cnd	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to c (k) \in ℂ$
395	394	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to c (k) \in ℂ$
396	395	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to c (k) \in ℂ$
397	347 374 396	subaddd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (\sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l) = c (k) \leftrightarrow \sum_{l = 1}^{k - 1} c (l) + c (k) = \sum_{l = 1}^{k} c (l))$
398	391 397	mpbird	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to \sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l) = c (k)$
399	381 398	eqtrd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 + (\sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)) - 1 = c (k)$
400	379 399	eqtrd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (k - (k - 1)) + (\sum_{l = 1}^{k} c (l) - \sum_{l = 1}^{k - 1} c (l)) - 1 = c (k)$
401	376 400	eqtrd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (k + \sum_{l = 1}^{k} c (l)) - (k - 1 + \sum_{l = 1}^{k - 1} c (l)) - 1 = c (k)$
402	322 401	eqtrd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k) - (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (k - 1) - 1 = c (k)$
403	234 402	eqtrd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to F (c) (k) - F (c) (k - 1) - 1 = c (k)$
404	220 403	ifeqda	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1) = c (k)$
405	166 404	ifeqda	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1)) = c (k)$
406	405	3expa	$⊢ ((φ \land c \in A) \land k \in (1 \dots K + 1)) \to if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1)) = c (k)$
407	406	mpteq2dva	$⊢ (φ \land c \in A) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1))) = (k \in (1 \dots K + 1) ⟼ c (k))$
408	97	ffnd	$⊢ (φ \land c \in A) \to c Fn (1 \dots K + 1)$
409		dffn5	$⊢ c Fn (1 \dots K + 1) \leftrightarrow c = (k \in (1 \dots K + 1) ⟼ c (k))$
410	409	biimpi	$⊢ c Fn (1 \dots K + 1) \to c = (k \in (1 \dots K + 1) ⟼ c (k))$
411	408 410	syl	$⊢ (φ \land c \in A) \to c = (k \in (1 \dots K + 1) ⟼ c (k))$
412	411	eqcomd	$⊢ (φ \land c \in A) \to (k \in (1 \dots K + 1) ⟼ c (k)) = c$
413	407 412	eqtrd	$⊢ (φ \land c \in A) \to (k \in (1 \dots K + 1) ⟼ if (k = K + 1, N + K - F (c) (K), if (k = 1, F (c) (1) - 1, F (c) (k) - F (c) (k - 1) - 1))) = c$
414	37 413	eqtrd	$⊢ (φ \land c \in A) \to G (F (c)) = c$
415	414	ralrimiva	$⊢ φ \to \forall c \in A G (F (c)) = c$
416	1 2 3 4 5 6	sticksstones12a	$⊢ φ \to \forall d \in B F (G (d)) = d$
417	8 9 415 416	2fvidf1od	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem sticksstones12

Proof