Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  dvnprodlem2 Structured version   Visualization version   GIF version

Theorem dvnprodlem2 46526
Description: Induction step for dvnprodlem2 46526. (Contributed by Glauco Siliprandi, 5-Apr-2020.)
Hypotheses
Ref Expression
dvnprodlem2.s (𝜑𝑆 ∈ {ℝ, ℂ})
dvnprodlem2.x (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
dvnprodlem2.t (𝜑𝑇 ∈ Fin)
dvnprodlem2.h ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
dvnprodlem2.n (𝜑𝑁 ∈ ℕ0)
dvnprodlem2.dvnh ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
dvnprodlem2.c 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
dvnprodlem2.r (𝜑𝑅𝑇)
dvnprodlem2.z (𝜑𝑍 ∈ (𝑇𝑅))
dvnprodlem2.ind (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
dvnprodlem2.j (𝜑𝐽 ∈ (0...𝑁))
dvnprodlem2.d 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
Assertion
Ref Expression
dvnprodlem2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Distinct variable groups:   𝐶,𝑐,𝑘,𝑡   𝐷,𝑐,𝑡   𝐻,𝑐,𝑗,𝑘,𝑡   𝑥,𝐻,𝑐,𝑘,𝑡   𝐽,𝑐,𝑗,𝑘,𝑡   𝑛,𝐽,𝑠,𝑐,𝑘,𝑡   𝑥,𝐽   𝑗,𝑁,𝑡   𝑅,𝑐,𝑘,𝑛,𝑠,𝑡   𝑥,𝑅   𝑆,𝑐,𝑗,𝑘,𝑡   𝑥,𝑆   𝑇,𝑗,𝑡   𝑇,𝑠   𝑋,𝑐,𝑗,𝑘,𝑡   𝑥,𝑋   𝑍,𝑐,𝑗,𝑘,𝑡   𝑛,𝑍,𝑠   𝑥,𝑍   𝜑,𝑐,𝑗,𝑘,𝑡   𝜑,𝑛,𝑠   𝜑,𝑥
Allowed substitution hints:   𝐶(𝑥,𝑗,𝑛,𝑠)   𝐷(𝑥,𝑗,𝑘,𝑛,𝑠)   𝑅(𝑗)   𝑆(𝑛,𝑠)   𝑇(𝑥,𝑘,𝑛,𝑐)   𝐻(𝑛,𝑠)   𝑁(𝑥,𝑘,𝑛,𝑠,𝑐)   𝑋(𝑛,𝑠)

Proof of Theorem dvnprodlem2
Dummy variables 𝑝 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1936 . . . . . 6 𝑡(𝜑𝑥𝑋)
2 nfcv 2926 . . . . . 6 𝑡((𝐻𝑍)‘𝑥)
3 dvnprodlem2.t . . . . . . . 8 (𝜑𝑇 ∈ Fin)
4 dvnprodlem2.r . . . . . . . 8 (𝜑𝑅𝑇)
5 ssfi 9143 . . . . . . . 8 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
63, 4, 5syl2anc 593 . . . . . . 7 (𝜑𝑅 ∈ Fin)
76adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → 𝑅 ∈ Fin)
8 dvnprodlem2.z . . . . . . 7 (𝜑𝑍 ∈ (𝑇𝑅))
98adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → 𝑍 ∈ (𝑇𝑅))
108eldifbd 3919 . . . . . . 7 (𝜑 → ¬ 𝑍𝑅)
1110adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → ¬ 𝑍𝑅)
12 simpl 486 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝜑)
134sselda 3938 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝑡𝑇)
14 dvnprodlem2.h . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
1512, 13, 14syl2anc 593 . . . . . . . 8 ((𝜑𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
1615adantlr 725 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
17 simplr 778 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → 𝑥𝑋)
1816, 17ffvelcdmd 7068 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → ((𝐻𝑡)‘𝑥) ∈ ℂ)
19 fveq2 6869 . . . . . . 7 (𝑡 = 𝑍 → (𝐻𝑡) = (𝐻𝑍))
2019fveq1d 6871 . . . . . 6 (𝑡 = 𝑍 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑍)‘𝑥))
21 id 22 . . . . . . . . 9 (𝜑𝜑)
22 eldifi 4086 . . . . . . . . . 10 (𝑍 ∈ (𝑇𝑅) → 𝑍𝑇)
238, 22syl 17 . . . . . . . . 9 (𝜑𝑍𝑇)
24 simpr 488 . . . . . . . . . 10 ((𝜑𝑍𝑇) → 𝑍𝑇)
25 id 22 . . . . . . . . . 10 ((𝜑𝑍𝑇) → (𝜑𝑍𝑇))
26 eleq1 2852 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (𝑡𝑇𝑍𝑇))
2726anbi2d 639 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝜑𝑡𝑇) ↔ (𝜑𝑍𝑇)))
2819feq1d 6675 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝐻𝑡):𝑋⟶ℂ ↔ (𝐻𝑍):𝑋⟶ℂ))
2927, 28imbi12d 346 . . . . . . . . . . 11 (𝑡 = 𝑍 → (((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)))
3029, 14vtoclg 3524 . . . . . . . . . 10 (𝑍𝑇 → ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ))
3124, 25, 30sylc 65 . . . . . . . . 9 ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)
3221, 23, 31syl2anc 593 . . . . . . . 8 (𝜑 → (𝐻𝑍):𝑋⟶ℂ)
3332adantr 484 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐻𝑍):𝑋⟶ℂ)
34 simpr 488 . . . . . . 7 ((𝜑𝑥𝑋) → 𝑥𝑋)
3533, 34ffvelcdmd 7068 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐻𝑍)‘𝑥) ∈ ℂ)
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 16021 . . . . 5 ((𝜑𝑥𝑋) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥) = (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))
3736mpteq2dva 5195 . . . 4 (𝜑 → (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))
3837oveq2d 7414 . . 3 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))))
3938fveq1d 6871 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽))
40 dvnprodlem2.s . . 3 (𝜑𝑆 ∈ {ℝ, ℂ})
41 dvnprodlem2.x . . 3 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
421, 7, 18fprodclf 16024 . . 3 ((𝜑𝑥𝑋) → ∏𝑡𝑅 ((𝐻𝑡)‘𝑥) ∈ ℂ)
43 dvnprodlem2.j . . . 4 (𝜑𝐽 ∈ (0...𝑁))
44 elfznn0 13627 . . . 4 (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℕ0)
4543, 44syl 17 . . 3 (𝜑𝐽 ∈ ℕ0)
46 eqid 2764 . . 3 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
47 eqid 2764 . . 3 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
48 dvnprodlem2.c . . . . . . . . . 10 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
49 oveq2 7406 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅))
50 rabeq 3430 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
5149, 50syl 17 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
52 sumeq1 15718 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
5352eqeq1d 2766 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
5453rabbidv 3423 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5551, 54eqtrd 2799 . . . . . . . . . . 11 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5655mpteq2dv 5196 . . . . . . . . . 10 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
57 ssexg 5281 . . . . . . . . . . . . . 14 ((𝑅𝑇𝑇 ∈ Fin) → 𝑅 ∈ V)
584, 3, 57syl2anc 593 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ V)
59 elpwg 4560 . . . . . . . . . . . . 13 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
614, 60mpbird 259 . . . . . . . . . . 11 (𝜑𝑅 ∈ 𝒫 𝑇)
6261adantr 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑅 ∈ 𝒫 𝑇)
63 nn0ex 12489 . . . . . . . . . . . 12 0 ∈ V
6463mptex 7209 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
6564a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
6648, 56, 62, 65fvmptd3 7001 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
67 oveq2 7406 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
6867oveq1d 7413 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅))
69 rabeq 3430 . . . . . . . . . . . 12 (((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
7068, 69syl 17 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
71 eqeq2 2776 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
7271rabbidv 3423 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7370, 72eqtrd 2799 . . . . . . . . . 10 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7473adantl 485 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
75 elfznn0 13627 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
7675adantl 485 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
77 fzfid 13988 . . . . . . . . . . . 12 (𝜑 → (0...𝑘) ∈ Fin)
78 mapfi 9293 . . . . . . . . . . . 12 (((0...𝑘) ∈ Fin ∧ 𝑅 ∈ Fin) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
7977, 6, 78syl2anc 593 . . . . . . . . . . 11 (𝜑 → ((0...𝑘) ↑m 𝑅) ∈ Fin)
8079adantr 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
81 ssrab2 4035 . . . . . . . . . . 11 {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)
8281a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅))
8380, 82ssexd 5282 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
8466, 74, 76, 83fvmptd 6985 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
85 ssfi 9143 . . . . . . . . . 10 ((((0...𝑘) ↑m 𝑅) ∈ Fin ∧ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8679, 81, 85sylancl 595 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8786adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8884, 87eqeltrd 2864 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
8988adantr 484 . . . . . 6 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → ((𝐶𝑅)‘𝑘) ∈ Fin)
9075faccld 14299 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℕ)
9190nncnd 12228 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℂ)
9291ad2antlr 737 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (!‘𝑘) ∈ ℂ)
936adantr 484 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
9493adantlr 725 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
95 elfznn0 13627 . . . . . . . . . . . . . . 15 (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0)
9695ssriv 3942 . . . . . . . . . . . . . 14 (0...𝑘) ⊆ ℕ0
9796a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℕ0)
98 simpr 488 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((𝐶𝑅)‘𝑘))
9984eleq2d 2850 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10099adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10198, 100mpbid 234 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
10281sseli 3934 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
104 elmapi 8832 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ((0...𝑘) ↑m 𝑅) → 𝑐:𝑅⟶(0...𝑘))
105103, 104syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐:𝑅⟶(0...𝑘))
106105adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑐:𝑅⟶(0...𝑘))
107 simpr 488 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑅)
108106, 107ffvelcdmd 7068 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑘))
10997, 108sseldd 3939 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
110109faccld 14299 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
111110nncnd 12228 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
11294, 111fprodcl 15984 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
113110nnne0d 12265 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ≠ 0)
11494, 111, 113fprodn0 16011 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
11592, 112, 114divcld 11969 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
116115adantlr 725 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
11794adantlr 725 . . . . . . . 8 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
11821ad4antr 742 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝜑)
119118, 13sylancom 597 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑇)
120 elfzuz3 13528 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ (ℤ𝑘))
121 fzss2 13571 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (ℤ𝑘) → (0...𝑘) ⊆ (0...𝐽))
122120, 121syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0...𝑘) ⊆ (0...𝐽))
123122adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝐽))
12445nn0zd 12595 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽 ∈ ℤ)
125 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
126125nn0zd 12595 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℤ)
127 elfzle2 13535 . . . . . . . . . . . . . . . . . . 19 (𝐽 ∈ (0...𝑁) → 𝐽𝑁)
12843, 127syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽𝑁)
129124, 126, 1283jca 1142 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
130 eluz2 12847 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝐽) ↔ (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
131129, 130sylibr 236 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝐽))
132 fzss2 13571 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐽) → (0...𝐽) ⊆ (0...𝑁))
133131, 132syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝐽) ⊆ (0...𝑁))
134133adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝐽) ⊆ (0...𝑁))
135123, 134sstrd 3948 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝑁))
136135ad2antrr 736 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ (0...𝑁))
137136, 108sseldd 3939 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
138137adantllr 729 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
139 fvex 6882 . . . . . . . . . . 11 (𝑐𝑡) ∈ V
140 eleq1 2852 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑡) ∈ (0...𝑁)))
1411403anbi3d 1465 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁))))
142 fveq2 6869 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
143142feq1d 6675 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ))
144141, 143imbi12d 346 . . . . . . . . . . 11 (𝑗 = (𝑐𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)))
145 dvnprodlem2.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
146139, 144, 145vtocl 3527 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
147118, 119, 138, 146syl3anc 1392 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
148 simpllr 785 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑥𝑋)
149147, 148ffvelcdmd 7068 . . . . . . . 8 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
150117, 149fprodcl 15984 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
151116, 150mulcld 11204 . . . . . 6 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
15289, 151fsumcl 15762 . . . . 5 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
153152fmpttd 7098 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ)
154 dvnprodlem2.ind . . . . . . 7 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
155154adantr 484 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
156 0zd 12582 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ∈ ℤ)
157126adantr 484 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℤ)
158 elfzelz 13531 . . . . . . . 8 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
159158adantl 485 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
160 elfzle1 13534 . . . . . . . 8 (𝑘 ∈ (0...𝐽) → 0 ≤ 𝑘)
161160adantl 485 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
162159zred 12679 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
16345nn0red 12545 . . . . . . . . 9 (𝜑𝐽 ∈ ℝ)
164163adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
165157zred 12679 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℝ)
166 elfzle2 13535 . . . . . . . . 9 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
167166adantl 485 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
168128adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽𝑁)
169162, 164, 165, 167, 168letrd 11342 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝑁)
170156, 157, 159, 161, 169elfzd 13522 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ (0...𝑁))
171 rspa 3253 . . . . . 6 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
172155, 170, 171syl2anc 593 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
173172feq1d 6675 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ))
174153, 173mpbird 259 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ)
17523adantr 484 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑍𝑇)
176 simpl 486 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝜑)
177176, 175, 1703jca 1142 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → (𝜑𝑍𝑇𝑘 ∈ (0...𝑁)))
178263anbi2d 1464 . . . . . . 7 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑘 ∈ (0...𝑁))))
17919oveq2d 7414 . . . . . . . . 9 (𝑡 = 𝑍 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑍)))
180179fveq1d 6871 . . . . . . . 8 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
181180feq1d 6675 . . . . . . 7 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
182178, 181imbi12d 346 . . . . . 6 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)))
183 eleq1 2852 . . . . . . . . 9 (𝑗 = 𝑘 → (𝑗 ∈ (0...𝑁) ↔ 𝑘 ∈ (0...𝑁)))
1841833anbi3d 1465 . . . . . . . 8 (𝑗 = 𝑘 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇𝑘 ∈ (0...𝑁))))
185 fveq2 6869 . . . . . . . . 9 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘𝑘))
186185feq1d 6675 . . . . . . . 8 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ))
187184, 186imbi12d 346 . . . . . . 7 (𝑗 = 𝑘 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)))
188187, 145chvarvv 2011 . . . . . 6 ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)
189182, 188vtoclg 3524 . . . . 5 (𝑍𝑇 → ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
190175, 177, 189sylc 65 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)
19132feqmptd 6937 . . . . . . . . 9 (𝜑 → (𝐻𝑍) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
192191eqcomd 2770 . . . . . . . 8 (𝜑 → (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝐻𝑍))
193192oveq2d 7414 . . . . . . 7 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))) = (𝑆 D𝑛 (𝐻𝑍)))
194193fveq1d 6871 . . . . . 6 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
195194adantr 484 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
196195feq1d 6675 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
197190, 196mpbird 259 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ)
198 fveq2 6869 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑡)‘𝑥))
199198prodeq2ad 46173 . . . . . . 7 (𝑦 = 𝑥 → ∏𝑡𝑅 ((𝐻𝑡)‘𝑦) = ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
200199cbvmptv 5206 . . . . . 6 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
201200oveq2i 7409 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))
202201fveq1i 6870 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘)
203202mpteq2i 5198 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
204 fveq2 6869 . . . . . . 7 (𝑦 = 𝑥 → ((𝐻𝑍)‘𝑦) = ((𝐻𝑍)‘𝑥))
205204cbvmptv 5206 . . . . . 6 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
206205oveq2i 7409 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
207206fveq1i 6870 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘)
208207mpteq2i 5198 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘))
20940, 41, 42, 35, 45, 46, 47, 174, 197, 203, 208dvnmul 46522 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽) = (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))))
210202a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
211154r19.21bi 3256 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
212176, 170, 211syl2anc 593 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
213210, 212eqtrd 2799 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
214213mpteq2dva 5195 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
215 mptexg 7207 . . . . . . . . . . . . . 14 (𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
21641, 215syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
217216adantr 484 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
218214, 217fvmpt2d 6991 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
219218adantlr 725 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
220219fveq1d 6871 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥))
22134adantr 484 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → 𝑥𝑋)
222152an32s 662 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
223 eqid 2764 . . . . . . . . . . 11 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
224223fvmpt2 6989 . . . . . . . . . 10 ((𝑥𝑋 ∧ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
225221, 222, 224syl2anc 593 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
226220, 225eqtrd 2799 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
227 fveq2 6869 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
228227cbvmptv 5206 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
229228a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)))
230206, 193eqtrid 2811 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝐻𝑍)))
231230fveq1d 6871 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
232231mpteq2dv 5196 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
233229, 232eqtrd 2799 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
234233adantr 484 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
235 fveq2 6869 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
236235adantl 485 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑗 = (𝐽𝑘)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
237 0zd 12582 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 0 ∈ ℤ)
238 elfzel2 13529 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
239238, 158zsubcld 12684 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ∈ ℤ)
240237, 238, 2393jca 1142 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ))
241238zred 12679 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
24275nn0red 12545 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
243241, 242subge0d 11779 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
244166, 243mpbird 259 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
245241, 242subge02d 11781 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
246160, 245mpbid 234 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ≤ 𝐽)
247240, 244, 246jca32 523 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝐽) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
248247adantl 485 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
249 elfz2 13521 . . . . . . . . . . . 12 ((𝐽𝑘) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
250248, 249sylibr 236 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ∈ (0...𝐽))
251 fvex 6882 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V
252251a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V)
253234, 236, 250, 252fvmptd 6985 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
254253adantlr 725 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
255254fveq1d 6871 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
256226, 255oveq12d 7416 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)) = (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
257256oveq2d 7414 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
25888adantlr 725 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
259 ovex 7431 . . . . . . . . . . . 12 (𝐽𝑘) ∈ V
260 eleq1 2852 . . . . . . . . . . . . . 14 (𝑗 = (𝐽𝑘) → (𝑗 ∈ (0...𝐽) ↔ (𝐽𝑘) ∈ (0...𝐽)))
261260anbi2d 639 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → ((𝜑𝑗 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽))))
262235feq1d 6675 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ))
263261, 262imbi12d 346 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → (((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)))
264 eleq1 2852 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ (0...𝐽) ↔ 𝑗 ∈ (0...𝐽)))
265264anbi2d 639 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ (0...𝐽)) ↔ (𝜑𝑗 ∈ (0...𝐽))))
266 fveq2 6869 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
267266feq1d 6675 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
268265, 267imbi12d 346 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
269268, 190chvarvv 2011 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
270259, 263, 269vtocl 3527 . . . . . . . . . . 11 ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
271176, 250, 270syl2anc 593 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
272271adantlr 725 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
273272, 221ffvelcdmd 7068 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
274 anass 472 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ (𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)))
275 ancom 464 . . . . . . . . . . . . . 14 ((𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋) ↔ (𝑥𝑋𝑘 ∈ (0...𝐽)))
276275anbi2i 632 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
277 anass 472 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
278277bicomi 226 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
279276, 278bitri 277 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
280274, 279bitri 277 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
281280anbi1i 633 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ↔ (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)))
282281imbi1i 351 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) ↔ ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ))
283151, 282mpbi 232 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
284258, 273, 283fsummulc1 15814 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
285284oveq2d 7414 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
286176, 45syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℕ0)
287286, 159bccld 45899 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℕ0)
288287nn0cnd 12546 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
289288adantlr 725 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
290273adantr 484 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
291283, 290mulcld 11204 . . . . . . 7 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
292258, 289, 291fsummulc2 15813 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
293257, 285, 2923eqtrd 2803 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
294293sumeq2dv 15731 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
295 vex 3460 . . . . . . . 8 𝑘 ∈ V
296 vex 3460 . . . . . . . 8 𝑐 ∈ V
297295, 296op1std 7982 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (1st𝑝) = 𝑘)
298297oveq2d 7414 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽C(1st𝑝)) = (𝐽C𝑘))
299297fveq2d 6873 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘(1st𝑝)) = (!‘𝑘))
300295, 296op2ndd 7983 . . . . . . . . . . . 12 (𝑝 = ⟨𝑘, 𝑐⟩ → (2nd𝑝) = 𝑐)
301300fveq1d 6871 . . . . . . . . . . 11 (𝑝 = ⟨𝑘, 𝑐⟩ → ((2nd𝑝)‘𝑡) = (𝑐𝑡))
302301fveq2d 6873 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘(𝑐𝑡)))
303302prodeq2ad 46173 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡)))
304299, 303oveq12d 7416 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
305301fveq2d 6873 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
306305fveq1d 6871 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
307306prodeq2ad 46173 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
308304, 307oveq12d 7416 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
309297oveq2d 7414 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽 − (1st𝑝)) = (𝐽𝑘))
310309fveq2d 6873 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
311310fveq1d 6871 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
312308, 311oveq12d 7416 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
313298, 312oveq12d 7416 . . . . 5 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
314 fzfid 13988 . . . . 5 ((𝜑𝑥𝑋) → (0...𝐽) ∈ Fin)
315289adantrr 727 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → (𝐽C𝑘) ∈ ℂ)
316291anasss 470 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
317315, 316mulcld 11204 . . . . 5 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) ∈ ℂ)
318313, 314, 258, 317fsum2d 15800 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))))
319 ovex 7431 . . . . . . . . 9 (𝐽 − (𝑐𝑍)) ∈ V
320296resex 6017 . . . . . . . . 9 (𝑐𝑅) ∈ V
321319, 320op1std 7982 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (1st𝑝) = (𝐽 − (𝑐𝑍)))
322321oveq2d 7414 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽C(1st𝑝)) = (𝐽C(𝐽 − (𝑐𝑍))))
323321fveq2d 6873 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘(1st𝑝)) = (!‘(𝐽 − (𝑐𝑍))))
324319, 320op2ndd 7983 . . . . . . . . . . . . 13 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (2nd𝑝) = (𝑐𝑅))
325324fveq1d 6871 . . . . . . . . . . . 12 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((2nd𝑝)‘𝑡) = ((𝑐𝑅)‘𝑡))
326325fveq2d 6873 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘((𝑐𝑅)‘𝑡)))
327326prodeq2ad 46173 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)))
328323, 327oveq12d 7416 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))))
329325fveq2d 6873 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)))
330329fveq1d 6871 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
331330prodeq2ad 46173 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
332328, 331oveq12d 7416 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)))
333321oveq2d 7414 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽 − (1st𝑝)) = (𝐽 − (𝐽 − (𝑐𝑍))))
334333fveq2d 6873 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))))
335334fveq1d 6871 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))
336332, 335oveq12d 7416 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)))
337322, 336oveq12d 7416 . . . . . 6 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
338 oveq2 7406 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})))
339 rabeq 3430 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
340338, 339syl 17 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
341 sumeq1 15718 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
342341eqeq1d 2766 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
343342rabbidv 3423 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
344340, 343eqtrd 2799 . . . . . . . . . . 11 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
345344mpteq2dv 5196 . . . . . . . . . 10 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
34623snssd 4747 . . . . . . . . . . . 12 (𝜑 → {𝑍} ⊆ 𝑇)
3474, 346unssd 4146 . . . . . . . . . . 11 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
3483, 347ssexd 5282 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
349 elpwg 4560 . . . . . . . . . . . 12 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
350348, 349syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
351347, 350mpbird 259 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
35263mptex 7209 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
353352a1i 11 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
35448, 345, 351, 353fvmptd3 7001 . . . . . . . . 9 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
355 oveq2 7406 . . . . . . . . . . . . 13 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
356355oveq1d 7413 . . . . . . . . . . . 12 (𝑛 = 𝐽 → ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
357 rabeq 3430 . . . . . . . . . . . 12 (((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
358356, 357syl 17 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
359 eqeq2 2776 . . . . . . . . . . . 12 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
360359rabbidv 3423 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
361358, 360eqtrd 2799 . . . . . . . . . 10 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
362361adantl 485 . . . . . . . . 9 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
363 ovex 7431 . . . . . . . . . . 11 ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ V
364363rabex 5297 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
365364a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
366354, 362, 45, 365fvmptd 6985 . . . . . . . 8 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
367 fzfid 13988 . . . . . . . . . 10 (𝜑 → (0...𝐽) ∈ Fin)
368 snfi 9026 . . . . . . . . . . . 12 {𝑍} ∈ Fin
369368a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑍} ∈ Fin)
370 unfi 9141 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ Fin)
3716, 369, 370syl2anc 593 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ Fin)
372 mapfi 9293 . . . . . . . . . 10 (((0...𝐽) ∈ Fin ∧ (𝑅 ∪ {𝑍}) ∈ Fin) → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
373367, 371, 372syl2anc 593 . . . . . . . . 9 (𝜑 → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
374 ssrab2 4035 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))
375374a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
376 ssfi 9143 . . . . . . . . 9 ((((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin ∧ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))) → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
377373, 375, 376syl2anc 593 . . . . . . . 8 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
378366, 377eqeltrd 2864 . . . . . . 7 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
379378adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
380 dvnprodlem2.d . . . . . . . 8 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38148, 45, 380, 3, 23, 10, 347dvnprodlem1 46525 . . . . . . 7 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
382381adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
383 simpr 488 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
384 opex 5433 . . . . . . . . 9 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
385384a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
386380fvmpt2 6989 . . . . . . . 8 ((𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
387383, 385, 386syl2anc 593 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
388387adantlr 725 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38945adantr 484 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℕ0)
390 eliun 4955 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
391390bilani 508 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
392 nfv 1936 . . . . . . . . . . . . . 14 𝑘𝜑
393 nfcv 2926 . . . . . . . . . . . . . . 15 𝑘𝑝
394 nfiu1 4987 . . . . . . . . . . . . . . 15 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
395393, 394nfel 2940 . . . . . . . . . . . . . 14 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
396392, 395nfan 1921 . . . . . . . . . . . . 13 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
397 nfv 1936 . . . . . . . . . . . . 13 𝑘(1st𝑝) ∈ (0...𝐽)
398 xp1st 8004 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
399 elsni 4601 . . . . . . . . . . . . . . . . . 18 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
400398, 399syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
401400adantl 485 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
402 simpl 486 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
403401, 402eqeltrd 2864 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
404403ex 416 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
405404a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
406396, 397, 405rexlimd 3271 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
407391, 406mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
408 elfzelz 13531 . . . . . . . . . . 11 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
409407, 408syl 17 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
410389, 409bccld 45899 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℕ0)
411410nn0cnd 12546 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
412411adantlr 725 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
413 elfznn0 13627 . . . . . . . . . . . . . 14 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℕ0)
414407, 413syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℕ0)
415414faccld 14299 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℕ)
416415nncnd 12228 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
417416adantlr 725 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
4186adantr 484 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
419 nfv 1936 . . . . . . . . . . . . . . . 16 𝑘(2nd𝑝):𝑅⟶(0...𝐽)
42084, 82eqsstrd 3972 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝑘) ↑m 𝑅))
421 ovex 7431 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0...𝐽) ∈ V
422421a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0...𝐽) ∈ V)
423 mapss 8873 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝐽) ∈ V ∧ (0...𝑘) ⊆ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
424422, 122, 423syl2anc 593 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
425424adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
426420, 425sstrd 3948 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
4274263adant3 1146 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
428 xp2nd 8005 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4294283ad2ant3 1149 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
430427, 429sseldd 3939 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅))
431 elmapi 8832 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅) → (2nd𝑝):𝑅⟶(0...𝐽))
432430, 431syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
4334323exp 1133 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
434433adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
435396, 419, 434rexlimd 3271 . . . . . . . . . . . . . . 15 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽)))
436391, 435mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
437436ffvelcdmda 7067 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝐽))
438 elfznn0 13627 . . . . . . . . . . . . . . 15 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((2nd𝑝)‘𝑡) ∈ ℕ0)
439438faccld 14299 . . . . . . . . . . . . . 14 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
440439nncnd 12228 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
441437, 440syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
442418, 441fprodcl 15984 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
443442adantlr 725 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
444437, 439syl 17 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
445 nnne0 12249 . . . . . . . . . . . . 13 ((!‘((2nd𝑝)‘𝑡)) ∈ ℕ → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
446444, 445syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
447418, 441, 446fprodn0 16011 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
448447adantlr 725 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
449417, 443, 448divcld 11969 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) ∈ ℂ)
4507adantr 484 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
451 simpll 776 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝜑)
452451, 13sylancom 597 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑡𝑇)
453451, 133syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
454453, 437sseldd 3939 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑁))
455451, 452, 4543jca 1142 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
456 eleq1 2852 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → (𝑗 ∈ (0...𝑁) ↔ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
4574563anbi3d 1465 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁))))
458 fveq2 6869 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)))
459458feq1d 6675 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
460457, 459imbi12d 346 . . . . . . . . . . . . . 14 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)))
461460, 145vtoclg 3524 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
462437, 455, 461sylc 65 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
463462adantllr 729 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
46417adantlr 725 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑥𝑋)
465463, 464ffvelcdmd 7068 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
466450, 465fprodcl 15984 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
467449, 466mulcld 11204 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) ∈ ℂ)
468 nfv 1936 . . . . . . . . . . . . 13 𝑘(𝐽 − (1st𝑝)) ∈ (0...𝐽)
469 simp1 1150 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
4704033adant1 1144 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
471 fznn0sub2 13642 . . . . . . . . . . . . . . . . 17 ((1st𝑝) ∈ (0...𝐽) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
472471adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (1st𝑝) ∈ (0...𝐽)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
473469, 470, 472syl2anc 593 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
4744733exp 1133 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
475474adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
476396, 468, 475rexlimd 3271 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽)))
477391, 476mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
478 simpl 486 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
479478, 23syl 17 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
480478, 133syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ⊆ (0...𝑁))
481480, 477sseldd 3939 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝑁))
482478, 479, 4813jca 1142 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
483 eleq1 2852 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → (𝑗 ∈ (0...𝑁) ↔ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
4844833anbi3d 1465 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁))))
485 fveq2 6869 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))))
486485feq1d 6675 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
487484, 486imbi12d 346 . . . . . . . . . . . 12 (𝑗 = (𝐽 − (1st𝑝)) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)))
488 simp2 1151 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → 𝑍𝑇)
489 id 22 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → (𝜑𝑍𝑇𝑗 ∈ (0...𝑁)))
490263anbi2d 1464 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑗 ∈ (0...𝑁))))
491179fveq1d 6871 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
492491feq1d 6675 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
493490, 492imbi12d 346 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
494493, 145vtoclg 3524 . . . . . . . . . . . . 13 (𝑍𝑇 → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
495488, 489, 494sylc 65 . . . . . . . . . . . 12 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
496487, 495vtoclg 3524 . . . . . . . . . . 11 ((𝐽 − (1st𝑝)) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
497477, 482, 496sylc 65 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
498497adantlr 725 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
49934adantr 484 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑥𝑋)
500498, 499ffvelcdmd 7068 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) ∈ ℂ)
501467, 500mulcld 11204 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) ∈ ℂ)
502412, 501mulcld 11204 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) ∈ ℂ)
503337, 379, 382, 388, 502fsumf1o 15752 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
504 simpl 486 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝜑)
505366adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
506383, 505eleqtrd 2866 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
507374sseli 3934 . . . . . . . . . . . . . . 15 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
508506, 507syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
509 elmapi 8832 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
510508, 509syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
511 snidg 4621 . . . . . . . . . . . . . . . 16 (𝑍𝑇𝑍 ∈ {𝑍})
51223, 511syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑍 ∈ {𝑍})
513 elun2 4137 . . . . . . . . . . . . . . 15 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
514512, 513syl 17 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
515514adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
516510, 515ffvelcdmd 7068 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
517 0zd 12582 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ∈ ℤ)
518124adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℤ)
519 fzssz 13533 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℤ
520519sseli 3934 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℤ)
521520adantl 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℤ)
522518, 521zsubcld 12684 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
523 elfzle2 13535 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
524523adantl 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ≤ 𝐽)
525163adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
526521zred 12679 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℝ)
527525, 526subge0d 11779 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
528524, 527mpbird 259 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
529 elfzle1 13534 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
530529adantl 485 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝑐𝑍))
531525, 526subge02d 11781 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
532530, 531mpbid 234 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
533517, 518, 522, 528, 532elfzd 13522 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
534504, 516, 533syl2anc 593 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
535 bcval2 14320 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
536534, 535syl 17 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
537163recnd 11212 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℂ)
538537adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
539 zsscn 12578 . . . . . . . . . . . . . . . . 17 ℤ ⊆ ℂ
540519, 539sstri 3947 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℂ
541540a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
542541, 516sseldd 3939 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
543538, 542nncand 11549 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
544543fveq2d 6873 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝐽 − (𝑐𝑍)))) = (!‘(𝑐𝑍)))
545544oveq1d 7413 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍)))) = ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍)))))
546545oveq2d 7414 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
54745faccld 14299 . . . . . . . . . . . . . 14 (𝜑 → (!‘𝐽) ∈ ℕ)
548547nncnd 12228 . . . . . . . . . . . . 13 (𝜑 → (!‘𝐽) ∈ ℂ)
549548adantr 484 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
550 elfznn0 13627 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℕ0)
551516, 550syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℕ0)
552551faccld 14299 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℕ)
553552nncnd 12228 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
554 elfznn0 13627 . . . . . . . . . . . . . . 15 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
555534, 554syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
556555faccld 14299 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℕ)
557556nncnd 12228 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
558552nnne0d 12265 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
559556nnne0d 12265 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
560549, 553, 557, 558, 559divdiv1d 12000 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
561560eqcomd 2770 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
562536, 546, 5613eqtrd 2803 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
563562adantlr 725 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
564 fvres 6888 . . . . . . . . . . . . . . . . 17 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
565564fveq2d 6873 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → (!‘((𝑐𝑅)‘𝑡)) = (!‘(𝑐𝑡)))
566565prodeq2i 15950 . . . . . . . . . . . . . . 15 𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡))
567566oveq2i 7409 . . . . . . . . . . . . . 14 ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡)))
568564fveq2d 6873 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
569568fveq1d 6871 . . . . . . . . . . . . . . 15 (𝑡𝑅 → (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
570569prodeq2i 15950 . . . . . . . . . . . . . 14 𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)
571567, 570oveq12i 7410 . . . . . . . . . . . . 13 (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
572571a1i 11 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
573572adantlr 725 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
574557adantlr 725 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
575504, 6syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
57675ssriv 3942 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℕ0
577576a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℕ0)
578510adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
579 elun1 4136 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑅𝑡 ∈ (𝑅 ∪ {𝑍}))
580579adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
581578, 580ffvelcdmd 7068 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
582577, 581sseldd 3939 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
583582faccld 14299 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
584583nncnd 12228 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
585575, 584fprodcl 15984 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
586585adantlr 725 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
5877adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
588504adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝜑)
589504, 13sylan 589 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑇)
590588, 133syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
591590, 581sseldd 3939 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
592588, 589, 591, 146syl3anc 1392 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
593592adantllr 729 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
59417adantlr 725 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑥𝑋)
595593, 594ffvelcdmd 7068 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
596587, 595fprodcl 15984 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
597575, 583fprodnncl 15987 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ)
598 nnne0 12249 . . . . . . . . . . . . . 14 (∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
599597, 598syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
600599adantlr 725 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
601574, 586, 596, 600div32d 11992 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
602573, 601eqtrd 2799 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
603543fveq2d 6873 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
604603fveq1d 6871 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
605604adantlr 725 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
606602, 605oveq12d 7416 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
607596, 586, 600divcld 11969 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
608504, 23syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
609504, 133syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ (0...𝑁))
610609, 516sseldd 3939 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝑁))
611504, 608, 6103jca 1142 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)))
612 eleq1 2852 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑍) ∈ (0...𝑁)))
6136123anbi3d 1465 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁))))
614 fveq2 6869 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
615614feq1d 6675 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
616613, 615imbi12d 346 . . . . . . . . . . . . . 14 (𝑗 = (𝑐𝑍) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)))
617616, 495vtoclg 3524 . . . . . . . . . . . . 13 ((𝑐𝑍) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
618516, 611, 617sylc 65 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
619618adantlr 725 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
62034adantr 484 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑥𝑋)
621619, 620ffvelcdmd 7068 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥) ∈ ℂ)
622574, 607, 621mulassd 11207 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
623606, 622eqtrd 2799 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
624563, 623oveq12d 7416 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))))
625548ad2antrr 736 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
626553adantlr 725 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
627558adantlr 725 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
628625, 626, 627divcld 11969 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / (!‘(𝑐𝑍))) ∈ ℂ)
629607, 621mulcld 11204 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) ∈ ℂ)
630559adantlr 725 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
631628, 574, 629, 630dmmcand 45897 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
632596, 621, 586, 600div23d 12006 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
633632eqcomd 2770 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
634 nfv 1936 . . . . . . . . . . . . 13 𝑡((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
635 nfcv 2926 . . . . . . . . . . . . 13 𝑡(((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)
636608adantlr 725 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
63711adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
638 fveq2 6869 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑐𝑡) = (𝑐𝑍))
639179, 638fveq12d 6876 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
640639fveq1d 6871 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
641634, 635, 587, 636, 637, 595, 640, 621fprodsplitsn 16021 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
642641eqcomd 2770 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
643642oveq1d 7413 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
644633, 643eqtrd 2799 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
645644oveq2d 7414 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
646587, 368, 370sylancl 595 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
647504adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝜑)
648347sselda 3938 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
649648adantlr 725 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
650510, 609fssd 6711 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝑁))
651650ffvelcdmda 7067 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝑁))
652647, 649, 651, 146syl3anc 1392 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
653652adantllr 729 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
654620adantr 484 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑥𝑋)
655653, 654ffvelcdmd 7068 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
656646, 655fprodcl 15984 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
657625, 626, 656, 586, 627, 600divmuldivd 12010 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))))
658553, 585mulcomd 11205 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
659 nfv 1936 . . . . . . . . . . . . . 14 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
660 nfcv 2926 . . . . . . . . . . . . . 14 𝑡(!‘(𝑐𝑍))
661504, 10syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
662638fveq2d 6873 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑍)))
663659, 660, 575, 608, 661, 584, 662, 553fprodsplitsn 16021 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
664663eqcomd 2770 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
665658, 664eqtrd 2799 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
666665oveq2d 7414 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
667666adantlr 725 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
668504, 371syl 17 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
669576a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0...𝐽) ⊆ ℕ0)
670510ffvelcdmda 7067 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝐽))
671669, 670sseldd 3939 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ ℕ0)
672671faccld 14299 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℕ)
673672nncnd 12228 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℂ)
674668, 673fprodcl 15984 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
675674adantlr 725 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
676672nnne0d 12265 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ≠ 0)
677668, 673, 676fprodn0 16011 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
678677adantlr 725 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
679625, 656, 675, 678div23d 12006 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
680 eqidd 2765 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
681667, 679, 6803eqtrd 2803 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
682645, 657, 6813eqtrd 2803 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
683624, 631, 6823eqtrd 2803 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
684683sumeq2dv 15731 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
685503, 684eqtrd 2799 . . . 4 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
686294, 318, 6853eqtrd 2803 . . 3 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
687686mpteq2dva 5195 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
68839, 209, 6873eqtrd 2803 1 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 208  wa 399  w3a 1099   = wceq 1562  wcel 2144  wne 2959  wral 3078  wrex 3088  {crab 3416  Vcvv 3456  cdif 3903  cun 3904  wss 3906  𝒫 cpw 4557  {csn 4584  {cpr 4586  cop 4590   ciun 4951   class class class wbr 5102  cmpt 5183   × cxp 5647  cres 5651  wf 6519  1-1-ontowf1o 6522  cfv 6523  (class class class)co 7398  1st c1st 7970  2nd c2nd 7971  m cmap 8810  Fincfn 8929  cc 11073  cr 11074  0cc0 11075   · cmul 11080  cle 11219  cmin 11416   / cdiv 11846  cn 12212  0cn0 12483  cz 12570  cuz 12841  ...cfz 13514  !cfa 14288  Ccbc 14317  Σcsu 15715  cprod 15935  t crest 17451  TopOpenctopn 17452  fldccnfld 21426   D𝑛 cdvn 25928
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-inf2 9598  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153  ax-addf 11154
This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-se 5603  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-isom 6532  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-of 7662  df-om 7849  df-1st 7972  df-2nd 7973  df-supp 8143  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-2o 8440  df-er 8680  df-map 8812  df-pm 8813  df-ixp 8882  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-fsupp 9310  df-fi 9359  df-sup 9390  df-inf 9391  df-oi 9460  df-card 9899  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12484  df-z 12571  df-dec 12691  df-uz 12842  df-q 12952  df-rp 12996  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ico 13357  df-icc 13358  df-fz 13515  df-fzo 13662  df-seq 14017  df-exp 14077  df-fac 14289  df-bc 14318  df-hash 14346  df-cj 15128  df-re 15129  df-im 15130  df-sqrt 15264  df-abs 15265  df-clim 15517  df-sum 15716  df-prod 15936  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17248  df-ress 17269  df-plusg 17301  df-mulr 17302  df-starv 17303  df-sca 17304  df-vsca 17305  df-ip 17306  df-tset 17307  df-ple 17308  df-ds 17310  df-unif 17311  df-hom 17312  df-cco 17313  df-rest 17453  df-topn 17454  df-0g 17472  df-gsum 17473  df-topgen 17474  df-pt 17475  df-prds 17478  df-xrs 17534  df-qtop 17539  df-imas 17540  df-xps 17542  df-mre 17616  df-mrc 17617  df-acs 17619  df-mgm 18676  df-sgrp 18755  df-mnd 18771  df-submnd 18820  df-mulg 19112  df-cntz 19359  df-cmn 19824  df-psmet 21418  df-xmet 21419  df-met 21420  df-bl 21421  df-mopn 21422  df-fbas 21423  df-fg 21424  df-cnfld 21427  df-top 22956  df-topon 22973  df-topsp 22995  df-bases 23008  df-cld 23081  df-ntr 23082  df-cls 23083  df-nei 23160  df-lp 23198  df-perf 23199  df-cn 23289  df-cnp 23290  df-haus 23377  df-tx 23624  df-hmeo 23817  df-fil 23908  df-fm 24000  df-flim 24001  df-flf 24002  df-xms 24382  df-ms 24383  df-tms 24384  df-cncf 24942  df-limc 25930  df-dv 25931  df-dvn 25932
This theorem is referenced by:  dvnprodlem3  46527
  Copyright terms: Public domain W3C validator