Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  breprexp Structured version   Visualization version   GIF version

Theorem breprexp 32185
Description: Express the 𝑆 th power of the finite series in terms of the number of representations of integers 𝑚 as sums of 𝑆 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 𝐿. See breprexpnat 32186 for the simple case presented in the proposition of [Nathanson] p. 123. (Contributed by Thierry Arnoux, 6-Dec-2021.)
Hypotheses
Ref Expression
breprexp.n (𝜑𝑁 ∈ ℕ0)
breprexp.s (𝜑𝑆 ∈ ℕ0)
breprexp.z (𝜑𝑍 ∈ ℂ)
breprexp.h (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
Assertion
Ref Expression
breprexp (𝜑 → ∏𝑎 ∈ (0..^𝑆𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
Distinct variable groups:   𝑁,𝑐,𝑚   𝑆,𝑎,𝑐,𝑚   𝑍,𝑐,𝑚,𝑏   𝜑,𝑐   𝐿,𝑐,𝑚,𝑎,𝑏   𝑁,𝑎,𝑏   𝑆,𝑏   𝑍,𝑎,𝑏   𝜑,𝑎,𝑏,𝑚

Proof of Theorem breprexp
Dummy variables 𝑠 𝑡 𝑖 𝑗 𝑘 𝑛 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breprexp.s . 2 (𝜑𝑆 ∈ ℕ0)
2 nn0ssre 11982 . . . . . 6 0 ⊆ ℝ
32a1i 11 . . . . 5 (𝜑 → ℕ0 ⊆ ℝ)
43sselda 3877 . . . 4 ((𝜑𝑆 ∈ ℕ0) → 𝑆 ∈ ℝ)
5 leid 10816 . . . 4 (𝑆 ∈ ℝ → 𝑆𝑆)
64, 5syl 17 . . 3 ((𝜑𝑆 ∈ ℕ0) → 𝑆𝑆)
7 breq1 5033 . . . . 5 (𝑡 = 0 → (𝑡𝑆 ↔ 0 ≤ 𝑆))
8 oveq2 7180 . . . . . . 7 (𝑡 = 0 → (0..^𝑡) = (0..^0))
98prodeq1d 15369 . . . . . 6 (𝑡 = 0 → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
10 oveq1 7179 . . . . . . . 8 (𝑡 = 0 → (𝑡 · 𝑁) = (0 · 𝑁))
1110oveq2d 7188 . . . . . . 7 (𝑡 = 0 → (0...(𝑡 · 𝑁)) = (0...(0 · 𝑁)))
12 fveq2 6676 . . . . . . . . . 10 (𝑡 = 0 → (repr‘𝑡) = (repr‘0))
1312oveqd 7189 . . . . . . . . 9 (𝑡 = 0 → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘0)𝑚))
148prodeq1d 15369 . . . . . . . . . . 11 (𝑡 = 0 → ∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) = ∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)))
1514oveq1d 7187 . . . . . . . . . 10 (𝑡 = 0 → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
1615adantr 484 . . . . . . . . 9 ((𝑡 = 0 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
1713, 16sumeq12dv 15158 . . . . . . . 8 (𝑡 = 0 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
1817adantr 484 . . . . . . 7 ((𝑡 = 0 ∧ 𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
1911, 18sumeq12dv 15158 . . . . . 6 (𝑡 = 0 → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
209, 19eqeq12d 2754 . . . . 5 (𝑡 = 0 → (∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) ↔ ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
217, 20imbi12d 348 . . . 4 (𝑡 = 0 → ((𝑡𝑆 → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))) ↔ (0 ≤ 𝑆 → ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))))
22 breq1 5033 . . . . 5 (𝑡 = 𝑠 → (𝑡𝑆𝑠𝑆))
23 oveq2 7180 . . . . . . 7 (𝑡 = 𝑠 → (0..^𝑡) = (0..^𝑠))
2423prodeq1d 15369 . . . . . 6 (𝑡 = 𝑠 → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
25 oveq1 7179 . . . . . . . 8 (𝑡 = 𝑠 → (𝑡 · 𝑁) = (𝑠 · 𝑁))
2625oveq2d 7188 . . . . . . 7 (𝑡 = 𝑠 → (0...(𝑡 · 𝑁)) = (0...(𝑠 · 𝑁)))
27 fveq2 6676 . . . . . . . . . 10 (𝑡 = 𝑠 → (repr‘𝑡) = (repr‘𝑠))
2827oveqd 7189 . . . . . . . . 9 (𝑡 = 𝑠 → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘𝑠)𝑚))
2923prodeq1d 15369 . . . . . . . . . . 11 (𝑡 = 𝑠 → ∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) = ∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)))
3029oveq1d 7187 . . . . . . . . . 10 (𝑡 = 𝑠 → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
3130adantr 484 . . . . . . . . 9 ((𝑡 = 𝑠𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
3228, 31sumeq12dv 15158 . . . . . . . 8 (𝑡 = 𝑠 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
3332adantr 484 . . . . . . 7 ((𝑡 = 𝑠𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
3426, 33sumeq12dv 15158 . . . . . 6 (𝑡 = 𝑠 → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
3524, 34eqeq12d 2754 . . . . 5 (𝑡 = 𝑠 → (∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) ↔ ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
3622, 35imbi12d 348 . . . 4 (𝑡 = 𝑠 → ((𝑡𝑆 → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))) ↔ (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))))
37 breq1 5033 . . . . 5 (𝑡 = (𝑠 + 1) → (𝑡𝑆 ↔ (𝑠 + 1) ≤ 𝑆))
38 oveq2 7180 . . . . . . 7 (𝑡 = (𝑠 + 1) → (0..^𝑡) = (0..^(𝑠 + 1)))
3938prodeq1d 15369 . . . . . 6 (𝑡 = (𝑠 + 1) → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
40 oveq1 7179 . . . . . . . 8 (𝑡 = (𝑠 + 1) → (𝑡 · 𝑁) = ((𝑠 + 1) · 𝑁))
4140oveq2d 7188 . . . . . . 7 (𝑡 = (𝑠 + 1) → (0...(𝑡 · 𝑁)) = (0...((𝑠 + 1) · 𝑁)))
42 fveq2 6676 . . . . . . . . . 10 (𝑡 = (𝑠 + 1) → (repr‘𝑡) = (repr‘(𝑠 + 1)))
4342oveqd 7189 . . . . . . . . 9 (𝑡 = (𝑠 + 1) → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘(𝑠 + 1))𝑚))
4438prodeq1d 15369 . . . . . . . . . . 11 (𝑡 = (𝑠 + 1) → ∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) = ∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)))
4544oveq1d 7187 . . . . . . . . . 10 (𝑡 = (𝑠 + 1) → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
4645adantr 484 . . . . . . . . 9 ((𝑡 = (𝑠 + 1) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
4743, 46sumeq12dv 15158 . . . . . . . 8 (𝑡 = (𝑠 + 1) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
4847adantr 484 . . . . . . 7 ((𝑡 = (𝑠 + 1) ∧ 𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
4941, 48sumeq12dv 15158 . . . . . 6 (𝑡 = (𝑠 + 1) → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
5039, 49eqeq12d 2754 . . . . 5 (𝑡 = (𝑠 + 1) → (∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) ↔ ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
5137, 50imbi12d 348 . . . 4 (𝑡 = (𝑠 + 1) → ((𝑡𝑆 → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))) ↔ ((𝑠 + 1) ≤ 𝑆 → ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))))
52 breq1 5033 . . . . 5 (𝑡 = 𝑆 → (𝑡𝑆𝑆𝑆))
53 oveq2 7180 . . . . . . 7 (𝑡 = 𝑆 → (0..^𝑡) = (0..^𝑆))
5453prodeq1d 15369 . . . . . 6 (𝑡 = 𝑆 → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ (0..^𝑆𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)))
55 oveq1 7179 . . . . . . . 8 (𝑡 = 𝑆 → (𝑡 · 𝑁) = (𝑆 · 𝑁))
5655oveq2d 7188 . . . . . . 7 (𝑡 = 𝑆 → (0...(𝑡 · 𝑁)) = (0...(𝑆 · 𝑁)))
57 fveq2 6676 . . . . . . . . . 10 (𝑡 = 𝑆 → (repr‘𝑡) = (repr‘𝑆))
5857oveqd 7189 . . . . . . . . 9 (𝑡 = 𝑆 → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘𝑆)𝑚))
5953prodeq1d 15369 . . . . . . . . . . 11 (𝑡 = 𝑆 → ∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)))
6059oveq1d 7187 . . . . . . . . . 10 (𝑡 = 𝑆 → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
6160adantr 484 . . . . . . . . 9 ((𝑡 = 𝑆𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
6258, 61sumeq12dv 15158 . . . . . . . 8 (𝑡 = 𝑆 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
6362adantr 484 . . . . . . 7 ((𝑡 = 𝑆𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
6456, 63sumeq12dv 15158 . . . . . 6 (𝑡 = 𝑆 → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
6554, 64eqeq12d 2754 . . . . 5 (𝑡 = 𝑆 → (∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) ↔ ∏𝑎 ∈ (0..^𝑆𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
6652, 65imbi12d 348 . . . 4 (𝑡 = 𝑆 → ((𝑡𝑆 → ∏𝑎 ∈ (0..^𝑡𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))) ↔ (𝑆𝑆 → ∏𝑎 ∈ (0..^𝑆𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))))
67 0nn0 11993 . . . . . . . 8 0 ∈ ℕ0
68 fz1ssnn 13031 . . . . . . . . . . . . 13 (1...𝑁) ⊆ ℕ
6968a1i 11 . . . . . . . . . . . 12 (𝜑 → (1...𝑁) ⊆ ℕ)
70 0zd 12076 . . . . . . . . . . . 12 (𝜑 → 0 ∈ ℤ)
71 breprexp.n . . . . . . . . . . . 12 (𝜑𝑁 ∈ ℕ0)
7269, 70, 71repr0 32163 . . . . . . . . . . 11 (𝜑 → ((1...𝑁)(repr‘0)0) = if(0 = 0, {∅}, ∅))
73 eqid 2738 . . . . . . . . . . . 12 0 = 0
7473iftruei 4421 . . . . . . . . . . 11 if(0 = 0, {∅}, ∅) = {∅}
7572, 74eqtrdi 2789 . . . . . . . . . 10 (𝜑 → ((1...𝑁)(repr‘0)0) = {∅})
76 snfi 8644 . . . . . . . . . 10 {∅} ∈ Fin
7775, 76eqeltrdi 2841 . . . . . . . . 9 (𝜑 → ((1...𝑁)(repr‘0)0) ∈ Fin)
78 fzo0 13154 . . . . . . . . . . . . . . . 16 (0..^0) = ∅
7978prodeq1i 15366 . . . . . . . . . . . . . . 15 𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) = ∏𝑎 ∈ ∅ ((𝐿𝑎)‘(𝑐𝑎))
80 prod0 15391 . . . . . . . . . . . . . . 15 𝑎 ∈ ∅ ((𝐿𝑎)‘(𝑐𝑎)) = 1
8179, 80eqtri 2761 . . . . . . . . . . . . . 14 𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) = 1
8281a1i 11 . . . . . . . . . . . . 13 (𝜑 → ∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) = 1)
83 breprexp.z . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ ℂ)
84 exp0 13527 . . . . . . . . . . . . . 14 (𝑍 ∈ ℂ → (𝑍↑0) = 1)
8583, 84syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑍↑0) = 1)
8682, 85oveq12d 7190 . . . . . . . . . . . 12 (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) = (1 · 1))
87 ax-1cn 10675 . . . . . . . . . . . . 13 1 ∈ ℂ
8887mulid1i 10725 . . . . . . . . . . . 12 (1 · 1) = 1
8986, 88eqtrdi 2789 . . . . . . . . . . 11 (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) = 1)
9089, 87eqeltrdi 2841 . . . . . . . . . 10 (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) ∈ ℂ)
9190adantr 484 . . . . . . . . 9 ((𝜑𝑐 ∈ ((1...𝑁)(repr‘0)0)) → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) ∈ ℂ)
9277, 91fsumcl 15185 . . . . . . . 8 (𝜑 → Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) ∈ ℂ)
93 oveq2 7180 . . . . . . . . . 10 (𝑚 = 0 → ((1...𝑁)(repr‘0)𝑚) = ((1...𝑁)(repr‘0)0))
94 simpl 486 . . . . . . . . . . . 12 ((𝑚 = 0 ∧ 𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)) → 𝑚 = 0)
9594oveq2d 7188 . . . . . . . . . . 11 ((𝑚 = 0 ∧ 𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)) → (𝑍𝑚) = (𝑍↑0))
9695oveq2d 7188 . . . . . . . . . 10 ((𝑚 = 0 ∧ 𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)) → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)))
9793, 96sumeq12dv 15158 . . . . . . . . 9 (𝑚 = 0 → Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)))
9897sumsn 15196 . . . . . . . 8 ((0 ∈ ℕ0 ∧ Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) ∈ ℂ) → Σ𝑚 ∈ {0}Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)))
9967, 92, 98sylancr 590 . . . . . . 7 (𝜑 → Σ𝑚 ∈ {0}Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)))
10075sumeq1d 15153 . . . . . . 7 (𝜑 → Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) = Σ𝑐 ∈ {∅} (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)))
101 0ex 5175 . . . . . . . . 9 ∅ ∈ V
10278prodeq1i 15366 . . . . . . . . . . . . 13 𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) = ∏𝑎 ∈ ∅ ((𝐿𝑎)‘(∅‘𝑎))
103 prod0 15391 . . . . . . . . . . . . 13 𝑎 ∈ ∅ ((𝐿𝑎)‘(∅‘𝑎)) = 1
104102, 103eqtri 2761 . . . . . . . . . . . 12 𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) = 1
105104a1i 11 . . . . . . . . . . 11 (𝜑 → ∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) = 1)
106105, 87eqeltrdi 2841 . . . . . . . . . 10 (𝜑 → ∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) ∈ ℂ)
10785, 87eqeltrdi 2841 . . . . . . . . . 10 (𝜑 → (𝑍↑0) ∈ ℂ)
108106, 107mulcld 10741 . . . . . . . . 9 (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) · (𝑍↑0)) ∈ ℂ)
109 fveq1 6675 . . . . . . . . . . . . . 14 (𝑐 = ∅ → (𝑐𝑎) = (∅‘𝑎))
110109fveq2d 6680 . . . . . . . . . . . . 13 (𝑐 = ∅ → ((𝐿𝑎)‘(𝑐𝑎)) = ((𝐿𝑎)‘(∅‘𝑎)))
111110ralrimivw 3097 . . . . . . . . . . . 12 (𝑐 = ∅ → ∀𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) = ((𝐿𝑎)‘(∅‘𝑎)))
112111prodeq2d 15370 . . . . . . . . . . 11 (𝑐 = ∅ → ∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) = ∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)))
113112oveq1d 7187 . . . . . . . . . 10 (𝑐 = ∅ → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) = (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) · (𝑍↑0)))
114113sumsn 15196 . . . . . . . . 9 ((∅ ∈ V ∧ (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) · (𝑍↑0)) ∈ ℂ) → Σ𝑐 ∈ {∅} (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) = (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) · (𝑍↑0)))
115101, 108, 114sylancr 590 . . . . . . . 8 (𝜑 → Σ𝑐 ∈ {∅} (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) = (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) · (𝑍↑0)))
116105, 85oveq12d 7190 . . . . . . . . 9 (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) · (𝑍↑0)) = (1 · 1))
117116, 86, 893eqtr2d 2779 . . . . . . . 8 (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(∅‘𝑎)) · (𝑍↑0)) = 1)
118115, 117eqtrd 2773 . . . . . . 7 (𝜑 → Σ𝑐 ∈ {∅} (∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍↑0)) = 1)
11999, 100, 1183eqtrd 2777 . . . . . 6 (𝜑 → Σ𝑚 ∈ {0}Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = 1)
12071nn0cnd 12040 . . . . . . . . . 10 (𝜑𝑁 ∈ ℂ)
121120mul02d 10918 . . . . . . . . 9 (𝜑 → (0 · 𝑁) = 0)
122121oveq2d 7188 . . . . . . . 8 (𝜑 → (0...(0 · 𝑁)) = (0...0))
123 fz0sn 13100 . . . . . . . 8 (0...0) = {0}
124122, 123eqtrdi 2789 . . . . . . 7 (𝜑 → (0...(0 · 𝑁)) = {0})
125124sumeq1d 15153 . . . . . 6 (𝜑 → Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑚 ∈ {0}Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
12678prodeq1i 15366 . . . . . . . 8 𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑎 ∈ ∅ Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏))
127 prod0 15391 . . . . . . . 8 𝑎 ∈ ∅ Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = 1
128126, 127eqtri 2761 . . . . . . 7 𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = 1
129128a1i 11 . . . . . 6 (𝜑 → ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = 1)
130119, 125, 1293eqtr4rd 2784 . . . . 5 (𝜑 → ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
131130a1d 25 . . . 4 (𝜑 → (0 ≤ 𝑆 → ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
132 simpll 767 . . . . . 6 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝜑𝑠 ∈ ℕ0))
133 simplr 769 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
134 oveq2 7180 . . . . . . . . . . . 12 (𝑚 = 𝑛 → ((1...𝑁)(repr‘𝑠)𝑚) = ((1...𝑁)(repr‘𝑠)𝑛))
135 oveq2 7180 . . . . . . . . . . . . . 14 (𝑚 = 𝑛 → (𝑍𝑚) = (𝑍𝑛))
136135oveq2d 7188 . . . . . . . . . . . . 13 (𝑚 = 𝑛 → (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)))
137136adantr 484 . . . . . . . . . . . 12 ((𝑚 = 𝑛𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)) → (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)))
138134, 137sumeq12dv 15158 . . . . . . . . . . 11 (𝑚 = 𝑛 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)))
139138cbvsumv 15148 . . . . . . . . . 10 Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛))
140139eqeq2i 2751 . . . . . . . . 9 (∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) ↔ ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)))
141 simpl 486 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝑖𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑖)
142141fveq2d 6680 . . . . . . . . . . . . . . 15 ((𝑎 = 𝑖𝑏 ∈ (1...𝑁)) → (𝐿𝑎) = (𝐿𝑖))
143142fveq1d 6678 . . . . . . . . . . . . . 14 ((𝑎 = 𝑖𝑏 ∈ (1...𝑁)) → ((𝐿𝑎)‘𝑏) = ((𝐿𝑖)‘𝑏))
144143oveq1d 7187 . . . . . . . . . . . . 13 ((𝑎 = 𝑖𝑏 ∈ (1...𝑁)) → (((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = (((𝐿𝑖)‘𝑏) · (𝑍𝑏)))
145144sumeq2dv 15155 . . . . . . . . . . . 12 (𝑎 = 𝑖 → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿𝑖)‘𝑏) · (𝑍𝑏)))
146145cbvprodv 15364 . . . . . . . . . . 11 𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑖 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑖)‘𝑏) · (𝑍𝑏))
147 fveq2 6676 . . . . . . . . . . . . . . 15 (𝑏 = 𝑗 → ((𝐿𝑖)‘𝑏) = ((𝐿𝑖)‘𝑗))
148 oveq2 7180 . . . . . . . . . . . . . . 15 (𝑏 = 𝑗 → (𝑍𝑏) = (𝑍𝑗))
149147, 148oveq12d 7190 . . . . . . . . . . . . . 14 (𝑏 = 𝑗 → (((𝐿𝑖)‘𝑏) · (𝑍𝑏)) = (((𝐿𝑖)‘𝑗) · (𝑍𝑗)))
150149cbvsumv 15148 . . . . . . . . . . . . 13 Σ𝑏 ∈ (1...𝑁)(((𝐿𝑖)‘𝑏) · (𝑍𝑏)) = Σ𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗))
151150a1i 11 . . . . . . . . . . . 12 (𝑖 ∈ (0..^𝑠) → Σ𝑏 ∈ (1...𝑁)(((𝐿𝑖)‘𝑏) · (𝑍𝑏)) = Σ𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)))
152151prodeq2i 15367 . . . . . . . . . . 11 𝑖 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑖)‘𝑏) · (𝑍𝑏)) = ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗))
153146, 152eqtri 2761 . . . . . . . . . 10 𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗))
154 fveq2 6676 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑖 → (𝐿𝑎) = (𝐿𝑖))
155 fveq2 6676 . . . . . . . . . . . . . . . . . 18 (𝑎 = 𝑖 → (𝑐𝑎) = (𝑐𝑖))
156154, 155fveq12d 6683 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝑖 → ((𝐿𝑎)‘(𝑐𝑎)) = ((𝐿𝑖)‘(𝑐𝑖)))
157156cbvprodv 15364 . . . . . . . . . . . . . . . 16 𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) = ∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑐𝑖))
158157oveq1i 7182 . . . . . . . . . . . . . . 15 (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)) = (∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑐𝑖)) · (𝑍𝑛))
159158a1i 11 . . . . . . . . . . . . . 14 (𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛) → (∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)) = (∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑐𝑖)) · (𝑍𝑛)))
160159sumeq2i 15151 . . . . . . . . . . . . 13 Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑐𝑖)) · (𝑍𝑛))
161 simpl 486 . . . . . . . . . . . . . . . . . 18 ((𝑐 = 𝑘𝑖 ∈ (0..^𝑠)) → 𝑐 = 𝑘)
162161fveq1d 6678 . . . . . . . . . . . . . . . . 17 ((𝑐 = 𝑘𝑖 ∈ (0..^𝑠)) → (𝑐𝑖) = (𝑘𝑖))
163162fveq2d 6680 . . . . . . . . . . . . . . . 16 ((𝑐 = 𝑘𝑖 ∈ (0..^𝑠)) → ((𝐿𝑖)‘(𝑐𝑖)) = ((𝐿𝑖)‘(𝑘𝑖)))
164163prodeq2dv 15371 . . . . . . . . . . . . . . 15 (𝑐 = 𝑘 → ∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑐𝑖)) = ∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)))
165164oveq1d 7187 . . . . . . . . . . . . . 14 (𝑐 = 𝑘 → (∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑐𝑖)) · (𝑍𝑛)) = (∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))
166165cbvsumv 15148 . . . . . . . . . . . . 13 Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑐𝑖)) · (𝑍𝑛)) = Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛))
167160, 166eqtri 2761 . . . . . . . . . . . 12 Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)) = Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛))
168167a1i 11 . . . . . . . . . . 11 (𝑛 ∈ (0...(𝑠 · 𝑁)) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)) = Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))
169168sumeq2i 15151 . . . . . . . . . 10 Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛))
170153, 169eqeq12i 2753 . . . . . . . . 9 (∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑛)) ↔ ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))
171140, 170bitri 278 . . . . . . . 8 (∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)) ↔ ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))
172171imbi2i 339 . . . . . . 7 ((𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))) ↔ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛))))
173133, 172sylib 221 . . . . . 6 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛))))
174 simpr 488 . . . . . 6 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠 + 1) ≤ 𝑆)
17571ad3antrrr 730 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑁 ∈ ℕ0)
1761ad3antrrr 730 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑆 ∈ ℕ0)
17783ad3antrrr 730 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑍 ∈ ℂ)
178 breprexp.h . . . . . . . 8 (𝜑𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
179178ad3antrrr 730 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
180 simpllr 776 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠 ∈ ℕ0)
181 simpr 488 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠 + 1) ≤ 𝑆)
1822, 180sseldi 3875 . . . . . . . . 9 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠 ∈ ℝ)
183 1red 10722 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 1 ∈ ℝ)
184182, 183readdcld 10750 . . . . . . . . 9 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠 + 1) ∈ ℝ)
1852, 176sseldi 3875 . . . . . . . . 9 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑆 ∈ ℝ)
186182ltp1d 11650 . . . . . . . . . 10 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠 < (𝑠 + 1))
187182, 184, 186ltled 10868 . . . . . . . . 9 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠 ≤ (𝑠 + 1))
188182, 184, 185, 187, 181letrd 10877 . . . . . . . 8 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠𝑆)
189 simplr 769 . . . . . . . . 9 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛))))
190189, 172sylibr 237 . . . . . . . 8 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
191188, 190mpd 15 . . . . . . 7 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
192175, 176, 177, 179, 180, 181, 191breprexplemc 32184 . . . . . 6 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑖 ∈ (0..^𝑠𝑗 ∈ (1...𝑁)(((𝐿𝑖)‘𝑗) · (𝑍𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿𝑖)‘(𝑘𝑖)) · (𝑍𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
193132, 173, 174, 192syl21anc 837 . . . . 5 ((((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))) ∧ (𝑠 + 1) ≤ 𝑆) → ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
194193ex 416 . . . 4 (((𝜑𝑠 ∈ ℕ0) ∧ (𝑠𝑆 → ∏𝑎 ∈ (0..^𝑠𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))) → ((𝑠 + 1) ≤ 𝑆 → ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
19521, 36, 51, 66, 131, 194nn0indd 12162 . . 3 ((𝜑𝑆 ∈ ℕ0) → (𝑆𝑆 → ∏𝑎 ∈ (0..^𝑆𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚))))
1966, 195mpd 15 . 2 ((𝜑𝑆 ∈ ℕ0) → ∏𝑎 ∈ (0..^𝑆𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
1971, 196mpdan 687 1 (𝜑 → ∏𝑎 ∈ (0..^𝑆𝑏 ∈ (1...𝑁)(((𝐿𝑎)‘𝑏) · (𝑍𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑐𝑎)) · (𝑍𝑚)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1542  wcel 2114  Vcvv 3398  wss 3843  c0 4211  ifcif 4414  {csn 4516   class class class wbr 5030  wf 6335  cfv 6339  (class class class)co 7172  m cmap 8439  Fincfn 8557  cc 10615  cr 10616  0cc0 10617  1c1 10618   + caddc 10620   · cmul 10622  cle 10756  cn 11718  0cn0 11978  ...cfz 12983  ..^cfzo 13126  cexp 13523  Σcsu 15137  cprod 15353  reprcrepr 32160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7481  ax-inf2 9179  ax-cnex 10673  ax-resscn 10674  ax-1cn 10675  ax-icn 10676  ax-addcl 10677  ax-addrcl 10678  ax-mulcl 10679  ax-mulrcl 10680  ax-mulcom 10681  ax-addass 10682  ax-mulass 10683  ax-distr 10684  ax-i2m1 10685  ax-1ne0 10686  ax-1rid 10687  ax-rnegex 10688  ax-rrecex 10689  ax-cnre 10690  ax-pre-lttri 10691  ax-pre-lttrn 10692  ax-pre-ltadd 10693  ax-pre-mulgt0 10694  ax-pre-sup 10695
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-pss 3862  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-tp 4521  df-op 4523  df-uni 4797  df-int 4837  df-iun 4883  df-disj 4996  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5429  df-eprel 5434  df-po 5442  df-so 5443  df-fr 5483  df-se 5484  df-we 5485  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-ord 6175  df-on 6176  df-lim 6177  df-suc 6178  df-iota 6297  df-fun 6341  df-fn 6342  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346  df-fv 6347  df-isom 6348  df-riota 7129  df-ov 7175  df-oprab 7176  df-mpo 7177  df-om 7602  df-1st 7716  df-2nd 7717  df-wrecs 7978  df-recs 8039  df-rdg 8077  df-1o 8133  df-er 8322  df-map 8441  df-pm 8442  df-en 8558  df-dom 8559  df-sdom 8560  df-fin 8561  df-sup 8981  df-oi 9049  df-card 9443  df-pnf 10757  df-mnf 10758  df-xr 10759  df-ltxr 10760  df-le 10761  df-sub 10952  df-neg 10953  df-div 11378  df-nn 11719  df-2 11781  df-3 11782  df-n0 11979  df-z 12065  df-uz 12327  df-rp 12475  df-ico 12829  df-fz 12984  df-fzo 13127  df-seq 13463  df-exp 13524  df-hash 13785  df-cj 14550  df-re 14551  df-im 14552  df-sqrt 14686  df-abs 14687  df-clim 14937  df-sum 15138  df-prod 15354  df-repr 32161
This theorem is referenced by:  breprexpnat  32186  vtsprod  32191
  Copyright terms: Public domain W3C validator