Metamath Proof Explorer

Theorem reprinfz1

Description: For the representation of N , it is sufficient to consider nonnegative integers up to N . Remark of Nathanson p. 123 (Contributed by Thierry Arnoux, 13-Dec-2021)

Ref Expression
Hypotheses reprinfz1.n 
|- ( ph -> N e. NN0 )
reprinfz1.s 
|- ( ph -> S e. NN0 )
reprinfz1.a 
|- ( ph -> A C_ NN )
Assertion reprinfz1 
|- ( ph -> ( A ( repr ` S ) N ) = ( ( A i^i ( 1 ... N ) ) ( repr ` S ) N ) )

Proof

Step Hyp Ref Expression
1 reprinfz1.n 
 |-  ( ph -> N e. NN0 )
2 reprinfz1.s 
 |-  ( ph -> S e. NN0 )
3 reprinfz1.a 
 |-  ( ph -> A C_ NN )
4 nnex 
 |-  NN e. _V
5 4 a1i 
 |-  ( ph -> NN e. _V )
6 5 3 ssexd 
 |-  ( ph -> A e. _V )
7 ovex 
 |-  ( 0 ..^ S ) e. _V
8 elmapg 
 |-  ( ( A e. _V /\ ( 0 ..^ S ) e. _V ) -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) )
9 6 7 8 sylancl 
 |-  ( ph -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) )
10 9 biimpa 
 |-  ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) -> c : ( 0 ..^ S ) --> A )
11 10 adantr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> c : ( 0 ..^ S ) --> A )
12 elmapfn 
 |-  ( c e. ( A ^m ( 0 ..^ S ) ) -> c Fn ( 0 ..^ S ) )
13 12 ad2antlr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> c Fn ( 0 ..^ S ) )
14 simplr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) /\ E. b e. ( 0 ..^ S ) -. ( c ` b ) e. ( 1 ... N ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) = N )
15 1 nn0red 
 |-  ( ph -> N e. RR )
16 15 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> N e. RR )
17 3 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> A C_ NN )
18 simpllr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> c e. ( A ^m ( 0 ..^ S ) ) )
19 9 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( c e. ( A ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> A ) )
20 18 19 mpbid 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> c : ( 0 ..^ S ) --> A )
21 simplr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> b e. ( 0 ..^ S ) )
22 20 21 ffvelrnd 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( c ` b ) e. A )
23 17 22 sseldd 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( c ` b ) e. NN )
24 23 nnred 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( c ` b ) e. RR )
25 fzofi 
 |-  ( 0 ..^ S ) e. Fin
26 25 a1i 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( 0 ..^ S ) e. Fin )
27 3 ad4antr 
 |-  ( ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) /\ a e. ( 0 ..^ S ) ) -> A C_ NN )
28 20 ffvelrnda 
 |-  ( ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. A )
29 27 28 sseldd 
 |-  ( ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN )
30 29 nnred 
 |-  ( ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. RR )
31 26 30 fsumrecl 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) e. RR )
32 simpr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> -. ( c ` b ) e. ( 1 ... N ) )
33 1 nn0zd 
 |-  ( ph -> N e. ZZ )
34 33 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> N e. ZZ )
35 fznn 
 |-  ( N e. ZZ -> ( ( c ` b ) e. ( 1 ... N ) <-> ( ( c ` b ) e. NN /\ ( c ` b ) <_ N ) ) )
36 34 35 syl 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( ( c ` b ) e. ( 1 ... N ) <-> ( ( c ` b ) e. NN /\ ( c ` b ) <_ N ) ) )
37 23 biantrurd 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( ( c ` b ) <_ N <-> ( ( c ` b ) e. NN /\ ( c ` b ) <_ N ) ) )
38 36 37 bitr4d 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( ( c ` b ) e. ( 1 ... N ) <-> ( c ` b ) <_ N ) )
39 38 notbid 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( -. ( c ` b ) e. ( 1 ... N ) <-> -. ( c ` b ) <_ N ) )
40 32 39 mpbid 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> -. ( c ` b ) <_ N )
41 16 24 ltnled 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( N < ( c ` b ) <-> -. ( c ` b ) <_ N ) )
42 40 41 mpbird 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> N < ( c ` b ) )
43 24 recnd 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( c ` b ) e. CC )
44 fveq2 
 |-  ( a = b -> ( c ` a ) = ( c ` b ) )
45 44 sumsn 
 |-  ( ( b e. ( 0 ..^ S ) /\ ( c ` b ) e. CC ) -> sum_ a e. { b } ( c ` a ) = ( c ` b ) )
46 21 43 45 syl2anc 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> sum_ a e. { b } ( c ` a ) = ( c ` b ) )
47 29 nnnn0d 
 |-  ( ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) /\ a e. ( 0 ..^ S ) ) -> ( c ` a ) e. NN0 )
48 nn0ge0 
 |-  ( ( c ` a ) e. NN0 -> 0 <_ ( c ` a ) )
49 47 48 syl 
 |-  ( ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) /\ a e. ( 0 ..^ S ) ) -> 0 <_ ( c ` a ) )
50 snssi 
 |-  ( b e. ( 0 ..^ S ) -> { b } C_ ( 0 ..^ S ) )
