Metamath Proof Explorer


Theorem breprexpnat

Description: Express the S th power of the finite series in terms of the number of representations of integers m as sums of S terms of elements of A , bounded by N . Proposition of Nathanson p. 123. (Contributed by Thierry Arnoux, 11-Dec-2021)

Ref Expression
Hypotheses breprexp.n ( 𝜑𝑁 ∈ ℕ0 )
breprexp.s ( 𝜑𝑆 ∈ ℕ0 )
breprexp.z ( 𝜑𝑍 ∈ ℂ )
breprexpnat.a ( 𝜑𝐴 ⊆ ℕ )
breprexpnat.p 𝑃 = Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 )
breprexpnat.r 𝑅 = ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) )
Assertion breprexpnat ( 𝜑 → ( 𝑃𝑆 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( 𝑅 · ( 𝑍𝑚 ) ) )

Proof

Step Hyp Ref Expression
1 breprexp.n ( 𝜑𝑁 ∈ ℕ0 )
2 breprexp.s ( 𝜑𝑆 ∈ ℕ0 )
3 breprexp.z ( 𝜑𝑍 ∈ ℂ )
4 breprexpnat.a ( 𝜑𝐴 ⊆ ℕ )
5 breprexpnat.p 𝑃 = Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 )
6 breprexpnat.r 𝑅 = ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) )
7 fvex ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ∈ V
8 7 fconst ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) : ( 0 ..^ 𝑆 ) ⟶ { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) }
9 nnex ℕ ∈ V
10 indf ( ( ℕ ∈ V ∧ 𝐴 ⊆ ℕ ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } )
11 9 4 10 sylancr ( 𝜑 → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } )
12 0cn 0 ∈ ℂ
13 ax-1cn 1 ∈ ℂ
14 prssi ( ( 0 ∈ ℂ ∧ 1 ∈ ℂ ) → { 0 , 1 } ⊆ ℂ )
15 12 13 14 mp2an { 0 , 1 } ⊆ ℂ
16 fss ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } ∧ { 0 , 1 } ⊆ ℂ ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ ℂ )
17 11 15 16 sylancl ( 𝜑 → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ ℂ )
18 cnex ℂ ∈ V
19 18 9 elmap ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ∈ ( ℂ ↑m ℕ ) ↔ ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ ℂ )
20 17 19 sylibr ( 𝜑 → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ∈ ( ℂ ↑m ℕ ) )
21 7 snss ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ∈ ( ℂ ↑m ℕ ) ↔ { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ⊆ ( ℂ ↑m ℕ ) )
22 20 21 sylib ( 𝜑 → { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ⊆ ( ℂ ↑m ℕ ) )
23 fss ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) : ( 0 ..^ 𝑆 ) ⟶ { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ∧ { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ⊆ ( ℂ ↑m ℕ ) ) → ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
24 8 22 23 sylancr ( 𝜑 → ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
25 1 2 3 24 breprexp ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
26 7 fvconst2 ( 𝑎 ∈ ( 0 ..^ 𝑆 ) → ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) = ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) )
27 26 ad2antlr ( ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) = ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) )
28 27 fveq1d ( ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ 𝑏 ) = ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ 𝑏 ) )
29 28 oveq1d ( ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
30 29 sumeq2dv ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
31 9 a1i ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ℕ ∈ V )
32 fzfi ( 1 ... 𝑁 ) ∈ Fin
33 32 a1i ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
34 fz1ssnn ( 1 ... 𝑁 ) ⊆ ℕ
35 34 a1i ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
36 4 adantr ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝐴 ⊆ ℕ )
37 3 ad2antrr ( ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑍 ∈ ℂ )
38 nnssnn0 ℕ ⊆ ℕ0
39 34 38 sstri ( 1 ... 𝑁 ) ⊆ ℕ0
40 simpr ( ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ( 1 ... 𝑁 ) )
41 39 40 sselid ( ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ℕ0 )
42 37 41 expcld ( ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 𝑍𝑏 ) ∈ ℂ )
43 31 33 35 36 42 indsumin ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑏 ∈ ( ( 1 ... 𝑁 ) ∩ 𝐴 ) ( 𝑍𝑏 ) )
44 incom ( ( 1 ... 𝑁 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 1 ... 𝑁 ) )
45 44 a1i ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 1 ... 𝑁 ) ∩ 𝐴 ) = ( 𝐴 ∩ ( 1 ... 𝑁 ) ) )
46 45 sumeq1d ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → Σ 𝑏 ∈ ( ( 1 ... 𝑁 ) ∩ 𝐴 ) ( 𝑍𝑏 ) = Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) )
47 30 43 46 3eqtrd ( ( 𝜑𝑎 ∈ ( 0 ..^ 𝑆 ) ) → Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) )
48 47 prodeq2dv ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) )
49 fzofi ( 0 ..^ 𝑆 ) ∈ Fin
50 49 a1i ( 𝜑 → ( 0 ..^ 𝑆 ) ∈ Fin )
51 inss2 ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ( 1 ... 𝑁 )
52 ssfi ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ( 1 ... 𝑁 ) ) → ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ∈ Fin )
53 32 51 52 mp2an ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ∈ Fin
54 53 a1i ( 𝜑 → ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ∈ Fin )
55 3 adantr ( ( 𝜑𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ) → 𝑍 ∈ ℂ )
56 51 39 sstri ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ⊆ ℕ0
57 simpr ( ( 𝜑𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ) → 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) )
58 56 57 sselid ( ( 𝜑𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ) → 𝑏 ∈ ℕ0 )
59 55 58 expcld ( ( 𝜑𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ) → ( 𝑍𝑏 ) ∈ ℂ )
60 54 59 fsumcl ( 𝜑 → Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ∈ ℂ )
61 fprodconst ( ( ( 0 ..^ 𝑆 ) ∈ Fin ∧ Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ∈ ℂ ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) = ( Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ↑ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ) )
62 50 60 61 syl2anc ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) = ( Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ↑ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ) )
63 hashfzo0 ( 𝑆 ∈ ℕ0 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
64 2 63 syl ( 𝜑 → ( ♯ ‘ ( 0 ..^ 𝑆 ) ) = 𝑆 )
65 64 oveq2d ( 𝜑 → ( Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ↑ ( ♯ ‘ ( 0 ..^ 𝑆 ) ) ) = ( Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ↑ 𝑆 ) )
66 48 62 65 3eqtrd ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ( Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ↑ 𝑆 ) )
67 34 a1i ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
68 fzssz ( 0 ... ( 𝑆 · 𝑁 ) ) ⊆ ℤ
69 simpr ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) )
70 68 69 sselid ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ℤ )
71 2 adantr ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑆 ∈ ℕ0 )
72 32 a1i ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 1 ... 𝑁 ) ∈ Fin )
73 67 70 71 72 reprfi ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∈ Fin )
74 3 adantr ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑍 ∈ ℂ )
75 fz0ssnn0 ( 0 ... ( 𝑆 · 𝑁 ) ) ⊆ ℕ0
76 75 69 sselid ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝑚 ∈ ℕ0 )
77 74 76 expcld ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( 𝑍𝑚 ) ∈ ℂ )
78 49 a1i ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
79 11 ad3antrrr ( ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) : ℕ ⟶ { 0 , 1 } )
80 34 a1i ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
81 70 adantr ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑚 ∈ ℤ )
82 71 adantr ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑆 ∈ ℕ0 )
83 simpr ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) )
84 80 81 82 83 reprf ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → 𝑐 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) )
85 84 ffvelrnda ( ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐𝑎 ) ∈ ( 1 ... 𝑁 ) )
86 34 85 sselid ( ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐𝑎 ) ∈ ℕ )
87 79 86 ffvelrnd ( ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) ∈ { 0 , 1 } )
88 15 87 sselid ( ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) ∈ ℂ )
89 78 88 fprodcl ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) ∈ ℂ )
90 73 77 89 fsummulc1 ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
91 4 adantr ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → 𝐴 ⊆ ℕ )
92 91 70 71 72 67 hashreprin ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) )
93 92 oveq1d ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ( ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) · ( 𝑍𝑚 ) ) = ( Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
94 26 fveq1d ( 𝑎 ∈ ( 0 ..^ 𝑆 ) → ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) = ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) )
95 94 adantl ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) = ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) )
96 95 prodeq2dv ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) )
97 96 adantr ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) )
98 97 oveq1d ( ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
99 98 sumeq2dv ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
100 90 93 99 3eqtr4rd ( ( 𝜑𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) · ( 𝑍𝑚 ) ) )
101 100 sumeq2dv ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( ( ( 0 ..^ 𝑆 ) × { ( ( 𝟭 ‘ ℕ ) ‘ 𝐴 ) } ) ‘ 𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) · ( 𝑍𝑚 ) ) )
102 25 66 101 3eqtr3d ( 𝜑 → ( Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ↑ 𝑆 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) · ( 𝑍𝑚 ) ) )
103 5 oveq1i ( 𝑃𝑆 ) = ( Σ 𝑏 ∈ ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( 𝑍𝑏 ) ↑ 𝑆 )
104 6 oveq1i ( 𝑅 · ( 𝑍𝑚 ) ) = ( ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) · ( 𝑍𝑚 ) )
105 104 a1i ( 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) → ( 𝑅 · ( 𝑍𝑚 ) ) = ( ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) · ( 𝑍𝑚 ) ) )
106 105 sumeq2i Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( 𝑅 · ( 𝑍𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( ( ♯ ‘ ( ( 𝐴 ∩ ( 1 ... 𝑁 ) ) ( repr ‘ 𝑆 ) 𝑚 ) ) · ( 𝑍𝑚 ) )
107 102 103 106 3eqtr4g ( 𝜑 → ( 𝑃𝑆 ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ( 𝑅 · ( 𝑍𝑚 ) ) )