Metamath Proof Explorer


Theorem breprexp

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. This is a general formulation which allows logarithmic weighting of the sums (see https://mathoverflow.net/questions/253246) and a mix of different smoothing functions taken into account in L . See breprexpnat for the simple case presented in the proposition of Nathanson p. 123. (Contributed by Thierry Arnoux, 6-Dec-2021)

Ref Expression
Hypotheses breprexp.n ( 𝜑𝑁 ∈ ℕ0 )
breprexp.s ( 𝜑𝑆 ∈ ℕ0 )
breprexp.z ( 𝜑𝑍 ∈ ℂ )
breprexp.h ( 𝜑𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
Assertion breprexp ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )

Proof

Step Hyp Ref Expression
1 breprexp.n ( 𝜑𝑁 ∈ ℕ0 )
2 breprexp.s ( 𝜑𝑆 ∈ ℕ0 )
3 breprexp.z ( 𝜑𝑍 ∈ ℂ )
4 breprexp.h ( 𝜑𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
5 nn0ssre 0 ⊆ ℝ
6 5 a1i ( 𝜑 → ℕ0 ⊆ ℝ )
7 6 sselda ( ( 𝜑𝑆 ∈ ℕ0 ) → 𝑆 ∈ ℝ )
8 leid ( 𝑆 ∈ ℝ → 𝑆𝑆 )
9 7 8 syl ( ( 𝜑𝑆 ∈ ℕ0 ) → 𝑆𝑆 )
10 breq1 ( 𝑡 = 0 → ( 𝑡𝑆 ↔ 0 ≤ 𝑆 ) )
11 oveq2 ( 𝑡 = 0 → ( 0 ..^ 𝑡 ) = ( 0 ..^ 0 ) )
12 11 prodeq1d ( 𝑡 = 0 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
13 oveq1 ( 𝑡 = 0 → ( 𝑡 · 𝑁 ) = ( 0 · 𝑁 ) )
14 13 oveq2d ( 𝑡 = 0 → ( 0 ... ( 𝑡 · 𝑁 ) ) = ( 0 ... ( 0 · 𝑁 ) ) )
15 fveq2 ( 𝑡 = 0 → ( repr ‘ 𝑡 ) = ( repr ‘ 0 ) )
16 15 oveqd ( 𝑡 = 0 → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) )
17 11 prodeq1d ( 𝑡 = 0 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) )
18 17 oveq1d ( 𝑡 = 0 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
19 18 adantr ( ( 𝑡 = 0 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
20 16 19 sumeq12dv ( 𝑡 = 0 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
21 20 adantr ( ( 𝑡 = 0 ∧ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
22 14 21 sumeq12dv ( 𝑡 = 0 → Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( 0 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
23 12 22 eqeq12d ( 𝑡 = 0 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ↔ ∏ 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 0 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
24 10 23 imbi12d ( 𝑡 = 0 → ( ( 𝑡𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ↔ ( 0 ≤ 𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 0 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) )
25 breq1 ( 𝑡 = 𝑠 → ( 𝑡𝑆𝑠𝑆 ) )
26 oveq2 ( 𝑡 = 𝑠 → ( 0 ..^ 𝑡 ) = ( 0 ..^ 𝑠 ) )
27 26 prodeq1d ( 𝑡 = 𝑠 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
28 oveq1 ( 𝑡 = 𝑠 → ( 𝑡 · 𝑁 ) = ( 𝑠 · 𝑁 ) )
29 28 oveq2d ( 𝑡 = 𝑠 → ( 0 ... ( 𝑡 · 𝑁 ) ) = ( 0 ... ( 𝑠 · 𝑁 ) ) )
30 fveq2 ( 𝑡 = 𝑠 → ( repr ‘ 𝑡 ) = ( repr ‘ 𝑠 ) )
31 30 oveqd ( 𝑡 = 𝑠 → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) )
32 26 prodeq1d ( 𝑡 = 𝑠 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) )
33 32 oveq1d ( 𝑡 = 𝑠 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
34 33 adantr ( ( 𝑡 = 𝑠𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
35 31 34 sumeq12dv ( 𝑡 = 𝑠 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
36 35 adantr ( ( 𝑡 = 𝑠𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
37 29 36 sumeq12dv ( 𝑡 = 𝑠 → Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
38 27 37 eqeq12d ( 𝑡 = 𝑠 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ↔ ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
39 25 38 imbi12d ( 𝑡 = 𝑠 → ( ( 𝑡𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ↔ ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) )
40 breq1 ( 𝑡 = ( 𝑠 + 1 ) → ( 𝑡𝑆 ↔ ( 𝑠 + 1 ) ≤ 𝑆 ) )
41 oveq2 ( 𝑡 = ( 𝑠 + 1 ) → ( 0 ..^ 𝑡 ) = ( 0 ..^ ( 𝑠 + 1 ) ) )
42 41 prodeq1d ( 𝑡 = ( 𝑠 + 1 ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
43 oveq1 ( 𝑡 = ( 𝑠 + 1 ) → ( 𝑡 · 𝑁 ) = ( ( 𝑠 + 1 ) · 𝑁 ) )
44 43 oveq2d ( 𝑡 = ( 𝑠 + 1 ) → ( 0 ... ( 𝑡 · 𝑁 ) ) = ( 0 ... ( ( 𝑠 + 1 ) · 𝑁 ) ) )
45 fveq2 ( 𝑡 = ( 𝑠 + 1 ) → ( repr ‘ 𝑡 ) = ( repr ‘ ( 𝑠 + 1 ) ) )
46 45 oveqd ( 𝑡 = ( 𝑠 + 1 ) → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) = ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) )
47 41 prodeq1d ( 𝑡 = ( 𝑠 + 1 ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) )
48 47 oveq1d ( 𝑡 = ( 𝑠 + 1 ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
49 48 adantr ( ( 𝑡 = ( 𝑠 + 1 ) ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
50 46 49 sumeq12dv ( 𝑡 = ( 𝑠 + 1 ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
51 50 adantr ( ( 𝑡 = ( 𝑠 + 1 ) ∧ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
52 44 51 sumeq12dv ( 𝑡 = ( 𝑠 + 1 ) → Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( ( 𝑠 + 1 ) · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
53 42 52 eqeq12d ( 𝑡 = ( 𝑠 + 1 ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ↔ ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( ( 𝑠 + 1 ) · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
54 40 53 imbi12d ( 𝑡 = ( 𝑠 + 1 ) → ( ( 𝑡𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ↔ ( ( 𝑠 + 1 ) ≤ 𝑆 → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( ( 𝑠 + 1 ) · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) )
55 breq1 ( 𝑡 = 𝑆 → ( 𝑡𝑆𝑆𝑆 ) )
56 oveq2 ( 𝑡 = 𝑆 → ( 0 ..^ 𝑡 ) = ( 0 ..^ 𝑆 ) )
57 56 prodeq1d ( 𝑡 = 𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
58 oveq1 ( 𝑡 = 𝑆 → ( 𝑡 · 𝑁 ) = ( 𝑆 · 𝑁 ) )
59 58 oveq2d ( 𝑡 = 𝑆 → ( 0 ... ( 𝑡 · 𝑁 ) ) = ( 0 ... ( 𝑆 · 𝑁 ) ) )
60 fveq2 ( 𝑡 = 𝑆 → ( repr ‘ 𝑡 ) = ( repr ‘ 𝑆 ) )
61 60 oveqd ( 𝑡 = 𝑆 → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) )
62 56 prodeq1d ( 𝑡 = 𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) )
63 62 oveq1d ( 𝑡 = 𝑆 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
64 63 adantr ( ( 𝑡 = 𝑆𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
65 61 64 sumeq12dv ( 𝑡 = 𝑆 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
66 65 adantr ( ( 𝑡 = 𝑆𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
67 59 66 sumeq12dv ( 𝑡 = 𝑆 → Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
68 57 67 eqeq12d ( 𝑡 = 𝑆 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ↔ ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
69 55 68 imbi12d ( 𝑡 = 𝑆 → ( ( 𝑡𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑡 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑡 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑡 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ↔ ( 𝑆𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) )
70 0nn0 0 ∈ ℕ0
71 fz1ssnn ( 1 ... 𝑁 ) ⊆ ℕ
72 71 a1i ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
73 0zd ( 𝜑 → 0 ∈ ℤ )
74 72 73 1 repr0 ( 𝜑 → ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) = if ( 0 = 0 , { ∅ } , ∅ ) )
75 eqid 0 = 0
76 75 iftruei if ( 0 = 0 , { ∅ } , ∅ ) = { ∅ }
77 74 76 eqtrdi ( 𝜑 → ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) = { ∅ } )
78 snfi { ∅ } ∈ Fin
79 77 78 eqeltrdi ( 𝜑 → ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ∈ Fin )
80 fzo0 ( 0 ..^ 0 ) = ∅
81 80 prodeq1i 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ∅ ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) )
82 prod0 𝑎 ∈ ∅ ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = 1
83 81 82 eqtri 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = 1
84 83 a1i ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = 1 )
85 exp0 ( 𝑍 ∈ ℂ → ( 𝑍 ↑ 0 ) = 1 )
86 3 85 syl ( 𝜑 → ( 𝑍 ↑ 0 ) = 1 )
87 84 86 oveq12d ( 𝜑 → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = ( 1 · 1 ) )
88 ax-1cn 1 ∈ ℂ
89 88 mulid1i ( 1 · 1 ) = 1
90 87 89 eqtrdi ( 𝜑 → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = 1 )
91 90 88 eqeltrdi ( 𝜑 → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) ∈ ℂ )
92 91 adantr ( ( 𝜑𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) ∈ ℂ )
93 79 92 fsumcl ( 𝜑 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) ∈ ℂ )
94 oveq2 ( 𝑚 = 0 → ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) )
95 simpl ( ( 𝑚 = 0 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ) → 𝑚 = 0 )
96 95 oveq2d ( ( 𝑚 = 0 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ) → ( 𝑍𝑚 ) = ( 𝑍 ↑ 0 ) )
97 96 oveq2d ( ( 𝑚 = 0 ∧ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
98 94 97 sumeq12dv ( 𝑚 = 0 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
99 98 sumsn ( ( 0 ∈ ℕ0 ∧ Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) ∈ ℂ ) → Σ 𝑚 ∈ { 0 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
100 70 93 99 sylancr ( 𝜑 → Σ 𝑚 ∈ { 0 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
101 77 sumeq1d ( 𝜑 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 0 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = Σ 𝑐 ∈ { ∅ } ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
102 0ex ∅ ∈ V
103 80 prodeq1i 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) = ∏ 𝑎 ∈ ∅ ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) )
104 prod0 𝑎 ∈ ∅ ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) = 1
105 103 104 eqtri 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) = 1
106 105 a1i ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) = 1 )
107 106 88 eqeltrdi ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) ∈ ℂ )
108 86 88 eqeltrdi ( 𝜑 → ( 𝑍 ↑ 0 ) ∈ ℂ )
109 107 108 mulcld ( 𝜑 → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) · ( 𝑍 ↑ 0 ) ) ∈ ℂ )
110 fveq1 ( 𝑐 = ∅ → ( 𝑐𝑎 ) = ( ∅ ‘ 𝑎 ) )
111 110 fveq2d ( 𝑐 = ∅ → ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) )
112 111 ralrimivw ( 𝑐 = ∅ → ∀ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) )
113 112 prodeq2d ( 𝑐 = ∅ → ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) )
114 113 oveq1d ( 𝑐 = ∅ → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
115 114 sumsn ( ( ∅ ∈ V ∧ ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) · ( 𝑍 ↑ 0 ) ) ∈ ℂ ) → Σ 𝑐 ∈ { ∅ } ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
116 102 109 115 sylancr ( 𝜑 → Σ 𝑐 ∈ { ∅ } ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) · ( 𝑍 ↑ 0 ) ) )
117 106 86 oveq12d ( 𝜑 → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = ( 1 · 1 ) )
118 117 87 90 3eqtr2d ( 𝜑 → ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( ∅ ‘ 𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = 1 )
119 116 118 eqtrd ( 𝜑 → Σ 𝑐 ∈ { ∅ } ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍 ↑ 0 ) ) = 1 )
120 100 101 119 3eqtrd ( 𝜑 → Σ 𝑚 ∈ { 0 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = 1 )
121 1 nn0cnd ( 𝜑𝑁 ∈ ℂ )
122 121 mul02d ( 𝜑 → ( 0 · 𝑁 ) = 0 )
123 122 oveq2d ( 𝜑 → ( 0 ... ( 0 · 𝑁 ) ) = ( 0 ... 0 ) )
124 fz0sn ( 0 ... 0 ) = { 0 }
125 123 124 eqtrdi ( 𝜑 → ( 0 ... ( 0 · 𝑁 ) ) = { 0 } )
126 125 sumeq1d ( 𝜑 → Σ 𝑚 ∈ ( 0 ... ( 0 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑚 ∈ { 0 } Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
127 80 prodeq1i 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑎 ∈ ∅ Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) )
128 prod0 𝑎 ∈ ∅ Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = 1
129 127 128 eqtri 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = 1
130 129 a1i ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = 1 )
131 120 126 130 3eqtr4rd ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 0 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
132 131 a1d ( 𝜑 → ( 0 ≤ 𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 0 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 0 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 0 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 0 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
133 simpll ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝜑𝑠 ∈ ℕ0 ) )
134 simplr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
135 oveq2 ( 𝑚 = 𝑛 → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) = ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) )
136 oveq2 ( 𝑚 = 𝑛 → ( 𝑍𝑚 ) = ( 𝑍𝑛 ) )
137 136 oveq2d ( 𝑚 = 𝑛 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) )
138 137 adantr ( ( 𝑚 = 𝑛𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) )
139 135 138 sumeq12dv ( 𝑚 = 𝑛 → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) )
140 139 cbvsumv Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) )
141 140 eqeq2i ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ↔ ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) )
142 simpl ( ( 𝑎 = 𝑖𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑎 = 𝑖 )
143 142 fveq2d ( ( 𝑎 = 𝑖𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 𝐿𝑎 ) = ( 𝐿𝑖 ) )
144 143 fveq1d ( ( 𝑎 = 𝑖𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( 𝐿𝑎 ) ‘ 𝑏 ) = ( ( 𝐿𝑖 ) ‘ 𝑏 ) )
145 144 oveq1d ( ( 𝑎 = 𝑖𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ( ( ( 𝐿𝑖 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
146 145 sumeq2dv ( 𝑎 = 𝑖 → Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) )
147 146 cbvprodv 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) )
148 fveq2 ( 𝑏 = 𝑗 → ( ( 𝐿𝑖 ) ‘ 𝑏 ) = ( ( 𝐿𝑖 ) ‘ 𝑗 ) )
149 oveq2 ( 𝑏 = 𝑗 → ( 𝑍𝑏 ) = ( 𝑍𝑗 ) )
150 148 149 oveq12d ( 𝑏 = 𝑗 → ( ( ( 𝐿𝑖 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) )
151 150 cbvsumv Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) )
152 151 a1i ( 𝑖 ∈ ( 0 ..^ 𝑠 ) → Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) )
153 152 prodeq2i 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) )
154 147 153 eqtri 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) )
155 fveq2 ( 𝑎 = 𝑖 → ( 𝐿𝑎 ) = ( 𝐿𝑖 ) )
156 fveq2 ( 𝑎 = 𝑖 → ( 𝑐𝑎 ) = ( 𝑐𝑖 ) )
157 155 156 fveq12d ( 𝑎 = 𝑖 → ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) )
158 157 cbvprodv 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) = ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) )
159 158 oveq1i ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) = ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) · ( 𝑍𝑛 ) )
160 159 a1i ( 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) = ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) · ( 𝑍𝑛 ) ) )
161 160 sumeq2i Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) = Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) · ( 𝑍𝑛 ) )
162 simpl ( ( 𝑐 = 𝑘𝑖 ∈ ( 0 ..^ 𝑠 ) ) → 𝑐 = 𝑘 )
163 162 fveq1d ( ( 𝑐 = 𝑘𝑖 ∈ ( 0 ..^ 𝑠 ) ) → ( 𝑐𝑖 ) = ( 𝑘𝑖 ) )
164 163 fveq2d ( ( 𝑐 = 𝑘𝑖 ∈ ( 0 ..^ 𝑠 ) ) → ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) = ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) )
165 164 prodeq2dv ( 𝑐 = 𝑘 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) = ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) )
166 165 oveq1d ( 𝑐 = 𝑘 → ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) · ( 𝑍𝑛 ) ) = ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) )
167 166 cbvsumv Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑐𝑖 ) ) · ( 𝑍𝑛 ) ) = Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) )
168 161 167 eqtri Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) = Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) )
169 168 a1i ( 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) → Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) = Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) )
170 169 sumeq2i Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) )
171 154 170 eqeq12i ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑛 ) ) ↔ ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) )
172 141 171 bitri ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ↔ ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) )
173 172 imbi2i ( ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ↔ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) )
174 134 173 sylib ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) )
175 simpr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝑠 + 1 ) ≤ 𝑆 )
176 1 ad3antrrr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑁 ∈ ℕ0 )
177 2 ad3antrrr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑆 ∈ ℕ0 )
178 3 ad3antrrr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑍 ∈ ℂ )
179 4 ad3antrrr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝐿 : ( 0 ..^ 𝑆 ) ⟶ ( ℂ ↑m ℕ ) )
180 simpllr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑠 ∈ ℕ0 )
181 simpr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝑠 + 1 ) ≤ 𝑆 )
182 5 180 sselid ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑠 ∈ ℝ )
183 1red ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 1 ∈ ℝ )
184 182 183 readdcld ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝑠 + 1 ) ∈ ℝ )
185 5 177 sselid ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑆 ∈ ℝ )
186 182 ltp1d ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑠 < ( 𝑠 + 1 ) )
187 182 184 186 ltled ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑠 ≤ ( 𝑠 + 1 ) )
188 182 184 185 187 181 letrd ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → 𝑠𝑆 )
189 simplr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) )
190 189 173 sylibr ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
191 188 190 mpd ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
192 176 177 178 179 180 181 191 breprexplemc ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) Σ 𝑗 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑖 ) ‘ 𝑗 ) · ( 𝑍𝑗 ) ) = Σ 𝑛 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑘 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑛 ) ( ∏ 𝑖 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑖 ) ‘ ( 𝑘𝑖 ) ) · ( 𝑍𝑛 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( ( 𝑠 + 1 ) · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
193 133 174 175 192 syl21anc ( ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) ∧ ( 𝑠 + 1 ) ≤ 𝑆 ) → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( ( 𝑠 + 1 ) · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
194 193 ex ( ( ( 𝜑𝑠 ∈ ℕ0 ) ∧ ( 𝑠𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑠 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑠 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) ) → ( ( 𝑠 + 1 ) ≤ 𝑆 → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( ( 𝑠 + 1 ) · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑠 + 1 ) ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ ( 𝑠 + 1 ) ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
195 24 39 54 69 132 194 nn0indd ( ( 𝜑𝑆 ∈ ℕ0 ) → ( 𝑆𝑆 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) ) )
196 9 195 mpd ( ( 𝜑𝑆 ∈ ℕ0 ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )
197 2 196 mpdan ( 𝜑 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) Σ 𝑏 ∈ ( 1 ... 𝑁 ) ( ( ( 𝐿𝑎 ) ‘ 𝑏 ) · ( 𝑍𝑏 ) ) = Σ 𝑚 ∈ ( 0 ... ( 𝑆 · 𝑁 ) ) Σ 𝑐 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) 𝑚 ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿𝑎 ) ‘ ( 𝑐𝑎 ) ) · ( 𝑍𝑚 ) ) )