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 | |
|
reprval.m | |
||
reprval.s | |
||
reprlt.1 | |
||
Assertion | reprlt | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reprval.a | |
|
2 | reprval.m | |
|
3 | reprval.s | |
|
4 | reprlt.1 | |
|
5 | 1 2 3 | reprval | |
6 | 2 | zred | |
7 | 6 | adantr | |
8 | 3 | nn0red | |
9 | 8 | adantr | |
10 | fzofi | |
|
11 | 10 | a1i | |
12 | nnssre | |
|
13 | 12 | a1i | |
14 | 1 13 | sstrd | |
15 | 14 | ad2antrr | |
16 | nnex | |
|
17 | 16 | a1i | |
18 | 17 1 | ssexd | |
19 | 18 | adantr | |
20 | 10 | elexi | |
21 | 20 | a1i | |
22 | simpr | |
|
23 | elmapg | |
|
24 | 23 | biimpa | |
25 | 19 21 22 24 | syl21anc | |
26 | 25 | adantr | |
27 | simpr | |
|
28 | 26 27 | ffvelcdmd | |
29 | 15 28 | sseldd | |
30 | 11 29 | fsumrecl | |
31 | 4 | adantr | |
32 | ax-1cn | |
|
33 | fsumconst | |
|
34 | 10 32 33 | mp2an | |
35 | hashcl | |
|
36 | 10 35 | ax-mp | |
37 | 36 | nn0cni | |
38 | 37 | mulridi | |
39 | 34 38 | eqtri | |
40 | hashfzo0 | |
|
41 | 3 40 | syl | |
42 | 39 41 | eqtrid | |
43 | 42 | adantr | |
44 | 1red | |
|
45 | 1 | ad2antrr | |
46 | 45 28 | sseldd | |
47 | nnge1 | |
|
48 | 46 47 | syl | |
49 | 11 44 29 48 | fsumle | |
50 | 43 49 | eqbrtrrd | |
51 | 7 9 30 31 50 | ltletrd | |
52 | 7 51 | ltned | |
53 | 52 | necomd | |
54 | 53 | neneqd | |
55 | 54 | ralrimiva | |
56 | rabeq0 | |
|
57 | 55 56 | sylibr | |
58 | 5 57 | eqtrd | |