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