reprsuc

Description: Express the representations recursively. (Contributed by Thierry Arnoux, 5-Dec-2021)

	Ref	Expression
Hypotheses	reprval.a	$⊢ φ \to A \subseteq ℕ$
	reprval.m	$⊢ φ \to M \in ℤ$
	reprval.s	$⊢ φ \to S \in ℕ_{0}$
	reprsuc.f	$⊢ F = (c \in (A repr (S) (M - b)) ⟼ c \cup \{⟨S, b⟩\})$
Assertion	reprsuc	$⊢ φ \to A repr (S + 1) M = ⋃_{b \in A} ran F$

Proof

Step	Hyp	Ref	Expression
1		reprval.a	$⊢ φ \to A \subseteq ℕ$
2		reprval.m	$⊢ φ \to M \in ℤ$
3		reprval.s	$⊢ φ \to S \in ℕ_{0}$
4		reprsuc.f	$⊢ F = (c \in (A repr (S) (M - b)) ⟼ c \cup \{⟨S, b⟩\})$
5		1nn0	$⊢ 1 \in ℕ_{0}$
6	5	a1i	$⊢ φ \to 1 \in ℕ_{0}$
7	3 6	nn0addcld	$⊢ φ \to S + 1 \in ℕ_{0}$
8	1 2 7	reprval	$⊢ φ \to A repr (S + 1) M = \{c \in (A^{(0 ..^S + 1)}) \| \sum_{a \in (0 ..^S + 1)} c (a) = M\}$
9		simplr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e \in (A^{(0 ..^S + 1)})$
10		elmapi	$⊢ e \in (A^{(0 ..^S + 1)}) \to e : (0 ..^S + 1) ⟶ A$
11	9 10	syl	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e : (0 ..^S + 1) ⟶ A$
12	3	ad2antrr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to S \in ℕ_{0}$
13		fzonn0p1	$⊢ S \in ℕ_{0} \to S \in (0 ..^S + 1)$
14	12 13	syl	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to S \in (0 ..^S + 1)$
15	11 14	ffvelcdmd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e (S) \in A$
16		simpr	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land b = e (S)) \to b = e (S)$
17	16	oveq2d	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land b = e (S)) \to M - b = M - e (S)$
18	17	oveq2d	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land b = e (S)) \to A repr (S) (M - b) = A repr (S) (M - e (S))$
19		opeq2	$⊢ b = e (S) \to ⟨S, b⟩ = ⟨S, e (S)⟩$
20	19	sneqd	$⊢ b = e (S) \to \{⟨S, b⟩\} = \{⟨S, e (S)⟩\}$
21	20	uneq2d	$⊢ b = e (S) \to c \cup \{⟨S, b⟩\} = c \cup \{⟨S, e (S)⟩\}$
22	21	eqeq2d	$⊢ b = e (S) \to (e = c \cup \{⟨S, b⟩\} \leftrightarrow e = c \cup \{⟨S, e (S)⟩\})$
23	22	adantl	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land b = e (S)) \to (e = c \cup \{⟨S, b⟩\} \leftrightarrow e = c \cup \{⟨S, e (S)⟩\})$
24	18 23	rexeqbidv	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land b = e (S)) \to (\exists c \in (A repr (S) (M - b)) e = c \cup \{⟨S, b⟩\} \leftrightarrow \exists c \in (A repr (S) (M - e (S))) e = c \cup \{⟨S, e (S)⟩\})$
25	10	adantl	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to e : (0 ..^S + 1) ⟶ A$
26	3	adantr	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to S \in ℕ_{0}$
27		fzossfzop1	$⊢ S \in ℕ_{0} \to (0 ..^S) \subseteq (0 ..^S + 1)$
28	26 27	syl	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to (0 ..^S) \subseteq (0 ..^S + 1)$
29	25 28	fssresd	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to ({e ↾}_{(0 ..^S)}) : (0 ..^S) ⟶ A$
30	29	adantr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to ({e ↾}_{(0 ..^S)}) : (0 ..^S) ⟶ A$
31		nnex	$⊢ ℕ \in V$
32	31	a1i	$⊢ φ \to ℕ \in V$
33	32 1	ssexd	$⊢ φ \to A \in V$
34		fzofi	$⊢ (0 ..^S) \in Fin$
35	34	elexi	$⊢ (0 ..^S) \in V$
36		elmapg	$⊢ (A \in V \land (0 ..^S) \in V) \to ({e ↾}_{(0 ..^S)} \in (A^{(0 ..^S)}) \leftrightarrow ({e ↾}_{(0 ..^S)}) : (0 ..^S) ⟶ A)$
37	33 35 36	sylancl	$⊢ φ \to ({e ↾}_{(0 ..^S)} \in (A^{(0 ..^S)}) \leftrightarrow ({e ↾}_{(0 ..^S)}) : (0 ..^S) ⟶ A)$
38	37	ad2antrr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to ({e ↾}_{(0 ..^S)} \in (A^{(0 ..^S)}) \leftrightarrow ({e ↾}_{(0 ..^S)}) : (0 ..^S) ⟶ A)$
39	30 38	mpbird	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to {e ↾}_{(0 ..^S)} \in (A^{(0 ..^S)})$
40	34	a1i	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to (0 ..^S) \in Fin$
41		nnsscn	$⊢ ℕ \subseteq ℂ$
42	41	a1i	$⊢ φ \to ℕ \subseteq ℂ$
43	1 42	sstrd	$⊢ φ \to A \subseteq ℂ$
44	43	ad2antrr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to A \subseteq ℂ$
45	29	ffvelcdmda	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to ({e ↾}_{(0 ..^S)}) (a) \in A$
46	44 45	sseldd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to ({e ↾}_{(0 ..^S)}) (a) \in ℂ$
47	40 46	fsumcl	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) \in ℂ$
48	47	adantr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) \in ℂ$
49	43	adantr	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to A \subseteq ℂ$
50	26 13	syl	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to S \in (0 ..^S + 1)$
51	25 50	ffvelcdmd	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to e (S) \in A$
52	49 51	sseldd	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to e (S) \in ℂ$
53	52	adantr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e (S) \in ℂ$
54	48 53	pncand	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) + e (S) - e (S) = \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a)$
55		nfv	$⊢ Ⅎ a (φ \land e \in (A^{(0 ..^S + 1)}))$
56		nfcv	$⊢ \underline{Ⅎ} a e (S)$
57		fzonel	$⊢ \neg S \in (0 ..^S)$
58	57	a1i	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to \neg S \in (0 ..^S)$
59	25	adantr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to e : (0 ..^S + 1) ⟶ A$
60	28	sselda	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to a \in (0 ..^S + 1)$
61	59 60	ffvelcdmd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to e (a) \in A$
62	44 61	sseldd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to e (a) \in ℂ$
63		fveq2	$⊢ a = S \to e (a) = e (S)$
64	55 56 40 26 58 62 63 52	fsumsplitsn	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to \sum_{a \in (0 ..^S) \cup \{S\}} e (a) = \sum_{a \in (0 ..^S)} e (a) + e (S)$
65		fzosplitsn	$⊢ S \in ℤ_{\geq 0} \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
66		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
67	65 66	eleq2s	$⊢ S \in ℕ_{0} \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
68	26 67	syl	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
69	68	sumeq1d	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to \sum_{a \in (0 ..^S + 1)} e (a) = \sum_{a \in (0 ..^S) \cup \{S\}} e (a)$
70		simpr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
71	70	fvresd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land a \in (0 ..^S)) \to ({e ↾}_{(0 ..^S)}) (a) = e (a)$
72	71	sumeq2dv	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) = \sum_{a \in (0 ..^S)} e (a)$
73	72	oveq1d	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) + e (S) = \sum_{a \in (0 ..^S)} e (a) + e (S)$
74	64 69 73	3eqtr4d	$⊢ (φ \land e \in (A^{(0 ..^S + 1)})) \to \sum_{a \in (0 ..^S + 1)} e (a) = \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) + e (S)$
75	74	adantr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \sum_{a \in (0 ..^S + 1)} e (a) = \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) + e (S)$
76		simpr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \sum_{a \in (0 ..^S + 1)} e (a) = M$
77	75 76	eqtr3d	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) + e (S) = M$
78	77	oveq1d	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) + e (S) - e (S) = M - e (S)$
79	54 78	eqtr3d	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) = M - e (S)$
80	39 79	jca	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to ({e ↾}_{(0 ..^S)} \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) = M - e (S))$
81		fveq1	$⊢ d = {e ↾}_{(0 ..^S)} \to d (a) = ({e ↾}_{(0 ..^S)}) (a)$
82	81	sumeq2sdv	$⊢ d = {e ↾}_{(0 ..^S)} \to \sum_{a \in (0 ..^S)} d (a) = \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a)$
83	82	eqeq1d	$⊢ d = {e ↾}_{(0 ..^S)} \to (\sum_{a \in (0 ..^S)} d (a) = M - e (S) \leftrightarrow \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) = M - e (S))$
84	83	elrab	$⊢ {e ↾}_{(0 ..^S)} \in \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M - e (S)\} \leftrightarrow ({e ↾}_{(0 ..^S)} \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} ({e ↾}_{(0 ..^S)}) (a) = M - e (S))$
85	80 84	sylibr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to {e ↾}_{(0 ..^S)} \in \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M - e (S)\}$
86	1	ad2antrr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to A \subseteq ℕ$
87	2	ad2antrr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to M \in ℤ$
88		nnssz	$⊢ ℕ \subseteq ℤ$
89	1 88	sstrdi	$⊢ φ \to A \subseteq ℤ$
90	89	ad2antrr	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to A \subseteq ℤ$
91	90 15	sseldd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e (S) \in ℤ$
92	87 91	zsubcld	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to M - e (S) \in ℤ$
93	86 92 12	reprval	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to A repr (S) (M - e (S)) = \{d \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} d (a) = M - e (S)\}$
94	85 93	eleqtrrd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to {e ↾}_{(0 ..^S)} \in (A repr (S) (M - e (S)))$
95		simpr	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land c = {e ↾}_{(0 ..^S)}) \to c = {e ↾}_{(0 ..^S)}$
96	95	uneq1d	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land c = {e ↾}_{(0 ..^S)}) \to c \cup \{⟨S, e (S)⟩\} = ({e ↾}_{(0 ..^S)}) \cup \{⟨S, e (S)⟩\}$
97	96	eqeq2d	$⊢ (((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \land c = {e ↾}_{(0 ..^S)}) \to (e = c \cup \{⟨S, e (S)⟩\} \leftrightarrow e = ({e ↾}_{(0 ..^S)}) \cup \{⟨S, e (S)⟩\})$
98	11	ffnd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e Fn (0 ..^S + 1)$
99		fnsnsplit	$⊢ (e Fn (0 ..^S + 1) \land S \in (0 ..^S + 1)) \to e = ({e ↾}_{((0 ..^S + 1) ∖ \{S\})}) \cup \{⟨S, e (S)⟩\}$
100	98 14 99	syl2anc	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e = ({e ↾}_{((0 ..^S + 1) ∖ \{S\})}) \cup \{⟨S, e (S)⟩\}$
101	12 66	eleqtrdi	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to S \in ℤ_{\geq 0}$
102		fzodif2	$⊢ S \in ℤ_{\geq 0} \to (0 ..^S + 1) ∖ \{S\} = (0 ..^S)$
103	101 102	syl	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to (0 ..^S + 1) ∖ \{S\} = (0 ..^S)$
104	103	reseq2d	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to {e ↾}_{((0 ..^S + 1) ∖ \{S\})} = {e ↾}_{(0 ..^S)}$
105	104	uneq1d	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to ({e ↾}_{((0 ..^S + 1) ∖ \{S\})}) \cup \{⟨S, e (S)⟩\} = ({e ↾}_{(0 ..^S)}) \cup \{⟨S, e (S)⟩\}$
106	100 105	eqtrd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to e = ({e ↾}_{(0 ..^S)}) \cup \{⟨S, e (S)⟩\}$
107	94 97 106	rspcedvd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \exists c \in (A repr (S) (M - e (S))) e = c \cup \{⟨S, e (S)⟩\}$
108	15 24 107	rspcedvd	$⊢ ((φ \land e \in (A^{(0 ..^S + 1)})) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \to \exists b \in A \exists c \in (A repr (S) (M - b)) e = c \cup \{⟨S, b⟩\}$
109	108	anasss	$⊢ (φ \land (e \in (A^{(0 ..^S + 1)}) \land \sum_{a \in (0 ..^S + 1)} e (a) = M)) \to \exists b \in A \exists c \in (A repr (S) (M - b)) e = c \cup \{⟨S, b⟩\}$
110		simpr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to e = c \cup \{⟨S, b⟩\}$
111	1	adantr	$⊢ (φ \land b \in A) \to A \subseteq ℕ$
112	111	adantr	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to A \subseteq ℕ$
113	2	adantr	$⊢ (φ \land b \in A) \to M \in ℤ$
114	89	sselda	$⊢ (φ \land b \in A) \to b \in ℤ$
115	113 114	zsubcld	$⊢ (φ \land b \in A) \to M - b \in ℤ$
116	115	adantr	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to M - b \in ℤ$
117	3	adantr	$⊢ (φ \land b \in A) \to S \in ℕ_{0}$
118	117	adantr	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to S \in ℕ_{0}$
119		simpr	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to c \in (A repr (S) (M - b))$
120	112 116 118 119	reprf	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to c : (0 ..^S) ⟶ A$
121		simplr	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to b \in A$
122	118 121	fsnd	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to \{⟨S, b⟩\} : \{S\} ⟶ A$
123		fzodisjsn	$⊢ (0 ..^S) \cap \{S\} = \emptyset$
124	123	a1i	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to (0 ..^S) \cap \{S\} = \emptyset$
125	120 122 124	fun2d	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to (c \cup \{⟨S, b⟩\}) : (0 ..^S) \cup \{S\} ⟶ A$
126	118 67	syl	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
127	126	feq2d	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to ((c \cup \{⟨S, b⟩\}) : (0 ..^S + 1) ⟶ A \leftrightarrow (c \cup \{⟨S, b⟩\}) : (0 ..^S) \cup \{S\} ⟶ A)$
128	125 127	mpbird	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to (c \cup \{⟨S, b⟩\}) : (0 ..^S + 1) ⟶ A$
129		ovex	$⊢ (0 ..^S + 1) \in V$
130		elmapg	$⊢ (A \in V \land (0 ..^S + 1) \in V) \to (c \cup \{⟨S, b⟩\} \in (A^{(0 ..^S + 1)}) \leftrightarrow (c \cup \{⟨S, b⟩\}) : (0 ..^S + 1) ⟶ A)$
131	33 129 130	sylancl	$⊢ φ \to (c \cup \{⟨S, b⟩\} \in (A^{(0 ..^S + 1)}) \leftrightarrow (c \cup \{⟨S, b⟩\}) : (0 ..^S + 1) ⟶ A)$
132	131	ad2antrr	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to (c \cup \{⟨S, b⟩\} \in (A^{(0 ..^S + 1)}) \leftrightarrow (c \cup \{⟨S, b⟩\}) : (0 ..^S + 1) ⟶ A)$
133	128 132	mpbird	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to c \cup \{⟨S, b⟩\} \in (A^{(0 ..^S + 1)})$
134	133	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to c \cup \{⟨S, b⟩\} \in (A^{(0 ..^S + 1)})$
135	110 134	eqeltrd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to e \in (A^{(0 ..^S + 1)})$
136	126	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
137	136	sumeq1d	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S + 1)} e (a) = \sum_{a \in (0 ..^S) \cup \{S\}} e (a)$
138		nfv	$⊢ Ⅎ a (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\})$
139	34	a1i	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to (0 ..^S) \in Fin$
140	118	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to S \in ℕ_{0}$
141	57	a1i	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \neg S \in (0 ..^S)$
142	43	ad4antr	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to A \subseteq ℂ$
143	128	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to (c \cup \{⟨S, b⟩\}) : (0 ..^S + 1) ⟶ A$
144	110	feq1d	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to (e : (0 ..^S + 1) ⟶ A \leftrightarrow (c \cup \{⟨S, b⟩\}) : (0 ..^S + 1) ⟶ A)$
145	143 144	mpbird	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to e : (0 ..^S + 1) ⟶ A$
146	145	adantr	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to e : (0 ..^S + 1) ⟶ A$
147		simpr	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
148		elun1	$⊢ a \in (0 ..^S) \to a \in ((0 ..^S) \cup \{S\})$
149	147 148	syl	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to a \in ((0 ..^S) \cup \{S\})$
150	126	ad2antrr	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to (0 ..^S + 1) = (0 ..^S) \cup \{S\}$
151	149 150	eleqtrrd	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to a \in (0 ..^S + 1)$
152	146 151	ffvelcdmd	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to e (a) \in A$
153	142 152	sseldd	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to e (a) \in ℂ$
154	43	ad3antrrr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to A \subseteq ℂ$
155	140 13	syl	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to S \in (0 ..^S + 1)$
156	145 155	ffvelcdmd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to e (S) \in A$
157	154 156	sseldd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to e (S) \in ℂ$
158	138 56 139 140 141 153 63 157	fsumsplitsn	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S) \cup \{S\}} e (a) = \sum_{a \in (0 ..^S)} e (a) + e (S)$
159		simplr	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to e = c \cup \{⟨S, b⟩\}$
160	159	fveq1d	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to e (a) = (c \cup \{⟨S, b⟩\}) (a)$
161	120	ffnd	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to c Fn (0 ..^S)$
162	161	ad2antrr	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to c Fn (0 ..^S)$
163	122	ffnd	$⊢ ((φ \land b \in A) \land c \in (A repr (S) (M - b))) \to \{⟨S, b⟩\} Fn \{S\}$
164	163	ad2antrr	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to \{⟨S, b⟩\} Fn \{S\}$
165	123	a1i	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to (0 ..^S) \cap \{S\} = \emptyset$
166		fvun1	$⊢ (c Fn (0 ..^S) \land \{⟨S, b⟩\} Fn \{S\} \land ((0 ..^S) \cap \{S\} = \emptyset \land a \in (0 ..^S))) \to (c \cup \{⟨S, b⟩\}) (a) = c (a)$
167	162 164 165 147 166	syl112anc	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to (c \cup \{⟨S, b⟩\}) (a) = c (a)$
168	160 167	eqtrd	$⊢ ((((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \land a \in (0 ..^S)) \to e (a) = c (a)$
169	168	ralrimiva	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \forall a \in (0 ..^S) e (a) = c (a)$
170	169	sumeq2d	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S)} e (a) = \sum_{a \in (0 ..^S)} c (a)$
171	112	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to A \subseteq ℕ$
172	116	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to M - b \in ℤ$
173	119	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to c \in (A repr (S) (M - b))$
174	171 172 140 173	reprsum	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S)} c (a) = M - b$
175	170 174	eqtrd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S)} e (a) = M - b$
176	110	fveq1d	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to e (S) = (c \cup \{⟨S, b⟩\}) (S)$
177	161	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to c Fn (0 ..^S)$
178	163	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \{⟨S, b⟩\} Fn \{S\}$
179	123	a1i	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to (0 ..^S) \cap \{S\} = \emptyset$
180		snidg	$⊢ S \in ℕ_{0} \to S \in \{S\}$
181	140 180	syl	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to S \in \{S\}$
182		fvun2	$⊢ (c Fn (0 ..^S) \land \{⟨S, b⟩\} Fn \{S\} \land ((0 ..^S) \cap \{S\} = \emptyset \land S \in \{S\})) \to (c \cup \{⟨S, b⟩\}) (S) = \{⟨S, b⟩\} (S)$
183	177 178 179 181 182	syl112anc	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to (c \cup \{⟨S, b⟩\}) (S) = \{⟨S, b⟩\} (S)$
184	121	adantr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to b \in A$
185		fvsng	$⊢ (S \in ℕ_{0} \land b \in A) \to \{⟨S, b⟩\} (S) = b$
186	140 184 185	syl2anc	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \{⟨S, b⟩\} (S) = b$
187	176 183 186	3eqtrd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to e (S) = b$
188	175 187	oveq12d	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S)} e (a) + e (S) = M - b + b$
189		zsscn	$⊢ ℤ \subseteq ℂ$
190	113	ad2antrr	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to M \in ℤ$
191	189 190	sselid	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to M \in ℂ$
192	187 157	eqeltrrd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to b \in ℂ$
193	191 192	npcand	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to M - b + b = M$
194	188 193	eqtrd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S)} e (a) + e (S) = M$
195	137 158 194	3eqtrd	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to \sum_{a \in (0 ..^S + 1)} e (a) = M$
196	135 195	jca	$⊢ (((φ \land b \in A) \land c \in (A repr (S) (M - b))) \land e = c \cup \{⟨S, b⟩\}) \to (e \in (A^{(0 ..^S + 1)}) \land \sum_{a \in (0 ..^S + 1)} e (a) = M)$
197	196	r19.29ffa	$⊢ (φ \land \exists b \in A \exists c \in (A repr (S) (M - b)) e = c \cup \{⟨S, b⟩\}) \to (e \in (A^{(0 ..^S + 1)}) \land \sum_{a \in (0 ..^S + 1)} e (a) = M)$
198	109 197	impbida	$⊢ φ \to ((e \in (A^{(0 ..^S + 1)}) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \leftrightarrow \exists b \in A \exists c \in (A repr (S) (M - b)) e = c \cup \{⟨S, b⟩\})$
199		vex	$⊢ c \in V$
200		snex	$⊢ \{⟨S, b⟩\} \in V$
201	199 200	unex	$⊢ c \cup \{⟨S, b⟩\} \in V$
202	4 201	elrnmpti	$⊢ e \in ran F \leftrightarrow \exists c \in (A repr (S) (M - b)) e = c \cup \{⟨S, b⟩\}$
203	202	rexbii	$⊢ \exists b \in A e \in ran F \leftrightarrow \exists b \in A \exists c \in (A repr (S) (M - b)) e = c \cup \{⟨S, b⟩\}$
204	198 203	bitr4di	$⊢ φ \to ((e \in (A^{(0 ..^S + 1)}) \land \sum_{a \in (0 ..^S + 1)} e (a) = M) \leftrightarrow \exists b \in A e \in ran F)$
205		fveq1	$⊢ c = e \to c (a) = e (a)$
206	205	sumeq2sdv	$⊢ c = e \to \sum_{a \in (0 ..^S + 1)} c (a) = \sum_{a \in (0 ..^S + 1)} e (a)$
207	206	eqeq1d	$⊢ c = e \to (\sum_{a \in (0 ..^S + 1)} c (a) = M \leftrightarrow \sum_{a \in (0 ..^S + 1)} e (a) = M)$
208	207	cbvrabv	$⊢ \{c \in (A^{(0 ..^S + 1)}) \| \sum_{a \in (0 ..^S + 1)} c (a) = M\} = \{e \in (A^{(0 ..^S + 1)}) \| \sum_{a \in (0 ..^S + 1)} e (a) = M\}$
209	208	reqabi	$⊢ e \in \{c \in (A^{(0 ..^S + 1)}) \| \sum_{a \in (0 ..^S + 1)} c (a) = M\} \leftrightarrow (e \in (A^{(0 ..^S + 1)}) \land \sum_{a \in (0 ..^S + 1)} e (a) = M)$
210		eliun	$⊢ e \in ⋃_{b \in A} ran F \leftrightarrow \exists b \in A e \in ran F$
211	204 209 210	3bitr4g	$⊢ φ \to (e \in \{c \in (A^{(0 ..^S + 1)}) \| \sum_{a \in (0 ..^S + 1)} c (a) = M\} \leftrightarrow e \in ⋃_{b \in A} ran F)$
212	211	eqrdv	$⊢ φ \to \{c \in (A^{(0 ..^S + 1)}) \| \sum_{a \in (0 ..^S + 1)} c (a) = M\} = ⋃_{b \in A} ran F$
213	8 212	eqtrd	$⊢ φ \to A repr (S + 1) M = ⋃_{b \in A} ran F$

Metamath Proof Explorer

Theorem reprsuc

Proof