reprgt

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

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

Proof

Step	Hyp	Ref	Expression
1		reprgt.n	$⊢ φ \to N \in ℕ_{0}$
2		reprgt.a	$⊢ φ \to A \subseteq (1 \dots N)$
3		reprgt.m	$⊢ φ \to M \in ℤ$
4		reprgt.s	$⊢ φ \to S \in ℕ_{0}$
5		reprgt.1	$⊢ φ \to S \cdot N < M$
6		fz1ssnn	$⊢ (1 \dots N) \subseteq ℕ$
7	2 6	sstrdi	$⊢ φ \to A \subseteq ℕ$
8	7 3 4	reprval	$⊢ φ \to A repr (S) M = \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\}$
9		fzofi	$⊢ (0 ..^S) \in Fin$
10	9	a1i	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to (0 ..^S) \in Fin$
11		nnssre	$⊢ ℕ \subseteq ℝ$
12	7 11	sstrdi	$⊢ φ \to A \subseteq ℝ$
13	12	ralrimivw	$⊢ φ \to \forall a \in (0 ..^S) A \subseteq ℝ$
14	13	ralrimivw	$⊢ φ \to \forall c \in (A^{(0 ..^S)}) \forall a \in (0 ..^S) A \subseteq ℝ$
15	14	r19.21bi	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \forall a \in (0 ..^S) A \subseteq ℝ$
16	15	r19.21bi	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to A \subseteq ℝ$
17		ovex	$⊢ (1 \dots N) \in V$
18	17	a1i	$⊢ φ \to (1 \dots N) \in V$
19	18 2	ssexd	$⊢ φ \to A \in V$
20	19	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to A \in V$
21	9	elexi	$⊢ (0 ..^S) \in V$
22	21	a1i	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to (0 ..^S) \in V$
23		simpr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to c \in (A^{(0 ..^S)})$
24		elmapg	$⊢ (A \in V \land (0 ..^S) \in V) \to (c \in (A^{(0 ..^S)}) \leftrightarrow c : (0 ..^S) ⟶ A)$
25	24	biimpa	$⊢ ((A \in V \land (0 ..^S) \in V) \land c \in (A^{(0 ..^S)})) \to c : (0 ..^S) ⟶ A$
26	20 22 23 25	syl21anc	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to c : (0 ..^S) ⟶ A$
27	26	adantr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c : (0 ..^S) ⟶ A$
28		simpr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to a \in (0 ..^S)$
29	27 28	ffvelrnd	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c (a) \in A$
30	16 29	sseldd	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c (a) \in ℝ$
31	10 30	fsumrecl	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} c (a) \in ℝ$
32	4	nn0red	$⊢ φ \to S \in ℝ$
33	32	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to S \in ℝ$
34	1	nn0red	$⊢ φ \to N \in ℝ$
35	34	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to N \in ℝ$
36	33 35	remulcld	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to S \cdot N \in ℝ$
37	3	zred	$⊢ φ \to M \in ℝ$
38	37	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to M \in ℝ$
39	34	ad2antrr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to N \in ℝ$
40	2	ad2antrr	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to A \subseteq (1 \dots N)$
41	40 29	sseldd	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c (a) \in (1 \dots N)$
42		elfzle2	$⊢ c (a) \in (1 \dots N) \to c (a) \leq N$
43	41 42	syl	$⊢ ((φ \land c \in (A^{(0 ..^S)})) \land a \in (0 ..^S)) \to c (a) \leq N$
44	10 30 39 43	fsumle	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} c (a) \leq \sum_{a \in (0 ..^S)} N$
45	34	recnd	$⊢ φ \to N \in ℂ$
46		fsumconst	$⊢ ((0 ..^S) \in Fin \land N \in ℂ) \to \sum_{a \in (0 ..^S)} N = \|(0 ..^S)\| \cdot N$
47	9 45 46	sylancr	$⊢ φ \to \sum_{a \in (0 ..^S)} N = \|(0 ..^S)\| \cdot N$
48		hashfzo0	$⊢ S \in ℕ_{0} \to \|(0 ..^S)\| = S$
49	4 48	syl	$⊢ φ \to \|(0 ..^S)\| = S$
50	49	oveq1d	$⊢ φ \to \|(0 ..^S)\| \cdot N = S \cdot N$
51	47 50	eqtrd	$⊢ φ \to \sum_{a \in (0 ..^S)} N = S \cdot N$
52	51	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} N = S \cdot N$
53	44 52	breqtrd	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} c (a) \leq S \cdot N$
54	5	adantr	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to S \cdot N < M$
55	31 36 38 53 54	lelttrd	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} c (a) < M$
56	31 55	ltned	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \sum_{a \in (0 ..^S)} c (a) \neq M$
57	56	neneqd	$⊢ (φ \land c \in (A^{(0 ..^S)})) \to \neg \sum_{a \in (0 ..^S)} c (a) = M$
58	57	ralrimiva	$⊢ φ \to \forall c \in (A^{(0 ..^S)}) \neg \sum_{a \in (0 ..^S)} c (a) = M$
59		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$
60	58 59	sylibr	$⊢ φ \to \{c \in (A^{(0 ..^S)}) \| \sum_{a \in (0 ..^S)} c (a) = M\} = \emptyset$
61	8 60	eqtrd	$⊢ φ \to A repr (S) M = \emptyset$

Metamath Proof Explorer

Theorem reprgt

Proof