Step | Hyp | Ref
| Expression |
1 | | breprexp.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
2 | | breprexp.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
3 | | breprexp.z |
. . . 4
⊢ (𝜑 → 𝑍 ∈ ℂ) |
4 | | fvex 6789 |
. . . . . 6
⊢
((𝟭‘ℕ)‘𝐴) ∈ V |
5 | 4 | fconst 6662 |
. . . . 5
⊢
((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶{((𝟭‘ℕ)‘𝐴)} |
6 | | nnex 11977 |
. . . . . . . . 9
⊢ ℕ
∈ V |
7 | | breprexpnat.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℕ) |
8 | | indf 31980 |
. . . . . . . . 9
⊢ ((ℕ
∈ V ∧ 𝐴 ⊆
ℕ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}) |
9 | 6, 7, 8 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 →
((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}) |
10 | | 0cn 10965 |
. . . . . . . . 9
⊢ 0 ∈
ℂ |
11 | | ax-1cn 10927 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
12 | | prssi 4756 |
. . . . . . . . 9
⊢ ((0
∈ ℂ ∧ 1 ∈ ℂ) → {0, 1} ⊆
ℂ) |
13 | 10, 11, 12 | mp2an 689 |
. . . . . . . 8
⊢ {0, 1}
⊆ ℂ |
14 | | fss 6619 |
. . . . . . . 8
⊢
((((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1} ∧ {0, 1} ⊆
ℂ) → ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
15 | 9, 13, 14 | sylancl 586 |
. . . . . . 7
⊢ (𝜑 →
((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
16 | | cnex 10950 |
. . . . . . . 8
⊢ ℂ
∈ V |
17 | 16, 6 | elmap 8657 |
. . . . . . 7
⊢
(((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m
ℕ) ↔ ((𝟭‘ℕ)‘𝐴):ℕ⟶ℂ) |
18 | 15, 17 | sylibr 233 |
. . . . . 6
⊢ (𝜑 →
((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m
ℕ)) |
19 | 4 | snss 4721 |
. . . . . 6
⊢
(((𝟭‘ℕ)‘𝐴) ∈ (ℂ ↑m
ℕ) ↔ {((𝟭‘ℕ)‘𝐴)} ⊆ (ℂ ↑m
ℕ)) |
20 | 18, 19 | sylib 217 |
. . . . 5
⊢ (𝜑 →
{((𝟭‘ℕ)‘𝐴)} ⊆ (ℂ ↑m
ℕ)) |
21 | | fss 6619 |
. . . . 5
⊢
((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶{((𝟭‘ℕ)‘𝐴)} ∧
{((𝟭‘ℕ)‘𝐴)} ⊆ (ℂ ↑m ℕ))
→ ((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
22 | 5, 20, 21 | sylancr 587 |
. . . 4
⊢ (𝜑 → ((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)}):(0..^𝑆)⟶(ℂ ↑m
ℕ)) |
23 | 1, 2, 3, 22 | breprexp 32610 |
. . 3
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
24 | 4 | fvconst2 7081 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0..^𝑆) → (((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴)) |
25 | 24 | ad2antlr 724 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → (((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎) = ((𝟭‘ℕ)‘𝐴)) |
26 | 25 | fveq1d 6778 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → ((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) = (((𝟭‘ℕ)‘𝐴)‘𝑏)) |
27 | 26 | oveq1d 7292 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → (((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ((((𝟭‘ℕ)‘𝐴)‘𝑏) · (𝑍↑𝑏))) |
28 | 27 | sumeq2dv 15413 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)((((𝟭‘ℕ)‘𝐴)‘𝑏) · (𝑍↑𝑏))) |
29 | 6 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → ℕ ∈ V) |
30 | | fzfi 13690 |
. . . . . . . 8
⊢
(1...𝑁) ∈
Fin |
31 | 30 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → (1...𝑁) ∈ Fin) |
32 | | fz1ssnn 13285 |
. . . . . . . 8
⊢
(1...𝑁) ⊆
ℕ |
33 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → (1...𝑁) ⊆ ℕ) |
34 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → 𝐴 ⊆ ℕ) |
35 | 3 | ad2antrr 723 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ) |
36 | | nnssnn0 12234 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℕ0 |
37 | 32, 36 | sstri 3931 |
. . . . . . . . 9
⊢
(1...𝑁) ⊆
ℕ0 |
38 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁)) |
39 | 37, 38 | sselid 3920 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0) |
40 | 35, 39 | expcld 13862 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ) |
41 | 29, 31, 33, 34, 40 | indsumin 31987 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ (1...𝑁)((((𝟭‘ℕ)‘𝐴)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ ((1...𝑁) ∩ 𝐴)(𝑍↑𝑏)) |
42 | | incom 4136 |
. . . . . . . 8
⊢
((1...𝑁) ∩ 𝐴) = (𝐴 ∩ (1...𝑁)) |
43 | 42 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → ((1...𝑁) ∩ 𝐴) = (𝐴 ∩ (1...𝑁))) |
44 | 43 | sumeq1d 15411 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ ((1...𝑁) ∩ 𝐴)(𝑍↑𝑏) = Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)) |
45 | 28, 41, 44 | 3eqtrd 2782 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑆)) → Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)) |
46 | 45 | prodeq2dv 15631 |
. . . 4
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)) |
47 | | fzofi 13692 |
. . . . . 6
⊢
(0..^𝑆) ∈
Fin |
48 | 47 | a1i 11 |
. . . . 5
⊢ (𝜑 → (0..^𝑆) ∈ Fin) |
49 | | inss2 4165 |
. . . . . . . 8
⊢ (𝐴 ∩ (1...𝑁)) ⊆ (1...𝑁) |
50 | | ssfi 8954 |
. . . . . . . 8
⊢
(((1...𝑁) ∈ Fin
∧ (𝐴 ∩ (1...𝑁)) ⊆ (1...𝑁)) → (𝐴 ∩ (1...𝑁)) ∈ Fin) |
51 | 30, 49, 50 | mp2an 689 |
. . . . . . 7
⊢ (𝐴 ∩ (1...𝑁)) ∈ Fin |
52 | 51 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∩ (1...𝑁)) ∈ Fin) |
53 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → 𝑍 ∈ ℂ) |
54 | 49, 37 | sstri 3931 |
. . . . . . . 8
⊢ (𝐴 ∩ (1...𝑁)) ⊆
ℕ0 |
55 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → 𝑏 ∈ (𝐴 ∩ (1...𝑁))) |
56 | 54, 55 | sselid 3920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → 𝑏 ∈ ℕ0) |
57 | 53, 56 | expcld 13862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ (𝐴 ∩ (1...𝑁))) → (𝑍↑𝑏) ∈ ℂ) |
58 | 52, 57 | fsumcl 15443 |
. . . . 5
⊢ (𝜑 → Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) ∈ ℂ) |
59 | | fprodconst 15686 |
. . . . 5
⊢
(((0..^𝑆) ∈ Fin
∧ Σ𝑏 ∈
(𝐴 ∩ (1...𝑁))(𝑍↑𝑏) ∈ ℂ) → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑(♯‘(0..^𝑆)))) |
60 | 48, 58, 59 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑(♯‘(0..^𝑆)))) |
61 | | hashfzo0 14143 |
. . . . . 6
⊢ (𝑆 ∈ ℕ0
→ (♯‘(0..^𝑆)) = 𝑆) |
62 | 2, 61 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘(0..^𝑆)) = 𝑆) |
63 | 62 | oveq2d 7293 |
. . . 4
⊢ (𝜑 → (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑(♯‘(0..^𝑆))) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆)) |
64 | 46, 60, 63 | 3eqtrd 2782 |
. . 3
⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑆)Σ𝑏 ∈ (1...𝑁)(((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆)) |
65 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ⊆ ℕ) |
66 | | fzssz 13256 |
. . . . . . . 8
⊢
(0...(𝑆 ·
𝑁)) ⊆
ℤ |
67 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ (0...(𝑆 · 𝑁))) |
68 | 66, 67 | sselid 3920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℤ) |
69 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑆 ∈
ℕ0) |
70 | 30 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (1...𝑁) ∈ Fin) |
71 | 65, 68, 69, 70 | reprfi 32593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((1...𝑁)(repr‘𝑆)𝑚) ∈ Fin) |
72 | 3 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑍 ∈ ℂ) |
73 | | fz0ssnn0 13349 |
. . . . . . . 8
⊢
(0...(𝑆 ·
𝑁)) ⊆
ℕ0 |
74 | 73, 67 | sselid 3920 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝑚 ∈ ℕ0) |
75 | 72, 74 | expcld 13862 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (𝑍↑𝑚) ∈ ℂ) |
76 | 47 | a1i 11 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (0..^𝑆) ∈ Fin) |
77 | 9 | ad3antrrr 727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) →
((𝟭‘ℕ)‘𝐴):ℕ⟶{0, 1}) |
78 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (1...𝑁) ⊆ ℕ) |
79 | 68 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑚 ∈ ℤ) |
80 | 69 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑆 ∈
ℕ0) |
81 | | simpr 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) |
82 | 78, 79, 80, 81 | reprf 32589 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → 𝑐:(0..^𝑆)⟶(1...𝑁)) |
83 | 82 | ffvelrnda 6963 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ (1...𝑁)) |
84 | 32, 83 | sselid 3920 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑐‘𝑎) ∈ ℕ) |
85 | 77, 84 | ffvelrnd 6964 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) →
(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) ∈ {0, 1}) |
86 | 13, 85 | sselid 3920 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) ∧ 𝑎 ∈ (0..^𝑆)) →
(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) ∈ ℂ) |
87 | 76, 86 | fprodcl 15660 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) ∈ ℂ) |
88 | 71, 75, 87 | fsummulc1 15495 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
89 | 7 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → 𝐴 ⊆ ℕ) |
90 | 89, 68, 69, 70, 65 | hashreprin 32597 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → (♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
91 | 90 | oveq1d 7292 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚)) = (Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
92 | 24 | fveq1d 6778 |
. . . . . . . . . 10
⊢ (𝑎 ∈ (0..^𝑆) → ((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
93 | 92 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑎 ∈ (0..^𝑆)) → ((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = (((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
94 | 93 | prodeq2dv 15631 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → ∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
95 | 94 | adantr 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → ∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎))) |
96 | 95 | oveq1d 7292 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) ∧ 𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)) → (∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
97 | 96 | sumeq2dv 15413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)(((𝟭‘ℕ)‘𝐴)‘(𝑐‘𝑎)) · (𝑍↑𝑚))) |
98 | 88, 91, 97 | 3eqtr4rd 2789 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑆 · 𝑁))) → Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
99 | 98 | sumeq2dv 15413 |
. . 3
⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑆 · 𝑁))Σ𝑐 ∈ ((1...𝑁)(repr‘𝑆)𝑚)(∏𝑎 ∈ (0..^𝑆)((((0..^𝑆) ×
{((𝟭‘ℕ)‘𝐴)})‘𝑎)‘(𝑐‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
100 | 23, 64, 99 | 3eqtr3d 2786 |
. 2
⊢ (𝜑 → (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
101 | | breprexpnat.p |
. . 3
⊢ 𝑃 = Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏) |
102 | 101 | oveq1i 7287 |
. 2
⊢ (𝑃↑𝑆) = (Σ𝑏 ∈ (𝐴 ∩ (1...𝑁))(𝑍↑𝑏)↑𝑆) |
103 | | breprexpnat.r |
. . . . 5
⊢ 𝑅 = (♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) |
104 | 103 | oveq1i 7287 |
. . . 4
⊢ (𝑅 · (𝑍↑𝑚)) = ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚)) |
105 | 104 | a1i 11 |
. . 3
⊢ (𝑚 ∈ (0...(𝑆 · 𝑁)) → (𝑅 · (𝑍↑𝑚)) = ((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚))) |
106 | 105 | sumeq2i 15409 |
. 2
⊢
Σ𝑚 ∈
(0...(𝑆 · 𝑁))(𝑅 · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))((♯‘((𝐴 ∩ (1...𝑁))(repr‘𝑆)𝑚)) · (𝑍↑𝑚)) |
107 | 100, 102,
106 | 3eqtr4g 2803 |
1
⊢ (𝜑 → (𝑃↑𝑆) = Σ𝑚 ∈ (0...(𝑆 · 𝑁))(𝑅 · (𝑍↑𝑚))) |