reprinfz1

Description: For the representation of N , it is sufficient to consider nonnegative integers up to N . Remark of Nathanson p. 123 (Contributed by Thierry Arnoux, 13-Dec-2021)

	Ref	Expression
Hypotheses	reprinfz1.n	$⊢ φ \to N \in ℕ_{0}$
	reprinfz1.s	$⊢ φ \to S \in ℕ_{0}$
	reprinfz1.a	$⊢ φ \to A \subseteq ℕ$
Assertion	reprinfz1	$⊢ φ \to A repr (S) N = (A \cap (1 \dots N)) repr (S) N$

Proof

Step	Hyp	Ref	Expression
1		reprinfz1.n	$⊢ φ \to N \in ℕ_{0}$
2		reprinfz1.s	$⊢ φ \to S \in ℕ_{0}$
3		reprinfz1.a	$⊢ φ \to A \subseteq ℕ$
4		nnex	$⊢ ℕ \in V$
5	4	a1i	$⊢ φ \to ℕ \in V$
6	5 3	ssexd	$⊢ φ \to A \in V$
7		ovex	$⊢ (0 ..^S) \in V$
8		elmapg	$⊢ (A \in V \land (0 ..^S) \in V) \to (c \in (A^{(0 ..^S)}) \leftrightarrow c : (0 ..^S) ⟶ A)$
9	6 7 8	sylancl	$⊢ φ \to (c \in (A^{(0 ..^S)}) \leftrightarrow c : (0 ..^S) ⟶ A)$
10	9	biimpa	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to c : (0 ..^S) ⟶ A$
11	10	adantr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to c : (0 ..^S) ⟶ A$
12		elmapfn	$⊢ c \in (A^{(0 ..^S)}) \to c Fn (0 ..^S)$
13	12	ad2antlr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to c Fn (0 ..^S)$
14		simplr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \land \exists b \in (0 ..^S) \neg c (b) \in (1 \dots N)) \to \sum_{a \in (0 ..^S)} c (a) = N$
15	1	nn0red	$⊢ φ \to N \in ℝ$
16	15	ad3antrrr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to N \in ℝ$
17	3	ad3antrrr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to A \subseteq ℕ$
18		simpllr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to c \in (A^{(0 ..^S)})$
19	9	ad3antrrr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to (c \in (A^{(0 ..^S)}) \leftrightarrow c : (0 ..^S) ⟶ A)$
20	18 19	mpbid	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to c : (0 ..^S) ⟶ A$
21		simplr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to b \in (0 ..^S)$
22	20 21	ffvelcdmd	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to c (b) \in A$
23	17 22	sseldd	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to c (b) \in ℕ$
24	23	nnred	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to c (b) \in ℝ$
25		fzofi	$⊢ (0 ..^S) \in Fin$
26	25	a1i	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to (0 ..^S) \in Fin$
27	3	ad4antr	$⊢ ((((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \land a \in (0 ..^S)) \to A \subseteq ℕ$
28	20	ffvelcdmda	$⊢ ((((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \land a \in (0 ..^S)) \to c (a) \in A$
29	27 28	sseldd	$⊢ ((((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \land a \in (0 ..^S)) \to c (a) \in ℕ$
30	29	nnred	$⊢ ((((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \land a \in (0 ..^S)) \to c (a) \in ℝ$
31	26 30	fsumrecl	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to \sum_{a \in (0 ..^S)} c (a) \in ℝ$
32		simpr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to \neg c (b) \in (1 \dots N)$
33	1	nn0zd	$⊢ φ \to N \in ℤ$
34	33	ad3antrrr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to N \in ℤ$
35		fznn	$⊢ N \in ℤ \to (c (b) \in (1 \dots N) \leftrightarrow (c (b) \in ℕ \land c (b) \leq N))$
36	34 35	syl	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to (c (b) \in (1 \dots N) \leftrightarrow (c (b) \in ℕ \land c (b) \leq N))$
37	23	biantrurd	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to (c (b) \leq N \leftrightarrow (c (b) \in ℕ \land c (b) \leq N))$
38	36 37	bitr4d	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to (c (b) \in (1 \dots N) \leftrightarrow c (b) \leq N)$
39	38	notbid	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to (\neg c (b) \in (1 \dots N) \leftrightarrow \neg c (b) \leq N)$
40	32 39	mpbid	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to \neg c (b) \leq N$
41	16 24	ltnled	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to (N < c (b) \leftrightarrow \neg c (b) \leq N)$
42	40 41	mpbird	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to N < c (b)$
43	24	recnd	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to c (b) \in ℂ$
44		fveq2	$⊢ a = b \to c (a) = c (b)$
45	44	sumsn	$⊢ (b \in (0 ..^S) \land c (b) \in ℂ) \to \sum_{a \in \{b\}} c (a) = c (b)$
46	21 43 45	syl2anc	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to \sum_{a \in \{b\}} c (a) = c (b)$
47	29	nnnn0d	$⊢ ((((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \land a \in (0 ..^S)) \to c (a) \in ℕ_{0}$
48		nn0ge0	$⊢ c (a) \in ℕ_{0} \to 0 \leq c (a)$
49	47 48	syl	$⊢ ((((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \land a \in (0 ..^S)) \to 0 \leq c (a)$
50		snssi	$⊢ b \in (0 ..^S) \to \{b\} \subseteq (0 ..^S)$
51	50	ad2antlr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to \{b\} \subseteq (0 ..^S)$
52	26 30 49 51	fsumless	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to \sum_{a \in \{b\}} c (a) \leq \sum_{a \in (0 ..^S)} c (a)$
53	46 52	eqbrtrrd	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to c (b) \leq \sum_{a \in (0 ..^S)} c (a)$
54	16 24 31 42 53	ltletrd	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to N < \sum_{a \in (0 ..^S)} c (a)$
55	16 54	ltned	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to N \neq \sum_{a \in (0 ..^S)} c (a)$
56	55	necomd	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land b \in (0 ..^S)) \land \neg c (b) \in (1 \dots N)) \to \sum_{a \in (0 ..^S)} c (a) \neq N$
57	56	r19.29an	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \exists b \in (0 ..^S) \neg c (b) \in (1 \dots N)) \to \sum_{a \in (0 ..^S)} c (a) \neq N$
58	57	neneqd	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \exists b \in (0 ..^S) \neg c (b) \in (1 \dots N)) \to \neg \sum_{a \in (0 ..^S)} c (a) = N$
59	58	adantlr	$⊢ (((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \land \exists b \in (0 ..^S) \neg c (b) \in (1 \dots N)) \to \neg \sum_{a \in (0 ..^S)} c (a) = N$
60	14 59	pm2.65da	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to \neg \exists b \in (0 ..^S) \neg c (b) \in (1 \dots N)$
61		dfral2	$⊢ \forall b \in (0 ..^S) c (b) \in (1 \dots N) \leftrightarrow \neg \exists b \in (0 ..^S) \neg c (b) \in (1 \dots N)$
62	60 61	sylibr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to \forall b \in (0 ..^S) c (b) \in (1 \dots N)$
63	44	eleq1d	$⊢ a = b \to (c (a) \in (1 \dots N) \leftrightarrow c (b) \in (1 \dots N))$
64	63	cbvralvw	$⊢ \forall a \in (0 ..^S) c (a) \in (1 \dots N) \leftrightarrow \forall b \in (0 ..^S) c (b) \in (1 \dots N)$
65	62 64	sylibr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to \forall a \in (0 ..^S) c (a) \in (1 \dots N)$
66	13 65	jca	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to (c Fn (0 ..^S) \land \forall a \in (0 ..^S) c (a) \in (1 \dots N))$
67		ffnfv	$⊢ c : (0 ..^S) ⟶ (1 \dots N) \leftrightarrow (c Fn (0 ..^S) \land \forall a \in (0 ..^S) c (a) \in (1 \dots N))$
68	66 67	sylibr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to c : (0 ..^S) ⟶ (1 \dots N)$
69	11 68	jca	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to (c : (0 ..^S) ⟶ A \land c : (0 ..^S) ⟶ (1 \dots N))$
70		fin	$⊢ c : (0 ..^S) ⟶ A \cap (1 \dots N) \leftrightarrow (c : (0 ..^S) ⟶ A \land c : (0 ..^S) ⟶ (1 \dots N))$
71	69 70	sylibr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to c : (0 ..^S) ⟶ A \cap (1 \dots N)$
72		ovex	$⊢ (1 \dots N) \in V$
73	72	inex2	$⊢ A \cap (1 \dots N) \in V$
74	73 7	elmap	$⊢ c \in ({(A \cap (1 \dots N))}^{(0 ..^S)}) \leftrightarrow c : (0 ..^S) ⟶ A \cap (1 \dots N)$
75	71 74	sylibr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land \sum_{a \in (0 ..^S)} c (a) = N) \to c \in ({(A \cap (1 \dots N))}^{(0 ..^S)})$
76	75	anasss	$⊢ (φ \land (c \in (A^{(0 ..^S)}) \land \sum_{a \in (0 ..^S)} c (a) = N)) \to c \in ({(A \cap (1 \dots N))}^{(0 ..^S)})$
77	76	rabss3d	$⊢ φ \to \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = N\} \subseteq \{c \in ({(A \cap (1 \dots N))}^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = N\}$
78	3 33 2	reprval	$⊢ φ \to A repr (S) N = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = N\}$
79		inss1	$⊢ A \cap (1 \dots N) \subseteq A$
80	79	a1i	$⊢ φ \to A \cap (1 \dots N) \subseteq A$
81	80 3	sstrd	$⊢ φ \to A \cap (1 \dots N) \subseteq ℕ$
82	81 33 2	reprval	$⊢ φ \to (A \cap (1 \dots N)) repr (S) N = \{c \in ({(A \cap (1 \dots N))}^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = N\}$
83	77 78 82	3sstr4d	$⊢ φ \to A repr (S) N \subseteq (A \cap (1 \dots N)) repr (S) N$
84	3 33 2 80	reprss	$⊢ φ \to (A \cap (1 \dots N)) repr (S) N \subseteq A repr (S) N$
85	83 84	eqssd	$⊢ φ \to A repr (S) N = (A \cap (1 \dots N)) repr (S) N$

Metamath Proof Explorer

Theorem reprinfz1

Proof