Metamath Proof Explorer

Theorem 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 
|- ( ph -> N e. NN0 )
reprgt.a 
|- ( ph -> A C_ ( 1 ... N ) )
reprgt.m 
|- ( ph -> M e. ZZ )
reprgt.s 
|- ( ph -> S e. NN0 )
reprgt.1 
|- ( ph -> ( S x. N ) < M )
Assertion reprgt 
|- ( ph -> ( A ( repr ` S ) M ) = (/) )

Proof

Step Hyp Ref Expression
1 reprgt.n 
 |-  ( ph -> N e. NN0 )
2 reprgt.a 
 |-  ( ph -> A C_ ( 1 ... N ) )
3 reprgt.m 
 |-  ( ph -> M e. ZZ )
4 reprgt.s 
 |-  ( ph -> S e. NN0 )
5 reprgt.1 
 |-  ( ph -> ( S x. N ) < M )
6 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
7 2 6 sstrdi 
 |-  ( ph -> A C_ NN )
8 7 3 4 reprval 
 |-  ( ph -> ( A ( repr ` S ) M ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } )
9 fzofi 
 |-  ( 0 ..^ S ) e. Fin
10 9 a1i 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( 0 ..^ S ) e. Fin )
11 nnssre 
 |-  NN C_ RR
12 7 11 sstrdi 
 |-  ( ph -> A C_ RR )
13 12 ralrimivw 
 |-  ( ph -> A. a e. ( 0 ..^ S ) A C_ RR )
14 13 ralrimivw 
 |-  ( ph -> A. c e. ( A ^m ( 0 ..^ S ) ) A. a e. ( 0 ..^ S ) A C_ RR )
15 14 r19.21bi 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> A. a e. ( 0 ..^ S ) A C_ RR )
16 15 r19.21bi 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ RR )
17 ovex 
 |-  ( 1 ... N ) e. _V
18 17 a1i 
 |-  ( ph -> ( 1 ... N ) e. _V )
19 18 2 ssexd 
 |-  ( ph -> A e. _V )
20 19 adantr 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> A e. _V )
21 9 elexi 
 |-  ( 0 ..^ S ) e. _V
22 21 a1i 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( 0 ..^ S ) e. _V )
23 simpr 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c e. ( A ^m ( 0 ..^ S ) ) )
24 elmapg 
 |-  ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) )
25 24 biimpa 
 |-  ( ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c : ( 0 ..^ S ) --> A )
26 20 22 23 25 syl21anc 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c : ( 0 ..^ S ) --> A )
27 26 adantr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> c : ( 0 ..^ S ) --> A )
28 simpr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> a e. ( 0 ..^ S ) )
29 27 28 ffvelcdmd 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. A )
30 16 29 sseldd 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. RR )
31 10 30 fsumrecl 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) e. RR )
32 4 nn0red 
 |-  ( ph -> S e. RR )
33 32 adantr 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> S e. RR )
34 1 nn0red 
 |-  ( ph -> N e. RR )
35 34 adantr 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> N e. RR )
36 33 35 remulcld 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( S x. N ) e. RR )
37 3 zred 
 |-  ( ph -> M e. RR )
38 37 adantr 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> M e. RR )
39 34 ad2antrr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> N e. RR )
40 2 ad2antrr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ ( 1 ... N ) )
41 40 29 sseldd 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. ( 1 ... N ) )
42 elfzle2 
 |-  ( ( c ` a ) e. ( 1 ... N ) -> ( c ` a ) <_ N )
43 41 42 syl 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) <_ N )
44 10 30 39 43 fsumle 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) <_ sum_ a e. ( 0 ..^ S ) N )
45 34 recnd 
 |-  ( ph -> N e. CC )
46 fsumconst 
 |-  ( ( ( 0 ..^ S ) e. Fin /\ N e. CC ) -> sum_ a e. ( 0 ..^ S ) N = ( ( # ` ( 0 ..^ S ) ) x. N ) )
47 9 45 46 sylancr 
 |-  ( ph -> sum_ a e. ( 0 ..^ S ) N = ( ( # ` ( 0 ..^ S ) ) x. N ) )
48 hashfzo0 
 |-  ( S e. NN0 -> ( # ` ( 0 ..^ S ) ) = S )
49 4 48 syl 
 |-  ( ph -> ( # ` ( 0 ..^ S ) ) = S )
50 49 oveq1d 
 |-  ( ph -> ( ( # ` ( 0 ..^ S ) ) x. N ) = ( S x. N ) )
51 47 50 eqtrd 
 |-  ( ph -> sum_ a e. ( 0 ..^ S ) N = ( S x. N ) )
52 51 adantr 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) N = ( S x. N ) )
53 44 52 breqtrd 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) <_ ( S x. N ) )
54 5 adantr 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> ( S x. N ) < M )
55 31 36 38 53 54 lelttrd 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) < M )
56 31 55 ltned 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) =/= M )
57 56 neneqd 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M )
58 57 ralrimiva 
 |-  ( ph -> A. c e. ( A ^m ( 0 ..^ S ) ) -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = M )
59 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 )
60 58 59 sylibr 
 |-  ( ph -> { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = M } = (/) )
61 8 60 eqtrd 
 |-  ( ph -> ( A ( repr ` S ) M ) = (/) )