Theorem breprexplemc 32612

Description: Lemma for breprexp 32613 (induction step). (Contributed by Thierry Arnoux, 6-Dec-2021.)

Hypotheses

Ref	Expression
breprexp.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
breprexp.s	⊢ (𝜑 → 𝑆 ∈ ℕ0)
breprexp.z	⊢ (𝜑 → 𝑍 ∈ ℂ)
breprexp.h	⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
breprexplemc.t	⊢ (𝜑 → 𝑇 ∈ ℕ0)
breprexplemc.s	⊢ (𝜑 → (𝑇 + 1) ≤ 𝑆)
breprexplemc.1	⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))

Assertion

Ref	Expression
breprexplemc	⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))

Distinct variable groups:   𝑚,𝑁   𝑆,𝑎,𝑚   𝑚,𝑍   𝑚,𝐿   𝑇,𝑎,𝑏,𝑑,𝑚   𝑍,𝑎,𝑏,𝑑   𝐿,𝑎,𝑏,𝑑   𝜑,𝑎,𝑏,𝑑,𝑚   𝑁,𝑎,𝑏,𝑑

Allowed substitution hints:   𝑆(𝑏,𝑑)

Proof of Theorem breprexplemc

Dummy variables 𝑛 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		breprexplemc.t	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ ℕ0)
2		nn0uz 12620	. . . . 5 ⊢ ℕ0 = (ℤ≥‘0)
3	1, 2	eleqtrdi 2849	. . . 4 ⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘0))
4		fzosplitsn 13495	. . . 4 ⊢ (𝑇 ∈ (ℤ≥‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
6	5	prodeq1d 15631	. 2 ⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)))
7		nfv 1917	. . 3 ⊢ Ⅎ𝑎𝜑
8		nfcv 2907	. . 3 ⊢ Ⅎ𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))
9		fzofi 13694	. . . 4 ⊢ (0..^𝑇) ∈ Fin
10	9	a1i 11	. . 3 ⊢ (𝜑 → (0..^𝑇) ∈ Fin)
11		fzonel 13401	. . . 4 ⊢ ¬ 𝑇 ∈ (0..^𝑇)
12	11	a1i 11	. . 3 ⊢ (𝜑 → ¬ 𝑇 ∈ (0..^𝑇))
13		fzfid 13693	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin)
14		breprexp.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
15	14	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
16		breprexp.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℕ0)
17	16	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
18		breprexp.z	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ ℂ)
19	18	ad2antrr 723	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
20		breprexp.h	. . . . . . . 8 ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
21	20	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
22	21	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
23	1	nn0zd 12424	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ℤ)
24	16	nn0zd 12424	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ℤ)
25	1	nn0red 12294	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℝ)
26		1red 10976	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
27	25, 26	readdcld 11004	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 + 1) ∈ ℝ)
28	16	nn0red 12294	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
29	25	lep1d 11906	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ≤ (𝑇 + 1))
30		breprexplemc.s	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 + 1) ≤ 𝑆)
31	25, 27, 28, 29, 30	letrd 11132	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≤ 𝑆)
32		eluz1 12586	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℤ → (𝑆 ∈ (ℤ≥‘𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)))
33	32	biimpar 478	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)) → 𝑆 ∈ (ℤ≥‘𝑇))
34	23, 24, 31, 33	syl12anc 834	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘𝑇))
35		fzoss2 13415	. . . . . . . . 9 ⊢ (𝑆 ∈ (ℤ≥‘𝑇) → (0..^𝑇) ⊆ (0..^𝑆))
36	34, 35	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑇) ⊆ (0..^𝑆))
37	36	sselda 3921	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
38	37	adantr 481	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆))
39		fz1ssnn 13287	. . . . . . . 8 ⊢ (1...𝑁) ⊆ ℕ
40	39	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
41	40	sselda 3921	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
42	15, 17, 19, 22, 38, 41	breprexplemb 32611	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) ∈ ℂ)
43		nnssnn0 12236	. . . . . . . . . . 11 ⊢ ℕ ⊆ ℕ0
44	39, 43	sstri 3930	. . . . . . . . . 10 ⊢ (1...𝑁) ⊆ ℕ0
45	44	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ0)
46	45	ralrimivw 3104	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆ ℕ0)
47	46	r19.21bi 3134	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ0)
48	47	sselda 3921	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
49	19, 48	expcld 13864	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ)
50	42, 49	mulcld 10995	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
51	13, 50	fsumcl 15445	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
52		simpl 483	. . . . . . 7 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇)
53	52	fveq2d 6778	. . . . . 6 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (𝐿‘𝑎) = (𝐿‘𝑇))
54	53	fveq1d 6776	. . . . 5 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) = ((𝐿‘𝑇)‘𝑏))
55	54	oveq1d 7290	. . . 4 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))
56	55	sumeq2dv 15415	. . 3 ⊢ (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))
57		fzfid 13693	. . . 4 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
58	14	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
59	16	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
60	18	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
61	20	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
62	1	nn0ge0d 12296	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝑇)
63		zltp1le 12370	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
64	23, 24, 63	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
65	30, 64	mpbird 256	. . . . . . . 8 ⊢ (𝜑 → 𝑇 < 𝑆)
66		0zd 12331	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
67		elfzo 13389	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆)))
68	23, 66, 24, 67	syl3anc 1370	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆)))
69	62, 65, 68	mpbir2and 710	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (0..^𝑆))
70	69	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
71	39	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
72	71	sselda 3921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
73	58, 59, 60, 61, 70, 72	breprexplemb 32611	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
74	45	sselda 3921	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
75	60, 74	expcld 13864	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ)
76	73, 75	mulcld 10995	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
77	57, 76	fsumcl 15445	. . 3 ⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
78	7, 8, 10, 1, 12, 51, 56, 77	fprodsplitsn 15699	. 2 ⊢ (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
79		breprexplemc.1	. . . 4 ⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
80	79	oveq1d 7290	. . 3 ⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
81		fzfid 13693	. . . 4 ⊢ (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin)
82	39	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ)
83		simpr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁)))
84	83	elfzelzd 13257	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ)
85	1	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈ ℕ0)
86	57	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin)
87	82, 84, 85, 86	reprfi 32596	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
88	9	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
89	14	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈ ℕ0)
90	89	ad2antrr 723	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
91	16	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
92	18	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
93	20	ad3antrrr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
94	36	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
95	94	sselda 3921	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
96	39	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
97	84	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ)
98	85	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
99		simplr 766	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
100	96, 97, 98, 99	reprf 32592	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
101		simpr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
102	100, 101	ffvelrnd 6962	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
103	39, 102	sselid 3919	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
104	90, 91, 92, 93, 95, 103	breprexplemb 32611	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
105	88, 104	fprodcl 15662	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
106	18	ad2antrr 723	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
107		fz0ssnn0 13351	. . . . . . . . 9 ⊢ (0...(𝑇 · 𝑁)) ⊆ ℕ0
108	107, 83	sselid 3919	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0)
109	108	adantr 481	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
110	106, 109	expcld 13864	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ)
111	105, 110	mulcld 10995	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
112	87, 111	fsumcl 15445	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
113	81, 57, 112, 76	fsum2mul 15501	. . 3 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
114	39	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
115		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁)))
116	115	elfzelzd 13257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ)
117	116	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
118		simpr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
119	118	elfzelzd 13257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
120	117, 119	zsubcld 12431	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − 𝑏) ∈ ℤ)
121	1	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈ ℕ0)
122	121	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
123	57	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin)
124	123	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
125	114, 120, 122, 124	reprfi 32596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)) ∈ Fin)
126	73	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
127	18	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ)
128		fz0ssnn0 13351	. . . . . . . . . . . . 13 ⊢ (0...((𝑇 + 1) · 𝑁)) ⊆ ℕ0
129	128, 115	sselid 3919	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0)
130	127, 129	expcld 13864	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍↑𝑚) ∈ ℂ)
131	130	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑚) ∈ ℂ)
132	126, 131	mulcld 10995	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) ∈ ℂ)
133	9	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (0..^𝑇) ∈ Fin)
134	14	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈ ℕ0)
135	134	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
136	135	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
137	16	ad4antr 729	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
138	127	ad3antrrr 727	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
139	20	ad4antr 729	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
140	37	ad5ant15 756	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
141	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
142	120	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚 − 𝑏) ∈ ℤ)
143	122	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
144		simplr 766	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)))
145	141, 142, 143, 144	reprf 32592	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
146		simpr 485	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
147	145, 146	ffvelrnd 6962	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
148	39, 147	sselid 3919	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
149	136, 137, 138, 139, 140, 148	breprexplemb 32611	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
150	133, 149	fprodcl 15662	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
151	125, 132, 150	fsummulc1 15497	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
152	151	sumeq2dv 15415	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
153		elfzle2 13260	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
154	153	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
155	134	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ0)
156	16	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈ ℕ0)
157	127	ad2antrr 723	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ)
158	20	ad3antrrr 727	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
159	23	peano2zd 12429	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇 + 1) ∈ ℤ)
160		eluz 12596	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈ (ℤ≥‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆))
161	160	biimpar 478	. . . . . . . . . . . . . . 15 ⊢ ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ≥‘(𝑇 + 1)))
162	159, 24, 30, 161	syl21anc 835	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘(𝑇 + 1)))
163		fzoss2 13415	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (ℤ≥‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
164	162, 163	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
165	164	ad3antrrr 727	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
166		simplr 766	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1)))
167	165, 166	sseldd 3922	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆))
168		simpr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
169	155, 156, 157, 158, 167, 168	breprexplemb 32611	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
170	134, 121, 129, 154, 169	breprexplema 32610	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)))
171	170	oveq1d 7290	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
172	126	adantr 481	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
173	150, 172	mulcld 10995	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ)
174	125, 173	fsumcl 15445	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ)
175	123, 130, 174	fsummulc1 15497	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
176	125, 131, 173	fsummulc1 15497	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
177	131	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (𝑍↑𝑚) ∈ ℂ)
178	150, 172, 177	mulassd 10998	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
179	178	sumeq2dv 15415	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
180	176, 179	eqtrd 2778	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
181	180	sumeq2dv 15415	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
182	171, 175, 181	3eqtrd 2782	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
183	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ)
184		1nn0 12249	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
185	184	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈ ℕ0)
186	121, 185	nn0addcld 12297	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈ ℕ0)
187	183, 116, 186, 123	reprfi 32596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin)
188		fzofi 13694	. . . . . . . . . 10 ⊢ (0..^(𝑇 + 1)) ∈ Fin
189	188	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin)
190	134	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈ ℕ0)
191	16	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈ ℕ0)
192	127	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ)
193	20	ad3antrrr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
194	164	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
195	194	sselda 3921	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆))
196	39	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ)
197	116	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ)
198	186	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈ ℕ0)
199		simplr 766	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚))
200	196, 197, 198, 199	reprf 32592	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁))
201		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1)))
202	200, 201	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁))
203	39, 202	sselid 3919	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ ℕ)
204	190, 191, 192, 193, 195, 203	breprexplemb 32611	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
205	189, 204	fprodcl 15662	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
206	187, 130, 205	fsummulc1 15497	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
207	152, 182, 206	3eqtr2rd 2785	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
208	207	sumeq2dv 15415	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
209		oveq1 7282	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝑛 − 𝑏) = (𝑚 − 𝑏))
210	209	oveq2d 7291	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)))
211	210	sumeq1d 15413	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
212		oveq2 7283	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → (𝑍↑𝑛) = (𝑍↑𝑚))
213	212	oveq2d 7291	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
214	211, 213	oveq12d 7293	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
215	214	adantr 481	. . . . . . 7 ⊢ ((𝑛 = 𝑚 ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
216	215	sumeq2dv 15415	. . . . . 6 ⊢ (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
217	216	cbvsumv 15408	. . . . 5 ⊢ Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
218	208, 217	eqtr4di 2796	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))))
219	1, 14	nn0mulcld 12298	. . . . . 6 ⊢ (𝜑 → (𝑇 · 𝑁) ∈ ℕ0)
220		oveq2 7283	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)))
221	220	sumeq1d 15413	. . . . . . 7 ⊢ (𝑚 = (𝑛 − 𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
222		oveq1 7282	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 − 𝑏) → (𝑚 + 𝑏) = ((𝑛 − 𝑏) + 𝑏))
223	222	oveq2d 7291	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛 − 𝑏) + 𝑏)))
224	223	oveq2d 7291	. . . . . . 7 ⊢ (𝑚 = (𝑛 − 𝑏) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))
225	221, 224	oveq12d 7293	. . . . . 6 ⊢ (𝑚 = (𝑛 − 𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
226	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
227		uzssz 12603	. . . . . . . . . 10 ⊢ (ℤ≥‘-𝑏) ⊆ ℤ
228		simp2 1136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ≥‘-𝑏))
229	227, 228	sselid 3919	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
230	1	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
231	57	3ad2ant1 1132	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
232	226, 229, 230, 231	reprfi 32596	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
233	9	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
234	58	3adant2 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
235	234	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
236	59	3adant2 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
237	236	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
238	60	3adant2 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
239	238	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
240	61	3adant2 1130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
241	240	ad2antrr 723	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
242	36	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆))
243	242	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
244	243	sselda 3921	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
245	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ)
246	229	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ)
247	230	adantr 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈ ℕ0)
248		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
249	245, 246, 247, 248	reprf 32592	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
250	249	adantr 481	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
251		simpr 485	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
252	250, 251	ffvelrnd 6962	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
253	39, 252	sselid 3919	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
254	235, 237, 239, 241, 244, 253	breprexplemb 32611	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
255	233, 254	fprodcl 15662	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
256	232, 255	fsumcl 15445	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
257	70	3adant2 1130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
258	72	3adant2 1130	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
259	234, 236, 238, 240, 257, 258	breprexplemb 32611	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
260	229	zcnd 12427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ)
261		simp3 1137	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
262	261	elfzelzd 13257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
263	262	zcnd 12427	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
264	260, 263	subnegd 11339	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏))
265	262	znegcld 12428	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ)
266		eluzle 12595	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ≥‘-𝑏) → -𝑏 ≤ 𝑚)
267	228, 266	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ≤ 𝑚)
268		znn0sub 12367	. . . . . . . . . . . 12 ⊢ ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏 ≤ 𝑚 ↔ (𝑚 − -𝑏) ∈ ℕ0))
269	268	biimpa 477	. . . . . . . . . . 11 ⊢ (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏 ≤ 𝑚) → (𝑚 − -𝑏) ∈ ℕ0)
270	265, 229, 267, 269	syl21anc 835	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈ ℕ0)
271	264, 270	eqeltrrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
272	238, 271	expcld 13864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
273	259, 272	mulcld 10995	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
274	256, 273	mulcld 10995	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ)
275	58	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℕ0)
276		ssidd 3944	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁))
277		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)))
278	277	elfzelzd 13257	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ)
279		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁))
280	279	elfzelzd 13257	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ)
281	278, 280	zsubcld 12431	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛 − 𝑏) ∈ ℤ)
282	1	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℕ0)
283	25	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ)
284	275	nn0red 12294	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ)
285	283, 284	remulcld 11005	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ)
286	280	zred 12426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ)
287	219	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈ ℕ0)
288	287, 74	nn0addcld 12297	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈ ℕ0)
289	184	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 1 ∈ ℕ0)
290	288, 289	nn0addcld 12297	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0)
291		fz2ssnn0 31106	. . . . . . . . . . . . . . 15 ⊢ ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
292	290, 291	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
293	292	sselda 3921	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0)
294	293	nn0red 12294	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ)
295	23	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ)
296	275	nn0zd 12424	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ)
297	295, 296	zmulcld 12432	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ)
298	297, 280	zaddcld 12430	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ)
299		elfzle1 13259	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
300	277, 299	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
301		zltp1le 12370	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛))
302	301	biimpar 478	. . . . . . . . . . . . 13 ⊢ (((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
303	298, 278, 300, 302	syl21anc 835	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
304		ltaddsub 11449	. . . . . . . . . . . . 13 ⊢ (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛 − 𝑏)))
305	304	biimpa 477	. . . . . . . . . . . 12 ⊢ ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛 − 𝑏))
306	285, 286, 294, 303, 305	syl31anc 1372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛 − 𝑏))
307	275, 276, 281, 282, 306	reprgt 32601	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅)
308	307	sumeq1d 15413	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
309		sum0 15433	. . . . . . . . 9 ⊢ Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0
310	308, 309	eqtrdi 2794	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0)
311	310	oveq1d 7290	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
312	73	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
313	60	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ)
314	278	zcnd 12427	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ)
315	280	zcnd 12427	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ)
316	314, 315	npcand 11336	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
317	316, 293	eqeltrd 2839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) ∈ ℕ0)
318	313, 317	expcld 13864	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ)
319	312, 318	mulcld 10995	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ)
320	319	mul02d 11173	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
321	311, 320	eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
322	39	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ)
323		fzossfz 13406	. . . . . . . . . . . . . 14 ⊢ (0..^𝑏) ⊆ (0...𝑏)
324		fzssz 13258	. . . . . . . . . . . . . 14 ⊢ (0...𝑏) ⊆ ℤ
325	323, 324	sstri 3930	. . . . . . . . . . . . 13 ⊢ (0..^𝑏) ⊆ ℤ
326		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏))
327	325, 326	sselid 3919	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ)
328		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁))
329	328	elfzelzd 13257	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ)
330	327, 329	zsubcld 12431	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℤ)
331	1	ad2antrr 723	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℕ0)
332	330	zred 12426	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℝ)
333		0red 10978	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ)
334	25	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ)
335		elfzolt2 13396	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏)
336	335	adantl 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏)
337	327	zred 12426	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ)
338	329	zred 12426	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ)
339	337, 338	sublt0d 11601	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) < 0 ↔ 𝑛 < 𝑏))
340	336, 339	mpbird 256	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 0)
341	62	ad2antrr 723	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇)
342	332, 333, 334, 340, 341	ltletrd 11135	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 𝑇)
343	322, 330, 331, 342	reprlt 32599	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅)
344	343	sumeq1d 15413	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
345	344, 309	eqtrdi 2794	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0)
346	345	oveq1d 7290	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
347	73	adantr 481	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
348	60	adantr 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ)
349	337	recnd 11003	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ)
350	338	recnd 11003	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ)
351	349, 350	npcand 11336	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
352		fzo0ssnn0 13468	. . . . . . . . . . . 12 ⊢ (0..^𝑏) ⊆ ℕ0
353	352, 326	sselid 3919	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0)
354	351, 353	eqeltrd 2839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) ∈ ℕ0)
355	348, 354	expcld 13864	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ)
356	347, 355	mulcld 10995	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ)
357	356	mul02d 11173	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
358	346, 357	eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
359	219, 14, 225, 274, 321, 358	fsum2dsub 32587	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
360		nn0sscn 12238	. . . . . . . . 9 ⊢ ℕ0 ⊆ ℂ
361	360, 1	sselid 3919	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
362	360, 14	sselid 3919	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
363	361, 362	adddirp1d 11001	. . . . . . 7 ⊢ (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁))
364	363	oveq2d 7291	. . . . . 6 ⊢ (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁)))
365	128, 360	sstri 3930	. . . . . . . . . . . . 13 ⊢ (0...((𝑇 + 1) · 𝑁)) ⊆ ℂ
366		simplr 766	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁)))
367	365, 366	sselid 3919	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
368	44, 360	sstri 3930	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℂ
369		simpr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
370	368, 369	sselid 3919	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
371	367, 370	npcand 11336	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
372	371	eqcomd 2744	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛 − 𝑏) + 𝑏))
373	372	oveq2d 7291	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑛) = (𝑍↑((𝑛 − 𝑏) + 𝑏)))
374	373	oveq2d 7291	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))
375	374	oveq2d 7291	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
376	375	sumeq2dv 15415	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
377	364, 376	sumeq12dv 15418	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
378	359, 377	eqtr4d 2781	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))))
379	105	adantlr 712	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
380	110	adantlr 712	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ)
381	76	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
382	381	adantr 481	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
383	379, 380, 382	mulassd 10998	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))))
384	73	ad4ant13 748	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
385	75	ad4ant13 748	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑏) ∈ ℂ)
386	380, 384, 385	mulassd 10998	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
387	384, 380, 385	mulassd 10998	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏))))
388	380, 384	mulcomd 10996	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
389	388	oveq1d 7290	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)))
390	106	adantlr 712	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
391	74	ad4ant13 748	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0)
392	109	adantlr 712	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
393	390, 391, 392	expaddd 13866	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍↑𝑚) · (𝑍↑𝑏)))
394	393	oveq2d 7291	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏))))
395	387, 389, 394	3eqtr4d 2788	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
396	386, 395	eqtr3d 2780	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
397	396	oveq2d 7291	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
398	383, 397	eqtrd 2778	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
399	398	sumeq2dv 15415	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
400	87	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
401	111	adantlr 712	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
402	400, 381, 401	fsummulc1 15497	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
403	73	adantlr 712	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
404	60	adantlr 712	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
405	108	adantr 481	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0)
406	74	adantlr 712	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
407	405, 406	nn0addcld 12297	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
408	404, 407	expcld 13864	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
409	403, 408	mulcld 10995	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
410	400, 409, 379	fsummulc1 15497	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
411	399, 402, 410	3eqtr4rd 2789	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
412	411	sumeq2dv 15415	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
413	412	sumeq2dv 15415	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
414	218, 378, 413	3eqtr2rd 2785	. . 3 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
415	80, 113, 414	3eqtr2d 2784	. 2 ⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
416	6, 78, 415	3eqtrd 2782	1 ⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ∪ cun 3885   ⊆ wss 3887  ∅c0 4256  {csn 4561   class class class wbr 5074  ⟶wf 6429  ‘cfv 6433  (class class class)co 7275   ↑_m cmap 8615  Fincfn 8733  ℂcc 10869  ℝcr 10870  0cc0 10871  1c1 10872   + caddc 10874   · cmul 10876   < clt 11009   ≤ cle 11010   − cmin 11205  -cneg 11206  ℕcn 11973  ℕ₀cn0 12233  ℤcz 12319  ℤ_≥cuz 12582  ...cfz 13239  ..^cfzo 13382  ↑cexp 13782  Σcsu 15397  ∏cprod 15615  reprcrepr 32588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-inf2 9399  ax-cnex 10927  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948  ax-pre-sup 10949

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rmo 3071  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-disj 5040  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-se 5545  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-isom 6442  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-1st 7831  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-1o 8297  df-er 8498  df-map 8617  df-pm 8618  df-en 8734  df-dom 8735  df-sdom 8736  df-fin 8737  df-sup 9201  df-oi 9269  df-card 9697  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-div 11633  df-nn 11974  df-2 12036  df-3 12037  df-n0 12234  df-z 12320  df-uz 12583  df-rp 12731  df-ico 13085  df-fz 13240  df-fzo 13383  df-seq 13722  df-exp 13783  df-hash 14045  df-cj 14810  df-re 14811  df-im 14812  df-sqrt 14946  df-abs 14947  df-clim 15197  df-sum 15398  df-prod 15616  df-repr 32589

This theorem is referenced by:  breprexp  32613