reprlt

Description: There are no representations of M with more than M terms. Remark of Nathanson p. 123. (Contributed by Thierry Arnoux, 7-Dec-2021)

	Ref	Expression
Hypotheses	reprval.a	$⊢ φ \to A \subseteq ℕ$
	reprval.m	$⊢ φ \to M \in ℤ$
	reprval.s	$⊢ φ \to S \in ℕ_{0}$
	reprlt.1	$⊢ φ \to M < S$
Assertion	reprlt	$⊢ φ \to A repr (S) M = \emptyset$

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		reprlt.1	$⊢ φ \to M < S$
5	1 2 3	reprval	$⊢ φ \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
6	2	zred	$⊢ φ \to M \in ℝ$
7	6	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to M \in ℝ$
8	3	nn0red	$⊢ φ \to S \in ℝ$
9	8	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to S \in ℝ$
10		fzofi	$⊢ (0 ..^S) \in Fin$
11	10	a1i	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to (0 ..^S) \in Fin$
12		nnssre	$⊢ ℕ \subseteq ℝ$
13	12	a1i	$⊢ φ \to ℕ \subseteq ℝ$
14	1 13	sstrd	$⊢ φ \to A \subseteq ℝ$
15	14	ad2antrr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to A \subseteq ℝ$
16		nnex	$⊢ ℕ \in V$
17	16	a1i	$⊢ φ \to ℕ \in V$
18	17 1	ssexd	$⊢ φ \to A \in V$
19	18	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to A \in V$
20	10	elexi	$⊢ (0 ..^S) \in V$
21	20	a1i	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to (0 ..^S) \in V$
22		simpr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to c \in (A^{(0 ..^S)})$
23		elmapg	$⊢ (A \in V \land (0 ..^S) \in V) \to (c \in (A^{(0 ..^S)}) \leftrightarrow c : (0 ..^S) ⟶ A)$
24	23	biimpa	$⊢ ((A \in V \land (0 ..^S) \in V) \land c \in (A^{(0 ..^S)})) \to c : (0 ..^S) ⟶ A$
25	19 21 22 24	syl21anc	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to c : (0 ..^S) ⟶ A$
26	25	adantr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c : (0 ..^S) ⟶ A$
27		simpr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
28	26 27	ffvelcdmd	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c (a) \in A$
29	15 28	sseldd	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c (a) \in ℝ$
30	11 29	fsumrecl	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} c (a) \in ℝ$
31	4	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to M < S$
32		ax-1cn	$⊢ 1 \in ℂ$
33		fsumconst	$⊢ ((0 ..^S) \in Fin \land 1 \in ℂ) \to \sum_{a \in (0 ..^S)} 1 = \|(0 ..^S)\| \cdot 1$
34	10 32 33	mp2an	$⊢ \sum_{a \in (0 ..^S)} 1 = \|(0 ..^S)\| \cdot 1$
35		hashcl	$⊢ (0 ..^S) \in Fin \to \|(0 ..^S)\| \in ℕ_{0}$
36	10 35	ax-mp	$⊢ \|(0 ..^S)\| \in ℕ_{0}$
37	36	nn0cni	$⊢ \|(0 ..^S)\| \in ℂ$
38	37	mulridi	$⊢ \|(0 ..^S)\| \cdot 1 = \|(0 ..^S)\|$
39	34 38	eqtri	$⊢ \sum_{a \in (0 ..^S)} 1 = \|(0 ..^S)\|$
40		hashfzo0	$⊢ S \in ℕ_{0} \to \|(0 ..^S)\| = S$
41	3 40	syl	$⊢ φ \to \|(0 ..^S)\| = S$
42	39 41	eqtrid	$⊢ φ \to \sum_{a \in (0 ..^S)} 1 = S$
43	42	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} 1 = S$
44		1red	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to 1 \in ℝ$
45	1	ad2antrr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to A \subseteq ℕ$
46	45 28	sseldd	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c (a) \in ℕ$
47		nnge1	$⊢ c (a) \in ℕ \to 1 \leq c (a)$
48	46 47	syl	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to 1 \leq c (a)$
49	11 44 29 48	fsumle	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} 1 \leq \sum_{a \in (0 ..^S)} c (a)$
50	43 49	eqbrtrrd	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to S \leq \sum_{a \in (0 ..^S)} c (a)$
51	7 9 30 31 50	ltletrd	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to M < \sum_{a \in (0 ..^S)} c (a)$
52	7 51	ltned	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to M \neq \sum_{a \in (0 ..^S)} c (a)$
53	52	necomd	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} c (a) \neq M$
54	53	neneqd	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \neg \sum_{a \in (0 ..^S)} c (a) = M$
55	54	ralrimiva	$⊢ φ \to \forall c \in (A^{(0 ..^S)}) \neg \sum_{a \in (0 ..^S)} c (a) = M$
56		rabeq0	$⊢ \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} = \emptyset \leftrightarrow \forall c \in (A^{(0 ..^S)}) \neg \sum_{a \in (0 ..^S)} c (a) = M$
57	55 56	sylibr	$⊢ φ \to \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} = \emptyset$
58	5 57	eqtrd	$⊢ φ \to A repr (S) M = \emptyset$

Metamath Proof Explorer

Theorem reprlt

Proof