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

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 mulridi ⊢ ( 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 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑐 ‘ 𝑎 ) ) · ( 𝑍 ↑ 𝑚 ) ) )