This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
86 34 85 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑐 ‘ 𝑎 ) ∈ ℕ )
87 79 86 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑚 ∈ ( 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 ... ( 𝑆 · 𝑁 ) ) ( 𝑅 · ( 𝑍 ↑ 𝑚 ) ) )