Metamath Proof Explorer


Theorem 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 φA
reprval.m φM
reprval.s φS0
reprlt.1 φM<S
Assertion reprlt φAreprSM=

Proof

Step Hyp Ref Expression
1 reprval.a φA
2 reprval.m φM
3 reprval.s φS0
4 reprlt.1 φM<S
5 1 2 3 reprval φAreprSM=cA0..^S|a0..^Sca=M
6 2 zred φM
7 6 adantr φcA0..^SM
8 3 nn0red φS
9 8 adantr φcA0..^SS
10 fzofi 0..^SFin
11 10 a1i φcA0..^S0..^SFin
12 nnssre
13 12 a1i φ
14 1 13 sstrd φA
15 14 ad2antrr φcA0..^Sa0..^SA
16 nnex V
17 16 a1i φV
18 17 1 ssexd φAV
19 18 adantr φcA0..^SAV
20 10 elexi 0..^SV
21 20 a1i φcA0..^S0..^SV
22 simpr φcA0..^ScA0..^S
23 elmapg AV0..^SVcA0..^Sc:0..^SA
24 23 biimpa AV0..^SVcA0..^Sc:0..^SA
25 19 21 22 24 syl21anc φcA0..^Sc:0..^SA
26 25 adantr φcA0..^Sa0..^Sc:0..^SA
27 simpr φcA0..^Sa0..^Sa0..^S
28 26 27 ffvelcdmd φcA0..^Sa0..^ScaA
29 15 28 sseldd φcA0..^Sa0..^Sca
30 11 29 fsumrecl φcA0..^Sa0..^Sca
31 4 adantr φcA0..^SM<S
32 ax-1cn 1
33 fsumconst 0..^SFin1a0..^S1=0..^S1
34 10 32 33 mp2an a0..^S1=0..^S1
35 hashcl 0..^SFin0..^S0
36 10 35 ax-mp 0..^S0
37 36 nn0cni 0..^S
38 37 mulridi 0..^S1=0..^S
39 34 38 eqtri a0..^S1=0..^S
40 hashfzo0 S00..^S=S
41 3 40 syl φ0..^S=S
42 39 41 eqtrid φa0..^S1=S
43 42 adantr φcA0..^Sa0..^S1=S
44 1red φcA0..^Sa0..^S1
45 1 ad2antrr φcA0..^Sa0..^SA
46 45 28 sseldd φcA0..^Sa0..^Sca
47 nnge1 ca1ca
48 46 47 syl φcA0..^Sa0..^S1ca
49 11 44 29 48 fsumle φcA0..^Sa0..^S1a0..^Sca
50 43 49 eqbrtrrd φcA0..^SSa0..^Sca
51 7 9 30 31 50 ltletrd φcA0..^SM<a0..^Sca
52 7 51 ltned φcA0..^SMa0..^Sca
53 52 necomd φcA0..^Sa0..^ScaM
54 53 neneqd φcA0..^S¬a0..^Sca=M
55 54 ralrimiva φcA0..^S¬a0..^Sca=M
56 rabeq0 cA0..^S|a0..^Sca=M=cA0..^S¬a0..^Sca=M
57 55 56 sylibr φcA0..^S|a0..^Sca=M=
58 5 57 eqtrd φAreprSM=