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

Metamath Proof Explorer

Theorem sticksstones12

Proof