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 40680
Description: Induction step for dvnprodlem2 40680. (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...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
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 1995 . . . . . 6 𝑡(𝜑𝑥𝑋)
2 nfcv 2913 . . . . . 6 𝑡((𝐻𝑍)‘𝑥)
3 dvnprodlem2.t . . . . . . . 8 (𝜑𝑇 ∈ Fin)
4 dvnprodlem2.r . . . . . . . 8 (𝜑𝑅𝑇)
5 ssfi 8336 . . . . . . . 8 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
63, 4, 5syl2anc 573 . . . . . . 7 (𝜑𝑅 ∈ Fin)
76adantr 466 . . . . . 6 ((𝜑𝑥𝑋) → 𝑅 ∈ Fin)
8 dvnprodlem2.z . . . . . . 7 (𝜑𝑍 ∈ (𝑇𝑅))
98adantr 466 . . . . . 6 ((𝜑𝑥𝑋) → 𝑍 ∈ (𝑇𝑅))
108eldifbd 3736 . . . . . . 7 (𝜑 → ¬ 𝑍𝑅)
1110adantr 466 . . . . . 6 ((𝜑𝑥𝑋) → ¬ 𝑍𝑅)
12 simpl 468 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝜑)
134sselda 3752 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝑡𝑇)
14 dvnprodlem2.h . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
1512, 13, 14syl2anc 573 . . . . . . . 8 ((𝜑𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
1615adantlr 694 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
17 simplr 752 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → 𝑥𝑋)
1816, 17ffvelrnd 6503 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → ((𝐻𝑡)‘𝑥) ∈ ℂ)
19 fveq2 6332 . . . . . . 7 (𝑡 = 𝑍 → (𝐻𝑡) = (𝐻𝑍))
2019fveq1d 6334 . . . . . 6 (𝑡 = 𝑍 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑍)‘𝑥))
21 id 22 . . . . . . . . 9 (𝜑𝜑)
22 eldifi 3883 . . . . . . . . . 10 (𝑍 ∈ (𝑇𝑅) → 𝑍𝑇)
238, 22syl 17 . . . . . . . . 9 (𝜑𝑍𝑇)
24 simpr 471 . . . . . . . . . 10 ((𝜑𝑍𝑇) → 𝑍𝑇)
25 id 22 . . . . . . . . . 10 ((𝜑𝑍𝑇) → (𝜑𝑍𝑇))
26 eleq1 2838 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (𝑡𝑇𝑍𝑇))
2726anbi2d 614 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝜑𝑡𝑇) ↔ (𝜑𝑍𝑇)))
2819feq1d 6170 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝐻𝑡):𝑋⟶ℂ ↔ (𝐻𝑍):𝑋⟶ℂ))
2927, 28imbi12d 333 . . . . . . . . . . 11 (𝑡 = 𝑍 → (((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)))
3029, 14vtoclg 3417 . . . . . . . . . 10 (𝑍𝑇 → ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ))
3124, 25, 30sylc 65 . . . . . . . . 9 ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)
3221, 23, 31syl2anc 573 . . . . . . . 8 (𝜑 → (𝐻𝑍):𝑋⟶ℂ)
3332adantr 466 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐻𝑍):𝑋⟶ℂ)
34 simpr 471 . . . . . . 7 ((𝜑𝑥𝑋) → 𝑥𝑋)
3533, 34ffvelrnd 6503 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐻𝑍)‘𝑥) ∈ ℂ)
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 14926 . . . . 5 ((𝜑𝑥𝑋) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥) = (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))
3736mpteq2dva 4878 . . . 4 (𝜑 → (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))
3837oveq2d 6809 . . 3 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))))
3938fveq1d 6334 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽))
40 dvnprodlem2.s . . 3 (𝜑𝑆 ∈ {ℝ, ℂ})
41 dvnprodlem2.x . . 3 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
421, 7, 18fprodclf 14929 . . 3 ((𝜑𝑥𝑋) → ∏𝑡𝑅 ((𝐻𝑡)‘𝑥) ∈ ℂ)
43 dvnprodlem2.j . . . 4 (𝜑𝐽 ∈ (0...𝑁))
44 elfznn0 12640 . . . 4 (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℕ0)
4543, 44syl 17 . . 3 (𝜑𝐽 ∈ ℕ0)
46 eqid 2771 . . 3 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
47 eqid 2771 . . 3 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
48 dvnprodlem2.c . . . . . . . . . . 11 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
4948a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})))
50 oveq2 6801 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅))
51 rabeq 3342 . . . . . . . . . . . . . 14 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
5250, 51syl 17 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
53 sumeq1 14627 . . . . . . . . . . . . . . 15 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
5453eqeq1d 2773 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
5554rabbidv 3339 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5652, 55eqtrd 2805 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5756mpteq2dv 4879 . . . . . . . . . . 11 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
5857adantl 467 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑠 = 𝑅) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
59 ssexg 4938 . . . . . . . . . . . . . 14 ((𝑅𝑇𝑇 ∈ Fin) → 𝑅 ∈ V)
604, 3, 59syl2anc 573 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ V)
61 elpwg 4305 . . . . . . . . . . . . 13 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
6260, 61syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
634, 62mpbird 247 . . . . . . . . . . 11 (𝜑𝑅 ∈ 𝒫 𝑇)
6463adantr 466 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑅 ∈ 𝒫 𝑇)
65 nn0ex 11500 . . . . . . . . . . . 12 0 ∈ V
6665mptex 6630 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
6766a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
6849, 58, 64, 67fvmptd 6430 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
69 oveq2 6801 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
7069oveq1d 6808 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅))
71 rabeq 3342 . . . . . . . . . . . 12 (((0...𝑛) ↑𝑚 𝑅) = ((0...𝑘) ↑𝑚 𝑅) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
7270, 71syl 17 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
73 eqeq2 2782 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
7473rabbidv 3339 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7572, 74eqtrd 2805 . . . . . . . . . 10 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7675adantl 467 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
77 elfznn0 12640 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
7877adantl 467 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
79 fzfid 12980 . . . . . . . . . . . 12 (𝜑 → (0...𝑘) ∈ Fin)
80 mapfi 8418 . . . . . . . . . . . 12 (((0...𝑘) ∈ Fin ∧ 𝑅 ∈ Fin) → ((0...𝑘) ↑𝑚 𝑅) ∈ Fin)
8179, 6, 80syl2anc 573 . . . . . . . . . . 11 (𝜑 → ((0...𝑘) ↑𝑚 𝑅) ∈ Fin)
8281adantr 466 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑𝑚 𝑅) ∈ Fin)
83 ssrab2 3836 . . . . . . . . . . 11 {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑𝑚 𝑅)
8483a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑𝑚 𝑅))
8582, 84ssexd 4939 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
8668, 76, 78, 85fvmptd 6430 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
87 ssfi 8336 . . . . . . . . . 10 ((((0...𝑘) ↑𝑚 𝑅) ∈ Fin ∧ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑𝑚 𝑅)) → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8881, 83, 87sylancl 574 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8988adantr 466 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
9086, 89eqeltrd 2850 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
9190adantr 466 . . . . . 6 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → ((𝐶𝑅)‘𝑘) ∈ Fin)
9277faccld 13275 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℕ)
9392nncnd 11238 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℂ)
9493ad2antlr 706 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (!‘𝑘) ∈ ℂ)
956adantr 466 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
9695adantlr 694 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
97 elfznn0 12640 . . . . . . . . . . . . . . 15 (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0)
9897ssriv 3756 . . . . . . . . . . . . . 14 (0...𝑘) ⊆ ℕ0
9998a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℕ0)
100 simpr 471 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((𝐶𝑅)‘𝑘))
10186eleq2d 2836 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
102101adantr 466 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
103100, 102mpbid 222 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
10483sseli 3748 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → 𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅))
105103, 104syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅))
106 elmapi 8031 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ((0...𝑘) ↑𝑚 𝑅) → 𝑐:𝑅⟶(0...𝑘))
107105, 106syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐:𝑅⟶(0...𝑘))
108107adantr 466 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑐:𝑅⟶(0...𝑘))
109 simpr 471 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑅)
110108, 109ffvelrnd 6503 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑘))
11199, 110sseldd 3753 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
112111faccld 13275 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
113112nncnd 11238 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
11496, 113fprodcl 14889 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
115112nnne0d 11267 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ≠ 0)
11696, 113, 115fprodn0 14916 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
11794, 114, 116divcld 11003 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
118117adantlr 694 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
11996adantlr 694 . . . . . . . 8 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
12021ad4antr 712 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝜑)
121120, 13sylancom 576 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑇)
122 elfzuz3 12546 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ (ℤ𝑘))
123 fzss2 12588 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (ℤ𝑘) → (0...𝑘) ⊆ (0...𝐽))
124122, 123syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0...𝑘) ⊆ (0...𝐽))
125124adantl 467 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝐽))
12645nn0zd 11682 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽 ∈ ℤ)
127 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
128127nn0zd 11682 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℤ)
129 elfzle2 12552 . . . . . . . . . . . . . . . . . . 19 (𝐽 ∈ (0...𝑁) → 𝐽𝑁)
13043, 129syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽𝑁)
131126, 128, 1303jca 1122 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
132 eluz2 11894 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝐽) ↔ (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
133131, 132sylibr 224 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝐽))
134 fzss2 12588 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐽) → (0...𝐽) ⊆ (0...𝑁))
135133, 134syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝐽) ⊆ (0...𝑁))
136135adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝐽) ⊆ (0...𝑁))
137125, 136sstrd 3762 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝑁))
138137ad2antrr 705 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ (0...𝑁))
139138, 110sseldd 3753 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
140139adantllr 698 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
141 fvex 6342 . . . . . . . . . . 11 (𝑐𝑡) ∈ V
142 eleq1 2838 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑡) ∈ (0...𝑁)))
1431423anbi3d 1553 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁))))
144 fveq2 6332 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
145144feq1d 6170 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ))
146143, 145imbi12d 333 . . . . . . . . . . 11 (𝑗 = (𝑐𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)))
147 dvnprodlem2.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
148141, 146, 147vtocl 3410 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
149120, 121, 140, 148syl3anc 1476 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
150 simpllr 760 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑥𝑋)
151149, 150ffvelrnd 6503 . . . . . . . 8 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
152119, 151fprodcl 14889 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
153118, 152mulcld 10262 . . . . . 6 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
15491, 153fsumcl 14672 . . . . 5 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
155 eqid 2771 . . . . 5 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
156154, 155fmptd 6527 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ)
157 dvnprodlem2.ind . . . . . . 7 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
158157adantr 466 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
159 0zd 11591 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ∈ ℤ)
160128adantr 466 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℤ)
161 elfzelz 12549 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
162161adantl 467 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
163159, 160, 1623jca 1122 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ))
164 elfzle1 12551 . . . . . . . . 9 (𝑘 ∈ (0...𝐽) → 0 ≤ 𝑘)
165164adantl 467 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
166162zred 11684 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
16745nn0red 11554 . . . . . . . . . 10 (𝜑𝐽 ∈ ℝ)
168167adantr 466 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
169160zred 11684 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℝ)
170 elfzle2 12552 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
171170adantl 467 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
172130adantr 466 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽𝑁)
173166, 168, 169, 171, 172letrd 10396 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝑁)
174163, 165, 173jca32 505 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (0 ≤ 𝑘𝑘𝑁)))
175 elfz2 12540 . . . . . . 7 (𝑘 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (0 ≤ 𝑘𝑘𝑁)))
176174, 175sylibr 224 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ (0...𝑁))
177 rspa 3079 . . . . . 6 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
178158, 176, 177syl2anc 573 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
179178feq1d 6170 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ))
180156, 179mpbird 247 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ)
18123adantr 466 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑍𝑇)
182 simpl 468 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝜑)
183182, 181, 1763jca 1122 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → (𝜑𝑍𝑇𝑘 ∈ (0...𝑁)))
184263anbi2d 1552 . . . . . . 7 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑘 ∈ (0...𝑁))))
18519oveq2d 6809 . . . . . . . . 9 (𝑡 = 𝑍 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑍)))
186185fveq1d 6334 . . . . . . . 8 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
187186feq1d 6170 . . . . . . 7 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
188184, 187imbi12d 333 . . . . . 6 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)))
189 eleq1 2838 . . . . . . . . 9 (𝑗 = 𝑘 → (𝑗 ∈ (0...𝑁) ↔ 𝑘 ∈ (0...𝑁)))
1901893anbi3d 1553 . . . . . . . 8 (𝑗 = 𝑘 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇𝑘 ∈ (0...𝑁))))
191 fveq2 6332 . . . . . . . . 9 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘𝑘))
192191feq1d 6170 . . . . . . . 8 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ))
193190, 192imbi12d 333 . . . . . . 7 (𝑗 = 𝑘 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)))
194193, 147chvarv 2425 . . . . . 6 ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)
195188, 194vtoclg 3417 . . . . 5 (𝑍𝑇 → ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
196181, 183, 195sylc 65 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)
19732feqmptd 6391 . . . . . . . . 9 (𝜑 → (𝐻𝑍) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
198197eqcomd 2777 . . . . . . . 8 (𝜑 → (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝐻𝑍))
199198oveq2d 6809 . . . . . . 7 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))) = (𝑆 D𝑛 (𝐻𝑍)))
200199fveq1d 6334 . . . . . 6 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
201200adantr 466 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
202201feq1d 6170 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
203196, 202mpbird 247 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ)
204 fveq2 6332 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑡)‘𝑥))
205204prodeq2ad 40342 . . . . . . 7 (𝑦 = 𝑥 → ∏𝑡𝑅 ((𝐻𝑡)‘𝑦) = ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
206205cbvmptv 4884 . . . . . 6 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
207206oveq2i 6804 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))
208207fveq1i 6333 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘)
209208mpteq2i 4875 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
210 fveq2 6332 . . . . . . 7 (𝑦 = 𝑥 → ((𝐻𝑍)‘𝑦) = ((𝐻𝑍)‘𝑥))
211210cbvmptv 4884 . . . . . 6 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
212211oveq2i 6804 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
213212fveq1i 6333 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘)
214213mpteq2i 4875 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘))
21540, 41, 42, 35, 45, 46, 47, 180, 203, 209, 214dvnmul 40676 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽) = (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))))
216208a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
217157r19.21bi 3081 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
218182, 176, 217syl2anc 573 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
219216, 218eqtrd 2805 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
220219mpteq2dva 4878 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
221 mptexg 6628 . . . . . . . . . . . . . 14 (𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
22241, 221syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
223222adantr 466 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
224220, 223fvmpt2d 6435 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
225224adantlr 694 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
226225fveq1d 6334 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥))
22734adantr 466 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → 𝑥𝑋)
228154an32s 631 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
229155fvmpt2 6433 . . . . . . . . . 10 ((𝑥𝑋 ∧ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
230227, 228, 229syl2anc 573 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
231226, 230eqtrd 2805 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
232 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
233232cbvmptv 4884 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
234233a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)))
235212, 199syl5eq 2817 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝐻𝑍)))
236235fveq1d 6334 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
237236mpteq2dv 4879 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
238234, 237eqtrd 2805 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
239238adantr 466 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
240 fveq2 6332 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
241240adantl 467 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑗 = (𝐽𝑘)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
242 0zd 11591 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 0 ∈ ℤ)
243 elfzel2 12547 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
244243, 161zsubcld 11689 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ∈ ℤ)
245242, 243, 2443jca 1122 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ))
246243zred 11684 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
24777nn0red 11554 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
248246, 247subge0d 10819 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
249170, 248mpbird 247 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
250246, 247subge02d 10821 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
251164, 250mpbid 222 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ≤ 𝐽)
252245, 249, 251jca32 505 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝐽) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
253252adantl 467 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
254 elfz2 12540 . . . . . . . . . . . 12 ((𝐽𝑘) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
255253, 254sylibr 224 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ∈ (0...𝐽))
256 fvex 6342 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V
257256a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V)
258239, 241, 255, 257fvmptd 6430 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
259258adantlr 694 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
260259fveq1d 6334 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
261231, 260oveq12d 6811 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)) = (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
262261oveq2d 6809 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
26390adantlr 694 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
264 ovex 6823 . . . . . . . . . . . 12 (𝐽𝑘) ∈ V
265 eleq1 2838 . . . . . . . . . . . . . 14 (𝑗 = (𝐽𝑘) → (𝑗 ∈ (0...𝐽) ↔ (𝐽𝑘) ∈ (0...𝐽)))
266265anbi2d 614 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → ((𝜑𝑗 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽))))
267240feq1d 6170 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ))
268266, 267imbi12d 333 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → (((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)))
269 eleq1 2838 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ (0...𝐽) ↔ 𝑗 ∈ (0...𝐽)))
270269anbi2d 614 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ (0...𝐽)) ↔ (𝜑𝑗 ∈ (0...𝐽))))
271 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
272271feq1d 6170 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
273270, 272imbi12d 333 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
274273, 196chvarv 2425 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
275264, 268, 274vtocl 3410 . . . . . . . . . . 11 ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
276182, 255, 275syl2anc 573 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
277276adantlr 694 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
278277, 227ffvelrnd 6503 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
279 anass 459 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ (𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)))
280 ancom 452 . . . . . . . . . . . . . 14 ((𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋) ↔ (𝑥𝑋𝑘 ∈ (0...𝐽)))
281280anbi2i 609 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
282 anass 459 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
283282bicomi 214 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
284281, 283bitri 264 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
285279, 284bitri 264 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
286285anbi1i 610 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ↔ (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)))
287286imbi1i 338 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) ↔ ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ))
288153, 287mpbi 220 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
289263, 278, 288fsummulc1 14724 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
290289oveq2d 6809 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
291182, 45syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℕ0)
292291, 162bccld 40047 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℕ0)
293292nn0cnd 11555 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
294293adantlr 694 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
295278adantr 466 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
296288, 295mulcld 10262 . . . . . . 7 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
297263, 294, 296fsummulc2 14723 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
298262, 290, 2973eqtrd 2809 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
299298sumeq2dv 14641 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
300 vex 3354 . . . . . . . 8 𝑘 ∈ V
301 vex 3354 . . . . . . . 8 𝑐 ∈ V
302300, 301op1std 7325 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (1st𝑝) = 𝑘)
303302oveq2d 6809 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽C(1st𝑝)) = (𝐽C𝑘))
304302fveq2d 6336 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘(1st𝑝)) = (!‘𝑘))
305300, 301op2ndd 7326 . . . . . . . . . . . 12 (𝑝 = ⟨𝑘, 𝑐⟩ → (2nd𝑝) = 𝑐)
306305fveq1d 6334 . . . . . . . . . . 11 (𝑝 = ⟨𝑘, 𝑐⟩ → ((2nd𝑝)‘𝑡) = (𝑐𝑡))
307306fveq2d 6336 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘(𝑐𝑡)))
308307prodeq2ad 40342 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡)))
309304, 308oveq12d 6811 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
310306fveq2d 6336 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
311310fveq1d 6334 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
312311prodeq2ad 40342 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
313309, 312oveq12d 6811 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
314302oveq2d 6809 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽 − (1st𝑝)) = (𝐽𝑘))
315314fveq2d 6336 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
316315fveq1d 6334 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
317313, 316oveq12d 6811 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
318303, 317oveq12d 6811 . . . . 5 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
319 fzfid 12980 . . . . 5 ((𝜑𝑥𝑋) → (0...𝐽) ∈ Fin)
320294adantrr 696 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → (𝐽C𝑘) ∈ ℂ)
321296anasss 457 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
322320, 321mulcld 10262 . . . . 5 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) ∈ ℂ)
323318, 319, 263, 322fsum2d 14710 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))))
324 ovex 6823 . . . . . . . . 9 (𝐽 − (𝑐𝑍)) ∈ V
325301resex 5584 . . . . . . . . 9 (𝑐𝑅) ∈ V
326324, 325op1std 7325 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (1st𝑝) = (𝐽 − (𝑐𝑍)))
327326oveq2d 6809 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽C(1st𝑝)) = (𝐽C(𝐽 − (𝑐𝑍))))
328326fveq2d 6336 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘(1st𝑝)) = (!‘(𝐽 − (𝑐𝑍))))
329324, 325op2ndd 7326 . . . . . . . . . . . . 13 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (2nd𝑝) = (𝑐𝑅))
330329fveq1d 6334 . . . . . . . . . . . 12 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((2nd𝑝)‘𝑡) = ((𝑐𝑅)‘𝑡))
331330fveq2d 6336 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘((𝑐𝑅)‘𝑡)))
332331prodeq2ad 40342 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)))
333328, 332oveq12d 6811 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))))
334330fveq2d 6336 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)))
335334fveq1d 6334 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
336335prodeq2ad 40342 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
337333, 336oveq12d 6811 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)))
338326oveq2d 6809 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽 − (1st𝑝)) = (𝐽 − (𝐽 − (𝑐𝑍))))
339338fveq2d 6336 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))))
340339fveq1d 6334 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))
341337, 340oveq12d 6811 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)))
342327, 341oveq12d 6811 . . . . . 6 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
34348a1i 11 . . . . . . . . . 10 (𝜑𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})))
344 oveq2 6801 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})))
345 rabeq 3342 . . . . . . . . . . . . . 14 (((0...𝑛) ↑𝑚 𝑠) = ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
346344, 345syl 17 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
347 sumeq1 14627 . . . . . . . . . . . . . . 15 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
348347eqeq1d 2773 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
349348rabbidv 3339 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
350346, 349eqtrd 2805 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
351350mpteq2dv 4879 . . . . . . . . . . 11 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
352351adantl 467 . . . . . . . . . 10 ((𝜑𝑠 = (𝑅 ∪ {𝑍})) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
35323snssd 4475 . . . . . . . . . . . 12 (𝜑 → {𝑍} ⊆ 𝑇)
3544, 353unssd 3940 . . . . . . . . . . 11 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
3553, 354ssexd 4939 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
356 elpwg 4305 . . . . . . . . . . . 12 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
357355, 356syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
358354, 357mpbird 247 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
35965mptex 6630 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
360359a1i 11 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
361343, 352, 358, 360fvmptd 6430 . . . . . . . . 9 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
362 oveq2 6801 . . . . . . . . . . . . 13 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
363362oveq1d 6808 . . . . . . . . . . . 12 (𝑛 = 𝐽 → ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
364 rabeq 3342 . . . . . . . . . . . 12 (((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
365363, 364syl 17 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
366 eqeq2 2782 . . . . . . . . . . . 12 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
367366rabbidv 3339 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
368365, 367eqtrd 2805 . . . . . . . . . 10 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
369368adantl 467 . . . . . . . . 9 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
370 ovex 6823 . . . . . . . . . . 11 ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∈ V
371370rabex 4946 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
372371a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
373361, 369, 45, 372fvmptd 6430 . . . . . . . 8 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
374 fzfid 12980 . . . . . . . . . 10 (𝜑 → (0...𝐽) ∈ Fin)
375 snfi 8194 . . . . . . . . . . . 12 {𝑍} ∈ Fin
376375a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑍} ∈ Fin)
377 unfi 8383 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ Fin)
3786, 376, 377syl2anc 573 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ Fin)
379 mapfi 8418 . . . . . . . . . 10 (((0...𝐽) ∈ Fin ∧ (𝑅 ∪ {𝑍}) ∈ Fin) → ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∈ Fin)
380374, 378, 379syl2anc 573 . . . . . . . . 9 (𝜑 → ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∈ Fin)
381 ssrab2 3836 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍}))
382381a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
383 ssfi 8336 . . . . . . . . 9 ((((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∈ Fin ∧ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍}))) → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
384380, 382, 383syl2anc 573 . . . . . . . 8 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
385373, 384eqeltrd 2850 . . . . . . 7 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
386385adantr 466 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
387 dvnprodlem2.d . . . . . . . 8 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38848, 45, 387, 3, 23, 10, 354dvnprodlem1 40679 . . . . . . 7 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
389388adantr 466 . . . . . 6 ((𝜑𝑥𝑋) → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
390 simpr 471 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
391 opex 5060 . . . . . . . . 9 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
392391a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
393387fvmpt2 6433 . . . . . . . 8 ((𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
394390, 392, 393syl2anc 573 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
395394adantlr 694 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
39645adantr 466 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℕ0)
397 eliun 4658 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
398397biimpi 206 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
399398adantl 467 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
400 nfv 1995 . . . . . . . . . . . . . 14 𝑘𝜑
401 nfcv 2913 . . . . . . . . . . . . . . 15 𝑘𝑝
402 nfiu1 4684 . . . . . . . . . . . . . . 15 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
403401, 402nfel 2926 . . . . . . . . . . . . . 14 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
404400, 403nfan 1980 . . . . . . . . . . . . 13 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
405 nfv 1995 . . . . . . . . . . . . 13 𝑘(1st𝑝) ∈ (0...𝐽)
406 xp1st 7347 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
407 elsni 4333 . . . . . . . . . . . . . . . . . 18 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
408406, 407syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
409408adantl 467 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
410 simpl 468 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
411409, 410eqeltrd 2850 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
412411ex 397 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
413412a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
414404, 405, 413rexlimd 3174 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
415399, 414mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
416 elfzelz 12549 . . . . . . . . . . 11 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
417415, 416syl 17 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
418396, 417bccld 40047 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℕ0)
419418nn0cnd 11555 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
420419adantlr 694 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
421 elfznn0 12640 . . . . . . . . . . . . . 14 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℕ0)
422415, 421syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℕ0)
423422faccld 13275 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℕ)
424423nncnd 11238 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
425424adantlr 694 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
4266adantr 466 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
427 nfv 1995 . . . . . . . . . . . . . . . 16 𝑘(2nd𝑝):𝑅⟶(0...𝐽)
42886, 84eqsstrd 3788 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝑘) ↑𝑚 𝑅))
429 ovex 6823 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0...𝐽) ∈ V
430429a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0...𝐽) ∈ V)
431 mapss 8054 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝐽) ∈ V ∧ (0...𝑘) ⊆ (0...𝐽)) → ((0...𝑘) ↑𝑚 𝑅) ⊆ ((0...𝐽) ↑𝑚 𝑅))
432430, 124, 431syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → ((0...𝑘) ↑𝑚 𝑅) ⊆ ((0...𝐽) ↑𝑚 𝑅))
433432adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑𝑚 𝑅) ⊆ ((0...𝐽) ↑𝑚 𝑅))
434428, 433sstrd 3762 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑𝑚 𝑅))
4354343adant3 1126 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑𝑚 𝑅))
436 xp2nd 7348 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4374363ad2ant3 1129 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
438435, 437sseldd 3753 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝐽) ↑𝑚 𝑅))
439 elmapi 8031 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑝) ∈ ((0...𝐽) ↑𝑚 𝑅) → (2nd𝑝):𝑅⟶(0...𝐽))
440438, 439syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
4414403exp 1112 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
442441adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
443404, 427, 442rexlimd 3174 . . . . . . . . . . . . . . 15 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽)))
444399, 443mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
445444ffvelrnda 6502 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝐽))
446 elfznn0 12640 . . . . . . . . . . . . . . 15 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((2nd𝑝)‘𝑡) ∈ ℕ0)
447446faccld 13275 . . . . . . . . . . . . . 14 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
448447nncnd 11238 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
449445, 448syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
450426, 449fprodcl 14889 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
451450adantlr 694 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
452445, 447syl 17 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
453 nnne0 11255 . . . . . . . . . . . . 13 ((!‘((2nd𝑝)‘𝑡)) ∈ ℕ → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
454452, 453syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
455426, 449, 454fprodn0 14916 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
456455adantlr 694 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
457425, 451, 456divcld 11003 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) ∈ ℂ)
4587adantr 466 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
459 simpll 750 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝜑)
460459, 13sylancom 576 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑡𝑇)
461459, 135syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
462461, 445sseldd 3753 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑁))
463459, 460, 4623jca 1122 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
464 eleq1 2838 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → (𝑗 ∈ (0...𝑁) ↔ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
4654643anbi3d 1553 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁))))
466 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)))
467466feq1d 6170 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
468465, 467imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)))
469468, 147vtoclg 3417 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
470445, 463, 469sylc 65 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
471470adantllr 698 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
47217adantlr 694 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑥𝑋)
473471, 472ffvelrnd 6503 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
474458, 473fprodcl 14889 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
475457, 474mulcld 10262 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) ∈ ℂ)
476 nfv 1995 . . . . . . . . . . . . 13 𝑘(𝐽 − (1st𝑝)) ∈ (0...𝐽)
477 simp1 1130 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
4784113adant1 1124 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
479 fznn0sub2 12654 . . . . . . . . . . . . . . . . 17 ((1st𝑝) ∈ (0...𝐽) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
480479adantl 467 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (1st𝑝) ∈ (0...𝐽)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
481477, 478, 480syl2anc 573 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
4824813exp 1112 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
483482adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
484404, 476, 483rexlimd 3174 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽)))
485399, 484mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
486 simpl 468 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
487486, 23syl 17 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
488486, 135syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ⊆ (0...𝑁))
489488, 485sseldd 3753 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝑁))
490486, 487, 4893jca 1122 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
491 eleq1 2838 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → (𝑗 ∈ (0...𝑁) ↔ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
4924913anbi3d 1553 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁))))
493 fveq2 6332 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))))
494493feq1d 6170 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
495492, 494imbi12d 333 . . . . . . . . . . . 12 (𝑗 = (𝐽 − (1st𝑝)) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)))
496 simp2 1131 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → 𝑍𝑇)
497 id 22 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → (𝜑𝑍𝑇𝑗 ∈ (0...𝑁)))
498263anbi2d 1552 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑗 ∈ (0...𝑁))))
499185fveq1d 6334 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
500499feq1d 6170 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
501498, 500imbi12d 333 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
502501, 147vtoclg 3417 . . . . . . . . . . . . 13 (𝑍𝑇 → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
503496, 497, 502sylc 65 . . . . . . . . . . . 12 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
504495, 503vtoclg 3417 . . . . . . . . . . 11 ((𝐽 − (1st𝑝)) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
505485, 490, 504sylc 65 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
506505adantlr 694 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
50734adantr 466 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑥𝑋)
508506, 507ffvelrnd 6503 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) ∈ ℂ)
509475, 508mulcld 10262 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) ∈ ℂ)
510420, 509mulcld 10262 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) ∈ ℂ)
511342, 386, 389, 395, 510fsumf1o 14662 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
512 simpl 468 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝜑)
513373adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
514390, 513eleqtrd 2852 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
515381sseli 3748 . . . . . . . . . . . . . . 15 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} → 𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
516514, 515syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})))
517 elmapi 8031 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0...𝐽) ↑𝑚 (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
518516, 517syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
519 snidg 4345 . . . . . . . . . . . . . . . 16 (𝑍𝑇𝑍 ∈ {𝑍})
52023, 519syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑍 ∈ {𝑍})
521 elun2 3932 . . . . . . . . . . . . . . 15 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
522520, 521syl 17 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
523522adantr 466 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
524518, 523ffvelrnd 6503 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
525 0zd 11591 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ∈ ℤ)
526126adantr 466 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℤ)
527 fzssz 12550 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℤ
528527sseli 3748 . . . . . . . . . . . . . . . . 17 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℤ)
529528adantl 467 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℤ)
530526, 529zsubcld 11689 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
531525, 526, 5303jca 1122 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ))
532 elfzle2 12552 . . . . . . . . . . . . . . . 16 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
533532adantl 467 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ≤ 𝐽)
534167adantr 466 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
535529zred 11684 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℝ)
536534, 535subge0d 10819 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
537533, 536mpbird 247 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
538 elfzle1 12551 . . . . . . . . . . . . . . . 16 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
539538adantl 467 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝑐𝑍))
540534, 535subge02d 10821 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
541539, 540mpbid 222 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
542531, 537, 541jca32 505 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
543 elfz2 12540 . . . . . . . . . . . . 13 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
544542, 543sylibr 224 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
545512, 524, 544syl2anc 573 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
546 bcval2 13296 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
547545, 546syl 17 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
548167recnd 10270 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℂ)
549548adantr 466 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
550 zsscn 11587 . . . . . . . . . . . . . . . . 17 ℤ ⊆ ℂ
551527, 550sstri 3761 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℂ
552551a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
553552, 524sseldd 3753 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
554549, 553nncand 10599 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
555554fveq2d 6336 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝐽 − (𝑐𝑍)))) = (!‘(𝑐𝑍)))
556555oveq1d 6808 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍)))) = ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍)))))
557556oveq2d 6809 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
55845faccld 13275 . . . . . . . . . . . . . 14 (𝜑 → (!‘𝐽) ∈ ℕ)
559558nncnd 11238 . . . . . . . . . . . . 13 (𝜑 → (!‘𝐽) ∈ ℂ)
560559adantr 466 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
561 elfznn0 12640 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℕ0)
562524, 561syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℕ0)
563562faccld 13275 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℕ)
564563nncnd 11238 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
565 elfznn0 12640 . . . . . . . . . . . . . . 15 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
566545, 565syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
567566faccld 13275 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℕ)
568567nncnd 11238 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
569563nnne0d 11267 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
570567nnne0d 11267 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
571560, 564, 568, 569, 570divdiv1d 11034 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
572571eqcomd 2777 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
573547, 557, 5723eqtrd 2809 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
574573adantlr 694 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
575 fvres 6348 . . . . . . . . . . . . . . . . 17 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
576575fveq2d 6336 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → (!‘((𝑐𝑅)‘𝑡)) = (!‘(𝑐𝑡)))
577576prodeq2i 14856 . . . . . . . . . . . . . . 15 𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡))
578577oveq2i 6804 . . . . . . . . . . . . . 14 ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡)))
579575fveq2d 6336 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
580579fveq1d 6334 . . . . . . . . . . . . . . 15 (𝑡𝑅 → (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
581580prodeq2i 14856 . . . . . . . . . . . . . 14 𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)
582578, 581oveq12i 6805 . . . . . . . . . . . . 13 (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
583582a1i 11 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
584583adantlr 694 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
585568adantlr 694 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
586512, 6syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
58777ssriv 3756 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℕ0
588587a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℕ0)
589518adantr 466 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
590 elun1 3931 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑅𝑡 ∈ (𝑅 ∪ {𝑍}))
591590adantl 467 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
592589, 591ffvelrnd 6503 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
593588, 592sseldd 3753 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
594593faccld 13275 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
595594nncnd 11238 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
596586, 595fprodcl 14889 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
597596adantlr 694 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
5987adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
599512adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝜑)
600512, 13sylan 569 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑇)
601599, 135syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
602601, 592sseldd 3753 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
603599, 600, 602, 148syl3anc 1476 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
604603adantllr 698 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
60517adantlr 694 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑥𝑋)
606604, 605ffvelrnd 6503 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
607598, 606fprodcl 14889 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
608586, 594fprodnncl 14892 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ)
609 nnne0 11255 . . . . . . . . . . . . . 14 (∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
610608, 609syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
611610adantlr 694 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
612585, 597, 607, 611div32d 11026 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
613584, 612eqtrd 2805 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
614554fveq2d 6336 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
615614fveq1d 6334 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
616615adantlr 694 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
617613, 616oveq12d 6811 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
618607, 597, 611divcld 11003 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
619512, 23syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
620512, 135syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ (0...𝑁))
621620, 524sseldd 3753 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝑁))
622512, 619, 6213jca 1122 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)))
623 eleq1 2838 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑍) ∈ (0...𝑁)))
6246233anbi3d 1553 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁))))
625 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
626625feq1d 6170 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
627624, 626imbi12d 333 . . . . . . . . . . . . . 14 (𝑗 = (𝑐𝑍) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)))
628627, 503vtoclg 3417 . . . . . . . . . . . . 13 ((𝑐𝑍) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
629524, 622, 628sylc 65 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
630629adantlr 694 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
63134adantr 466 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑥𝑋)
632630, 631ffvelrnd 6503 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥) ∈ ℂ)
633585, 618, 632mulassd 10265 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
634617, 633eqtrd 2805 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
635574, 634oveq12d 6811 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))))
636559ad2antrr 705 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
637564adantlr 694 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
638569adantlr 694 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
639636, 637, 638divcld 11003 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / (!‘(𝑐𝑍))) ∈ ℂ)
640618, 632mulcld 10262 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) ∈ ℂ)
641570adantlr 694 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
642639, 585, 640, 641dmmcand 40044 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
643607, 632, 597, 611div23d 11040 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
644643eqcomd 2777 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
645 nfv 1995 . . . . . . . . . . . . 13 𝑡((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
646 nfcv 2913 . . . . . . . . . . . . 13 𝑡(((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)
647619adantlr 694 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
64811adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
649 fveq2 6332 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑐𝑡) = (𝑐𝑍))
650185, 649fveq12d 6338 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
651650fveq1d 6334 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
652645, 646, 598, 647, 648, 606, 651, 632fprodsplitsn 14926 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
653652eqcomd 2777 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
654653oveq1d 6808 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
655644, 654eqtrd 2805 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
656655oveq2d 6809 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
657598, 375, 377sylancl 574 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
658512adantr 466 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝜑)
659354sselda 3752 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
660659adantlr 694 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
661518, 620fssd 6197 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝑁))
662661ffvelrnda 6502 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝑁))
663658, 660, 662, 148syl3anc 1476 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
664663adantllr 698 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
665631adantr 466 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑥𝑋)
666664, 665ffvelrnd 6503 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
667657, 666fprodcl 14889 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
668636, 637, 667, 597, 638, 611divmuldivd 11044 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))))
669564, 596mulcomd 10263 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
670 nfv 1995 . . . . . . . . . . . . . 14 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
671 nfcv 2913 . . . . . . . . . . . . . 14 𝑡(!‘(𝑐𝑍))
672512, 10syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
673649fveq2d 6336 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑍)))
674670, 671, 586, 619, 672, 595, 673, 564fprodsplitsn 14926 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
675674eqcomd 2777 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
676669, 675eqtrd 2805 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
677676oveq2d 6809 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
678677adantlr 694 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
679512, 378syl 17 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
680587a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0...𝐽) ⊆ ℕ0)
681518ffvelrnda 6502 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝐽))
682680, 681sseldd 3753 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ ℕ0)
683682faccld 13275 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℕ)
684683nncnd 11238 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℂ)
685679, 684fprodcl 14889 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
686685adantlr 694 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
687683nnne0d 11267 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ≠ 0)
688679, 684, 687fprodn0 14916 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
689688adantlr 694 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
690636, 667, 686, 689div23d 11040 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
691 eqidd 2772 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
692678, 690, 6913eqtrd 2809 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
693656, 668, 6923eqtrd 2809 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
694635, 642, 6933eqtrd 2809 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
695694sumeq2dv 14641 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
696511, 695eqtrd 2805 . . . 4 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
697299, 323, 6963eqtrd 2809 . . 3 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
698697mpteq2dva 4878 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
69939, 215, 6983eqtrd 2809 1 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {crab 3065  Vcvv 3351  cdif 3720  cun 3721  wss 3723  𝒫 cpw 4297  {csn 4316  {cpr 4318  cop 4322   ciun 4654   class class class wbr 4786  cmpt 4863   × cxp 5247  cres 5251  wf 6027  1-1-ontowf1o 6030  cfv 6031  (class class class)co 6793  1st c1st 7313  2nd c2nd 7314  𝑚 cmap 8009  Fincfn 8109  cc 10136  cr 10137  0cc0 10138   · cmul 10143  cle 10277  cmin 10468   / cdiv 10886  cn 11222  0cn0 11494  cz 11579  cuz 11888  ...cfz 12533  !cfa 13264  Ccbc 13293  Σcsu 14624  cprod 14842  t crest 16289  TopOpenctopn 16290  fldccnfld 19961   D𝑛 cdvn 23848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-inf2 8702  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216  ax-addf 10217  ax-mulf 10218
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-iin 4657  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-of 7044  df-om 7213  df-1st 7315  df-2nd 7316  df-supp 7447  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-ixp 8063  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fsupp 8432  df-fi 8473  df-sup 8504  df-inf 8505  df-oi 8571  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-q 11992  df-rp 12036  df-xneg 12151  df-xadd 12152  df-xmul 12153  df-ico 12386  df-icc 12387  df-fz 12534  df-fzo 12674  df-seq 13009  df-exp 13068  df-fac 13265  df-bc 13294  df-hash 13322  df-cj 14047  df-re 14048  df-im 14049  df-sqrt 14183  df-abs 14184  df-clim 14427  df-sum 14625  df-prod 14843  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16172  df-unif 16173  df-hom 16174  df-cco 16175  df-rest 16291  df-topn 16292  df-0g 16310  df-gsum 16311  df-topgen 16312  df-pt 16313  df-prds 16316  df-xrs 16370  df-qtop 16375  df-imas 16376  df-xps 16378  df-mre 16454  df-mrc 16455  df-acs 16457  df-mgm 17450  df-sgrp 17492  df-mnd 17503  df-submnd 17544  df-mulg 17749  df-cntz 17957  df-cmn 18402  df-psmet 19953  df-xmet 19954  df-met 19955  df-bl 19956  df-mopn 19957  df-fbas 19958  df-fg 19959  df-cnfld 19962  df-top 20919  df-topon 20936  df-topsp 20958  df-bases 20971  df-cld 21044  df-ntr 21045  df-cls 21046  df-nei 21123  df-lp 21161  df-perf 21162  df-cn 21252  df-cnp 21253  df-haus 21340  df-tx 21586  df-hmeo 21779  df-fil 21870  df-fm 21962  df-flim 21963  df-flf 21964  df-xms 22345  df-ms 22346  df-tms 22347  df-cncf 22901  df-limc 23850  df-dv 23851  df-dvn 23852
This theorem is referenced by:  dvnprodlem3  40681
  Copyright terms: Public domain W3C validator