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 c (l)$
131		nfcv	$⊢ \underline{Ⅎ} l c (i)$
132	129 130 131	cbvsum	$⊢ \sum_{l = 1}^{K + 1} c (l) = \sum_{i = 1}^{K + 1} c (i)$
133	132	a1i	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1} c (l) = \sum_{i = 1}^{K + 1} c (i)$
134	96	simprd	$⊢ (φ \land c \in A) \to \sum_{i = 1}^{K + 1} c (i) = N$
135	133 134	eqtrd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K + 1} c (l) = N$
136	128 135	eqtrd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{K} c (l) + c (K + 1) = N$
137		1zzd	$⊢ (φ \land c \in A) \to 1 \in ℤ$
138	53	adantr	$⊢ (φ \land c \in A) \to K \in ℤ$
139	138	peano2zd	$⊢ (φ \land c \in A) \to K + 1 \in ℤ$
140		1e0p1	$⊢ 1 = 0 + 1$
141	140	a1i	$⊢ (φ \land c \in A) \to 1 = 0 + 1$
142		0red	$⊢ (φ \land c \in A) \to 0 \in ℝ$
143	55	adantr	$⊢ (φ \land c \in A) \to K \in ℝ$
144		1red	$⊢ (φ \land c \in A) \to 1 \in ℝ$
145	11 55 12	ltled	$⊢ φ \to 0 \leq K$
146	145	adantr	$⊢ (φ \land c \in A) \to 0 \leq K$
147	142 143 144 146	leadd1dd	$⊢ (φ \land c \in A) \to 0 + 1 \leq K + 1$
148	141 147	eqbrtrd	$⊢ (φ \land c \in A) \to 1 \leq K + 1$
149	55 55 108 56	leadd1dd	$⊢ φ \to K + 1 \leq K + 1$
150	149	adantr	$⊢ (φ \land c \in A) \to K + 1 \leq K + 1$
151	137 139 139 148 150	elfzd	$⊢ (φ \land c \in A) \to K + 1 \in (1 \dots K + 1)$
152	97 151	ffvelcdmd	$⊢ (φ \land c \in A) \to c (K + 1) \in ℕ_{0}$
153	152	nn0cnd	$⊢ (φ \land c \in A) \to c (K + 1) \in ℂ$
154	63 102 153	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)$
155	136 154	mpbird	$⊢ (φ \land c \in A) \to N - \sum_{l = 1}^{K} c (l) = c (K + 1)$
156	103 155	eqtrd	$⊢ (φ \land c \in A) \to K + N - (K + \sum_{l = 1}^{K} c (l)) = c (K + 1)$
157	67 156	eqtrd	$⊢ (φ \land c \in A) \to N + K - (K + \sum_{l = 1}^{K} c (l)) = c (K + 1)$
158	61 157	eqtrd	$⊢ (φ \land c \in A) \to N + K - F (c) (K) = c (K + 1)$
159	158	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to N + K - F (c) (K) = c (K + 1)$
160	159	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)$
161		simpr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to k = K + 1$
162	161	fveq2d	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to c (k) = c (K + 1)$
163	162	eqcomd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to c (K + 1) = c (k)$
164	160 163	eqtrd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land k = K + 1) \to N + K - F (c) (K) = c (k)$
165	47	fveq1d	$⊢ (φ \land c \in A) \to F (c) (1) = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1)$
166	165	oveq1d	$⊢ (φ \land c \in A) \to F (c) (1) - 1 = (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1) - 1$
167		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))$
168		simpr	$⊢ ((φ \land c \in A) \land j = 1) \to j = 1$
169	168	oveq2d	$⊢ ((φ \land c \in A) \land j = 1) \to (1 \dots j) = (1 \dots 1)$
170	169	sumeq1d	$⊢ ((φ \land c \in A) \land j = 1) \to \sum_{l = 1}^{j} c (l) = \sum_{l = 1}^{1} c (l)$
171	168 170	oveq12d	$⊢ ((φ \land c \in A) \land j = 1) \to j + \sum_{l = 1}^{j} c (l) = 1 + \sum_{l = 1}^{1} c (l)$
172	144	leidd	$⊢ (φ \land c \in A) \to 1 \leq 1$
173	54	adantr	$⊢ (φ \land c \in A) \to 1 \leq K$
174	137 138 137 172 173	elfzd	$⊢ (φ \land c \in A) \to 1 \in (1 \dots K)$
175		ovexd	$⊢ (φ \land c \in A) \to 1 + \sum_{l = 1}^{1} c (l) \in V$
176	167 171 174 175	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)$
177	176	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$
178		fzfid	$⊢ (φ \land c \in A) \to (1 \dots 1) \in Fin$
179		1zzd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 \in ℤ$
180	138	adantr	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to K \in ℤ$
181	180	peano2zd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to K + 1 \in ℤ$
182		elfzelz	$⊢ l \in (1 \dots 1) \to l \in ℤ$
183	182	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \in ℤ$
184		elfzle1	$⊢ l \in (1 \dots 1) \to 1 \leq l$
185	184	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 \leq l$
186	183	zred	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \in ℝ$
187		0red	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 0 \in ℝ$
188		1red	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 \in ℝ$
189	187 188	readdcld	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 0 + 1 \in ℝ$
190	181	zred	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to K + 1 \in ℝ$
191		elfzle2	$⊢ l \in (1 \dots 1) \to l \leq 1$
192	191	adantl	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \leq 1$
193	140	a1i	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 1 = 0 + 1$
194	192 193	breqtrd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \leq 0 + 1$
195	147	adantr	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to 0 + 1 \leq K + 1$
196	186 189 190 194 195	letrd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \leq K + 1$
197	179 181 183 185 196	elfzd	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to l \in (1 \dots K + 1)$
198	118	adantlr	$⊢ (((φ \land c \in A) \land l \in (1 \dots 1)) \land l \in (1 \dots K + 1)) \to c (l) \in ℕ_{0}$
199	197 198	mpdan	$⊢ ((φ \land c \in A) \land l \in (1 \dots 1)) \to c (l) \in ℕ_{0}$
200	178 199	fsumnn0cl	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{1} c (l) \in ℕ_{0}$
201	200	nn0cnd	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{1} c (l) \in ℂ$
202	122 201	pncan2d	$⊢ (φ \land c \in A) \to 1 + \sum_{l = 1}^{1} c (l) - 1 = \sum_{l = 1}^{1} c (l)$
203	137 139 137 172 148	elfzd	$⊢ (φ \land c \in A) \to 1 \in (1 \dots K + 1)$
204	97 203	ffvelcdmd	$⊢ (φ \land c \in A) \to c (1) \in ℕ_{0}$
205	204	nn0cnd	$⊢ (φ \land c \in A) \to c (1) \in ℂ$
206		fveq2	$⊢ l = 1 \to c (l) = c (1)$
207	206	fsum1	$⊢ (1 \in ℤ \land c (1) \in ℂ) \to \sum_{l = 1}^{1} c (l) = c (1)$
208	137 205 207	syl2anc	$⊢ (φ \land c \in A) \to \sum_{l = 1}^{1} c (l) = c (1)$
209	202 208	eqtrd	$⊢ (φ \land c \in A) \to 1 + \sum_{l = 1}^{1} c (l) - 1 = c (1)$
210	177 209	eqtrd	$⊢ (φ \land c \in A) \to (j \in (1 \dots K) ⟼ j + \sum_{l = 1}^{j} c (l)) (1) - 1 = c (1)$
211	166 210	eqtrd	$⊢ (φ \land c \in A) \to F (c) (1) - 1 = c (1)$
212	211	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to F (c) (1) - 1 = c (1)$
213	212	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to F (c) (1) - 1 = c (1)$
214	213	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)$
215		simpr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land k = 1) \to k = 1$
216	215	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)$
217	216	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)$
218	214 217	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)$
219	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)))$
220		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$
221	220	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)$
222	221	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)$
223	222	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)$
224	223	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))$
225		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$
226		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$
227	226	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$
228	219 224 225 227	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))$
229	228	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)$
230	228	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)$
231	229 230	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)$
232	231	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$
233		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))$
234		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$
235	234	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)$
236	235	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)$
237	234 236	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)$
238		1zzd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \in ℤ$
239	138	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to K \in ℤ$
240	239	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K \in ℤ$
241	240	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to K \in ℤ$
242		elfznn	$⊢ k \in (1 \dots K + 1) \to k \in ℕ$
243	242	3ad2ant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in ℕ$
244	243	nnzd	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in ℤ$
245	244	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℤ$
246	245	adantr	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in ℤ$
247	243	nnge1d	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to 1 \leq k$
248	247	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to 1 \leq k$
249	248	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$
250		simpl3	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in (1 \dots K + 1)$
251		1zzd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to 1 \in ℤ$
252	240	peano2zd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \in ℤ$
253		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))$
254	245 251 252 253	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))$
255	254	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))$
256	250 255	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)$
257	256	simprd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \leq K + 1$
258		neqne	$⊢ \neg k = K + 1 \to k \neq K + 1$
259	258	adantl	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \neq K + 1$
260	259	necomd	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \neq k$
261	257 260	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)$
262	245	zred	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℝ$
263	252	zred	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to K + 1 \in ℝ$
264	262 263	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))$
265	261 264	mpbird	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k < K + 1$
266		zleltp1	$⊢ (k \in ℤ \land K \in ℤ) \to (k \leq K \leftrightarrow k < K + 1)$
267	245 240 266	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)$
268	265 267	mpbird	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \leq K$
269	268	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$
270	238 241 246 249 269	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)$
271		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$
272	233 237 270 271	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)$
273		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$
274	273	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)$
275	274	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)$
276	273 275	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)$
277		1zzd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℤ$
278	53	ad2antrr	$⊢ ((φ \land k \in (1 \dots K + 1)) \land \neg k = 1) \to K \in ℤ$
279	278	3impa	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \in ℤ$
280	242	nnzd	$⊢ k \in (1 \dots K + 1) \to k \in ℤ$
281	280	adantl	$⊢ (φ \land k \in (1 \dots K + 1)) \to k \in ℤ$
282	281	adantr	$⊢ ((φ \land k \in (1 \dots K + 1)) \land \neg k = 1) \to k \in ℤ$
283	282	3impa	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \in ℤ$
284	283 277	zsubcld	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \in ℤ$
285		neqne	$⊢ \neg k = 1 \to k \neq 1$
286	285	3ad2ant3	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \neq 1$
287	108	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℝ$
288	283	zred	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \in ℝ$
289		simp2	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \in (1 \dots K + 1)$
290		elfzle1	$⊢ k \in (1 \dots K + 1) \to 1 \leq k$
291	289 290	syl	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \leq k$
292	287 288 291	leltned	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to (1 < k \leftrightarrow k \neq 1)$
293	286 292	mpbird	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 < k$
294	277 283	zltp1led	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to (1 < k \leftrightarrow 1 + 1 \leq k)$
295	293 294	mpbid	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 + 1 \leq k$
296		leaddsub	$⊢ (1 \in ℝ \land 1 \in ℝ \land k \in ℝ) \to (1 + 1 \leq k \leftrightarrow 1 \leq k - 1)$
297	287 287 288 296	syl3anc	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to (1 + 1 \leq k \leftrightarrow 1 \leq k - 1)$
298	295 297	mpbid	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \leq k - 1$
299	284	zred	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \in ℝ$
300	55	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \in ℝ$
301		1red	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℝ$
302	300 301	readdcld	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 \in ℝ$
303	302 301	resubcld	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 - 1 \in ℝ$
304		elfzle2	$⊢ k \in (1 \dots K + 1) \to k \leq K + 1$
305	304	3ad2ant2	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k \leq K + 1$
306	288 302 301 305	lesub1dd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \leq K + 1 - 1$
307	64	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \in ℂ$
308		1cnd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to 1 \in ℂ$
309	307 308	pncand	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 - 1 = K$
310	56	3ad2ant1	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K \leq K$
311	309 310	eqbrtrd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to K + 1 - 1 \leq K$
312	299 303 300 306 311	letrd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \leq K$
313	277 279 284 298 312	elfzd	$⊢ (φ \land k \in (1 \dots K + 1) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
314	313	3expa	$⊢ ((φ \land k \in (1 \dots K + 1)) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
315	314	3adantl2	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = 1) \to k - 1 \in (1 \dots K)$
316	315	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)$
317		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$
318	233 276 316 317	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)$
319	272 318	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))$
320	319	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$
321	246	zcnd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to k \in ℂ$
322		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$
323		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 ℤ$
324	241	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 ℤ$
325	324	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 ℤ$
326		elfznn	$⊢ l \in (1 \dots k) \to l \in ℕ$
327	326	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 ℕ$
328	327	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 ℤ$
329	327	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$
330	327	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 ℝ$
331	262	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 ℝ$
332	263	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 ℝ$
333		elfzle2	$⊢ l \in (1 \dots k) \to l \leq k$
334	333	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$
335	257	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$
336	330 331 332 334 335	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$
337	323 325 328 329 336	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)$
338	97	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
339	338	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to c : (1 \dots K + 1) ⟶ ℕ_{0}$
340	339	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}$
341	340	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}$
342	341	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}$
343	337 342	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}$
344	322 343	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}$
345	344	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 ℂ$
346		1cnd	$⊢ (((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \land \neg k = 1) \to 1 \in ℂ$
347	321 346	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 ℂ$
348		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$
349		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 ℤ$
350	241	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 ℤ$
351	350	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 ℤ$
352		elfznn	$⊢ l \in (1 \dots k - 1) \to l \in ℕ$
353	352	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 ℕ$
354	353	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 ℤ$
355	353	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$
356	353	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 ℝ$
357	262	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 ℝ$
358		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 ℝ$
359	357 358	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 ℝ$
360	263	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 ℝ$
361		elfzle2	$⊢ l \in (1 \dots k - 1) \to l \leq k - 1$
362	361	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$
363	357	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$
364	257	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$
365	359 357 360 363 364	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$
366	356 359 360 362 365	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$
367	349 351 354 355 366	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)$
368	340	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}$
369	368	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}$
370	367 369	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}$
371	348 370	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}$
372	371	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 ℂ$
373	321 345 347 372	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)$
374	373	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$
375	321 346	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$
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 - (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)$
377	376	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$
378	345 372	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 ℂ$
379	346 378	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)$
380	137	3adant3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to 1 \in ℤ$
381	380 244 247	3jca	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to (1 \in ℤ \land k \in ℤ \land 1 \leq k)$
382		eluz2	$⊢ k \in ℤ_{\geq 1} \leftrightarrow (1 \in ℤ \land k \in ℤ \land 1 \leq k)$
383	381 382	sylibr	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in ℤ_{\geq 1}$
384	383	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to k \in ℤ_{\geq 1}$
385	384	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}$
386	343	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 ℂ$
387		fveq2	$⊢ l = k \to c (l) = c (k)$
388	385 386 387	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)$
389	388	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)$
390		simp3	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to k \in (1 \dots K + 1)$
391	338 390	ffvelcdmd	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to c (k) \in ℕ_{0}$
392	391	nn0cnd	$⊢ (φ \land c \in A \land k \in (1 \dots K + 1)) \to c (k) \in ℂ$
393	392	adantr	$⊢ ((φ \land c \in A \land k \in (1 \dots K + 1)) \land \neg k = K + 1) \to c (k) \in ℂ$
394	393	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 ℂ$
395	345 372 394	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))$
396	389 395	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)$
397	379 396	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)$
398	377 397	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)$
399	374 398	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)$
400	320 399	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)$
401	232 400	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)$
402	218 401	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)$
403	164 402	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)$
404	403	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)$
405	404	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))$
406	97	ffnd	$⊢ (φ \land c \in A) \to c Fn (1 \dots K + 1)$
407		dffn5	$⊢ c Fn (1 \dots K + 1) \leftrightarrow c = (k \in (1 \dots K + 1) ⟼ c (k))$
408	407	biimpi	$⊢ c Fn (1 \dots K + 1) \to c = (k \in (1 \dots K + 1) ⟼ c (k))$
409	406 408	syl	$⊢ (φ \land c \in A) \to c = (k \in (1 \dots K + 1) ⟼ c (k))$
410	409	eqcomd	$⊢ (φ \land c \in A) \to (k \in (1 \dots K + 1) ⟼ c (k)) = c$
411	405 410	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$
412	37 411	eqtrd	$⊢ (φ \land c \in A) \to G (F (c)) = c$
413	412	ralrimiva	$⊢ φ \to \forall c \in A G (F (c)) = c$
414	1 2 3 4 5 6	sticksstones12a	$⊢ φ \to \forall d \in B F (G (d)) = d$
415	8 9 413 414	2fvidf1od	$⊢ φ \to F : A \underset{1-1 onto}{⟶} B$

Metamath Proof Explorer

Theorem sticksstones12

Proof