Theorem breprexplemc 34966

Description: Lemma for breprexp 34967 (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 12902	. . . . 5 ⊢ ℕ0 = (ℤ≥‘0)
3	1, 2	eleqtrdi 2879	. . . 4 ⊢ (𝜑 → 𝑇 ∈ (ℤ≥‘0))
4		fzosplitsn 13807	. . . 4 ⊢ (𝑇 ∈ (ℤ≥‘0) → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
5	3, 4	syl 18	. . 3 ⊢ (𝜑 → (0..^(𝑇 + 1)) = ((0..^𝑇) ∪ {𝑇}))
6	5	prodeq1d 15976	. 2 ⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)))
7		nfv 1941	. . 3 ⊢ Ⅎ𝑎𝜑
8		nfcv 2931	. . 3 ⊢ Ⅎ𝑎Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))
9		fzofi 14012	. . . 4 ⊢ (0..^𝑇) ∈ Fin
10	9	a1i 11	. . 3 ⊢ (𝜑 → (0..^𝑇) ∈ Fin)
11		fzonel 13704	. . . 4 ⊢ ¬ 𝑇 ∈ (0..^𝑇)
12	11	a1i 11	. . 3 ⊢ (𝜑 → ¬ 𝑇 ∈ (0..^𝑇))
13		fzfid 14011	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ∈ Fin)
14		breprexp.n	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
15	14	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
16		breprexp.s	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℕ0)
17	16	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
18		breprexp.z	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ ℂ)
19	18	ad2antrr 738	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
20		breprexp.h	. . . . . . . 8 ⊢ (𝜑 → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
21	20	adantr 485	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
22	21	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
23	1	nn0zd 12618	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ∈ ℤ)
24	16	nn0zd 12618	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ ℤ)
25	1	nn0red 12568	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ∈ ℝ)
26		1red 11211	. . . . . . . . . . . 12 ⊢ (𝜑 → 1 ∈ ℝ)
27	25, 26	readdcld 11240	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 + 1) ∈ ℝ)
28	16	nn0red 12568	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ ℝ)
29	25	lep1d 12148	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑇 ≤ (𝑇 + 1))
30		breprexplemc.s	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑇 + 1) ≤ 𝑆)
31	25, 27, 28, 29, 30	letrd 11369	. . . . . . . . . 10 ⊢ (𝜑 → 𝑇 ≤ 𝑆)
32		eluz1 12868	. . . . . . . . . . 11 ⊢ (𝑇 ∈ ℤ → (𝑆 ∈ (ℤ≥‘𝑇) ↔ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)))
33	32	biimpar 482	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℤ ∧ (𝑆 ∈ ℤ ∧ 𝑇 ≤ 𝑆)) → 𝑆 ∈ (ℤ≥‘𝑇))
34	23, 24, 31, 33	syl12anc 849	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘𝑇))
35		fzoss2 13718	. . . . . . . . 9 ⊢ (𝑆 ∈ (ℤ≥‘𝑇) → (0..^𝑇) ⊆ (0..^𝑆))
36	34, 35	syl 18	. . . . . . . 8 ⊢ (𝜑 → (0..^𝑇) ⊆ (0..^𝑆))
37	36	sselda 3945	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
38	37	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 ∈ (0..^𝑆))
39		fz1ssnn 13585	. . . . . . . 8 ⊢ (1...𝑁) ⊆ ℕ
40	39	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
41	40	sselda 3945	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
42	15, 17, 19, 22, 38, 41	breprexplemb 34965	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) ∈ ℂ)
43		nnssnn0 12509	. . . . . . . . . . 11 ⊢ ℕ ⊆ ℕ0
44	39, 43	sstri 3954	. . . . . . . . . 10 ⊢ (1...𝑁) ⊆ ℕ0
45	44	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ0)
46	45	ralrimivw 3167	. . . . . . . 8 ⊢ (𝜑 → ∀𝑎 ∈ (0..^𝑇)(1...𝑁) ⊆ ℕ0)
47	46	r19.21bi 3263	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ0)
48	47	sselda 3945	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
49	19, 48	expcld 14184	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ)
50	42, 49	mulcld 11231	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
51	13, 50	fsumcl 15786	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ (0..^𝑇)) → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
52		simpl 487	. . . . . . 7 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → 𝑎 = 𝑇)
53	52	fveq2d 6888	. . . . . 6 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (𝐿‘𝑎) = (𝐿‘𝑇))
54	53	fveq1d 6886	. . . . 5 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑎)‘𝑏) = ((𝐿‘𝑇)‘𝑏))
55	54	oveq1d 7428	. . . 4 ⊢ ((𝑎 = 𝑇 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))
56	55	sumeq2dv 15755	. . 3 ⊢ (𝑎 = 𝑇 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))
57		fzfid 14011	. . . 4 ⊢ (𝜑 → (1...𝑁) ∈ Fin)
58	14	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
59	16	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
60	18	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
61	20	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
62	1	nn0ge0d 12570	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ 𝑇)
63		zltp1le 12646	. . . . . . . . . 10 ⊢ ((𝑇 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
64	23, 24, 63	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝑇 < 𝑆 ↔ (𝑇 + 1) ≤ 𝑆))
65	30, 64	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 𝑇 < 𝑆)
66		0zd 12605	. . . . . . . . 9 ⊢ (𝜑 → 0 ∈ ℤ)
67		elfzo 13691	. . . . . . . . 9 ⊢ ((𝑇 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆)))
68	23, 66, 24, 67	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → (𝑇 ∈ (0..^𝑆) ↔ (0 ≤ 𝑇 ∧ 𝑇 < 𝑆)))
69	62, 65, 68	mpbir2and 725	. . . . . . 7 ⊢ (𝜑 → 𝑇 ∈ (0..^𝑆))
70	69	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
71	39	a1i 11	. . . . . . 7 ⊢ (𝜑 → (1...𝑁) ⊆ ℕ)
72	71	sselda 3945	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
73	58, 59, 60, 61, 70, 72	breprexplemb 34965	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
74	45	sselda 3945	. . . . . 6 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
75	60, 74	expcld 14184	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑏) ∈ ℂ)
76	73, 75	mulcld 11231	. . . 4 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
77	57, 76	fsumcl 15786	. . 3 ⊢ (𝜑 → Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
78	7, 8, 10, 1, 12, 51, 56, 77	fprodsplitsn 16045	. 2 ⊢ (𝜑 → ∏𝑎 ∈ ((0..^𝑇) ∪ {𝑇})Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
79		breprexplemc.1	. . . 4 ⊢ (𝜑 → ∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
80	79	oveq1d 7428	. . 3 ⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
81		fzfid 14011	. . . 4 ⊢ (𝜑 → (0...(𝑇 · 𝑁)) ∈ Fin)
82	39	a1i 11	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ⊆ ℕ)
83		simpr 489	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ (0...(𝑇 · 𝑁)))
84	83	elfzelzd 13555	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℤ)
85	1	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑇 ∈ ℕ0)
86	57	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → (1...𝑁) ∈ Fin)
87	82, 84, 85, 86	reprfi 34950	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
88	9	a1i 11	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
89	14	adantr 485	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑁 ∈ ℕ0)
90	89	ad2antrr 738	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
91	16	ad3antrrr 742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
92	18	ad3antrrr 742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
93	20	ad3antrrr 742	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
94	36	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
95	94	sselda 3945	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
96	39	a1i 11	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
97	84	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑚 ∈ ℤ)
98	85	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
99		simplr 780	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
100	96, 97, 98, 99	reprf 34946	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
101		simpr 489	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
102	100, 101	ffvelcdmd 7083	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
103	39, 102	sselid 3943	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
104	90, 91, 92, 93, 95, 103	breprexplemb 34965	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
105	88, 104	fprodcl 16008	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
106	18	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
107		fz0ssnn0 13652	. . . . . . . . 9 ⊢ (0...(𝑇 · 𝑁)) ⊆ ℕ0
108	107, 83	sselid 3943	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → 𝑚 ∈ ℕ0)
109	108	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
110	106, 109	expcld 14184	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ)
111	105, 110	mulcld 11231	. . . . 5 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
112	87, 111	fsumcl 15786	. . . 4 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
113	81, 57, 112, 76	fsum2mul 15842	. . 3 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
114	39	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
115		simpr 489	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ (0...((𝑇 + 1) · 𝑁)))
116	115	elfzelzd 13555	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℤ)
117	116	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
118		simpr 489	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
119	118	elfzelzd 13555	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
120	117, 119	zsubcld 12707	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − 𝑏) ∈ ℤ)
121	1	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑇 ∈ ℕ0)
122	121	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
123	57	adantr 485	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ∈ Fin)
124	123	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
125	114, 120, 122, 124	reprfi 34950	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)) ∈ Fin)
126	73	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
127	18	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑍 ∈ ℂ)
128		fz0ssnn0 13652	. . . . . . . . . . . . 13 ⊢ (0...((𝑇 + 1) · 𝑁)) ⊆ ℕ0
129	128, 115	sselid 3943	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ∈ ℕ0)
130	127, 129	expcld 14184	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑍↑𝑚) ∈ ℂ)
131	130	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑚) ∈ ℂ)
132	126, 131	mulcld 11231	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) ∈ ℂ)
133	9	a1i 11	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (0..^𝑇) ∈ Fin)
134	14	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑁 ∈ ℕ0)
135	134	adantr 485	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
136	135	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
137	16	ad4antr 744	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
138	127	ad3antrrr 742	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
139	20	ad4antr 744	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
140	37	ad5ant15 770	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
141	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (1...𝑁) ⊆ ℕ)
142	120	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑚 − 𝑏) ∈ ℤ)
143	122	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑇 ∈ ℕ0)
144		simplr 780	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)))
145	141, 142, 143, 144	reprf 34946	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
146		simpr 489	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
147	145, 146	ffvelcdmd 7083	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
148	39, 147	sselid 3943	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
149	136, 137, 138, 139, 140, 148	breprexplemb 34965	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
150	133, 149	fprodcl 16008	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
151	125, 132, 150	fsummulc1 15838	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
152	151	sumeq2dv 15755	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
153		elfzle2 13558	. . . . . . . . . . 11 ⊢ (𝑚 ∈ (0...((𝑇 + 1) · 𝑁)) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
154	153	adantl 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 𝑚 ≤ ((𝑇 + 1) · 𝑁))
155	134	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑁 ∈ ℕ0)
156	16	ad3antrrr 742	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑆 ∈ ℕ0)
157	127	ad2antrr 738	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑍 ∈ ℂ)
158	20	ad3antrrr 742	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
159	23	peano2zd 12705	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑇 + 1) ∈ ℤ)
160		eluz 12878	. . . . . . . . . . . . . . . 16 ⊢ (((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) → (𝑆 ∈ (ℤ≥‘(𝑇 + 1)) ↔ (𝑇 + 1) ≤ 𝑆))
161	160	biimpar 482	. . . . . . . . . . . . . . 15 ⊢ ((((𝑇 + 1) ∈ ℤ ∧ 𝑆 ∈ ℤ) ∧ (𝑇 + 1) ≤ 𝑆) → 𝑆 ∈ (ℤ≥‘(𝑇 + 1)))
162	159, 24, 30, 161	syl21anc 850	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑆 ∈ (ℤ≥‘(𝑇 + 1)))
163		fzoss2 13718	. . . . . . . . . . . . . 14 ⊢ (𝑆 ∈ (ℤ≥‘(𝑇 + 1)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
164	162, 163	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
165	164	ad3antrrr 742	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
166		simplr 780	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^(𝑇 + 1)))
167	165, 166	sseldd 3946	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑥 ∈ (0..^𝑆))
168		simpr 489	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → 𝑦 ∈ ℕ)
169	155, 156, 157, 158, 167, 168	breprexplemb 34965	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑥 ∈ (0..^(𝑇 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿‘𝑥)‘𝑦) ∈ ℂ)
170	134, 121, 129, 154, 169	breprexplema 34964	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)))
171	170	oveq1d 7428	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
172	126	adantr 485	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
173	150, 172	mulcld 11231	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ)
174	125, 173	fsumcl 15786	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) ∈ ℂ)
175	123, 130, 174	fsummulc1 15838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
176	125, 131, 173	fsummulc1 15838	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)))
177	131	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → (𝑍↑𝑚) ∈ ℂ)
178	150, 172, 177	mulassd 11234	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
179	178	sumeq2dv 15755	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
180	176, 179	eqtrd 2804	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
181	180	sumeq2dv 15755	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
182	171, 175, 181	3eqtrd 2808	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
183	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (1...𝑁) ⊆ ℕ)
184		1nn0 12522	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
185	184	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → 1 ∈ ℕ0)
186	121, 185	nn0addcld 12571	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (𝑇 + 1) ∈ ℕ0)
187	183, 116, 186, 123	reprfi 34950	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → ((1...𝑁)(repr‘(𝑇 + 1))𝑚) ∈ Fin)
188		fzofi 14012	. . . . . . . . . 10 ⊢ (0..^(𝑇 + 1)) ∈ Fin
189	188	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ∈ Fin)
190	134	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑁 ∈ ℕ0)
191	16	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑆 ∈ ℕ0)
192	127	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑍 ∈ ℂ)
193	20	ad3antrrr 742	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
194	164	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → (0..^(𝑇 + 1)) ⊆ (0..^𝑆))
195	194	sselda 3945	. . . . . . . . . 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 738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑚 ∈ ℤ)
198	186	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑇 + 1) ∈ ℕ0)
199		simplr 780	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚))
200	196, 197, 198, 199	reprf 34946	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑑:(0..^(𝑇 + 1))⟶(1...𝑁))
201		simpr 489	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → 𝑎 ∈ (0..^(𝑇 + 1)))
202	200, 201	ffvelcdmd 7083	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ (1...𝑁))
203	39, 202	sselid 3943	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → (𝑑‘𝑎) ∈ ℕ)
204	190, 191, 192, 193, 195, 203	breprexplemb 34965	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) ∧ 𝑎 ∈ (0..^(𝑇 + 1))) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
205	189, 204	fprodcl 16008	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)) → ∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
206	187, 130, 205	fsummulc1 15838	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
207	152, 182, 206	3eqtr2rd 2811	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
208	207	sumeq2dv 15755	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
209		oveq1 7420	. . . . . . . . . . 11 ⊢ (𝑛 = 𝑚 → (𝑛 − 𝑏) = (𝑚 − 𝑏))
210	209	oveq2d 7429	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏)))
211	210	sumeq1d 15753	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
212		oveq2 7421	. . . . . . . . . 10 ⊢ (𝑛 = 𝑚 → (𝑍↑𝑛) = (𝑍↑𝑚))
213	212	oveq2d 7429	. . . . . . . . 9 ⊢ (𝑛 = 𝑚 → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
214	211, 213	oveq12d 7431	. . . . . . . 8 ⊢ (𝑛 = 𝑚 → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
215	214	adantr 485	. . . . . . 7 ⊢ ((𝑛 = 𝑚 ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
216	215	sumeq2dv 15755	. . . . . 6 ⊢ (𝑛 = 𝑚 → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚))))
217	216	cbvsumv 15749	. . . . 5 ⊢ Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑚 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
218	208, 217	eqtr4di 2822	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))))
219	1, 14	nn0mulcld 12572	. . . . . 6 ⊢ (𝜑 → (𝑇 · 𝑁) ∈ ℕ0)
220		oveq2 7421	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑏) → ((1...𝑁)(repr‘𝑇)𝑚) = ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)))
221	220	sumeq1d 15753	. . . . . . 7 ⊢ (𝑚 = (𝑛 − 𝑏) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
222		oveq1 7420	. . . . . . . . 9 ⊢ (𝑚 = (𝑛 − 𝑏) → (𝑚 + 𝑏) = ((𝑛 − 𝑏) + 𝑏))
223	222	oveq2d 7429	. . . . . . . 8 ⊢ (𝑚 = (𝑛 − 𝑏) → (𝑍↑(𝑚 + 𝑏)) = (𝑍↑((𝑛 − 𝑏) + 𝑏)))
224	223	oveq2d 7429	. . . . . . 7 ⊢ (𝑚 = (𝑛 − 𝑏) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))
225	221, 224	oveq12d 7431	. . . . . 6 ⊢ (𝑚 = (𝑛 − 𝑏) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
226	39	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
227		uzssz 12885	. . . . . . . . . 10 ⊢ (ℤ≥‘-𝑏) ⊆ ℤ
228		simp2 1153	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ (ℤ≥‘-𝑏))
229	227, 228	sselid 3943	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℤ)
230	1	3ad2ant1 1149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ ℕ0)
231	57	3ad2ant1 1149	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
232	226, 229, 230, 231	reprfi 34950	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
233	9	a1i 11	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ∈ Fin)
234	58	3adant2 1147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑁 ∈ ℕ0)
235	234	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑁 ∈ ℕ0)
236	59	3adant2 1147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
237	236	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑆 ∈ ℕ0)
238	60	3adant2 1147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
239	238	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑍 ∈ ℂ)
240	61	3adant2 1147	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
241	240	ad2antrr 738	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝐿:(0..^𝑆)⟶(ℂ ↑m ℕ))
242	36	3ad2ant1 1149	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (0..^𝑇) ⊆ (0..^𝑆))
243	242	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (0..^𝑇) ⊆ (0..^𝑆))
244	243	sselda 3945	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑆))
245	39	a1i 11	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (1...𝑁) ⊆ ℕ)
246	229	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℤ)
247	230	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑇 ∈ ℕ0)
248		simpr 489	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚))
249	245, 246, 247, 248	reprf 34946	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
250	249	adantr 485	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑑:(0..^𝑇)⟶(1...𝑁))
251		simpr 489	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → 𝑎 ∈ (0..^𝑇))
252	250, 251	ffvelcdmd 7083	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ (1...𝑁))
253	39, 252	sselid 3943	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → (𝑑‘𝑎) ∈ ℕ)
254	235, 237, 239, 241, 244, 253	breprexplemb 34965	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) ∧ 𝑎 ∈ (0..^𝑇)) → ((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
255	233, 254	fprodcl 16008	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
256	232, 255	fsumcl 15786	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
257	70	3adant2 1147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑇 ∈ (0..^𝑆))
258	72	3adant2 1147	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ)
259	234, 236, 238, 240, 257, 258	breprexplemb 34965	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
260	229	zcnd 12703	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℂ)
261		simp3 1154	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
262	261	elfzelzd 13555	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
263	262	zcnd 12703	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
264	260, 263	subnegd 11578	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) = (𝑚 + 𝑏))
265	262	znegcld 12704	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ∈ ℤ)
266		eluzle 12877	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ (ℤ≥‘-𝑏) → -𝑏 ≤ 𝑚)
267	228, 266	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → -𝑏 ≤ 𝑚)
268		znn0sub 12643	. . . . . . . . . . . 12 ⊢ ((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (-𝑏 ≤ 𝑚 ↔ (𝑚 − -𝑏) ∈ ℕ0))
269	268	biimpa 481	. . . . . . . . . . 11 ⊢ (((-𝑏 ∈ ℤ ∧ 𝑚 ∈ ℤ) ∧ -𝑏 ≤ 𝑚) → (𝑚 − -𝑏) ∈ ℕ0)
270	265, 229, 267, 269	syl21anc 850	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 − -𝑏) ∈ ℕ0)
271	264, 270	eqeltrrd 2870	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
272	238, 271	expcld 14184	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
273	259, 272	mulcld 11231	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
274	256, 273	mulcld 11231	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (ℤ≥‘-𝑏) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) ∈ ℂ)
275	58	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℕ0)
276		ssidd 3968	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (1...𝑁) ⊆ (1...𝑁))
277		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)))
278	277	elfzelzd 13555	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℤ)
279		simplr 780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ (1...𝑁))
280	279	elfzelzd 13555	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℤ)
281	278, 280	zsubcld 12707	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑛 − 𝑏) ∈ ℤ)
282	1	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℕ0)
283	25	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℝ)
284	275	nn0red 12568	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℝ)
285	283, 284	remulcld 11241	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℝ)
286	280	zred 12702	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℝ)
287	219	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (𝑇 · 𝑁) ∈ ℕ0)
288	287, 74	nn0addcld 12571	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((𝑇 · 𝑁) + 𝑏) ∈ ℕ0)
289	184	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → 1 ∈ ℕ0)
290	288, 289	nn0addcld 12571	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0)
291		fz2ssnn0 33073	. . . . . . . . . . . . . . 15 ⊢ ((((𝑇 · 𝑁) + 𝑏) + 1) ∈ ℕ0 → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
292	290, 291	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑏 ∈ (1...𝑁)) → ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) ⊆ ℕ0)
293	292	sselda 3945	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℕ0)
294	293	nn0red 12568	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℝ)
295	23	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑇 ∈ ℤ)
296	275	nn0zd 12618	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑁 ∈ ℤ)
297	295, 296	zmulcld 12708	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) ∈ ℤ)
298	297, 280	zaddcld 12706	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) ∈ ℤ)
299		elfzle1 13557	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁)) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
300	277, 299	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛)
301		zltp1le 12646	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛))
302	301	biimpar 482	. . . . . . . . . . . . 13 ⊢ (((((𝑇 · 𝑁) + 𝑏) ∈ ℤ ∧ 𝑛 ∈ ℤ) ∧ (((𝑇 · 𝑁) + 𝑏) + 1) ≤ 𝑛) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
303	298, 278, 300, 302	syl21anc 850	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑇 · 𝑁) + 𝑏) < 𝑛)
304		ltaddsub 11690	. . . . . . . . . . . . 13 ⊢ (((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) → (((𝑇 · 𝑁) + 𝑏) < 𝑛 ↔ (𝑇 · 𝑁) < (𝑛 − 𝑏)))
305	304	biimpa 481	. . . . . . . . . . . 12 ⊢ ((((𝑇 · 𝑁) ∈ ℝ ∧ 𝑏 ∈ ℝ ∧ 𝑛 ∈ ℝ) ∧ ((𝑇 · 𝑁) + 𝑏) < 𝑛) → (𝑇 · 𝑁) < (𝑛 − 𝑏))
306	285, 286, 294, 303, 305	syl31anc 1398	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑇 · 𝑁) < (𝑛 − 𝑏))
307	275, 276, 281, 282, 306	reprgt 34955	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅)
308	307	sumeq1d 15753	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
309		sum0 15774	. . . . . . . . 9 ⊢ Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0
310	308, 309	eqtrdi 2820	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0)
311	310	oveq1d 7428	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
312	73	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
313	60	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑍 ∈ ℂ)
314	278	zcnd 12703	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑛 ∈ ℂ)
315	280	zcnd 12703	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → 𝑏 ∈ ℂ)
316	314, 315	npcand 11575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
317	316, 293	eqeltrd 2869	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → ((𝑛 − 𝑏) + 𝑏) ∈ ℕ0)
318	313, 317	expcld 14184	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ)
319	312, 318	mulcld 11231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ)
320	319	mul02d 11410	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
321	311, 320	eqtrd 2804	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ ((((𝑇 · 𝑁) + 𝑏) + 1)...((𝑇 · 𝑁) + 𝑁))) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
322	39	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (1...𝑁) ⊆ ℕ)
323		fzossfz 13709	. . . . . . . . . . . . . 14 ⊢ (0..^𝑏) ⊆ (0...𝑏)
324		fzssz 13556	. . . . . . . . . . . . . 14 ⊢ (0...𝑏) ⊆ ℤ
325	323, 324	sstri 3954	. . . . . . . . . . . . 13 ⊢ (0..^𝑏) ⊆ ℤ
326		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ (0..^𝑏))
327	325, 326	sselid 3943	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℤ)
328		simplr 780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ (1...𝑁))
329	328	elfzelzd 13555	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℤ)
330	327, 329	zsubcld 12707	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℤ)
331	1	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℕ0)
332	330	zred 12702	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) ∈ ℝ)
333		0red 11213	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ∈ ℝ)
334	25	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑇 ∈ ℝ)
335		elfzolt2 13699	. . . . . . . . . . . . . 14 ⊢ (𝑛 ∈ (0..^𝑏) → 𝑛 < 𝑏)
336	335	adantl 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 < 𝑏)
337	327	zred 12702	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℝ)
338	329	zred 12702	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℝ)
339	337, 338	sublt0d 11842	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) < 0 ↔ 𝑛 < 𝑏))
340	336, 339	mpbird 260	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 0)
341	62	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 0 ≤ 𝑇)
342	332, 333, 334, 340, 341	ltletrd 11372	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑛 − 𝑏) < 𝑇)
343	322, 330, 331, 342	reprlt 34953	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏)) = ∅)
344	343	sumeq1d 15753	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = Σ𝑑 ∈ ∅ ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)))
345	344, 309	eqtrdi 2820	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) = 0)
346	345	oveq1d 7428	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
347	73	adantr 485	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
348	60	adantr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑍 ∈ ℂ)
349	337	recnd 11239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℂ)
350	338	recnd 11239	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑏 ∈ ℂ)
351	349, 350	npcand 11575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
352		fzo0ssnn0 13777	. . . . . . . . . . . 12 ⊢ (0..^𝑏) ⊆ ℕ0
353	352, 326	sselid 3943	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → 𝑛 ∈ ℕ0)
354	351, 353	eqeltrd 2869	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → ((𝑛 − 𝑏) + 𝑏) ∈ ℕ0)
355	348, 354	expcld 14184	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (𝑍↑((𝑛 − 𝑏) + 𝑏)) ∈ ℂ)
356	347, 355	mulcld 11231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))) ∈ ℂ)
357	356	mul02d 11410	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (0 · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
358	346, 357	eqtrd 2804	. . . . . 6 ⊢ (((𝜑 ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑛 ∈ (0..^𝑏)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))) = 0)
359	219, 14, 225, 274, 321, 358	fsum2dsub 34941	. . . . 5 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
360		nn0sscn 12511	. . . . . . . . 9 ⊢ ℕ0 ⊆ ℂ
361	360, 1	sselid 3943	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ ℂ)
362	360, 14	sselid 3943	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℂ)
363	361, 362	adddirp1d 11237	. . . . . . 7 ⊢ (𝜑 → ((𝑇 + 1) · 𝑁) = ((𝑇 · 𝑁) + 𝑁))
364	363	oveq2d 7429	. . . . . 6 ⊢ (𝜑 → (0...((𝑇 + 1) · 𝑁)) = (0...((𝑇 · 𝑁) + 𝑁)))
365	128, 360	sstri 3954	. . . . . . . . . . . . 13 ⊢ (0...((𝑇 + 1) · 𝑁)) ⊆ ℂ
366		simplr 780	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ (0...((𝑇 + 1) · 𝑁)))
367	365, 366	sselid 3943	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 ∈ ℂ)
368	44, 360	sstri 3954	. . . . . . . . . . . . 13 ⊢ (1...𝑁) ⊆ ℂ
369		simpr 489	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
370	368, 369	sselid 3943	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℂ)
371	367, 370	npcand 11575	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝑛 − 𝑏) + 𝑏) = 𝑛)
372	371	eqcomd 2775	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑛 = ((𝑛 − 𝑏) + 𝑏))
373	372	oveq2d 7429	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑𝑛) = (𝑍↑((𝑛 − 𝑏) + 𝑏)))
374	373	oveq2d 7429	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏))))
375	374	oveq2d 7429	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
376	375	sumeq2dv 15755	. . . . . 6 ⊢ ((𝜑 ∧ 𝑛 ∈ (0...((𝑇 + 1) · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
377	364, 376	sumeq12dv 15759	. . . . 5 ⊢ (𝜑 → Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))) = Σ𝑛 ∈ (0...((𝑇 · 𝑁) + 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑((𝑛 − 𝑏) + 𝑏)))))
378	359, 377	eqtr4d 2807	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑛 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)(𝑛 − 𝑏))∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑛))))
379	105	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) ∈ ℂ)
380	110	adantlr 727	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑚) ∈ ℂ)
381	76	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
382	381	adantr 485	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)) ∈ ℂ)
383	379, 380, 382	mulassd 11234	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))))
384	73	ad4ant13 763	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
385	75	ad4ant13 763	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑𝑏) ∈ ℂ)
386	380, 384, 385	mulassd 11234	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
387	384, 380, 385	mulassd 11234	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏))))
388	380, 384	mulcomd 11232	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)))
389	388	oveq1d 7428	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = ((((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑚)) · (𝑍↑𝑏)))
390	106	adantlr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑍 ∈ ℂ)
391	74	ad4ant13 763	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑏 ∈ ℕ0)
392	109	adantlr 727	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → 𝑚 ∈ ℕ0)
393	390, 391, 392	expaddd 14186	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (𝑍↑(𝑚 + 𝑏)) = ((𝑍↑𝑚) · (𝑍↑𝑏)))
394	393	oveq2d 7429	. . . . . . . . . . . 12 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) = (((𝐿‘𝑇)‘𝑏) · ((𝑍↑𝑚) · (𝑍↑𝑏))))
395	387, 389, 394	3eqtr4d 2814	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (((𝑍↑𝑚) · ((𝐿‘𝑇)‘𝑏)) · (𝑍↑𝑏)) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
396	386, 395	eqtr3d 2806	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))))
397	396	oveq2d 7429	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · ((𝑍↑𝑚) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏)))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
398	383, 397	eqtrd 2804	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → ((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
399	398	sumeq2dv 15755	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
400	87	adantr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑇)𝑚) ∈ Fin)
401	111	adantlr 727	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)) → (∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) ∈ ℂ)
402	400, 381, 401	fsummulc1 15838	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)((∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
403	73	adantlr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → ((𝐿‘𝑇)‘𝑏) ∈ ℂ)
404	60	adantlr 727	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑍 ∈ ℂ)
405	108	adantr 485	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑚 ∈ ℕ0)
406	74	adantlr 727	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℕ0)
407	405, 406	nn0addcld 12571	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑚 + 𝑏) ∈ ℕ0)
408	404, 407	expcld 14184	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (𝑍↑(𝑚 + 𝑏)) ∈ ℂ)
409	403, 408	mulcld 11231	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏))) ∈ ℂ)
410	400, 409, 379	fsummulc1 15838	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))))
411	399, 402, 410	3eqtr4rd 2815	. . . . . 6 ⊢ (((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) ∧ 𝑏 ∈ (1...𝑁)) → (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = (Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
412	411	sumeq2dv 15755	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝑇 · 𝑁))) → Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
413	412	sumeq2dv 15755	. . . 4 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑(𝑚 + 𝑏)))) = Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))))
414	218, 378, 413	3eqtr2rd 2811	. . 3 ⊢ (𝜑 → Σ𝑚 ∈ (0...(𝑇 · 𝑁))Σ𝑏 ∈ (1...𝑁)(Σ𝑑 ∈ ((1...𝑁)(repr‘𝑇)𝑚)(∏𝑎 ∈ (0..^𝑇)((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)) · (((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
415	80, 113, 414	3eqtr2d 2810	. 2 ⊢ (𝜑 → (∏𝑎 ∈ (0..^𝑇)Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) · Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑇)‘𝑏) · (𝑍↑𝑏))) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))
416	6, 78, 415	3eqtrd 2808	1 ⊢ (𝜑 → ∏𝑎 ∈ (0..^(𝑇 + 1))Σ𝑏 ∈ (1...𝑁)(((𝐿‘𝑎)‘𝑏) · (𝑍↑𝑏)) = Σ𝑚 ∈ (0...((𝑇 + 1) · 𝑁))Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑇 + 1))𝑚)(∏𝑎 ∈ (0..^(𝑇 + 1))((𝐿‘𝑎)‘(𝑑‘𝑎)) · (𝑍↑𝑚)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ∪ cun 3911   ⊆ wss 3913  ∅c0 4294  {csn 4594   class class class wbr 5113  ⟶wf 6535  ‘cfv 6539  (class class class)co 7413   ↑_m cmap 8826  Fincfn 8945  ℂcc 11100  ℝcr 11101  0cc0 11102  1c1 11103   + caddc 11105   · cmul 11107   < clt 11245   ≤ cle 11246   − cmin 11443  -cneg 11444  ℕcn 12235  ℕ₀cn0 12506  ℤcz 12593  ℤ_≥cuz 12864  ...cfz 13537  ..^cfzo 13684  ↑cexp 14099  Σcsu 15739  ∏cprod 15959  reprcrepr 34942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5273  ax-pow 5339  ax-pr 5407  ax-un 7735  ax-inf2 9612  ax-cnex 11158  ax-resscn 11159  ax-1cn 11160  ax-icn 11161  ax-addcl 11162  ax-addrcl 11163  ax-mulcl 11164  ax-mulrcl 11165  ax-mulcom 11166  ax-addass 11167  ax-mulass 11168  ax-distr 11169  ax-i2m1 11170  ax-1ne0 11171  ax-1rid 11172  ax-rnegex 11173  ax-rrecex 11174  ax-cnre 11175  ax-pre-lttri 11176  ax-pre-lttrn 11177  ax-pre-ltadd 11178  ax-pre-mulgt0 11179  ax-pre-sup 11180

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-disj 5081  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-se 5618  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6305  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6495  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-isom 6548  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7865  df-1st 7988  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-1o 8455  df-er 8696  df-map 8828  df-pm 8829  df-en 8946  df-dom 8947  df-sdom 8948  df-fin 8949  df-sup 9404  df-oi 9474  df-card 9927  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11445  df-neg 11446  df-div 11874  df-nn 12236  df-2 12305  df-3 12306  df-n0 12507  df-z 12594  df-uz 12865  df-rp 13019  df-ico 13380  df-fz 13538  df-fzo 13685  df-seq 14040  df-exp 14100  df-hash 14369  df-cj 15152  df-re 15153  df-im 15154  df-sqrt 15288  df-abs 15289  df-clim 15541  df-sum 15740  df-prod 15960  df-repr 34943

This theorem is referenced by:  breprexp  34967