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 45948
Description: Induction step for dvnprodlem2 45948. (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 1914 . . . . . 6 𝑡(𝜑𝑥𝑋)
2 nfcv 2891 . . . . . 6 𝑡((𝐻𝑍)‘𝑥)
3 dvnprodlem2.t . . . . . . . 8 (𝜑𝑇 ∈ Fin)
4 dvnprodlem2.r . . . . . . . 8 (𝜑𝑅𝑇)
5 ssfi 9087 . . . . . . . 8 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
63, 4, 5syl2anc 584 . . . . . . 7 (𝜑𝑅 ∈ Fin)
76adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝑅 ∈ Fin)
8 dvnprodlem2.z . . . . . . 7 (𝜑𝑍 ∈ (𝑇𝑅))
98adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝑍 ∈ (𝑇𝑅))
108eldifbd 3916 . . . . . . 7 (𝜑 → ¬ 𝑍𝑅)
1110adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → ¬ 𝑍𝑅)
12 simpl 482 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝜑)
134sselda 3935 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝑡𝑇)
14 dvnprodlem2.h . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
1512, 13, 14syl2anc 584 . . . . . . . 8 ((𝜑𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
1615adantlr 715 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
17 simplr 768 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → 𝑥𝑋)
1816, 17ffvelcdmd 7019 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → ((𝐻𝑡)‘𝑥) ∈ ℂ)
19 fveq2 6822 . . . . . . 7 (𝑡 = 𝑍 → (𝐻𝑡) = (𝐻𝑍))
2019fveq1d 6824 . . . . . 6 (𝑡 = 𝑍 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑍)‘𝑥))
21 id 22 . . . . . . . . 9 (𝜑𝜑)
22 eldifi 4082 . . . . . . . . . 10 (𝑍 ∈ (𝑇𝑅) → 𝑍𝑇)
238, 22syl 17 . . . . . . . . 9 (𝜑𝑍𝑇)
24 simpr 484 . . . . . . . . . 10 ((𝜑𝑍𝑇) → 𝑍𝑇)
25 id 22 . . . . . . . . . 10 ((𝜑𝑍𝑇) → (𝜑𝑍𝑇))
26 eleq1 2816 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (𝑡𝑇𝑍𝑇))
2726anbi2d 630 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝜑𝑡𝑇) ↔ (𝜑𝑍𝑇)))
2819feq1d 6634 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝐻𝑡):𝑋⟶ℂ ↔ (𝐻𝑍):𝑋⟶ℂ))
2927, 28imbi12d 344 . . . . . . . . . . 11 (𝑡 = 𝑍 → (((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)))
3029, 14vtoclg 3509 . . . . . . . . . 10 (𝑍𝑇 → ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ))
3124, 25, 30sylc 65 . . . . . . . . 9 ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)
3221, 23, 31syl2anc 584 . . . . . . . 8 (𝜑 → (𝐻𝑍):𝑋⟶ℂ)
3332adantr 480 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐻𝑍):𝑋⟶ℂ)
34 simpr 484 . . . . . . 7 ((𝜑𝑥𝑋) → 𝑥𝑋)
3533, 34ffvelcdmd 7019 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐻𝑍)‘𝑥) ∈ ℂ)
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 15896 . . . . 5 ((𝜑𝑥𝑋) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥) = (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))
3736mpteq2dva 5185 . . . 4 (𝜑 → (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))
3837oveq2d 7365 . . 3 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))))
3938fveq1d 6824 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽))
40 dvnprodlem2.s . . 3 (𝜑𝑆 ∈ {ℝ, ℂ})
41 dvnprodlem2.x . . 3 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
421, 7, 18fprodclf 15899 . . 3 ((𝜑𝑥𝑋) → ∏𝑡𝑅 ((𝐻𝑡)‘𝑥) ∈ ℂ)
43 dvnprodlem2.j . . . 4 (𝜑𝐽 ∈ (0...𝑁))
44 elfznn0 13523 . . . 4 (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℕ0)
4543, 44syl 17 . . 3 (𝜑𝐽 ∈ ℕ0)
46 eqid 2729 . . 3 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
47 eqid 2729 . . 3 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
48 dvnprodlem2.c . . . . . . . . . 10 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
49 oveq2 7357 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅))
50 rabeq 3409 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
5149, 50syl 17 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
52 sumeq1 15596 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
5352eqeq1d 2731 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
5453rabbidv 3402 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5551, 54eqtrd 2764 . . . . . . . . . . 11 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5655mpteq2dv 5186 . . . . . . . . . 10 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
57 ssexg 5262 . . . . . . . . . . . . . 14 ((𝑅𝑇𝑇 ∈ Fin) → 𝑅 ∈ V)
584, 3, 57syl2anc 584 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ V)
59 elpwg 4554 . . . . . . . . . . . . 13 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
614, 60mpbird 257 . . . . . . . . . . 11 (𝜑𝑅 ∈ 𝒫 𝑇)
6261adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑅 ∈ 𝒫 𝑇)
63 nn0ex 12390 . . . . . . . . . . . 12 0 ∈ V
6463mptex 7159 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
6564a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
6648, 56, 62, 65fvmptd3 6953 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
67 oveq2 7357 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
6867oveq1d 7364 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅))
69 rabeq 3409 . . . . . . . . . . . 12 (((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
7068, 69syl 17 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
71 eqeq2 2741 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
7271rabbidv 3402 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7370, 72eqtrd 2764 . . . . . . . . . 10 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7473adantl 481 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
75 elfznn0 13523 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
7675adantl 481 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
77 fzfid 13880 . . . . . . . . . . . 12 (𝜑 → (0...𝑘) ∈ Fin)
78 mapfi 9238 . . . . . . . . . . . 12 (((0...𝑘) ∈ Fin ∧ 𝑅 ∈ Fin) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
7977, 6, 78syl2anc 584 . . . . . . . . . . 11 (𝜑 → ((0...𝑘) ↑m 𝑅) ∈ Fin)
8079adantr 480 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
81 ssrab2 4031 . . . . . . . . . . 11 {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)
8281a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅))
8380, 82ssexd 5263 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
8466, 74, 76, 83fvmptd 6937 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
85 ssfi 9087 . . . . . . . . . 10 ((((0...𝑘) ↑m 𝑅) ∈ Fin ∧ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8679, 81, 85sylancl 586 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8786adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8884, 87eqeltrd 2828 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
8988adantr 480 . . . . . 6 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → ((𝐶𝑅)‘𝑘) ∈ Fin)
9075faccld 14191 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℕ)
9190nncnd 12144 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℂ)
9291ad2antlr 727 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (!‘𝑘) ∈ ℂ)
936adantr 480 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
9493adantlr 715 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
95 elfznn0 13523 . . . . . . . . . . . . . . 15 (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0)
9695ssriv 3939 . . . . . . . . . . . . . 14 (0...𝑘) ⊆ ℕ0
9796a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℕ0)
98 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((𝐶𝑅)‘𝑘))
9984eleq2d 2814 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10099adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10198, 100mpbid 232 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
10281sseli 3931 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
104 elmapi 8776 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ((0...𝑘) ↑m 𝑅) → 𝑐:𝑅⟶(0...𝑘))
105103, 104syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐:𝑅⟶(0...𝑘))
106105adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑐:𝑅⟶(0...𝑘))
107 simpr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑅)
108106, 107ffvelcdmd 7019 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑘))
10997, 108sseldd 3936 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
110109faccld 14191 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
111110nncnd 12144 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
11294, 111fprodcl 15859 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
113110nnne0d 12178 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ≠ 0)
11494, 111, 113fprodn0 15886 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
11592, 112, 114divcld 11900 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
116115adantlr 715 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
11794adantlr 715 . . . . . . . 8 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
11821ad4antr 732 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝜑)
119118, 13sylancom 588 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑇)
120 elfzuz3 13424 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ (ℤ𝑘))
121 fzss2 13467 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (ℤ𝑘) → (0...𝑘) ⊆ (0...𝐽))
122120, 121syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0...𝑘) ⊆ (0...𝐽))
123122adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝐽))
12445nn0zd 12497 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽 ∈ ℤ)
125 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
126125nn0zd 12497 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℤ)
127 elfzle2 13431 . . . . . . . . . . . . . . . . . . 19 (𝐽 ∈ (0...𝑁) → 𝐽𝑁)
12843, 127syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽𝑁)
129124, 126, 1283jca 1128 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
130 eluz2 12741 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝐽) ↔ (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
131129, 130sylibr 234 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝐽))
132 fzss2 13467 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐽) → (0...𝐽) ⊆ (0...𝑁))
133131, 132syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝐽) ⊆ (0...𝑁))
134133adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝐽) ⊆ (0...𝑁))
135123, 134sstrd 3946 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝑁))
136135ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ (0...𝑁))
137136, 108sseldd 3936 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
138137adantllr 719 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
139 fvex 6835 . . . . . . . . . . 11 (𝑐𝑡) ∈ V
140 eleq1 2816 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑡) ∈ (0...𝑁)))
1411403anbi3d 1444 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁))))
142 fveq2 6822 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
143142feq1d 6634 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ))
144141, 143imbi12d 344 . . . . . . . . . . 11 (𝑗 = (𝑐𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)))
145 dvnprodlem2.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
146139, 144, 145vtocl 3513 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
147118, 119, 138, 146syl3anc 1373 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
148 simpllr 775 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑥𝑋)
149147, 148ffvelcdmd 7019 . . . . . . . 8 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
150117, 149fprodcl 15859 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
151116, 150mulcld 11135 . . . . . 6 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
15289, 151fsumcl 15640 . . . . 5 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
153152fmpttd 7049 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ)
154 dvnprodlem2.ind . . . . . . 7 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
155154adantr 480 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
156 0zd 12483 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ∈ ℤ)
157126adantr 480 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℤ)
158 elfzelz 13427 . . . . . . . 8 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
159158adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
160 elfzle1 13430 . . . . . . . 8 (𝑘 ∈ (0...𝐽) → 0 ≤ 𝑘)
161160adantl 481 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
162159zred 12580 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
16345nn0red 12446 . . . . . . . . 9 (𝜑𝐽 ∈ ℝ)
164163adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
165157zred 12580 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℝ)
166 elfzle2 13431 . . . . . . . . 9 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
167166adantl 481 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
168128adantr 480 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽𝑁)
169162, 164, 165, 167, 168letrd 11273 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝑁)
170156, 157, 159, 161, 169elfzd 13418 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ (0...𝑁))
171 rspa 3218 . . . . . 6 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
172155, 170, 171syl2anc 584 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
173172feq1d 6634 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ))
174153, 173mpbird 257 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ)
17523adantr 480 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑍𝑇)
176 simpl 482 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝜑)
177176, 175, 1703jca 1128 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → (𝜑𝑍𝑇𝑘 ∈ (0...𝑁)))
178263anbi2d 1443 . . . . . . 7 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑘 ∈ (0...𝑁))))
17919oveq2d 7365 . . . . . . . . 9 (𝑡 = 𝑍 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑍)))
180179fveq1d 6824 . . . . . . . 8 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
181180feq1d 6634 . . . . . . 7 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
182178, 181imbi12d 344 . . . . . 6 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)))
183 eleq1 2816 . . . . . . . . 9 (𝑗 = 𝑘 → (𝑗 ∈ (0...𝑁) ↔ 𝑘 ∈ (0...𝑁)))
1841833anbi3d 1444 . . . . . . . 8 (𝑗 = 𝑘 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇𝑘 ∈ (0...𝑁))))
185 fveq2 6822 . . . . . . . . 9 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘𝑘))
186185feq1d 6634 . . . . . . . 8 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ))
187184, 186imbi12d 344 . . . . . . 7 (𝑗 = 𝑘 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)))
188187, 145chvarvv 1989 . . . . . 6 ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)
189182, 188vtoclg 3509 . . . . 5 (𝑍𝑇 → ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
190175, 177, 189sylc 65 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)
19132feqmptd 6891 . . . . . . . . 9 (𝜑 → (𝐻𝑍) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
192191eqcomd 2735 . . . . . . . 8 (𝜑 → (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝐻𝑍))
193192oveq2d 7365 . . . . . . 7 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))) = (𝑆 D𝑛 (𝐻𝑍)))
194193fveq1d 6824 . . . . . 6 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
195194adantr 480 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
196195feq1d 6634 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
197190, 196mpbird 257 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ)
198 fveq2 6822 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑡)‘𝑥))
199198prodeq2ad 45593 . . . . . . 7 (𝑦 = 𝑥 → ∏𝑡𝑅 ((𝐻𝑡)‘𝑦) = ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
200199cbvmptv 5196 . . . . . 6 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
201200oveq2i 7360 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))
202201fveq1i 6823 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘)
203202mpteq2i 5188 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
204 fveq2 6822 . . . . . . 7 (𝑦 = 𝑥 → ((𝐻𝑍)‘𝑦) = ((𝐻𝑍)‘𝑥))
205204cbvmptv 5196 . . . . . 6 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
206205oveq2i 7360 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
207206fveq1i 6823 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘)
208207mpteq2i 5188 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘))
20940, 41, 42, 35, 45, 46, 47, 174, 197, 203, 208dvnmul 45944 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽) = (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))))
210202a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
211154r19.21bi 3221 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
212176, 170, 211syl2anc 584 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
213210, 212eqtrd 2764 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
214213mpteq2dva 5185 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
215 mptexg 7157 . . . . . . . . . . . . . 14 (𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
21641, 215syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
217216adantr 480 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
218214, 217fvmpt2d 6943 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
219218adantlr 715 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
220219fveq1d 6824 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥))
22134adantr 480 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → 𝑥𝑋)
222152an32s 652 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
223 eqid 2729 . . . . . . . . . . 11 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
224223fvmpt2 6941 . . . . . . . . . 10 ((𝑥𝑋 ∧ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
225221, 222, 224syl2anc 584 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
226220, 225eqtrd 2764 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
227 fveq2 6822 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
228227cbvmptv 5196 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
229228a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)))
230206, 193eqtrid 2776 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝐻𝑍)))
231230fveq1d 6824 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
232231mpteq2dv 5186 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
233229, 232eqtrd 2764 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
234233adantr 480 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
235 fveq2 6822 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
236235adantl 481 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑗 = (𝐽𝑘)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
237 0zd 12483 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 0 ∈ ℤ)
238 elfzel2 13425 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
239238, 158zsubcld 12585 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ∈ ℤ)
240237, 238, 2393jca 1128 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ))
241238zred 12580 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
24275nn0red 12446 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
243241, 242subge0d 11710 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
244166, 243mpbird 257 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
245241, 242subge02d 11712 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
246160, 245mpbid 232 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ≤ 𝐽)
247240, 244, 246jca32 515 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝐽) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
248247adantl 481 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
249 elfz2 13417 . . . . . . . . . . . 12 ((𝐽𝑘) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
250248, 249sylibr 234 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ∈ (0...𝐽))
251 fvex 6835 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V
252251a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V)
253234, 236, 250, 252fvmptd 6937 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
254253adantlr 715 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
255254fveq1d 6824 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
256226, 255oveq12d 7367 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)) = (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
257256oveq2d 7365 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
25888adantlr 715 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
259 ovex 7382 . . . . . . . . . . . 12 (𝐽𝑘) ∈ V
260 eleq1 2816 . . . . . . . . . . . . . 14 (𝑗 = (𝐽𝑘) → (𝑗 ∈ (0...𝐽) ↔ (𝐽𝑘) ∈ (0...𝐽)))
261260anbi2d 630 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → ((𝜑𝑗 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽))))
262235feq1d 6634 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ))
263261, 262imbi12d 344 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → (((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)))
264 eleq1 2816 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ (0...𝐽) ↔ 𝑗 ∈ (0...𝐽)))
265264anbi2d 630 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ (0...𝐽)) ↔ (𝜑𝑗 ∈ (0...𝐽))))
266 fveq2 6822 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
267266feq1d 6634 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
268265, 267imbi12d 344 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
269268, 190chvarvv 1989 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
270259, 263, 269vtocl 3513 . . . . . . . . . . 11 ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
271176, 250, 270syl2anc 584 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
272271adantlr 715 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
273272, 221ffvelcdmd 7019 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
274 anass 468 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ (𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)))
275 ancom 460 . . . . . . . . . . . . . 14 ((𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋) ↔ (𝑥𝑋𝑘 ∈ (0...𝐽)))
276275anbi2i 623 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
277 anass 468 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
278277bicomi 224 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
279276, 278bitri 275 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
280274, 279bitri 275 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
281280anbi1i 624 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ↔ (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)))
282281imbi1i 349 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) ↔ ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ))
283151, 282mpbi 230 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
284258, 273, 283fsummulc1 15692 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
285284oveq2d 7365 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
286176, 45syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℕ0)
287286, 159bccld 45317 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℕ0)
288287nn0cnd 12447 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
289288adantlr 715 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
290273adantr 480 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
291283, 290mulcld 11135 . . . . . . 7 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
292258, 289, 291fsummulc2 15691 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
293257, 285, 2923eqtrd 2768 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
294293sumeq2dv 15609 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
295 vex 3440 . . . . . . . 8 𝑘 ∈ V
296 vex 3440 . . . . . . . 8 𝑐 ∈ V
297295, 296op1std 7934 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (1st𝑝) = 𝑘)
298297oveq2d 7365 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽C(1st𝑝)) = (𝐽C𝑘))
299297fveq2d 6826 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘(1st𝑝)) = (!‘𝑘))
300295, 296op2ndd 7935 . . . . . . . . . . . 12 (𝑝 = ⟨𝑘, 𝑐⟩ → (2nd𝑝) = 𝑐)
301300fveq1d 6824 . . . . . . . . . . 11 (𝑝 = ⟨𝑘, 𝑐⟩ → ((2nd𝑝)‘𝑡) = (𝑐𝑡))
302301fveq2d 6826 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘(𝑐𝑡)))
303302prodeq2ad 45593 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡)))
304299, 303oveq12d 7367 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
305301fveq2d 6826 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
306305fveq1d 6824 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
307306prodeq2ad 45593 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
308304, 307oveq12d 7367 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
309297oveq2d 7365 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽 − (1st𝑝)) = (𝐽𝑘))
310309fveq2d 6826 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
311310fveq1d 6824 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
312308, 311oveq12d 7367 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
313298, 312oveq12d 7367 . . . . 5 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
314 fzfid 13880 . . . . 5 ((𝜑𝑥𝑋) → (0...𝐽) ∈ Fin)
315289adantrr 717 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → (𝐽C𝑘) ∈ ℂ)
316291anasss 466 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
317315, 316mulcld 11135 . . . . 5 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) ∈ ℂ)
318313, 314, 258, 317fsum2d 15678 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))))
319 ovex 7382 . . . . . . . . 9 (𝐽 − (𝑐𝑍)) ∈ V
320296resex 5980 . . . . . . . . 9 (𝑐𝑅) ∈ V
321319, 320op1std 7934 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (1st𝑝) = (𝐽 − (𝑐𝑍)))
322321oveq2d 7365 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽C(1st𝑝)) = (𝐽C(𝐽 − (𝑐𝑍))))
323321fveq2d 6826 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘(1st𝑝)) = (!‘(𝐽 − (𝑐𝑍))))
324319, 320op2ndd 7935 . . . . . . . . . . . . 13 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (2nd𝑝) = (𝑐𝑅))
325324fveq1d 6824 . . . . . . . . . . . 12 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((2nd𝑝)‘𝑡) = ((𝑐𝑅)‘𝑡))
326325fveq2d 6826 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘((𝑐𝑅)‘𝑡)))
327326prodeq2ad 45593 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)))
328323, 327oveq12d 7367 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))))
329325fveq2d 6826 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)))
330329fveq1d 6824 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
331330prodeq2ad 45593 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
332328, 331oveq12d 7367 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)))
333321oveq2d 7365 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽 − (1st𝑝)) = (𝐽 − (𝐽 − (𝑐𝑍))))
334333fveq2d 6826 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))))
335334fveq1d 6824 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))
336332, 335oveq12d 7367 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)))
337322, 336oveq12d 7367 . . . . . 6 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
338 oveq2 7357 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})))
339 rabeq 3409 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
340338, 339syl 17 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
341 sumeq1 15596 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
342341eqeq1d 2731 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
343342rabbidv 3402 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
344340, 343eqtrd 2764 . . . . . . . . . . 11 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
345344mpteq2dv 5186 . . . . . . . . . 10 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
34623snssd 4760 . . . . . . . . . . . 12 (𝜑 → {𝑍} ⊆ 𝑇)
3474, 346unssd 4143 . . . . . . . . . . 11 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
3483, 347ssexd 5263 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
349 elpwg 4554 . . . . . . . . . . . 12 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
350348, 349syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
351347, 350mpbird 257 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
35263mptex 7159 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
353352a1i 11 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
35448, 345, 351, 353fvmptd3 6953 . . . . . . . . 9 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
355 oveq2 7357 . . . . . . . . . . . . 13 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
356355oveq1d 7364 . . . . . . . . . . . 12 (𝑛 = 𝐽 → ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
357 rabeq 3409 . . . . . . . . . . . 12 (((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
358356, 357syl 17 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
359 eqeq2 2741 . . . . . . . . . . . 12 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
360359rabbidv 3402 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
361358, 360eqtrd 2764 . . . . . . . . . 10 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
362361adantl 481 . . . . . . . . 9 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
363 ovex 7382 . . . . . . . . . . 11 ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ V
364363rabex 5278 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
365364a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
366354, 362, 45, 365fvmptd 6937 . . . . . . . 8 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
367 fzfid 13880 . . . . . . . . . 10 (𝜑 → (0...𝐽) ∈ Fin)
368 snfi 8968 . . . . . . . . . . . 12 {𝑍} ∈ Fin
369368a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑍} ∈ Fin)
370 unfi 9085 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ Fin)
3716, 369, 370syl2anc 584 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ Fin)
372 mapfi 9238 . . . . . . . . . 10 (((0...𝐽) ∈ Fin ∧ (𝑅 ∪ {𝑍}) ∈ Fin) → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
373367, 371, 372syl2anc 584 . . . . . . . . 9 (𝜑 → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
374 ssrab2 4031 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))
375374a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
376 ssfi 9087 . . . . . . . . 9 ((((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin ∧ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))) → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
377373, 375, 376syl2anc 584 . . . . . . . 8 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
378366, 377eqeltrd 2828 . . . . . . 7 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
379378adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
380 dvnprodlem2.d . . . . . . . 8 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38148, 45, 380, 3, 23, 10, 347dvnprodlem1 45947 . . . . . . 7 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
382381adantr 480 . . . . . 6 ((𝜑𝑥𝑋) → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
383 simpr 484 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
384 opex 5407 . . . . . . . . 9 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
385384a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
386380fvmpt2 6941 . . . . . . . 8 ((𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
387383, 385, 386syl2anc 584 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
388387adantlr 715 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38945adantr 480 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℕ0)
390 eliun 4945 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
391390biimpi 216 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
392391adantl 481 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
393 nfv 1914 . . . . . . . . . . . . . 14 𝑘𝜑
394 nfcv 2891 . . . . . . . . . . . . . . 15 𝑘𝑝
395 nfiu1 4977 . . . . . . . . . . . . . . 15 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
396394, 395nfel 2906 . . . . . . . . . . . . . 14 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
397393, 396nfan 1899 . . . . . . . . . . . . 13 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
398 nfv 1914 . . . . . . . . . . . . 13 𝑘(1st𝑝) ∈ (0...𝐽)
399 xp1st 7956 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
400 elsni 4594 . . . . . . . . . . . . . . . . . 18 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
401399, 400syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
402401adantl 481 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
403 simpl 482 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
404402, 403eqeltrd 2828 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
405404ex 412 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
406405a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
407397, 398, 406rexlimd 3236 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
408392, 407mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
409 elfzelz 13427 . . . . . . . . . . 11 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
410408, 409syl 17 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
411389, 410bccld 45317 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℕ0)
412411nn0cnd 12447 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
413412adantlr 715 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
414 elfznn0 13523 . . . . . . . . . . . . . 14 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℕ0)
415408, 414syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℕ0)
416415faccld 14191 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℕ)
417416nncnd 12144 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
418417adantlr 715 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
4196adantr 480 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
420 nfv 1914 . . . . . . . . . . . . . . . 16 𝑘(2nd𝑝):𝑅⟶(0...𝐽)
42184, 82eqsstrd 3970 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝑘) ↑m 𝑅))
422 ovex 7382 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0...𝐽) ∈ V
423422a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0...𝐽) ∈ V)
424 mapss 8816 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝐽) ∈ V ∧ (0...𝑘) ⊆ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
425423, 122, 424syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
426425adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
427421, 426sstrd 3946 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
4284273adant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
429 xp2nd 7957 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4304293ad2ant3 1135 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
431428, 430sseldd 3936 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅))
432 elmapi 8776 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅) → (2nd𝑝):𝑅⟶(0...𝐽))
433431, 432syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
4344333exp 1119 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
435434adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
436397, 420, 435rexlimd 3236 . . . . . . . . . . . . . . 15 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽)))
437392, 436mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
438437ffvelcdmda 7018 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝐽))
439 elfznn0 13523 . . . . . . . . . . . . . . 15 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((2nd𝑝)‘𝑡) ∈ ℕ0)
440439faccld 14191 . . . . . . . . . . . . . 14 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
441440nncnd 12144 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
442438, 441syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
443419, 442fprodcl 15859 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
444443adantlr 715 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
445438, 440syl 17 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
446 nnne0 12162 . . . . . . . . . . . . 13 ((!‘((2nd𝑝)‘𝑡)) ∈ ℕ → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
447445, 446syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
448419, 442, 447fprodn0 15886 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
449448adantlr 715 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
450418, 444, 449divcld 11900 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) ∈ ℂ)
4517adantr 480 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
452 simpll 766 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝜑)
453452, 13sylancom 588 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑡𝑇)
454452, 133syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
455454, 438sseldd 3936 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑁))
456452, 453, 4553jca 1128 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
457 eleq1 2816 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → (𝑗 ∈ (0...𝑁) ↔ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
4584573anbi3d 1444 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁))))
459 fveq2 6822 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)))
460459feq1d 6634 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
461458, 460imbi12d 344 . . . . . . . . . . . . . 14 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)))
462461, 145vtoclg 3509 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
463438, 456, 462sylc 65 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
464463adantllr 719 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
46517adantlr 715 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑥𝑋)
466464, 465ffvelcdmd 7019 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
467451, 466fprodcl 15859 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
468450, 467mulcld 11135 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) ∈ ℂ)
469 nfv 1914 . . . . . . . . . . . . 13 𝑘(𝐽 − (1st𝑝)) ∈ (0...𝐽)
470 simp1 1136 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
4714043adant1 1130 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
472 fznn0sub2 13538 . . . . . . . . . . . . . . . . 17 ((1st𝑝) ∈ (0...𝐽) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
473472adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (1st𝑝) ∈ (0...𝐽)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
474470, 471, 473syl2anc 584 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
4754743exp 1119 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
476475adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
477397, 469, 476rexlimd 3236 . . . . . . . . . . . 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 3936 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝑁))
483479, 480, 4823jca 1128 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
484 eleq1 2816 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → (𝑗 ∈ (0...𝑁) ↔ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
4854843anbi3d 1444 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁))))
486 fveq2 6822 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))))
487486feq1d 6634 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
488485, 487imbi12d 344 . . . . . . . . . . . 12 (𝑗 = (𝐽 − (1st𝑝)) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)))
489 simp2 1137 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → 𝑍𝑇)
490 id 22 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → (𝜑𝑍𝑇𝑗 ∈ (0...𝑁)))
491263anbi2d 1443 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑗 ∈ (0...𝑁))))
492179fveq1d 6824 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
493492feq1d 6634 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
494491, 493imbi12d 344 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
495494, 145vtoclg 3509 . . . . . . . . . . . . 13 (𝑍𝑇 → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
496489, 490, 495sylc 65 . . . . . . . . . . . 12 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
497488, 496vtoclg 3509 . . . . . . . . . . 11 ((𝐽 − (1st𝑝)) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
498478, 483, 497sylc 65 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
499498adantlr 715 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
50034adantr 480 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑥𝑋)
501499, 500ffvelcdmd 7019 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) ∈ ℂ)
502468, 501mulcld 11135 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) ∈ ℂ)
503413, 502mulcld 11135 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) ∈ ℂ)
504337, 379, 382, 388, 503fsumf1o 15630 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
505 simpl 482 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝜑)
506366adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
507383, 506eleqtrd 2830 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
508374sseli 3931 . . . . . . . . . . . . . . 15 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
509507, 508syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
510 elmapi 8776 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
511509, 510syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
512 snidg 4612 . . . . . . . . . . . . . . . 16 (𝑍𝑇𝑍 ∈ {𝑍})
51323, 512syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑍 ∈ {𝑍})
514 elun2 4134 . . . . . . . . . . . . . . 15 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
515513, 514syl 17 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
516515adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
517511, 516ffvelcdmd 7019 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
518 0zd 12483 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ∈ ℤ)
519124adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℤ)
520 fzssz 13429 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℤ
521520sseli 3931 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℤ)
522521adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℤ)
523519, 522zsubcld 12585 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
524 elfzle2 13431 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
525524adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ≤ 𝐽)
526163adantr 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
527522zred 12580 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℝ)
528526, 527subge0d 11710 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
529525, 528mpbird 257 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
530 elfzle1 13430 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
531530adantl 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝑐𝑍))
532526, 527subge02d 11712 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
533531, 532mpbid 232 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
534518, 519, 523, 529, 533elfzd 13418 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
535505, 517, 534syl2anc 584 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
536 bcval2 14212 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
537535, 536syl 17 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
538163recnd 11143 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℂ)
539538adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
540 zsscn 12479 . . . . . . . . . . . . . . . . 17 ℤ ⊆ ℂ
541520, 540sstri 3945 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℂ
542541a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
543542, 517sseldd 3936 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
544539, 543nncand 11480 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
545544fveq2d 6826 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝐽 − (𝑐𝑍)))) = (!‘(𝑐𝑍)))
546545oveq1d 7364 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍)))) = ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍)))))
547546oveq2d 7365 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
54845faccld 14191 . . . . . . . . . . . . . 14 (𝜑 → (!‘𝐽) ∈ ℕ)
549548nncnd 12144 . . . . . . . . . . . . 13 (𝜑 → (!‘𝐽) ∈ ℂ)
550549adantr 480 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
551 elfznn0 13523 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℕ0)
552517, 551syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℕ0)
553552faccld 14191 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℕ)
554553nncnd 12144 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
555 elfznn0 13523 . . . . . . . . . . . . . . 15 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
556535, 555syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
557556faccld 14191 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℕ)
558557nncnd 12144 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
559553nnne0d 12178 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
560557nnne0d 12178 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
561550, 554, 558, 559, 560divdiv1d 11931 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
562561eqcomd 2735 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
563537, 547, 5623eqtrd 2768 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
564563adantlr 715 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
565 fvres 6841 . . . . . . . . . . . . . . . . 17 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
566565fveq2d 6826 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → (!‘((𝑐𝑅)‘𝑡)) = (!‘(𝑐𝑡)))
567566prodeq2i 15825 . . . . . . . . . . . . . . 15 𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡))
568567oveq2i 7360 . . . . . . . . . . . . . 14 ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡)))
569565fveq2d 6826 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
570569fveq1d 6824 . . . . . . . . . . . . . . 15 (𝑡𝑅 → (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
571570prodeq2i 15825 . . . . . . . . . . . . . 14 𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)
572568, 571oveq12i 7361 . . . . . . . . . . . . 13 (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
573572a1i 11 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
574573adantlr 715 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
575558adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
576505, 6syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
57775ssriv 3939 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℕ0
578577a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℕ0)
579511adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
580 elun1 4133 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑅𝑡 ∈ (𝑅 ∪ {𝑍}))
581580adantl 481 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
582579, 581ffvelcdmd 7019 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
583578, 582sseldd 3936 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
584583faccld 14191 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
585584nncnd 12144 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
586576, 585fprodcl 15859 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
587586adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
5887adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
589505adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝜑)
590505, 13sylan 580 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑇)
591589, 133syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
592591, 582sseldd 3936 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
593589, 590, 592, 146syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
594593adantllr 719 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
59517adantlr 715 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑥𝑋)
596594, 595ffvelcdmd 7019 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
597588, 596fprodcl 15859 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
598576, 584fprodnncl 15862 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ)
599 nnne0 12162 . . . . . . . . . . . . . 14 (∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
600598, 599syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
601600adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
602575, 587, 597, 601div32d 11923 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
603574, 602eqtrd 2764 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
604544fveq2d 6826 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
605604fveq1d 6824 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
606605adantlr 715 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
607603, 606oveq12d 7367 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
608597, 587, 601divcld 11900 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
609505, 23syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
610505, 133syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ (0...𝑁))
611610, 517sseldd 3936 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝑁))
612505, 609, 6113jca 1128 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)))
613 eleq1 2816 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑍) ∈ (0...𝑁)))
6146133anbi3d 1444 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁))))
615 fveq2 6822 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
616615feq1d 6634 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
617614, 616imbi12d 344 . . . . . . . . . . . . . 14 (𝑗 = (𝑐𝑍) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)))
618617, 496vtoclg 3509 . . . . . . . . . . . . 13 ((𝑐𝑍) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
619517, 612, 618sylc 65 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
620619adantlr 715 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
62134adantr 480 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑥𝑋)
622620, 621ffvelcdmd 7019 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥) ∈ ℂ)
623575, 608, 622mulassd 11138 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
624607, 623eqtrd 2764 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
625564, 624oveq12d 7367 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))))
626549ad2antrr 726 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
627554adantlr 715 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
628559adantlr 715 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
629626, 627, 628divcld 11900 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / (!‘(𝑐𝑍))) ∈ ℂ)
630608, 622mulcld 11135 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) ∈ ℂ)
631560adantlr 715 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
632629, 575, 630, 631dmmcand 45315 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
633597, 622, 587, 601div23d 11937 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
634633eqcomd 2735 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
635 nfv 1914 . . . . . . . . . . . . 13 𝑡((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
636 nfcv 2891 . . . . . . . . . . . . 13 𝑡(((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)
637609adantlr 715 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
63811adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
639 fveq2 6822 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑐𝑡) = (𝑐𝑍))
640179, 639fveq12d 6829 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
641640fveq1d 6824 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
642635, 636, 588, 637, 638, 596, 641, 622fprodsplitsn 15896 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
643642eqcomd 2735 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
644643oveq1d 7364 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
645634, 644eqtrd 2764 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
646645oveq2d 7365 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
647588, 368, 370sylancl 586 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
648505adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝜑)
649347sselda 3935 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
650649adantlr 715 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
651511, 610fssd 6669 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝑁))
652651ffvelcdmda 7018 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝑁))
653648, 650, 652, 146syl3anc 1373 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
654653adantllr 719 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
655621adantr 480 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑥𝑋)
656654, 655ffvelcdmd 7019 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
657647, 656fprodcl 15859 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
658626, 627, 657, 587, 628, 601divmuldivd 11941 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))))
659554, 586mulcomd 11136 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
660 nfv 1914 . . . . . . . . . . . . . 14 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
661 nfcv 2891 . . . . . . . . . . . . . 14 𝑡(!‘(𝑐𝑍))
662505, 10syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
663639fveq2d 6826 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑍)))
664660, 661, 576, 609, 662, 585, 663, 554fprodsplitsn 15896 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
665664eqcomd 2735 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
666659, 665eqtrd 2764 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
667666oveq2d 7365 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
668667adantlr 715 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
669505, 371syl 17 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
670577a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0...𝐽) ⊆ ℕ0)
671511ffvelcdmda 7018 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝐽))
672670, 671sseldd 3936 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ ℕ0)
673672faccld 14191 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℕ)
674673nncnd 12144 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℂ)
675669, 674fprodcl 15859 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
676675adantlr 715 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
677673nnne0d 12178 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ≠ 0)
678669, 674, 677fprodn0 15886 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
679678adantlr 715 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
680626, 657, 676, 679div23d 11937 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
681 eqidd 2730 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
682668, 680, 6813eqtrd 2768 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
683646, 658, 6823eqtrd 2768 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
684625, 632, 6833eqtrd 2768 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
685684sumeq2dv 15609 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
686504, 685eqtrd 2764 . . . 4 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
687294, 318, 6863eqtrd 2768 . . 3 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
688687mpteq2dva 5185 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
68939, 209, 6883eqtrd 2768 1 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1540  wcel 2109  wne 2925  wral 3044  wrex 3053  {crab 3394  Vcvv 3436  cdif 3900  cun 3901  wss 3903  𝒫 cpw 4551  {csn 4577  {cpr 4579  cop 4583   ciun 4941   class class class wbr 5092  cmpt 5173   × cxp 5617  cres 5621  wf 6478  1-1-ontowf1o 6481  cfv 6482  (class class class)co 7349  1st c1st 7922  2nd c2nd 7923  m cmap 8753  Fincfn 8872  cc 11007  cr 11008  0cc0 11009   · cmul 11014  cle 11150  cmin 11347   / cdiv 11777  cn 12128  0cn0 12384  cz 12471  cuz 12735  ...cfz 13410  !cfa 14180  Ccbc 14209  Σcsu 15593  cprod 15810  t crest 17324  TopOpenctopn 17325  fldccnfld 21261   D𝑛 cdvn 25763
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5218  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-inf2 9537  ax-cnex 11065  ax-resscn 11066  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-mulcom 11073  ax-addass 11074  ax-mulass 11075  ax-distr 11076  ax-i2m1 11077  ax-1ne0 11078  ax-1rid 11079  ax-rnegex 11080  ax-rrecex 11081  ax-cnre 11082  ax-pre-lttri 11083  ax-pre-lttrn 11084  ax-pre-ltadd 11085  ax-pre-mulgt0 11086  ax-pre-sup 11087  ax-addf 11088
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3343  df-reu 3344  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-tp 4582  df-op 4584  df-uni 4859  df-int 4897  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5174  df-tr 5200  df-id 5514  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-se 5573  df-we 5574  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-pred 6249  df-ord 6310  df-on 6311  df-lim 6312  df-suc 6313  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-isom 6491  df-riota 7306  df-ov 7352  df-oprab 7353  df-mpo 7354  df-of 7613  df-om 7800  df-1st 7924  df-2nd 7925  df-supp 8094  df-frecs 8214  df-wrecs 8245  df-recs 8294  df-rdg 8332  df-1o 8388  df-2o 8389  df-er 8625  df-map 8755  df-pm 8756  df-ixp 8825  df-en 8873  df-dom 8874  df-sdom 8875  df-fin 8876  df-fsupp 9252  df-fi 9301  df-sup 9332  df-inf 9333  df-oi 9402  df-card 9835  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-sub 11349  df-neg 11350  df-div 11778  df-nn 12129  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196  df-8 12197  df-9 12198  df-n0 12385  df-z 12472  df-dec 12592  df-uz 12736  df-q 12850  df-rp 12894  df-xneg 13014  df-xadd 13015  df-xmul 13016  df-ico 13254  df-icc 13255  df-fz 13411  df-fzo 13558  df-seq 13909  df-exp 13969  df-fac 14181  df-bc 14210  df-hash 14238  df-cj 15006  df-re 15007  df-im 15008  df-sqrt 15142  df-abs 15143  df-clim 15395  df-sum 15594  df-prod 15811  df-struct 17058  df-sets 17075  df-slot 17093  df-ndx 17105  df-base 17121  df-ress 17142  df-plusg 17174  df-mulr 17175  df-starv 17176  df-sca 17177  df-vsca 17178  df-ip 17179  df-tset 17180  df-ple 17181  df-ds 17183  df-unif 17184  df-hom 17185  df-cco 17186  df-rest 17326  df-topn 17327  df-0g 17345  df-gsum 17346  df-topgen 17347  df-pt 17348  df-prds 17351  df-xrs 17406  df-qtop 17411  df-imas 17412  df-xps 17414  df-mre 17488  df-mrc 17489  df-acs 17491  df-mgm 18514  df-sgrp 18593  df-mnd 18609  df-submnd 18658  df-mulg 18947  df-cntz 19196  df-cmn 19661  df-psmet 21253  df-xmet 21254  df-met 21255  df-bl 21256  df-mopn 21257  df-fbas 21258  df-fg 21259  df-cnfld 21262  df-top 22779  df-topon 22796  df-topsp 22818  df-bases 22831  df-cld 22904  df-ntr 22905  df-cls 22906  df-nei 22983  df-lp 23021  df-perf 23022  df-cn 23112  df-cnp 23113  df-haus 23200  df-tx 23447  df-hmeo 23640  df-fil 23731  df-fm 23823  df-flim 23824  df-flf 23825  df-xms 24206  df-ms 24207  df-tms 24208  df-cncf 24769  df-limc 25765  df-dv 25766  df-dvn 25767
This theorem is referenced by:  dvnprodlem3  45949
  Copyright terms: Public domain W3C validator