Theorem breprexplemc 31019

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

Hypotheses

Ref	Expression
breprexp.n	⊢ (𝜑 → 𝑁 ∈ ℕ0)
breprexp.s	⊢ (𝜑 → 𝑆 ∈ ℕ0)
breprexp.z	⊢ (𝜑 → 𝑍 ∈ ℂ)
breprexp.h	⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
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 11915	. . . . 5 ⊢ ℕ0 = (ℤ≥‘0)
3	1, 2	syl6eleq 2849	. . . 4 ⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘0))
4		fzosplitsn 12770	. . . 4 ⊢ (𝑇 ∈ (ℤ≥‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
5	3, 4	syl 17	. . 3 ⊢ (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
6	5	prodeq1d 14850	. 2 ⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)))
7		nfv 1992	. . 3 ⊢ Ⅎ𝑎𝜑
8		nfcv 2902	. . 3 ⊢ Ⅎ𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))
9		fzofi 12967	. . . 4 ⊢ (0..^𝑇) ∈ Fin
10	9	a1i 11	. . 3 ⊢ (𝜑 → (0..^𝑇) ∈ Fin)
11		fzonel 12677	. . . 4 ⊢ ¬ 𝑇 ∈ (0..^𝑇)
12	11	a1i 11	. . 3 ⊢ (𝜑 → ¬ 𝑇 ∈ (0..^𝑇))
13		fzfid 12966	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin)
14		breprexp.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
15	14	ad2antrr 764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
16		breprexp.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℕ0)
17	16	ad2antrr 764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
18		breprexp.z	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ ℂ)
19	18	ad2antrr 764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
20		breprexp.h	. . . . . . . 8 ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
21	20	adantr 472	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
22	21	adantr 472	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
23	1	nn0zd 11672	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ℤ)
24	16	nn0zd 11672	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ℤ)
25	1	nn0red 11544	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℝ)
26		1red 10247	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
27	25, 26	readdcld 10261	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 + 1) ∈ ℝ)
28	16	nn0red 11544	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
29	25	lep1d 11147	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ≤ (𝑇 + 1))
30		breprexplemc.s	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 + 1) ≤ 𝑆)
31	25, 27, 28, 29, 30	letrd 10386	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≤ 𝑆)
32		eluz1 11883	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℤ → (𝑆 ∈ (ℤ≥‘𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)))
33	32	biimpar 503	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)) → 𝑆 ∈ (ℤ≥‘𝑇))
34	23, 24, 31, 33	syl12anc 1475	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘𝑇))
35		fzoss2 12690	. . . . . . . . 9 ⊢ (𝑆 ∈ (ℤ≥‘𝑇) → (0..^𝑇) ⊆ (0..^𝑆))
36	34, 35	syl 17	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑇) ⊆ (0..^𝑆))
37	36	sselda 3744	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
38	37	adantr 472	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆))
39		fz1ssnn 12565	. . . . . . . 8 ⊢ (1...𝑁) ⊆ ℕ
40	39	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
41	40	sselda 3744	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
42	15, 17, 19, 22, 38, 41	breprexplemb 31018	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) ∈ ℂ)
43		nnssnn0 11487	. . . . . . . . . . 11 ⊢ ℕ ⊆ ℕ0
44	39, 43	sstri 3753	. . . . . . . . . 10 ⊢ (1...𝑁) ⊆ ℕ0
45	44	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ0)
46	45	ralrimivw 3105	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆ ℕ0)
47	46	r19.21bi 3070	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ0)
48	47	sselda 3744	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
49	19, 48	expcld 13202	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ)
50	42, 49	mulcld 10252	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
51	13, 50	fsumcl 14663	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
52		simpl 474	. . . . . . 7 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇)
53	52	fveq2d 6356	. . . . . 6 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (𝐿‘𝑎) = (𝐿‘𝑇))
54	53	fveq1d 6354	. . . . 5 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) = ((𝐿‘𝑇)‘𝑏))
55	54	oveq1d 6828	. . . 4 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))
56	55	sumeq2dv 14632	. . 3 ⊢ (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))
57		fzfid 12966	. . . 4 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
58	14	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
59	16	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
60	18	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
61	20	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
62	1	nn0ge0d 11546	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝑇)
63		zltp1le 11619	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
64	23, 24, 63	syl2anc 696	. . . . . . . . 9 ⊢ (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
65	30, 64	mpbird 247	. . . . . . . 8 ⊢ (𝜑 → 𝑇 < 𝑆)
66		0zd 11581	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
67		elfzo 12666	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆)))
68	23, 66, 24, 67	syl3anc 1477	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆)))
69	62, 65, 68	mpbir2and 995	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (0..^𝑆))
70	69	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
71	39	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
72	71	sselda 3744	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
73	58, 59, 60, 61, 70, 72	breprexplemb 31018	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
74	45	sselda 3744	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
75	60, 74	expcld 13202	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ)
76	73, 75	mulcld 10252	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
77	57, 76	fsumcl 14663	. . 3 ⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
78	7, 8, 10, 1, 12, 51, 56, 77	fprodsplitsn 14919	. 2 ⊢ (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
79		breprexplemc.1	. . . 4 ⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
80	79	oveq1d 6828	. . 3 ⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
81		fzfid 12966	. . . 4 ⊢ (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin)
82	39	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ)
83		fz0ssnn0 12628	. . . . . . . 8 ⊢ (0...(𝑇 · 𝑁)) ⊆ ℕ0
84		simpr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁)))
85	83, 84	sseldi 3742	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0)
86	85	nn0zd 11672	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ)
87	1	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈ ℕ0)
88	57	adantr 472	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin)
89	82, 86, 87, 88	reprfi 31003	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
90	9	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
91	14	adantr 472	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈ ℕ0)
92	91	ad2antrr 764	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
93	16	ad3antrrr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
94	18	ad3antrrr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
95	20	ad3antrrr 768	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
96	36	ad2antrr 764	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
97	96	sselda 3744	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
98	39	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
99	86	ad2antrr 764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ)
100	87	ad2antrr 764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
101		simplr 809	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
102	98, 99, 100, 101	reprf 30999	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
103		simpr 479	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
104	102, 103	ffvelrnd 6523	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
105	39, 104	sseldi 3742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
106	92, 93, 94, 95, 97, 105	breprexplemb 31018	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
107	90, 106	fprodcl 14881	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
108	18	ad2antrr 764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
109	85	adantr 472	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
110	108, 109	expcld 13202	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ)
111	107, 110	mulcld 10252	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
112	89, 111	fsumcl 14663	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
113	81, 57, 112, 76	fsum2mul 14720	. . 3 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
114	39	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
115		fzssz 12536	. . . . . . . . . . . . 13 ⊢ (0...((𝑇 + 1) · 𝑁)) ⊆ ℤ
116		simpr 479	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁)))
117	115, 116	sseldi 3742	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ)
118	117	adantr 472	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
119		fzssz 12536	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ ℤ
120		simpr 479	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
121	119, 120	sseldi 3742	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
122	118, 121	zsubcld 11679	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − 𝑏) ∈ ℤ)
123	1	adantr 472	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈ ℕ0)
124	123	adantr 472	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
125	57	adantr 472	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin)
126	125	adantr 472	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
127	114, 122, 124, 126	reprfi 31003	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)) ∈ Fin)
128	73	adantlr 753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
129	18	adantr 472	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ)
130		fz0ssnn0 12628	. . . . . . . . . . . . 13 ⊢ (0...((𝑇 + 1) · 𝑁)) ⊆ ℕ0
131	130, 116	sseldi 3742	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0)
132	129, 131	expcld 13202	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍↑𝑚) ∈ ℂ)
133	132	adantr 472	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑚) ∈ ℂ)
134	128, 133	mulcld 10252	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) ∈ ℂ)
135	9	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (0..^𝑇) ∈ Fin)
136	14	adantr 472	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈ ℕ0)
137	136	adantr 472	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
138	137	ad2antrr 764	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
139	16	ad4antr 771	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
140	129	ad3antrrr 768	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
141	20	ad4antr 771	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
142	37	ad5ant15 1220	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
143	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
144	122	ad2antrr 764	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚 − 𝑏) ∈ ℤ)
145	124	ad2antrr 764	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
146		simplr 809	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)))
147	143, 144, 145, 146	reprf 30999	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
148		simpr 479	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
149	147, 148	ffvelrnd 6523	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
150	39, 149	sseldi 3742	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
151	138, 139, 140, 141, 142, 150	breprexplemb 31018	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
152	135, 151	fprodcl 14881	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
153	127, 134, 152	fsummulc1 14716	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
154	153	sumeq2dv 14632	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
155		elfzle2 12538	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
156	155	adantl 473	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
157	136	ad2antrr 764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ0)
158	16	ad3antrrr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈ ℕ0)
159	129	ad2antrr 764	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ)
160	20	ad3antrrr 768	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
161	23	peano2zd 11677	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇 + 1) ∈ ℤ)
162		eluz 11893	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈ (ℤ≥‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆))
163	162	biimpar 503	. . . . . . . . . . . . . . 15 ⊢ ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ≥‘(𝑇 + 1)))
164	161, 24, 30, 163	syl21anc 1476	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘(𝑇 + 1)))
165		fzoss2 12690	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (ℤ≥‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
166	164, 165	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
167	166	ad3antrrr 768	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
168		simplr 809	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1)))
169	167, 168	sseldd 3745	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆))
170		simpr 479	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
171	157, 158, 159, 160, 169, 170	breprexplemb 31018	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
172	136, 123, 131, 156, 171	breprexplema 31017	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)))
173	172	oveq1d 6828	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
174	128	adantr 472	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
175	152, 174	mulcld 10252	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ)
176	127, 175	fsumcl 14663	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ)
177	125, 132, 176	fsummulc1 14716	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
178	127, 133, 175	fsummulc1 14716	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
179	133	adantr 472	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (𝑍↑𝑚) ∈ ℂ)
180	152, 174, 179	mulassd 10255	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
181	180	sumeq2dv 14632	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
182	178, 181	eqtrd 2794	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
183	182	sumeq2dv 14632	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
184	173, 177, 183	3eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
185	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ)
186		1nn0 11500	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
187	186	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈ ℕ0)
188	123, 187	nn0addcld 11547	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈ ℕ0)
189	185, 117, 188, 125	reprfi 31003	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin)
190		fzofi 12967	. . . . . . . . . 10 ⊢ (0..^(𝑇 + 1)) ∈ Fin
191	190	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin)
192	136	ad2antrr 764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈ ℕ0)
193	16	ad3antrrr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈ ℕ0)
194	129	ad2antrr 764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ)
195	20	ad3antrrr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
196	166	ad2antrr 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
197	196	sselda 3744	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^𝑆))
198	39	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (1...𝑁) ⊆ ℕ)
199	117	ad2antrr 764	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ)
200	188	ad2antrr 764	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈ ℕ0)
201		simplr 809	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚))
202	198, 199, 200, 201	reprf 30999	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁))
203		simpr 479	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1)))
204	202, 203	ffvelrnd 6523	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁))
205	39, 204	sseldi 3742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ ℕ)
206	192, 193, 194, 195, 197, 205	breprexplemb 31018	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
207	191, 206	fprodcl 14881	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
208	189, 132, 207	fsummulc1 14716	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
209	154, 184, 208	3eqtr2rd 2801	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
210	209	sumeq2dv 14632	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
211		oveq1 6820	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝑛 − 𝑏) = (𝑚 − 𝑏))
212	211	oveq2d 6829	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)))
213	212	sumeq1d 14630	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
214		oveq2 6821	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → (𝑍↑𝑛) = (𝑍↑𝑚))
215	214	oveq2d 6829	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
216	213, 215	oveq12d 6831	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
217	216	adantr 472	. . . . . . 7 ⊢ ((𝑛 = 𝑚 ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
218	217	sumeq2dv 14632	. . . . . 6 ⊢ (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
219	218	cbvsumv 14625	. . . . 5 ⊢ Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
220	210, 219	syl6eqr 2812	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))))
221	1, 14	nn0mulcld 11548	. . . . . 6 ⊢ (𝜑 → (𝑇 · 𝑁) ∈ ℕ0)
222		oveq2 6821	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)))
223	222	sumeq1d 14630	. . . . . . 7 ⊢ (𝑚 = (𝑛 − 𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
224		oveq1 6820	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 − 𝑏) → (𝑚 + 𝑏) = ((𝑛 − 𝑏) + 𝑏))
225	224	oveq2d 6829	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛 − 𝑏) + 𝑏)))
226	225	oveq2d 6829	. . . . . . 7 ⊢ (𝑚 = (𝑛 − 𝑏) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))
227	223, 226	oveq12d 6831	. . . . . 6 ⊢ (𝑚 = (𝑛 − 𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
228	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
229		uzssz 11899	. . . . . . . . . 10 ⊢ (ℤ≥‘-𝑏) ⊆ ℤ
230		simp2 1132	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ≥‘-𝑏))
231	229, 230	sseldi 3742	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
232	1	3ad2ant1 1128	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
233	57	3ad2ant1 1128	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
234	228, 231, 232, 233	reprfi 31003	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
235	9	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
236	58	3adant2 1126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
237	236	ad2antrr 764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
238	59	3adant2 1126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
239	238	ad2antrr 764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
240	60	3adant2 1126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
241	240	ad2antrr 764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
242	61	3adant2 1126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
243	242	ad2antrr 764	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑𝑚 ℕ))
244	36	3ad2ant1 1128	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆))
245	244	adantr 472	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
246	245	sselda 3744	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
247	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ)
248	231	adantr 472	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ)
249	232	adantr 472	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈ ℕ0)
250		simpr 479	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
251	247, 248, 249, 250	reprf 30999	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
252	251	adantr 472	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
253		simpr 479	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
254	252, 253	ffvelrnd 6523	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
255	39, 254	sseldi 3742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
256	237, 239, 241, 243, 246, 255	breprexplemb 31018	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
257	235, 256	fprodcl 14881	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
258	234, 257	fsumcl 14663	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
259	70	3adant2 1126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
260	72	3adant2 1126	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
261	236, 238, 240, 242, 259, 260	breprexplemb 31018	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
262	231	zcnd 11675	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ)
263		simp3 1133	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
264	119, 263	sseldi 3742	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
265	264	zcnd 11675	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
266	262, 265	subnegd 10591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏))
267	264	znegcld 11676	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ)
268		eluzle 11892	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ≥‘-𝑏) → -𝑏 ≤ 𝑚)
269	230, 268	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ≤ 𝑚)
270		znn0sub 11616	. . . . . . . . . . . 12 ⊢ ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏 ≤ 𝑚 ↔ (𝑚 − -𝑏) ∈ ℕ0))
271	270	biimpa 502	. . . . . . . . . . 11 ⊢ (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏 ≤ 𝑚) → (𝑚 − -𝑏) ∈ ℕ0)
272	267, 231, 269, 271	syl21anc 1476	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈ ℕ0)
273	266, 272	eqeltrrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
274	240, 273	expcld 13202	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
275	261, 274	mulcld 10252	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
276	258, 275	mulcld 10252	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ)
277	58	adantr 472	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℕ0)
278		ssid 3765	. . . . . . . . . . . 12 ⊢ (1...𝑁) ⊆ (1...𝑁)
279	278	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁))
280		fzssz 12536	. . . . . . . . . . . . 13 ⊢ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℤ
281		simpr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)))
282	280, 281	sseldi 3742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ)
283		simplr 809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁))
284	119, 283	sseldi 3742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ)
285	282, 284	zsubcld 11679	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛 − 𝑏) ∈ ℤ)
286	1	ad2antrr 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℕ0)
287	25	ad2antrr 764	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ)
288	277	nn0red 11544	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ)
289	287, 288	remulcld 10262	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ)
290	284	zred 11674	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ)
291	221	adantr 472	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈ ℕ0)
292	291, 74	nn0addcld 11547	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈ ℕ0)
293	186	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 1 ∈ ℕ0)
294	292, 293	nn0addcld 11547	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0)
295		fz2ssnn0 29856	. . . . . . . . . . . . . . 15 ⊢ ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
296	294, 295	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
297	296	sselda 3744	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0)
298	297	nn0red 11544	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ)
299	23	ad2antrr 764	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ)
300	277	nn0zd 11672	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ)
301	299, 300	zmulcld 11680	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ)
302	301, 284	zaddcld 11678	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ)
303		elfzle1 12537	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
304	281, 303	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
305		zltp1le 11619	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛))
306	305	biimpar 503	. . . . . . . . . . . . 13 ⊢ (((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
307	302, 282, 304, 306	syl21anc 1476	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
308		ltaddsub 10694	. . . . . . . . . . . . 13 ⊢ (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛 − 𝑏)))
309	308	biimpa 502	. . . . . . . . . . . 12 ⊢ ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛 − 𝑏))
310	289, 290, 298, 307, 309	syl31anc 1480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛 − 𝑏))
311	277, 279, 285, 286, 310	reprgt 31008	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅)
312	311	sumeq1d 14630	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
313		sum0 14651	. . . . . . . . 9 ⊢ Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0
314	312, 313	syl6eq 2810	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0)
315	314	oveq1d 6828	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
316	73	adantr 472	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
317	60	adantr 472	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ)
318	282	zcnd 11675	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ)
319	284	zcnd 11675	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ)
320	318, 319	npcand 10588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
321	320, 297	eqeltrd 2839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) ∈ ℕ0)
322	317, 321	expcld 13202	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ)
323	316, 322	mulcld 10252	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ)
324	323	mul02d 10426	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
325	315, 324	eqtrd 2794	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
326	39	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ)
327		fzossfz 12682	. . . . . . . . . . . . . 14 ⊢ (0..^𝑏) ⊆ (0...𝑏)
328		fzssz 12536	. . . . . . . . . . . . . 14 ⊢ (0...𝑏) ⊆ ℤ
329	327, 328	sstri 3753	. . . . . . . . . . . . 13 ⊢ (0..^𝑏) ⊆ ℤ
330		simpr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏))
331	329, 330	sseldi 3742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ)
332		simplr 809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁))
333	119, 332	sseldi 3742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ)
334	331, 333	zsubcld 11679	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℤ)
335	1	ad2antrr 764	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℕ0)
336	334	zred 11674	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℝ)
337		0red 10233	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ)
338	25	ad2antrr 764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ)
339		elfzolt2 12673	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏)
340	339	adantl 473	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏)
341	331	zred 11674	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ)
342	333	zred 11674	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ)
343	341, 342	sublt0d 10845	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) < 0 ↔ 𝑛 < 𝑏))
344	340, 343	mpbird 247	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 0)
345	62	ad2antrr 764	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇)
346	336, 337, 338, 344, 345	ltletrd 10389	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 𝑇)
347	326, 334, 335, 346	reprlt 31006	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅)
348	347	sumeq1d 14630	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
349	348, 313	syl6eq 2810	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0)
350	349	oveq1d 6828	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
351	73	adantr 472	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
352	60	adantr 472	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ)
353	341	recnd 10260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ)
354	342	recnd 10260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ)
355	353, 354	npcand 10588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
356		fzo0ssnn0 12743	. . . . . . . . . . . 12 ⊢ (0..^𝑏) ⊆ ℕ0
357	356, 330	sseldi 3742	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0)
358	355, 357	eqeltrd 2839	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) ∈ ℕ0)
359	352, 358	expcld 13202	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ)
360	351, 359	mulcld 10252	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ)
361	360	mul02d 10426	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
362	350, 361	eqtrd 2794	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
363	221, 14, 227, 276, 325, 362	fsum2dsub 30994	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
364		nn0sscn 11489	. . . . . . . . 9 ⊢ ℕ0 ⊆ ℂ
365	364, 1	sseldi 3742	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
366	364, 14	sseldi 3742	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
367	365, 366	adddirp1d 10258	. . . . . . 7 ⊢ (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁))
368	367	oveq2d 6829	. . . . . 6 ⊢ (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁)))
369	130, 364	sstri 3753	. . . . . . . . . . . . 13 ⊢ (0...((𝑇 + 1) · 𝑁)) ⊆ ℂ
370		simplr 809	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁)))
371	369, 370	sseldi 3742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
372	44, 364	sstri 3753	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℂ
373		simpr 479	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
374	372, 373	sseldi 3742	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
375	371, 374	npcand 10588	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
376	375	eqcomd 2766	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛 − 𝑏) + 𝑏))
377	376	oveq2d 6829	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑛) = (𝑍↑((𝑛 − 𝑏) + 𝑏)))
378	377	oveq2d 6829	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))
379	378	oveq2d 6829	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
380	379	sumeq2dv 14632	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
381	368, 380	sumeq12dv 14636	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
382	363, 381	eqtr4d 2797	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))))
383	107	adantlr 753	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
384	110	adantlr 753	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ)
385	76	adantlr 753	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
386	385	adantr 472	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
387	383, 384, 386	mulassd 10255	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))))
388	73	ad4ant13 1207	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
389	75	ad4ant13 1207	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑏) ∈ ℂ)
390	384, 388, 389	mulassd 10255	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
391	388, 384, 389	mulassd 10255	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏))))
392	384, 388	mulcomd 10253	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
393	392	oveq1d 6828	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)))
394	108	adantlr 753	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
395	74	ad4ant13 1207	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0)
396	109	adantlr 753	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
397	394, 395, 396	expaddd 13204	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍↑𝑚) · (𝑍↑𝑏)))
398	397	oveq2d 6829	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏))))
399	391, 393, 398	3eqtr4d 2804	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
400	390, 399	eqtr3d 2796	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
401	400	oveq2d 6829	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
402	387, 401	eqtrd 2794	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
403	402	sumeq2dv 14632	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
404	89	adantr 472	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
405	111	adantlr 753	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
406	404, 385, 405	fsummulc1 14716	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
407	73	adantlr 753	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
408	60	adantlr 753	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
409	85	adantr 472	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0)
410	74	adantlr 753	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
411	409, 410	nn0addcld 11547	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
412	408, 411	expcld 13202	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
413	407, 412	mulcld 10252	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
414	404, 413, 383	fsummulc1 14716	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
415	403, 406, 414	3eqtr4rd 2805	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
416	415	sumeq2dv 14632	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
417	416	sumeq2dv 14632	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
418	220, 382, 417	3eqtr2rd 2801	. . 3 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
419	80, 113, 418	3eqtr2d 2800	. 2 ⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
420	6, 78, 419	3eqtrd 2798	1 ⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139   ∪ cun 3713   ⊆ wss 3715  ∅c0 4058  {csn 4321   class class class wbr 4804  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813   ↑_𝑚 cmap 8023  Fincfn 8121  ℂcc 10126  ℝcr 10127  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133   < clt 10266   ≤ cle 10267   − cmin 10458  -cneg 10459  ℕcn 11212  ℕ₀cn0 11484  ℤcz 11569  ℤ_≥cuz 11879  ...cfz 12519  ..^cfzo 12659  ↑cexp 13054  Σcsu 14615  ∏cprod 14834  reprcrepr 30995

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-oi 8580  df-card 8955  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-z 11570  df-uz 11880  df-rp 12026  df-ico 12374  df-fz 12520  df-fzo 12660  df-seq 12996  df-exp 13055  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-clim 14418  df-sum 14616  df-prod 14835  df-repr 30996

This theorem is referenced by:  breprexp  31020