Step | Hyp | Ref
| Expression |
1 | | breprexp.s |
. 2
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
2 | | nn0ssre 11982 |
. . . . . 6
⊢
ℕ0 ⊆ ℝ |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ0
⊆ ℝ) |
4 | 3 | sselda 3877 |
. . . 4
⊢ ((𝜑 ∧ 𝑆 ∈ ℕ0) → 𝑆 ∈
ℝ) |
5 | | leid 10816 |
. . . 4
⊢ (𝑆 ∈ ℝ → 𝑆 ≤ 𝑆) |
6 | 4, 5 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ ℕ0) → 𝑆 ≤ 𝑆) |
7 | | breq1 5033 |
. . . . 5
⊢ (𝑡 = 0 → (𝑡 ≤ 𝑆 ↔ 0 ≤ 𝑆)) |
8 | | oveq2 7180 |
. . . . . . 7
⊢ (𝑡 = 0 → (0..^𝑡) = (0..^0)) |
9 | 8 | prodeq1d 15369 |
. . . . . 6
⊢ (𝑡 = 0 → ∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏))) |
10 | | oveq1 7179 |
. . . . . . . 8
⊢ (𝑡 = 0 → (𝑡 · 𝑁) = (0 · 𝑁)) |
11 | 10 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = 0 → (0...(𝑡 · 𝑁)) = (0...(0 · 𝑁))) |
12 | | fveq2 6676 |
. . . . . . . . . 10
⊢ (𝑡 = 0 → (repr‘𝑡) =
(repr‘0)) |
13 | 12 | oveqd 7189 |
. . . . . . . . 9
⊢ (𝑡 = 0 → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘0)𝑚)) |
14 | 8 | prodeq1d 15369 |
. . . . . . . . . . 11
⊢ (𝑡 = 0 → ∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
15 | 14 | oveq1d 7187 |
. . . . . . . . . 10
⊢ (𝑡 = 0 → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
16 | 15 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑡 = 0 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
17 | 13, 16 | sumeq12dv 15158 |
. . . . . . . 8
⊢ (𝑡 = 0 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
18 | 17 | adantr 484 |
. . . . . . 7
⊢ ((𝑡 = 0 ∧ 𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
19 | 11, 18 | sumeq12dv 15158 |
. . . . . 6
⊢ (𝑡 = 0 → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
20 | 9, 19 | eqeq12d 2754 |
. . . . 5
⊢ (𝑡 = 0 → (∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) ↔ ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) |
21 | 7, 20 | imbi12d 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..^𝑠)) |
24 | 23 | prodeq1d 15369 |
. . . . . 6
⊢ (𝑡 = 𝑠 → ∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏))) |
25 | | oveq1 7179 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → (𝑡 · 𝑁) = (𝑠 · 𝑁)) |
26 | 25 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = 𝑠 → (0...(𝑡 · 𝑁)) = (0...(𝑠 · 𝑁))) |
27 | | fveq2 6676 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (repr‘𝑡) = (repr‘𝑠)) |
28 | 27 | oveqd 7189 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘𝑠)𝑚)) |
29 | 23 | prodeq1d 15369 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑠 → ∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
30 | 29 | oveq1d 7187 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
31 | 30 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑡 = 𝑠 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
32 | 28, 31 | sumeq12dv 15158 |
. . . . . . . 8
⊢ (𝑡 = 𝑠 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
33 | 32 | adantr 484 |
. . . . . . 7
⊢ ((𝑡 = 𝑠 ∧ 𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
34 | 26, 33 | sumeq12dv 15158 |
. . . . . 6
⊢ (𝑡 = 𝑠 → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
35 | 24, 34 | eqeq12d 2754 |
. . . . 5
⊢ (𝑡 = 𝑠 → (∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) ↔ ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) |
36 | 22, 35 | imbi12d 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))) |
39 | 38 | prodeq1d 15369 |
. . . . . 6
⊢ (𝑡 = (𝑠 + 1) → ∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏))) |
40 | | oveq1 7179 |
. . . . . . . 8
⊢ (𝑡 = (𝑠 + 1) → (𝑡 · 𝑁) = ((𝑠 + 1) · 𝑁)) |
41 | 40 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = (𝑠 + 1) → (0...(𝑡 · 𝑁)) = (0...((𝑠 + 1) · 𝑁))) |
42 | | fveq2 6676 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑠 + 1) → (repr‘𝑡) = (repr‘(𝑠 + 1))) |
43 | 42 | oveqd 7189 |
. . . . . . . . 9
⊢ (𝑡 = (𝑠 + 1) → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘(𝑠 + 1))𝑚)) |
44 | 38 | prodeq1d 15369 |
. . . . . . . . . . 11
⊢ (𝑡 = (𝑠 + 1) → ∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎))) |
45 | 44 | oveq1d 7187 |
. . . . . . . . . 10
⊢ (𝑡 = (𝑠 + 1) → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
46 | 45 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑡 = (𝑠 + 1) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
47 | 43, 46 | sumeq12dv 15158 |
. . . . . . . 8
⊢ (𝑡 = (𝑠 + 1) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
48 | 47 | adantr 484 |
. . . . . . 7
⊢ ((𝑡 = (𝑠 + 1) ∧ 𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
49 | 41, 48 | sumeq12dv 15158 |
. . . . . 6
⊢ (𝑡 = (𝑠 + 1) → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
50 | 39, 49 | eqeq12d 2754 |
. . . . 5
⊢ (𝑡 = (𝑠 + 1) → (∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) ↔ ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) |
51 | 37, 50 | imbi12d 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..^𝑆)) |
54 | 53 | prodeq1d 15369 |
. . . . . 6
⊢ (𝑡 = 𝑆 → ∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏))) |
55 | | oveq1 7179 |
. . . . . . . 8
⊢ (𝑡 = 𝑆 → (𝑡 · 𝑁) = (𝑆 · 𝑁)) |
56 | 55 | oveq2d 7188 |
. . . . . . 7
⊢ (𝑡 = 𝑆 → (0...(𝑡 · 𝑁)) = (0...(𝑆 · 𝑁))) |
57 | | fveq2 6676 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑆 → (repr‘𝑡) = (repr‘𝑆)) |
58 | 57 | oveqd 7189 |
. . . . . . . . 9
⊢ (𝑡 = 𝑆 → ((1...𝑁)(repr‘𝑡)𝑚) = ((1...𝑁)(repr‘𝑆)𝑚)) |
59 | 53 | prodeq1d 15369 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑆 → ∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎))) |
60 | 59 | oveq1d 7187 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑆 → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
61 | 60 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑡 = 𝑆 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)) → (∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
62 | 58, 61 | sumeq12dv 15158 |
. . . . . . . 8
⊢ (𝑡 = 𝑆 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
63 | 62 | adantr 484 |
. . . . . . 7
⊢ ((𝑡 = 𝑆 ∧ 𝑚 ∈ (0...(𝑡 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
64 | 56, 63 | sumeq12dv 15158 |
. . . . . 6
⊢ (𝑡 = 𝑆 → Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
65 | 54, 64 | eqeq12d 2754 |
. . . . 5
⊢ (𝑡 = 𝑆 → (∏𝑎 ∈ (0..^𝑡)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑡 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑡)𝑚)(∏𝑎 ∈ (0..^𝑡)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) ↔ ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) |
66 | 52, 65 | imbi12d 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...𝑁) ⊆
ℕ |
69 | 68 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1...𝑁) ⊆ ℕ) |
70 | | 0zd 12076 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈
ℤ) |
71 | | breprexp.n |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
72 | 69, 70, 71 | repr0 32163 |
. . . . . . . . . . 11
⊢ (𝜑 → ((1...𝑁)(repr‘0)0) = if(0 = 0, {∅},
∅)) |
73 | | eqid 2738 |
. . . . . . . . . . . 12
⊢ 0 =
0 |
74 | 73 | iftruei 4421 |
. . . . . . . . . . 11
⊢ if(0 = 0,
{∅}, ∅) = {∅} |
75 | 72, 74 | eqtrdi 2789 |
. . . . . . . . . 10
⊢ (𝜑 → ((1...𝑁)(repr‘0)0) =
{∅}) |
76 | | snfi 8644 |
. . . . . . . . . 10
⊢ {∅}
∈ Fin |
77 | 75, 76 | eqeltrdi 2841 |
. . . . . . . . 9
⊢ (𝜑 → ((1...𝑁)(repr‘0)0) ∈
Fin) |
78 | | fzo0 13154 |
. . . . . . . . . . . . . . . 16
⊢ (0..^0) =
∅ |
79 | 78 | prodeq1i 15366 |
. . . . . . . . . . . . . . 15
⊢
∏𝑎 ∈
(0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ ∅ ((𝐿‘𝑎)‘(𝑐‘𝑎)) |
80 | | prod0 15391 |
. . . . . . . . . . . . . . 15
⊢
∏𝑎 ∈
∅ ((𝐿‘𝑎)‘(𝑐‘𝑎)) = 1 |
81 | 79, 80 | eqtri 2761 |
. . . . . . . . . . . . . 14
⊢
∏𝑎 ∈
(0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) = 1 |
82 | 81 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) = 1) |
83 | | breprexp.z |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑍 ∈ ℂ) |
84 | | exp0 13527 |
. . . . . . . . . . . . . 14
⊢ (𝑍 ∈ ℂ → (𝑍↑0) = 1) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑍↑0) = 1) |
86 | 82, 85 | oveq12d 7190 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) = (1 · 1)) |
87 | | ax-1cn 10675 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
88 | 87 | mulid1i 10725 |
. . . . . . . . . . . 12
⊢ (1
· 1) = 1 |
89 | 86, 88 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) = 1) |
90 | 89, 87 | eqeltrdi 2841 |
. . . . . . . . . 10
⊢ (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) ∈ ℂ) |
91 | 90 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑐 ∈ ((1...𝑁)(repr‘0)0)) → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) ∈ ℂ) |
92 | 77, 91 | fsumcl 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) |
95 | 94 | oveq2d 7188 |
. . . . . . . . . . 11
⊢ ((𝑚 = 0 ∧ 𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)) → (𝑍↑𝑚) = (𝑍↑0)) |
96 | 95 | oveq2d 7188 |
. . . . . . . . . 10
⊢ ((𝑚 = 0 ∧ 𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)) → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0))) |
97 | 93, 96 | sumeq12dv 15158 |
. . . . . . . . 9
⊢ (𝑚 = 0 → Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0))) |
98 | 97 | sumsn 15196 |
. . . . . . . 8
⊢ ((0
∈ ℕ0 ∧ Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) ∈ ℂ) →
Σ𝑚 ∈
{0}Σ𝑐 ∈
((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0))) |
99 | 67, 92, 98 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ {0}Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0))) |
100 | 75 | sumeq1d 15153 |
. . . . . . 7
⊢ (𝜑 → Σ𝑐 ∈ ((1...𝑁)(repr‘0)0)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) = Σ𝑐 ∈ {∅} (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0))) |
101 | | 0ex 5175 |
. . . . . . . . 9
⊢ ∅
∈ V |
102 | 78 | prodeq1i 15366 |
. . . . . . . . . . . . 13
⊢
∏𝑎 ∈
(0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) = ∏𝑎 ∈ ∅ ((𝐿‘𝑎)‘(∅‘𝑎)) |
103 | | prod0 15391 |
. . . . . . . . . . . . 13
⊢
∏𝑎 ∈
∅ ((𝐿‘𝑎)‘(∅‘𝑎)) = 1 |
104 | 102, 103 | eqtri 2761 |
. . . . . . . . . . . 12
⊢
∏𝑎 ∈
(0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) = 1 |
105 | 104 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → ∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) = 1) |
106 | 105, 87 | eqeltrdi 2841 |
. . . . . . . . . 10
⊢ (𝜑 → ∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) ∈ ℂ) |
107 | 85, 87 | eqeltrdi 2841 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑍↑0) ∈ ℂ) |
108 | 106, 107 | mulcld 10741 |
. . . . . . . . 9
⊢ (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) · (𝑍↑0)) ∈ ℂ) |
109 | | fveq1 6675 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = ∅ → (𝑐‘𝑎) = (∅‘𝑎)) |
110 | 109 | fveq2d 6680 |
. . . . . . . . . . . . 13
⊢ (𝑐 = ∅ → ((𝐿‘𝑎)‘(𝑐‘𝑎)) = ((𝐿‘𝑎)‘(∅‘𝑎))) |
111 | 110 | ralrimivw 3097 |
. . . . . . . . . . . 12
⊢ (𝑐 = ∅ → ∀𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ((𝐿‘𝑎)‘(∅‘𝑎))) |
112 | 111 | prodeq2d 15370 |
. . . . . . . . . . 11
⊢ (𝑐 = ∅ → ∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎))) |
113 | 112 | oveq1d 7187 |
. . . . . . . . . 10
⊢ (𝑐 = ∅ → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) = (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) · (𝑍↑0))) |
114 | 113 | sumsn 15196 |
. . . . . . . . 9
⊢ ((∅
∈ V ∧ (∏𝑎
∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) · (𝑍↑0)) ∈ ℂ) →
Σ𝑐 ∈ {∅}
(∏𝑎 ∈
(0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) = (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) · (𝑍↑0))) |
115 | 101, 108,
114 | sylancr 590 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑐 ∈ {∅} (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) = (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) · (𝑍↑0))) |
116 | 105, 85 | oveq12d 7190 |
. . . . . . . . 9
⊢ (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) · (𝑍↑0)) = (1 · 1)) |
117 | 116, 86, 89 | 3eqtr2d 2779 |
. . . . . . . 8
⊢ (𝜑 → (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(∅‘𝑎)) · (𝑍↑0)) = 1) |
118 | 115, 117 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → Σ𝑐 ∈ {∅} (∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑0)) = 1) |
119 | 99, 100, 118 | 3eqtrd 2777 |
. . . . . 6
⊢ (𝜑 → Σ𝑚 ∈ {0}Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = 1) |
120 | 71 | nn0cnd 12040 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℂ) |
121 | 120 | mul02d 10918 |
. . . . . . . . 9
⊢ (𝜑 → (0 · 𝑁) = 0) |
122 | 121 | oveq2d 7188 |
. . . . . . . 8
⊢ (𝜑 → (0...(0 · 𝑁)) = (0...0)) |
123 | | fz0sn 13100 |
. . . . . . . 8
⊢ (0...0) =
{0} |
124 | 122, 123 | eqtrdi 2789 |
. . . . . . 7
⊢ (𝜑 → (0...(0 · 𝑁)) = {0}) |
125 | 124 | sumeq1d 15153 |
. . . . . 6
⊢ (𝜑 → Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ {0}Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
126 | 78 | prodeq1i 15366 |
. . . . . . . 8
⊢
∏𝑎 ∈
(0..^0)Σ𝑏 ∈
(1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ ∅ Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) |
127 | | prod0 15391 |
. . . . . . . 8
⊢
∏𝑎 ∈
∅ Σ𝑏 ∈
(1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = 1 |
128 | 126, 127 | eqtri 2761 |
. . . . . . 7
⊢
∏𝑎 ∈
(0..^0)Σ𝑏 ∈
(1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = 1 |
129 | 128 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = 1) |
130 | 119, 125,
129 | 3eqtr4rd 2784 |
. . . . 5
⊢ (𝜑 → ∏𝑎 ∈ (0..^0)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(0 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘0)𝑚)(∏𝑎 ∈ (0..^0)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
131 | 130 | a1d 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
⊢ (𝑚 = 𝑛 → (𝑍↑𝑚) = (𝑍↑𝑛)) |
136 | 135 | oveq2d 7188 |
. . . . . . . . . . . . 13
⊢ (𝑚 = 𝑛 → (∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛))) |
137 | 136 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 𝑛 ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)) → (∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛))) |
138 | 134, 137 | sumeq12dv 15158 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑛 → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛))) |
139 | 138 | cbvsumv 15148 |
. . . . . . . . . 10
⊢
Σ𝑚 ∈
(0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) |
140 | 139 | eqeq2i 2751 |
. . . . . . . . 9
⊢
(∏𝑎 ∈
(0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) ↔ ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛))) |
141 | | simpl 486 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑎 = 𝑖 ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑖) |
142 | 141 | fveq2d 6680 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝑖 ∧ 𝑏 ∈ (1...𝑁)) → (𝐿‘𝑎) = (𝐿‘𝑖)) |
143 | 142 | fveq1d 6678 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 = 𝑖 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) = ((𝐿‘𝑖)‘𝑏)) |
144 | 143 | oveq1d 7187 |
. . . . . . . . . . . . 13
⊢ ((𝑎 = 𝑖 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (((𝐿‘𝑖)‘𝑏) · (𝑍↑𝑏))) |
145 | 144 | sumeq2dv 15155 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑖 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑏) · (𝑍↑𝑏))) |
146 | 145 | cbvprodv 15364 |
. . . . . . . . . . 11
⊢
∏𝑎 ∈
(0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑖 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑏) · (𝑍↑𝑏)) |
147 | | fveq2 6676 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑗 → ((𝐿‘𝑖)‘𝑏) = ((𝐿‘𝑖)‘𝑗)) |
148 | | oveq2 7180 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = 𝑗 → (𝑍↑𝑏) = (𝑍↑𝑗)) |
149 | 147, 148 | oveq12d 7190 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝑗 → (((𝐿‘𝑖)‘𝑏) · (𝑍↑𝑏)) = (((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗))) |
150 | 149 | cbvsumv 15148 |
. . . . . . . . . . . . 13
⊢
Σ𝑏 ∈
(1...𝑁)(((𝐿‘𝑖)‘𝑏) · (𝑍↑𝑏)) = Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) |
151 | 150 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝑖 ∈ (0..^𝑠) → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑏) · (𝑍↑𝑏)) = Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗))) |
152 | 151 | prodeq2i 15367 |
. . . . . . . . . . 11
⊢
∏𝑖 ∈
(0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑏) · (𝑍↑𝑏)) = ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) |
153 | 146, 152 | eqtri 2761 |
. . . . . . . . . 10
⊢
∏𝑎 ∈
(0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) |
154 | | fveq2 6676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑖 → (𝐿‘𝑎) = (𝐿‘𝑖)) |
155 | | fveq2 6676 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 = 𝑖 → (𝑐‘𝑎) = (𝑐‘𝑖)) |
156 | 154, 155 | fveq12d 6683 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = 𝑖 → ((𝐿‘𝑎)‘(𝑐‘𝑎)) = ((𝐿‘𝑖)‘(𝑐‘𝑖))) |
157 | 156 | cbvprodv 15364 |
. . . . . . . . . . . . . . . 16
⊢
∏𝑎 ∈
(0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) = ∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑐‘𝑖)) |
158 | 157 | oveq1i 7182 |
. . . . . . . . . . . . . . 15
⊢
(∏𝑎 ∈
(0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) = (∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑐‘𝑖)) · (𝑍↑𝑛)) |
159 | 158 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛) → (∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) = (∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑐‘𝑖)) · (𝑍↑𝑛))) |
160 | 159 | sumeq2i 15151 |
. . . . . . . . . . . . 13
⊢
Σ𝑐 ∈
((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑐‘𝑖)) · (𝑍↑𝑛)) |
161 | | simpl 486 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑐 = 𝑘 ∧ 𝑖 ∈ (0..^𝑠)) → 𝑐 = 𝑘) |
162 | 161 | fveq1d 6678 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑐 = 𝑘 ∧ 𝑖 ∈ (0..^𝑠)) → (𝑐‘𝑖) = (𝑘‘𝑖)) |
163 | 162 | fveq2d 6680 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑐 = 𝑘 ∧ 𝑖 ∈ (0..^𝑠)) → ((𝐿‘𝑖)‘(𝑐‘𝑖)) = ((𝐿‘𝑖)‘(𝑘‘𝑖))) |
164 | 163 | prodeq2dv 15371 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 = 𝑘 → ∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑐‘𝑖)) = ∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖))) |
165 | 164 | oveq1d 7187 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝑘 → (∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑐‘𝑖)) · (𝑍↑𝑛)) = (∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛))) |
166 | 165 | cbvsumv 15148 |
. . . . . . . . . . . . 13
⊢
Σ𝑐 ∈
((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑐‘𝑖)) · (𝑍↑𝑛)) = Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)) |
167 | 160, 166 | eqtri 2761 |
. . . . . . . . . . . 12
⊢
Σ𝑐 ∈
((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) = Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)) |
168 | 167 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (0...(𝑠 · 𝑁)) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) = Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛))) |
169 | 168 | sumeq2i 15151 |
. . . . . . . . . 10
⊢
Σ𝑛 ∈
(0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)) |
170 | 153, 169 | eqeq12i 2753 |
. . . . . . . . 9
⊢
(∏𝑎 ∈
(0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑛)) ↔ ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛))) |
171 | 140, 170 | bitri 278 |
. . . . . . . 8
⊢
(∏𝑎 ∈
(0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) ↔ ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛))) |
172 | 171 | imbi2i 339 |
. . . . . . 7
⊢ ((𝑠 ≤ 𝑆 → ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) ↔ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) |
173 | 133, 172 | sylib 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) ≤ 𝑆) |
175 | 71 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑁 ∈
ℕ0) |
176 | 1 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑆 ∈
ℕ0) |
177 | 83 | ad3antrrr 730 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑍 ∈ ℂ) |
178 | | breprexp.h |
. . . . . . . 8
⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
179 | 178 | ad3antrrr 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) ≤ 𝑆) |
182 | 2, 180 | sseldi 3875 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠 ∈ ℝ) |
183 | | 1red 10722 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 1 ∈ ℝ) |
184 | 182, 183 | readdcld 10750 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠 + 1) ∈ ℝ) |
185 | 2, 176 | sseldi 3875 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑆 ∈ ℝ) |
186 | 182 | ltp1d 11650 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠 < (𝑠 + 1)) |
187 | 182, 184,
186 | ltled 10868 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → 𝑠 ≤ (𝑠 + 1)) |
188 | 182, 184,
185, 187, 181 | letrd 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..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) |
190 | 189, 172 | sylibr 237 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → (𝑠 ≤ 𝑆 → ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) |
191 | 188, 190 | mpd 15 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
192 | 175, 176,
177, 179, 180, 181, 191 | breprexplemc 32184 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑖 ∈ (0..^𝑠)Σ𝑗 ∈ (1...𝑁)(((𝐿‘𝑖)‘𝑗) · (𝑍↑𝑗)) = Σ𝑛 ∈ (0...(𝑠 · 𝑁))Σ𝑘 ∈ ((1...𝑁)(repr‘𝑠)𝑛)(∏𝑖 ∈ (0..^𝑠)((𝐿‘𝑖)‘(𝑘‘𝑖)) · (𝑍↑𝑛)))) ∧ (𝑠 + 1) ≤ 𝑆) → ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
193 | 132, 173,
174, 192 | syl21anc 837 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) ∧ (𝑠 + 1) ≤ 𝑆) → ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
194 | 193 | ex 416 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ ℕ0) ∧ (𝑠 ≤ 𝑆 → ∏𝑎 ∈ (0..^𝑠)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑠 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑠)𝑚)(∏𝑎 ∈ (0..^𝑠)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) → ((𝑠 + 1) ≤ 𝑆 → ∏𝑎 ∈ (0..^(𝑠 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑠 + 1) · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘(𝑠 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑠 + 1))((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) |
195 | 21, 36, 51, 66, 131, 194 | nn0indd 12162 |
. . 3
⊢ ((𝜑 ∧ 𝑆 ∈ ℕ0) → (𝑆 ≤ 𝑆 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)))) |
196 | 6, 195 | mpd 15 |
. 2
⊢ ((𝜑 ∧ 𝑆 ∈ ℕ0) →
∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
197 | 1, 196 | mpdan 687 |
1
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((𝐿‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |