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
|- ( ph -> A C_ NN )
reprval.m
|- ( ph -> M e. ZZ )
reprval.s
|- ( ph -> S e. NN0 )
reprlt.1
|- ( ph -> M < S )
Assertion reprlt
|- ( ph -> ( A ( repr ` S ) M ) = (/) )

Proof

Step Hyp Ref Expression
1 reprval.a
 |-  ( ph -> A C_ NN )
2 reprval.m
 |-  ( ph -> M e. ZZ )
3 reprval.s
 |-  ( ph -> S e. NN0 )
4 reprlt.1
 |-  ( ph -> M < S )
5 1 2 3 reprval
 |-  ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
6 2 zred
 |-  ( ph -> M e. RR )
7 6 adantr
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M e. RR )
8 3 nn0red
 |-  ( ph -> S e. RR )
9 8 adantr
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> S e. RR )
10 fzofi
 |-  ( 0 ..^ S ) e. Fin
11 10 a1i
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( 0 ..^ S ) e. Fin )
12 nnssre
 |-  NN C_ RR
13 12 a1i
 |-  ( ph -> NN C_ RR )
14 1 13 sstrd
 |-  ( ph -> A C_ RR )
15 14 ad2antrr
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ RR )
16 nnex
 |-  NN e. _V
17 16 a1i
 |-  ( ph -> NN e. _V )
18 17 1 ssexd
 |-  ( ph -> A e. _V )
19 18 adantr
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> A e. _V )
20 10 elexi
 |-  ( 0 ..^ S ) e. _V
21 20 a1i
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( 0 ..^ S ) e. _V )
22 simpr
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c e. ( A ^m ( 0 ..^ S ) ) )
23 elmapg
 |-  ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) )
24 23 biimpa
 |-  ( ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c : ( 0 ..^ S ) --> A )
25 19 21 22 24 syl21anc
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c : ( 0 ..^ S ) --> A )
26 25 adantr
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> c : ( 0 ..^ S ) --> A )
27 simpr
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
28 26 27 ffvelrnd
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. A )
29 15 28 sseldd
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. RR )
30 11 29 fsumrecl
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) e. RR )
31 4 adantr
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M < S )
32 ax-1cn
 |-  1 e. CC
33 fsumconst
 |-  ( ( ( 0 ..^ S ) e. Fin /\ 1 e. CC ) -> sum_ a e. ( 0 ..^ S ) 1 = ( ( # ` ( 0 ..^ S ) ) x. 1 ) )
34 10 32 33 mp2an
 |-  sum_ a e. ( 0 ..^ S ) 1 = ( ( # ` ( 0 ..^ S ) ) x. 1 )
35 hashcl
 |-  ( ( 0 ..^ S ) e. Fin -> ( # ` ( 0 ..^ S ) ) e. NN0 )
36 10 35 ax-mp
 |-  ( # ` ( 0 ..^ S ) ) e. NN0
37 36 nn0cni
 |-  ( # ` ( 0 ..^ S ) ) e. CC
38 37 mulid1i
 |-  ( ( # ` ( 0 ..^ S ) ) x. 1 ) = ( # ` ( 0 ..^ S ) )
39 34 38 eqtri
 |-  sum_ a e. ( 0 ..^ S ) 1 = ( # ` ( 0 ..^ S ) )
40 hashfzo0
 |-  ( S e. NN0 -> ( # ` ( 0 ..^ S ) ) = S )
41 3 40 syl
 |-  ( ph -> ( # ` ( 0 ..^ S ) ) = S )
42 39 41 syl5eq
 |-  ( ph -> sum_ a e. ( 0 ..^ S ) 1 = S )
43 42 adantr
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) 1 = S )
44 1red
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> 1 e. RR )
45 1 ad2antrr
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ NN )
46 45 28 sseldd
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN )
47 nnge1
 |-  ( ( c ` a ) e. NN -> 1 <_ ( c ` a ) )
48 46 47 syl
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> 1 <_ ( c ` a ) )
49 11 44 29 48 fsumle
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) 1 <_ sum_ a e. ( 0 ..^ S ) ( c ` a ) )
50 43 49 eqbrtrrd
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> S <_ sum_ a e. ( 0 ..^ S ) ( c ` a ) )
51 7 9 30 31 50 ltletrd
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M < sum_ a e. ( 0 ..^ S ) ( c ` a ) )
52 7 51 ltned
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M =/= sum_ a e. ( 0 ..^ S ) ( c ` a ) )
53 52 necomd
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) =/= M )
54 53 neneqd
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M )
55 54 ralrimiva
 |-  ( ph -> A. c e. ( A ^m ( 0 ..^ S ) ) -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M )
56 rabeq0
 |-  ( { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } = (/) <-> A. c e. ( A ^m ( 0 ..^ S ) ) -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M )
57 55 56 sylibr
 |-  ( ph -> { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } = (/) )
58 5 57 eqtrd
 |-  ( ph -> ( A ( repr ` S ) M ) = (/) )