51 50 ad2antlr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> { b } C_ ( 0 ..^ S ) )
52 26 30 49 51 fsumless 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> sum_ a e. { b } ( c ` a ) <_ sum_ a e. ( 0 ..^ S ) ( c ` a ) )
53 46 52 eqbrtrrd 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> ( c ` b ) <_ sum_ a e. ( 0 ..^ S ) ( c ` a ) )
54 16 24 31 42 53 ltletrd 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> N < sum_ a e. ( 0 ..^ S ) ( c ` a ) )
55 16 54 ltned 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> N =/= sum_ a e. ( 0 ..^ S ) ( c ` a ) )
56 55 necomd 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ b e. ( 0 ..^ S ) ) /\ -. ( c ` b ) e. ( 1 ... N ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) =/= N )
57 56 r19.29an 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ E. b e. ( 0 ..^ S ) -. ( c ` b ) e. ( 1 ... N ) ) -> sum_ a e. ( 0 ..^ S ) ( c ` a ) =/= N )
58 57 neneqd 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ E. b e. ( 0 ..^ S ) -. ( c ` b ) e. ( 1 ... N ) ) -> -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = N )
59 58 adantlr 
 |-  ( ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) /\ E. b e. ( 0 ..^ S ) -. ( c ` b ) e. ( 1 ... N ) ) -> -. sum_ a e. ( 0 ..^ S ) ( c ` a ) = N )
60 14 59 pm2.65da 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> -. E. b e. ( 0 ..^ S ) -. ( c ` b ) e. ( 1 ... N ) )
61 dfral2 
 |-  ( A. b e. ( 0 ..^ S ) ( c ` b ) e. ( 1 ... N ) <-> -. E. b e. ( 0 ..^ S ) -. ( c ` b ) e. ( 1 ... N ) )
62 60 61 sylibr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> A. b e. ( 0 ..^ S ) ( c ` b ) e. ( 1 ... N ) )
63 44 eleq1d 
 |-  ( a = b -> ( ( c ` a ) e. ( 1 ... N ) <-> ( c ` b ) e. ( 1 ... N ) ) )
64 63 cbvralvw 
 |-  ( A. a e. ( 0 ..^ S ) ( c ` a ) e. ( 1 ... N ) <-> A. b e. ( 0 ..^ S ) ( c ` b ) e. ( 1 ... N ) )
65 62 64 sylibr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> A. a e. ( 0 ..^ S ) ( c ` a ) e. ( 1 ... N ) )
66 13 65 jca 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> ( c Fn ( 0 ..^ S ) /\ A. a e. ( 0 ..^ S ) ( c ` a ) e. ( 1 ... N ) ) )
67 ffnfv 
 |-  ( c : ( 0 ..^ S ) --> ( 1 ... N ) <-> ( c Fn ( 0 ..^ S ) /\ A. a e. ( 0 ..^ S ) ( c ` a ) e. ( 1 ... N ) ) )
68 66 67 sylibr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> c : ( 0 ..^ S ) --> ( 1 ... N ) )
69 11 68 jca 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> ( c : ( 0 ..^ S ) --> A /\ c : ( 0 ..^ S ) --> ( 1 ... N ) ) )
70 fin 
 |-  ( c : ( 0 ..^ S ) --> ( A i^i ( 1 ... N ) ) <-> ( c : ( 0 ..^ S ) --> A /\ c : ( 0 ..^ S ) --> ( 1 ... N ) ) )
71 69 70 sylibr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> c : ( 0 ..^ S ) --> ( A i^i ( 1 ... N ) ) )
72 ovex 
 |-  ( 1 ... N ) e. _V
73 72 inex2 
 |-  ( A i^i ( 1 ... N ) ) e. _V
74 73 7 elmap 
 |-  ( c e. ( ( A i^i ( 1 ... N ) ) ^m ( 0 ..^ S ) ) <-> c : ( 0 ..^ S ) --> ( A i^i ( 1 ... N ) ) )
75 71 74 sylibr 
 |-  ( ( ( ph /\ c e. ( A ^m ( 0 ..^ S ) ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) -> c e. ( ( A i^i ( 1 ... N ) ) ^m ( 0 ..^ S ) ) )
76 75 anasss 
 |-  ( ( ph /\ ( c e. ( A ^m ( 0 ..^ S ) ) /\ sum_ a e. ( 0 ..^ S ) ( c ` a ) = N ) ) -> c e. ( ( A i^i ( 1 ... N ) ) ^m ( 0 ..^ S ) ) )
77 76 rabss3d 
 |-  ( ph -> { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = N } C_ { c e. ( ( A i^i ( 1 ... N ) ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = N } )
78 3 33 2 reprval 
 |-  ( ph -> ( A ( repr ` S ) N ) = { c e. ( A ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = N } )
79 inss1 
 |-  ( A i^i ( 1 ... N ) ) C_ A
80 79 a1i 
 |-  ( ph -> ( A i^i ( 1 ... N ) ) C_ A )
81 80 3 sstrd 
 |-  ( ph -> ( A i^i ( 1 ... N ) ) C_ NN )
82 81 33 2 reprval 
 |-  ( ph -> ( ( A i^i ( 1 ... N ) ) ( repr ` S ) N ) = { c e. ( ( A i^i ( 1 ... N ) ) ^m ( 0 ..^ S ) ) | sum_ a e. ( 0 ..^ S ) ( c ` a ) = N } )
83 77 78 82 3sstr4d 
 |-  ( ph -> ( A ( repr ` S ) N ) C_ ( ( A i^i ( 1 ... N ) ) ( repr ` S ) N ) )
84 3 33 2 80 reprss 
 |-  ( ph -> ( ( A i^i ( 1 ... N ) ) ( repr ` S ) N ) C_ ( A ( repr ` S ) N ) )
85 83 84 eqssd 
 |-  ( ph -> ( A ( repr ` S ) N ) = ( ( A i^i ( 1 ... N ) ) ( repr ` S ) N ) )