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 43378
Description: Induction step for dvnprodlem2 43378. (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 1918 . . . . . 6 𝑡(𝜑𝑥𝑋)
2 nfcv 2906 . . . . . 6 𝑡((𝐻𝑍)‘𝑥)
3 dvnprodlem2.t . . . . . . . 8 (𝜑𝑇 ∈ Fin)
4 dvnprodlem2.r . . . . . . . 8 (𝜑𝑅𝑇)
5 ssfi 8918 . . . . . . . 8 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
63, 4, 5syl2anc 583 . . . . . . 7 (𝜑𝑅 ∈ Fin)
76adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝑅 ∈ Fin)
8 dvnprodlem2.z . . . . . . 7 (𝜑𝑍 ∈ (𝑇𝑅))
98adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝑍 ∈ (𝑇𝑅))
108eldifbd 3896 . . . . . . 7 (𝜑 → ¬ 𝑍𝑅)
1110adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → ¬ 𝑍𝑅)
12 simpl 482 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝜑)
134sselda 3917 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝑡𝑇)
14 dvnprodlem2.h . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
1512, 13, 14syl2anc 583 . . . . . . . 8 ((𝜑𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
1615adantlr 711 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
17 simplr 765 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → 𝑥𝑋)
1816, 17ffvelrnd 6944 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → ((𝐻𝑡)‘𝑥) ∈ ℂ)
19 fveq2 6756 . . . . . . 7 (𝑡 = 𝑍 → (𝐻𝑡) = (𝐻𝑍))
2019fveq1d 6758 . . . . . 6 (𝑡 = 𝑍 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑍)‘𝑥))
21 id 22 . . . . . . . . 9 (𝜑𝜑)
22 eldifi 4057 . . . . . . . . . 10 (𝑍 ∈ (𝑇𝑅) → 𝑍𝑇)
238, 22syl 17 . . . . . . . . 9 (𝜑𝑍𝑇)
24 simpr 484 . . . . . . . . . 10 ((𝜑𝑍𝑇) → 𝑍𝑇)
25 id 22 . . . . . . . . . 10 ((𝜑𝑍𝑇) → (𝜑𝑍𝑇))
26 eleq1 2826 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (𝑡𝑇𝑍𝑇))
2726anbi2d 628 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝜑𝑡𝑇) ↔ (𝜑𝑍𝑇)))
2819feq1d 6569 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝐻𝑡):𝑋⟶ℂ ↔ (𝐻𝑍):𝑋⟶ℂ))
2927, 28imbi12d 344 . . . . . . . . . . 11 (𝑡 = 𝑍 → (((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)))
3029, 14vtoclg 3495 . . . . . . . . . 10 (𝑍𝑇 → ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ))
3124, 25, 30sylc 65 . . . . . . . . 9 ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)
3221, 23, 31syl2anc 583 . . . . . . . 8 (𝜑 → (𝐻𝑍):𝑋⟶ℂ)
3332adantr 480 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐻𝑍):𝑋⟶ℂ)
34 simpr 484 . . . . . . 7 ((𝜑𝑥𝑋) → 𝑥𝑋)
3533, 34ffvelrnd 6944 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐻𝑍)‘𝑥) ∈ ℂ)
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 15627 . . . . 5 ((𝜑𝑥𝑋) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥) = (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))
3736mpteq2dva 5170 . . . 4 (𝜑 → (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))
3837oveq2d 7271 . . 3 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))))
3938fveq1d 6758 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽))
40 dvnprodlem2.s . . 3 (𝜑𝑆 ∈ {ℝ, ℂ})
41 dvnprodlem2.x . . 3 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
421, 7, 18fprodclf 15630 . . 3 ((𝜑𝑥𝑋) → ∏𝑡𝑅 ((𝐻𝑡)‘𝑥) ∈ ℂ)
43 dvnprodlem2.j . . . 4 (𝜑𝐽 ∈ (0...𝑁))
44 elfznn0 13278 . . . 4 (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℕ0)
4543, 44syl 17 . . 3 (𝜑𝐽 ∈ ℕ0)
46 eqid 2738 . . 3 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
47 eqid 2738 . . 3 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
48 dvnprodlem2.c . . . . . . . . . 10 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
49 oveq2 7263 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅))
50 rabeq 3408 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
5149, 50syl 17 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
52 sumeq1 15328 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
5352eqeq1d 2740 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
5453rabbidv 3404 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5551, 54eqtrd 2778 . . . . . . . . . . 11 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5655mpteq2dv 5172 . . . . . . . . . 10 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
57 ssexg 5242 . . . . . . . . . . . . . 14 ((𝑅𝑇𝑇 ∈ Fin) → 𝑅 ∈ V)
584, 3, 57syl2anc 583 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ V)
59 elpwg 4533 . . . . . . . . . . . . 13 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
614, 60mpbird 256 . . . . . . . . . . 11 (𝜑𝑅 ∈ 𝒫 𝑇)
6261adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑅 ∈ 𝒫 𝑇)
63 nn0ex 12169 . . . . . . . . . . . 12 0 ∈ V
6463mptex 7081 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
6564a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
6648, 56, 62, 65fvmptd3 6880 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
67 oveq2 7263 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
6867oveq1d 7270 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅))
69 rabeq 3408 . . . . . . . . . . . 12 (((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
7068, 69syl 17 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
71 eqeq2 2750 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
7271rabbidv 3404 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7370, 72eqtrd 2778 . . . . . . . . . 10 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7473adantl 481 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
75 elfznn0 13278 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
7675adantl 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
77 fzfid 13621 . . . . . . . . . . . 12 (𝜑 → (0...𝑘) ∈ Fin)
78 mapfi 9045 . . . . . . . . . . . 12 (((0...𝑘) ∈ Fin ∧ 𝑅 ∈ Fin) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
7977, 6, 78syl2anc 583 . . . . . . . . . . 11 (𝜑 → ((0...𝑘) ↑m 𝑅) ∈ Fin)
8079adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
81 ssrab2 4009 . . . . . . . . . . 11 {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)
8281a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅))
8380, 82ssexd 5243 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
8466, 74, 76, 83fvmptd 6864 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
85 ssfi 8918 . . . . . . . . . 10 ((((0...𝑘) ↑m 𝑅) ∈ Fin ∧ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8679, 81, 85sylancl 585 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8786adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8884, 87eqeltrd 2839 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
8988adantr 480 . . . . . 6 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → ((𝐶𝑅)‘𝑘) ∈ Fin)
9075faccld 13926 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℕ)
9190nncnd 11919 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℂ)
9291ad2antlr 723 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (!‘𝑘) ∈ ℂ)
936adantr 480 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
9493adantlr 711 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
95 elfznn0 13278 . . . . . . . . . . . . . . 15 (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0)
9695ssriv 3921 . . . . . . . . . . . . . 14 (0...𝑘) ⊆ ℕ0
9796a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℕ0)
98 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((𝐶𝑅)‘𝑘))
9984eleq2d 2824 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10099adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10198, 100mpbid 231 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
10281sseli 3913 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
104 elmapi 8595 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ((0...𝑘) ↑m 𝑅) → 𝑐:𝑅⟶(0...𝑘))
105103, 104syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐:𝑅⟶(0...𝑘))
106105adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑐:𝑅⟶(0...𝑘))
107 simpr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑅)
108106, 107ffvelrnd 6944 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑘))
10997, 108sseldd 3918 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
110109faccld 13926 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
111110nncnd 11919 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
11294, 111fprodcl 15590 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
113110nnne0d 11953 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ≠ 0)
11494, 111, 113fprodn0 15617 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
11592, 112, 114divcld 11681 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
116115adantlr 711 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
11794adantlr 711 . . . . . . . 8 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
11821ad4antr 728 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝜑)
119118, 13sylancom 587 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑇)
120 elfzuz3 13182 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ (ℤ𝑘))
121 fzss2 13225 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (ℤ𝑘) → (0...𝑘) ⊆ (0...𝐽))
122120, 121syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0...𝑘) ⊆ (0...𝐽))
123122adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝐽))
12445nn0zd 12353 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽 ∈ ℤ)
125 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
126125nn0zd 12353 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℤ)
127 elfzle2 13189 . . . . . . . . . . . . . . . . . . 19 (𝐽 ∈ (0...𝑁) → 𝐽𝑁)
12843, 127syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽𝑁)
129124, 126, 1283jca 1126 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
130 eluz2 12517 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝐽) ↔ (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
131129, 130sylibr 233 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝐽))
132 fzss2 13225 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐽) → (0...𝐽) ⊆ (0...𝑁))
133131, 132syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝐽) ⊆ (0...𝑁))
134133adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝐽) ⊆ (0...𝑁))
135123, 134sstrd 3927 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝑁))
136135ad2antrr 722 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ (0...𝑁))
137136, 108sseldd 3918 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
138137adantllr 715 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
139 fvex 6769 . . . . . . . . . . 11 (𝑐𝑡) ∈ V
140 eleq1 2826 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑡) ∈ (0...𝑁)))
1411403anbi3d 1440 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁))))
142 fveq2 6756 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
143142feq1d 6569 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ))
144141, 143imbi12d 344 . . . . . . . . . . 11 (𝑗 = (𝑐𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)))
145 dvnprodlem2.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
146139, 144, 145vtocl 3488 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
147118, 119, 138, 146syl3anc 1369 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
148 simpllr 772 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑥𝑋)
149147, 148ffvelrnd 6944 . . . . . . . 8 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
150117, 149fprodcl 15590 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
151116, 150mulcld 10926 . . . . . 6 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
15289, 151fsumcl 15373 . . . . 5 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
153152fmpttd 6971 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ)
154 dvnprodlem2.ind . . . . . . 7 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
155154adantr 480 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
156 0zd 12261 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ∈ ℤ)
157126adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℤ)
158 elfzelz 13185 . . . . . . . 8 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
159158adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
160 elfzle1 13188 . . . . . . . 8 (𝑘 ∈ (0...𝐽) → 0 ≤ 𝑘)
161160adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
162159zred 12355 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
16345nn0red 12224 . . . . . . . . 9 (𝜑𝐽 ∈ ℝ)
164163adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
165157zred 12355 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℝ)
166 elfzle2 13189 . . . . . . . . 9 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
167166adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
168128adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽𝑁)
169162, 164, 165, 167, 168letrd 11062 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝑁)
170156, 157, 159, 161, 169elfzd 13176 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ (0...𝑁))
171 rspa 3130 . . . . . 6 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
172155, 170, 171syl2anc 583 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
173172feq1d 6569 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ))
174153, 173mpbird 256 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ)
17523adantr 480 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑍𝑇)
176 simpl 482 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝜑)
177176, 175, 1703jca 1126 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → (𝜑𝑍𝑇𝑘 ∈ (0...𝑁)))
178263anbi2d 1439 . . . . . . 7 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑘 ∈ (0...𝑁))))
17919oveq2d 7271 . . . . . . . . 9 (𝑡 = 𝑍 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑍)))
180179fveq1d 6758 . . . . . . . 8 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
181180feq1d 6569 . . . . . . 7 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
182178, 181imbi12d 344 . . . . . 6 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)))
183 eleq1 2826 . . . . . . . . 9 (𝑗 = 𝑘 → (𝑗 ∈ (0...𝑁) ↔ 𝑘 ∈ (0...𝑁)))
1841833anbi3d 1440 . . . . . . . 8 (𝑗 = 𝑘 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇𝑘 ∈ (0...𝑁))))
185 fveq2 6756 . . . . . . . . 9 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘𝑘))
186185feq1d 6569 . . . . . . . 8 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ))
187184, 186imbi12d 344 . . . . . . 7 (𝑗 = 𝑘 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)))
188187, 145chvarvv 2003 . . . . . 6 ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)
189182, 188vtoclg 3495 . . . . 5 (𝑍𝑇 → ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
190175, 177, 189sylc 65 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)
19132feqmptd 6819 . . . . . . . . 9 (𝜑 → (𝐻𝑍) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
192191eqcomd 2744 . . . . . . . 8 (𝜑 → (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝐻𝑍))
193192oveq2d 7271 . . . . . . 7 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))) = (𝑆 D𝑛 (𝐻𝑍)))
194193fveq1d 6758 . . . . . 6 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
195194adantr 480 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
196195feq1d 6569 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
197190, 196mpbird 256 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ)
198 fveq2 6756 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑡)‘𝑥))
199198prodeq2ad 43023 . . . . . . 7 (𝑦 = 𝑥 → ∏𝑡𝑅 ((𝐻𝑡)‘𝑦) = ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
200199cbvmptv 5183 . . . . . 6 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
201200oveq2i 7266 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))
202201fveq1i 6757 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘)
203202mpteq2i 5175 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
204 fveq2 6756 . . . . . . 7 (𝑦 = 𝑥 → ((𝐻𝑍)‘𝑦) = ((𝐻𝑍)‘𝑥))
205204cbvmptv 5183 . . . . . 6 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
206205oveq2i 7266 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
207206fveq1i 6757 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘)
208207mpteq2i 5175 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘))
20940, 41, 42, 35, 45, 46, 47, 174, 197, 203, 208dvnmul 43374 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽) = (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))))
210202a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
211154r19.21bi 3132 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
212176, 170, 211syl2anc 583 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
213210, 212eqtrd 2778 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
214213mpteq2dva 5170 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
215 mptexg 7079 . . . . . . . . . . . . . 14 (𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
21641, 215syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
217216adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
218214, 217fvmpt2d 6870 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
219218adantlr 711 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
220219fveq1d 6758 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥))
22134adantr 480 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → 𝑥𝑋)
222152an32s 648 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
223 eqid 2738 . . . . . . . . . . 11 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
224223fvmpt2 6868 . . . . . . . . . 10 ((𝑥𝑋 ∧ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
225221, 222, 224syl2anc 583 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
226220, 225eqtrd 2778 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
227 fveq2 6756 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
228227cbvmptv 5183 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
229228a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)))
230206, 193syl5eq 2791 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝐻𝑍)))
231230fveq1d 6758 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
232231mpteq2dv 5172 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
233229, 232eqtrd 2778 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
234233adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
235 fveq2 6756 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
236235adantl 481 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑗 = (𝐽𝑘)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
237 0zd 12261 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 0 ∈ ℤ)
238 elfzel2 13183 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
239238, 158zsubcld 12360 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ∈ ℤ)
240237, 238, 2393jca 1126 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ))
241238zred 12355 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
24275nn0red 12224 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
243241, 242subge0d 11495 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
244166, 243mpbird 256 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
245241, 242subge02d 11497 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
246160, 245mpbid 231 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ≤ 𝐽)
247240, 244, 246jca32 515 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝐽) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
248247adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
249 elfz2 13175 . . . . . . . . . . . 12 ((𝐽𝑘) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
250248, 249sylibr 233 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ∈ (0...𝐽))
251 fvex 6769 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V
252251a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V)
253234, 236, 250, 252fvmptd 6864 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
254253adantlr 711 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
255254fveq1d 6758 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
256226, 255oveq12d 7273 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)) = (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
257256oveq2d 7271 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
25888adantlr 711 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
259 ovex 7288 . . . . . . . . . . . 12 (𝐽𝑘) ∈ V
260 eleq1 2826 . . . . . . . . . . . . . 14 (𝑗 = (𝐽𝑘) → (𝑗 ∈ (0...𝐽) ↔ (𝐽𝑘) ∈ (0...𝐽)))
261260anbi2d 628 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → ((𝜑𝑗 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽))))
262235feq1d 6569 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ))
263261, 262imbi12d 344 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → (((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)))
264 eleq1 2826 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ (0...𝐽) ↔ 𝑗 ∈ (0...𝐽)))
265264anbi2d 628 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ (0...𝐽)) ↔ (𝜑𝑗 ∈ (0...𝐽))))
266 fveq2 6756 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
267266feq1d 6569 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
268265, 267imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
269268, 190chvarvv 2003 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
270259, 263, 269vtocl 3488 . . . . . . . . . . 11 ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
271176, 250, 270syl2anc 583 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
272271adantlr 711 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
273272, 221ffvelrnd 6944 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
274 anass 468 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ (𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)))
275 ancom 460 . . . . . . . . . . . . . 14 ((𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋) ↔ (𝑥𝑋𝑘 ∈ (0...𝐽)))
276275anbi2i 622 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
277 anass 468 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
278277bicomi 223 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
279276, 278bitri 274 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
280274, 279bitri 274 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
281280anbi1i 623 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ↔ (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)))
282281imbi1i 349 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) ↔ ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ))
283151, 282mpbi 229 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
284258, 273, 283fsummulc1 15425 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
285284oveq2d 7271 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
286176, 45syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℕ0)
287286, 159bccld 42744 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℕ0)
288287nn0cnd 12225 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
289288adantlr 711 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
290273adantr 480 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
291283, 290mulcld 10926 . . . . . . 7 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
292258, 289, 291fsummulc2 15424 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
293257, 285, 2923eqtrd 2782 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
294293sumeq2dv 15343 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
295 vex 3426 . . . . . . . 8 𝑘 ∈ V
296 vex 3426 . . . . . . . 8 𝑐 ∈ V
297295, 296op1std 7814 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (1st𝑝) = 𝑘)
298297oveq2d 7271 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽C(1st𝑝)) = (𝐽C𝑘))
299297fveq2d 6760 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘(1st𝑝)) = (!‘𝑘))
300295, 296op2ndd 7815 . . . . . . . . . . . 12 (𝑝 = ⟨𝑘, 𝑐⟩ → (2nd𝑝) = 𝑐)
301300fveq1d 6758 . . . . . . . . . . 11 (𝑝 = ⟨𝑘, 𝑐⟩ → ((2nd𝑝)‘𝑡) = (𝑐𝑡))
302301fveq2d 6760 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘(𝑐𝑡)))
303302prodeq2ad 43023 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡)))
304299, 303oveq12d 7273 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
305301fveq2d 6760 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
306305fveq1d 6758 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
307306prodeq2ad 43023 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
308304, 307oveq12d 7273 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
309297oveq2d 7271 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽 − (1st𝑝)) = (𝐽𝑘))
310309fveq2d 6760 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
311310fveq1d 6758 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
312308, 311oveq12d 7273 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
313298, 312oveq12d 7273 . . . . 5 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
314 fzfid 13621 . . . . 5 ((𝜑𝑥𝑋) → (0...𝐽) ∈ Fin)
315289adantrr 713 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → (𝐽C𝑘) ∈ ℂ)
316291anasss 466 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
317315, 316mulcld 10926 . . . . 5 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) ∈ ℂ)
318313, 314, 258, 317fsum2d 15411 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))))
319 ovex 7288 . . . . . . . . 9 (𝐽 − (𝑐𝑍)) ∈ V
320296resex 5928 . . . . . . . . 9 (𝑐𝑅) ∈ V
321319, 320op1std 7814 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (1st𝑝) = (𝐽 − (𝑐𝑍)))
322321oveq2d 7271 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽C(1st𝑝)) = (𝐽C(𝐽 − (𝑐𝑍))))
323321fveq2d 6760 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘(1st𝑝)) = (!‘(𝐽 − (𝑐𝑍))))
324319, 320op2ndd 7815 . . . . . . . . . . . . 13 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (2nd𝑝) = (𝑐𝑅))
325324fveq1d 6758 . . . . . . . . . . . 12 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((2nd𝑝)‘𝑡) = ((𝑐𝑅)‘𝑡))
326325fveq2d 6760 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘((𝑐𝑅)‘𝑡)))
327326prodeq2ad 43023 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)))
328323, 327oveq12d 7273 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))))
329325fveq2d 6760 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)))
330329fveq1d 6758 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
331330prodeq2ad 43023 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
332328, 331oveq12d 7273 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)))
333321oveq2d 7271 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽 − (1st𝑝)) = (𝐽 − (𝐽 − (𝑐𝑍))))
334333fveq2d 6760 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))))
335334fveq1d 6758 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))
336332, 335oveq12d 7273 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)))
337322, 336oveq12d 7273 . . . . . 6 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
338 oveq2 7263 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})))
339 rabeq 3408 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
340338, 339syl 17 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
341 sumeq1 15328 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
342341eqeq1d 2740 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
343342rabbidv 3404 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
344340, 343eqtrd 2778 . . . . . . . . . . 11 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
345344mpteq2dv 5172 . . . . . . . . . 10 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
34623snssd 4739 . . . . . . . . . . . 12 (𝜑 → {𝑍} ⊆ 𝑇)
3474, 346unssd 4116 . . . . . . . . . . 11 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
3483, 347ssexd 5243 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
349 elpwg 4533 . . . . . . . . . . . 12 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
350348, 349syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
351347, 350mpbird 256 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
35263mptex 7081 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
353352a1i 11 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
35448, 345, 351, 353fvmptd3 6880 . . . . . . . . 9 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
355 oveq2 7263 . . . . . . . . . . . . 13 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
356355oveq1d 7270 . . . . . . . . . . . 12 (𝑛 = 𝐽 → ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
357 rabeq 3408 . . . . . . . . . . . 12 (((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
358356, 357syl 17 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
359 eqeq2 2750 . . . . . . . . . . . 12 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
360359rabbidv 3404 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
361358, 360eqtrd 2778 . . . . . . . . . 10 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
362361adantl 481 . . . . . . . . 9 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
363 ovex 7288 . . . . . . . . . . 11 ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ V
364363rabex 5251 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
365364a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
366354, 362, 45, 365fvmptd 6864 . . . . . . . 8 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
367 fzfid 13621 . . . . . . . . . 10 (𝜑 → (0...𝐽) ∈ Fin)
368 snfi 8788 . . . . . . . . . . . 12 {𝑍} ∈ Fin
369368a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑍} ∈ Fin)
370 unfi 8917 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ Fin)
3716, 369, 370syl2anc 583 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ Fin)
372 mapfi 9045 . . . . . . . . . 10 (((0...𝐽) ∈ Fin ∧ (𝑅 ∪ {𝑍}) ∈ Fin) → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
373367, 371, 372syl2anc 583 . . . . . . . . 9 (𝜑 → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
374 ssrab2 4009 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))
375374a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
376 ssfi 8918 . . . . . . . . 9 ((((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin ∧ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))) → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
377373, 375, 376syl2anc 583 . . . . . . . 8 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
378366, 377eqeltrd 2839 . . . . . . 7 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
379378adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
380 dvnprodlem2.d . . . . . . . 8 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38148, 45, 380, 3, 23, 10, 347dvnprodlem1 43377 . . . . . . 7 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
382381adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
383 simpr 484 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
384 opex 5373 . . . . . . . . 9 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
385384a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
386380fvmpt2 6868 . . . . . . . 8 ((𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
387383, 385, 386syl2anc 583 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
388387adantlr 711 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38945adantr 480 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℕ0)
390 eliun 4925 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
391390biimpi 215 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
392391adantl 481 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
393 nfv 1918 . . . . . . . . . . . . . 14 𝑘𝜑
394 nfcv 2906 . . . . . . . . . . . . . . 15 𝑘𝑝
395 nfiu1 4955 . . . . . . . . . . . . . . 15 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
396394, 395nfel 2920 . . . . . . . . . . . . . 14 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
397393, 396nfan 1903 . . . . . . . . . . . . 13 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
398 nfv 1918 . . . . . . . . . . . . 13 𝑘(1st𝑝) ∈ (0...𝐽)
399 xp1st 7836 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
400 elsni 4575 . . . . . . . . . . . . . . . . . 18 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
401399, 400syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
402401adantl 481 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
403 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
404402, 403eqeltrd 2839 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
405404ex 412 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
406405a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
407397, 398, 406rexlimd 3245 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
408392, 407mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
409 elfzelz 13185 . . . . . . . . . . 11 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
410408, 409syl 17 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
411389, 410bccld 42744 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℕ0)
412411nn0cnd 12225 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
413412adantlr 711 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
414 elfznn0 13278 . . . . . . . . . . . . . 14 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℕ0)
415408, 414syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℕ0)
416415faccld 13926 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℕ)
417416nncnd 11919 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
418417adantlr 711 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
4196adantr 480 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
420 nfv 1918 . . . . . . . . . . . . . . . 16 𝑘(2nd𝑝):𝑅⟶(0...𝐽)
42184, 82eqsstrd 3955 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝑘) ↑m 𝑅))
422 ovex 7288 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0...𝐽) ∈ V
423422a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0...𝐽) ∈ V)
424 mapss 8635 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝐽) ∈ V ∧ (0...𝑘) ⊆ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
425423, 122, 424syl2anc 583 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
426425adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
427421, 426sstrd 3927 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
4284273adant3 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
429 xp2nd 7837 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4304293ad2ant3 1133 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
431428, 430sseldd 3918 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅))
432 elmapi 8595 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅) → (2nd𝑝):𝑅⟶(0...𝐽))
433431, 432syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
4344333exp 1117 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
435434adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
436397, 420, 435rexlimd 3245 . . . . . . . . . . . . . . 15 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽)))
437392, 436mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
438437ffvelrnda 6943 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝐽))
439 elfznn0 13278 . . . . . . . . . . . . . . 15 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((2nd𝑝)‘𝑡) ∈ ℕ0)
440439faccld 13926 . . . . . . . . . . . . . 14 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
441440nncnd 11919 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
442438, 441syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
443419, 442fprodcl 15590 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
444443adantlr 711 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
445438, 440syl 17 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
446 nnne0 11937 . . . . . . . . . . . . 13 ((!‘((2nd𝑝)‘𝑡)) ∈ ℕ → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
447445, 446syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
448419, 442, 447fprodn0 15617 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
449448adantlr 711 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
450418, 444, 449divcld 11681 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) ∈ ℂ)
4517adantr 480 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
452 simpll 763 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝜑)
453452, 13sylancom 587 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑡𝑇)
454452, 133syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
455454, 438sseldd 3918 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑁))
456452, 453, 4553jca 1126 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
457 eleq1 2826 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → (𝑗 ∈ (0...𝑁) ↔ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
4584573anbi3d 1440 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁))))
459 fveq2 6756 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)))
460459feq1d 6569 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
461458, 460imbi12d 344 . . . . . . . . . . . . . 14 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)))
462461, 145vtoclg 3495 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
463438, 456, 462sylc 65 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
464463adantllr 715 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
46517adantlr 711 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑥𝑋)
466464, 465ffvelrnd 6944 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
467451, 466fprodcl 15590 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
468450, 467mulcld 10926 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) ∈ ℂ)
469 nfv 1918 . . . . . . . . . . . . 13 𝑘(𝐽 − (1st𝑝)) ∈ (0...𝐽)
470 simp1 1134 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
4714043adant1 1128 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
472 fznn0sub2 13292 . . . . . . . . . . . . . . . . 17 ((1st𝑝) ∈ (0...𝐽) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
473472adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (1st𝑝) ∈ (0...𝐽)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
474470, 471, 473syl2anc 583 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
4754743exp 1117 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
476475adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
477397, 469, 476rexlimd 3245 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽)))
478392, 477mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
479 simpl 482 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
480479, 23syl 17 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
481479, 133syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ⊆ (0...𝑁))
482481, 478sseldd 3918 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝑁))
483479, 480, 4823jca 1126 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
484 eleq1 2826 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → (𝑗 ∈ (0...𝑁) ↔ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
4854843anbi3d 1440 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁))))
486 fveq2 6756 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))))
487486feq1d 6569 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
488485, 487imbi12d 344 . . . . . . . . . . . 12 (𝑗 = (𝐽 − (1st𝑝)) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)))
489 simp2 1135 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → 𝑍𝑇)
490 id 22 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → (𝜑𝑍𝑇𝑗 ∈ (0...𝑁)))
491263anbi2d 1439 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑗 ∈ (0...𝑁))))
492179fveq1d 6758 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
493492feq1d 6569 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
494491, 493imbi12d 344 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
495494, 145vtoclg 3495 . . . . . . . . . . . . 13 (𝑍𝑇 → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
496489, 490, 495sylc 65 . . . . . . . . . . . 12 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
497488, 496vtoclg 3495 . . . . . . . . . . 11 ((𝐽 − (1st𝑝)) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
498478, 483, 497sylc 65 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
499498adantlr 711 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
50034adantr 480 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑥𝑋)
501499, 500ffvelrnd 6944 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) ∈ ℂ)
502468, 501mulcld 10926 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) ∈ ℂ)
503413, 502mulcld 10926 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) ∈ ℂ)
504337, 379, 382, 388, 503fsumf1o 15363 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
505 simpl 482 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝜑)
506366adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
507383, 506eleqtrd 2841 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
508374sseli 3913 . . . . . . . . . . . . . . 15 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
509507, 508syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
510 elmapi 8595 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
511509, 510syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
512 snidg 4592 . . . . . . . . . . . . . . . 16 (𝑍𝑇𝑍 ∈ {𝑍})
51323, 512syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑍 ∈ {𝑍})
514 elun2 4107 . . . . . . . . . . . . . . 15 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
515513, 514syl 17 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
516515adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
517511, 516ffvelrnd 6944 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
518 0zd 12261 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ∈ ℤ)
519124adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℤ)
520 fzssz 13187 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℤ
521520sseli 3913 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℤ)
522521adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℤ)
523519, 522zsubcld 12360 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
524 elfzle2 13189 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
525524adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ≤ 𝐽)
526163adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
527522zred 12355 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℝ)
528526, 527subge0d 11495 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
529525, 528mpbird 256 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
530 elfzle1 13188 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
531530adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝑐𝑍))
532526, 527subge02d 11497 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
533531, 532mpbid 231 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
534518, 519, 523, 529, 533elfzd 13176 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
535505, 517, 534syl2anc 583 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
536 bcval2 13947 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
537535, 536syl 17 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
538163recnd 10934 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℂ)
539538adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
540 zsscn 12257 . . . . . . . . . . . . . . . . 17 ℤ ⊆ ℂ
541520, 540sstri 3926 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℂ
542541a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
543542, 517sseldd 3918 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
544539, 543nncand 11267 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
545544fveq2d 6760 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝐽 − (𝑐𝑍)))) = (!‘(𝑐𝑍)))
546545oveq1d 7270 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍)))) = ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍)))))
547546oveq2d 7271 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
54845faccld 13926 . . . . . . . . . . . . . 14 (𝜑 → (!‘𝐽) ∈ ℕ)
549548nncnd 11919 . . . . . . . . . . . . 13 (𝜑 → (!‘𝐽) ∈ ℂ)
550549adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
551 elfznn0 13278 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℕ0)
552517, 551syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℕ0)
553552faccld 13926 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℕ)
554553nncnd 11919 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
555 elfznn0 13278 . . . . . . . . . . . . . . 15 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
556535, 555syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
557556faccld 13926 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℕ)
558557nncnd 11919 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
559553nnne0d 11953 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
560557nnne0d 11953 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
561550, 554, 558, 559, 560divdiv1d 11712 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
562561eqcomd 2744 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
563537, 547, 5623eqtrd 2782 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
564563adantlr 711 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
565 fvres 6775 . . . . . . . . . . . . . . . . 17 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
566565fveq2d 6760 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → (!‘((𝑐𝑅)‘𝑡)) = (!‘(𝑐𝑡)))
567566prodeq2i 15557 . . . . . . . . . . . . . . 15 𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡))
568567oveq2i 7266 . . . . . . . . . . . . . 14 ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡)))
569565fveq2d 6760 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
570569fveq1d 6758 . . . . . . . . . . . . . . 15 (𝑡𝑅 → (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
571570prodeq2i 15557 . . . . . . . . . . . . . 14 𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)
572568, 571oveq12i 7267 . . . . . . . . . . . . 13 (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
573572a1i 11 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
574573adantlr 711 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
575558adantlr 711 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
576505, 6syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
57775ssriv 3921 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℕ0
578577a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℕ0)
579511adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
580 elun1 4106 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑅𝑡 ∈ (𝑅 ∪ {𝑍}))
581580adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
582579, 581ffvelrnd 6944 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
583578, 582sseldd 3918 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
584583faccld 13926 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
585584nncnd 11919 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
586576, 585fprodcl 15590 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
587586adantlr 711 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
5887adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
589505adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝜑)
590505, 13sylan 579 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑇)
591589, 133syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
592591, 582sseldd 3918 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
593589, 590, 592, 146syl3anc 1369 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
594593adantllr 715 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
59517adantlr 711 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑥𝑋)
596594, 595ffvelrnd 6944 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
597588, 596fprodcl 15590 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
598576, 584fprodnncl 15593 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ)
599 nnne0 11937 . . . . . . . . . . . . . 14 (∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
600598, 599syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
601600adantlr 711 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
602575, 587, 597, 601div32d 11704 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
603574, 602eqtrd 2778 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
604544fveq2d 6760 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
605604fveq1d 6758 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
606605adantlr 711 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
607603, 606oveq12d 7273 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
608597, 587, 601divcld 11681 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
609505, 23syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
610505, 133syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ (0...𝑁))
611610, 517sseldd 3918 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝑁))
612505, 609, 6113jca 1126 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)))
613 eleq1 2826 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑍) ∈ (0...𝑁)))
6146133anbi3d 1440 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁))))
615 fveq2 6756 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
616615feq1d 6569 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
617614, 616imbi12d 344 . . . . . . . . . . . . . 14 (𝑗 = (𝑐𝑍) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)))
618617, 496vtoclg 3495 . . . . . . . . . . . . 13 ((𝑐𝑍) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
619517, 612, 618sylc 65 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
620619adantlr 711 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
62134adantr 480 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑥𝑋)
622620, 621ffvelrnd 6944 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥) ∈ ℂ)
623575, 608, 622mulassd 10929 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
624607, 623eqtrd 2778 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
625564, 624oveq12d 7273 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))))
626549ad2antrr 722 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
627554adantlr 711 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
628559adantlr 711 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
629626, 627, 628divcld 11681 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / (!‘(𝑐𝑍))) ∈ ℂ)
630608, 622mulcld 10926 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) ∈ ℂ)
631560adantlr 711 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
632629, 575, 630, 631dmmcand 42742 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
633597, 622, 587, 601div23d 11718 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
634633eqcomd 2744 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
635 nfv 1918 . . . . . . . . . . . . 13 𝑡((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
636 nfcv 2906 . . . . . . . . . . . . 13 𝑡(((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)
637609adantlr 711 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
63811adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
639 fveq2 6756 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑐𝑡) = (𝑐𝑍))
640179, 639fveq12d 6763 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
641640fveq1d 6758 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
642635, 636, 588, 637, 638, 596, 641, 622fprodsplitsn 15627 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
643642eqcomd 2744 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
644643oveq1d 7270 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
645634, 644eqtrd 2778 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
646645oveq2d 7271 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
647588, 368, 370sylancl 585 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
648505adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝜑)
649347sselda 3917 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
650649adantlr 711 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
651511, 610fssd 6602 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝑁))
652651ffvelrnda 6943 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝑁))
653648, 650, 652, 146syl3anc 1369 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
654653adantllr 715 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
655621adantr 480 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑥𝑋)
656654, 655ffvelrnd 6944 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
657647, 656fprodcl 15590 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
658626, 627, 657, 587, 628, 601divmuldivd 11722 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))))
659554, 586mulcomd 10927 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
660 nfv 1918 . . . . . . . . . . . . . 14 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
661 nfcv 2906 . . . . . . . . . . . . . 14 𝑡(!‘(𝑐𝑍))
662505, 10syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
663639fveq2d 6760 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑍)))
664660, 661, 576, 609, 662, 585, 663, 554fprodsplitsn 15627 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
665664eqcomd 2744 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
666659, 665eqtrd 2778 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
667666oveq2d 7271 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
668667adantlr 711 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
669505, 371syl 17 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
670577a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0...𝐽) ⊆ ℕ0)
671511ffvelrnda 6943 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝐽))
672670, 671sseldd 3918 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ ℕ0)
673672faccld 13926 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℕ)
674673nncnd 11919 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℂ)
675669, 674fprodcl 15590 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
676675adantlr 711 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
677673nnne0d 11953 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ≠ 0)
678669, 674, 677fprodn0 15617 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
679678adantlr 711 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
680626, 657, 676, 679div23d 11718 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
681 eqidd 2739 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
682668, 680, 6813eqtrd 2782 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
683646, 658, 6823eqtrd 2782 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
684625, 632, 6833eqtrd 2782 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
685684sumeq2dv 15343 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
686504, 685eqtrd 2778 . . . 4 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
687294, 318, 6863eqtrd 2782 . . 3 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
688687mpteq2dva 5170 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
68939, 209, 6883eqtrd 2782 1 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1085   = wceq 1539  wcel 2108  wne 2942  wral 3063  wrex 3064  {crab 3067  Vcvv 3422  cdif 3880  cun 3881  wss 3883  𝒫 cpw 4530  {csn 4558  {cpr 4560  cop 4564   ciun 4921   class class class wbr 5070  cmpt 5153   × cxp 5578  cres 5582  wf 6414  1-1-ontowf1o 6417  cfv 6418  (class class class)co 7255  1st c1st 7802  2nd c2nd 7803  m cmap 8573  Fincfn 8691  cc 10800  cr 10801  0cc0 10802   · cmul 10807  cle 10941  cmin 11135   / cdiv 11562  cn 11903  0cn0 12163  cz 12249  cuz 12511  ...cfz 13168  !cfa 13915  Ccbc 13944  Σcsu 15325  cprod 15543  t crest 17048  TopOpenctopn 17049  fldccnfld 20510   D𝑛 cdvn 24933
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880  ax-addf 10881  ax-mulf 10882
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-iin 4924  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-of 7511  df-om 7688  df-1st 7804  df-2nd 7805  df-supp 7949  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-2o 8268  df-er 8456  df-map 8575  df-pm 8576  df-ixp 8644  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-fsupp 9059  df-fi 9100  df-sup 9131  df-inf 9132  df-oi 9199  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971  df-8 11972  df-9 11973  df-n0 12164  df-z 12250  df-dec 12367  df-uz 12512  df-q 12618  df-rp 12660  df-xneg 12777  df-xadd 12778  df-xmul 12779  df-ico 13014  df-icc 13015  df-fz 13169  df-fzo 13312  df-seq 13650  df-exp 13711  df-fac 13916  df-bc 13945  df-hash 13973  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-clim 15125  df-sum 15326  df-prod 15544  df-struct 16776  df-sets 16793  df-slot 16811  df-ndx 16823  df-base 16841  df-ress 16868  df-plusg 16901  df-mulr 16902  df-starv 16903  df-sca 16904  df-vsca 16905  df-ip 16906  df-tset 16907  df-ple 16908  df-ds 16910  df-unif 16911  df-hom 16912  df-cco 16913  df-rest 17050  df-topn 17051  df-0g 17069  df-gsum 17070  df-topgen 17071  df-pt 17072  df-prds 17075  df-xrs 17130  df-qtop 17135  df-imas 17136  df-xps 17138  df-mre 17212  df-mrc 17213  df-acs 17215  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-submnd 18346  df-mulg 18616  df-cntz 18838  df-cmn 19303  df-psmet 20502  df-xmet 20503  df-met 20504  df-bl 20505  df-mopn 20506  df-fbas 20507  df-fg 20508  df-cnfld 20511  df-top 21951  df-topon 21968  df-topsp 21990  df-bases 22004  df-cld 22078  df-ntr 22079  df-cls 22080  df-nei 22157  df-lp 22195  df-perf 22196  df-cn 22286  df-cnp 22287  df-haus 22374  df-tx 22621  df-hmeo 22814  df-fil 22905  df-fm 22997  df-flim 22998  df-flf 22999  df-xms 23381  df-ms 23382  df-tms 23383  df-cncf 23947  df-limc 24935  df-dv 24936  df-dvn 24937
This theorem is referenced by:  dvnprodlem3  43379
  Copyright terms: Public domain W3C validator