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 ) = (/) )