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 42589
Description: Induction step for dvnprodlem2 42589. (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 1915 . . . . . 6 𝑡(𝜑𝑥𝑋)
2 nfcv 2955 . . . . . 6 𝑡((𝐻𝑍)‘𝑥)
3 dvnprodlem2.t . . . . . . . 8 (𝜑𝑇 ∈ Fin)
4 dvnprodlem2.r . . . . . . . 8 (𝜑𝑅𝑇)
5 ssfi 8722 . . . . . . . 8 ((𝑇 ∈ Fin ∧ 𝑅𝑇) → 𝑅 ∈ Fin)
63, 4, 5syl2anc 587 . . . . . . 7 (𝜑𝑅 ∈ Fin)
76adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → 𝑅 ∈ Fin)
8 dvnprodlem2.z . . . . . . 7 (𝜑𝑍 ∈ (𝑇𝑅))
98adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → 𝑍 ∈ (𝑇𝑅))
108eldifbd 3894 . . . . . . 7 (𝜑 → ¬ 𝑍𝑅)
1110adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → ¬ 𝑍𝑅)
12 simpl 486 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝜑)
134sselda 3915 . . . . . . . . 9 ((𝜑𝑡𝑅) → 𝑡𝑇)
14 dvnprodlem2.h . . . . . . . . 9 ((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ)
1512, 13, 14syl2anc 587 . . . . . . . 8 ((𝜑𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
1615adantlr 714 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → (𝐻𝑡):𝑋⟶ℂ)
17 simplr 768 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → 𝑥𝑋)
1816, 17ffvelrnd 6829 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑡𝑅) → ((𝐻𝑡)‘𝑥) ∈ ℂ)
19 fveq2 6645 . . . . . . 7 (𝑡 = 𝑍 → (𝐻𝑡) = (𝐻𝑍))
2019fveq1d 6647 . . . . . 6 (𝑡 = 𝑍 → ((𝐻𝑡)‘𝑥) = ((𝐻𝑍)‘𝑥))
21 id 22 . . . . . . . . 9 (𝜑𝜑)
22 eldifi 4054 . . . . . . . . . 10 (𝑍 ∈ (𝑇𝑅) → 𝑍𝑇)
238, 22syl 17 . . . . . . . . 9 (𝜑𝑍𝑇)
24 simpr 488 . . . . . . . . . 10 ((𝜑𝑍𝑇) → 𝑍𝑇)
25 id 22 . . . . . . . . . 10 ((𝜑𝑍𝑇) → (𝜑𝑍𝑇))
26 eleq1 2877 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (𝑡𝑇𝑍𝑇))
2726anbi2d 631 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝜑𝑡𝑇) ↔ (𝜑𝑍𝑇)))
2819feq1d 6472 . . . . . . . . . . . 12 (𝑡 = 𝑍 → ((𝐻𝑡):𝑋⟶ℂ ↔ (𝐻𝑍):𝑋⟶ℂ))
2927, 28imbi12d 348 . . . . . . . . . . 11 (𝑡 = 𝑍 → (((𝜑𝑡𝑇) → (𝐻𝑡):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)))
3029, 14vtoclg 3515 . . . . . . . . . 10 (𝑍𝑇 → ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ))
3124, 25, 30sylc 65 . . . . . . . . 9 ((𝜑𝑍𝑇) → (𝐻𝑍):𝑋⟶ℂ)
3221, 23, 31syl2anc 587 . . . . . . . 8 (𝜑 → (𝐻𝑍):𝑋⟶ℂ)
3332adantr 484 . . . . . . 7 ((𝜑𝑥𝑋) → (𝐻𝑍):𝑋⟶ℂ)
34 simpr 488 . . . . . . 7 ((𝜑𝑥𝑋) → 𝑥𝑋)
3533, 34ffvelrnd 6829 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐻𝑍)‘𝑥) ∈ ℂ)
361, 2, 7, 9, 11, 18, 20, 35fprodsplitsn 15335 . . . . 5 ((𝜑𝑥𝑋) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥) = (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))
3736mpteq2dva 5125 . . . 4 (𝜑 → (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))
3837oveq2d 7151 . . 3 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥))) = (𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥)))))
3938fveq1d 6647 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽))
40 dvnprodlem2.s . . 3 (𝜑𝑆 ∈ {ℝ, ℂ})
41 dvnprodlem2.x . . 3 (𝜑𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
421, 7, 18fprodclf 15338 . . 3 ((𝜑𝑥𝑋) → ∏𝑡𝑅 ((𝐻𝑡)‘𝑥) ∈ ℂ)
43 dvnprodlem2.j . . . 4 (𝜑𝐽 ∈ (0...𝑁))
44 elfznn0 12995 . . . 4 (𝐽 ∈ (0...𝑁) → 𝐽 ∈ ℕ0)
4543, 44syl 17 . . 3 (𝜑𝐽 ∈ ℕ0)
46 eqid 2798 . . 3 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
47 eqid 2798 . . 3 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
48 dvnprodlem2.c . . . . . . . . . 10 𝐶 = (𝑠 ∈ 𝒫 𝑇 ↦ (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}))
49 oveq2 7143 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅))
50 rabeq 3431 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
5149, 50syl 17 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
52 sumeq1 15037 . . . . . . . . . . . . . 14 (𝑠 = 𝑅 → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡𝑅 (𝑐𝑡))
5352eqeq1d 2800 . . . . . . . . . . . . 13 (𝑠 = 𝑅 → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑛))
5453rabbidv 3427 . . . . . . . . . . . 12 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5551, 54eqtrd 2833 . . . . . . . . . . 11 (𝑠 = 𝑅 → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
5655mpteq2dv 5126 . . . . . . . . . 10 (𝑠 = 𝑅 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
57 ssexg 5191 . . . . . . . . . . . . . 14 ((𝑅𝑇𝑇 ∈ Fin) → 𝑅 ∈ V)
584, 3, 57syl2anc 587 . . . . . . . . . . . . 13 (𝜑𝑅 ∈ V)
59 elpwg 4500 . . . . . . . . . . . . 13 (𝑅 ∈ V → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
6058, 59syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∈ 𝒫 𝑇𝑅𝑇))
614, 60mpbird 260 . . . . . . . . . . 11 (𝜑𝑅 ∈ 𝒫 𝑇)
6261adantr 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑅 ∈ 𝒫 𝑇)
63 nn0ex 11891 . . . . . . . . . . . 12 0 ∈ V
6463mptex 6963 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V
6564a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}) ∈ V)
6648, 56, 62, 65fvmptd3 6768 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐶𝑅) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛}))
67 oveq2 7143 . . . . . . . . . . . . 13 (𝑛 = 𝑘 → (0...𝑛) = (0...𝑘))
6867oveq1d 7150 . . . . . . . . . . . 12 (𝑛 = 𝑘 → ((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅))
69 rabeq 3431 . . . . . . . . . . . 12 (((0...𝑛) ↑m 𝑅) = ((0...𝑘) ↑m 𝑅) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
7068, 69syl 17 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛})
71 eqeq2 2810 . . . . . . . . . . . 12 (𝑛 = 𝑘 → (Σ𝑡𝑅 (𝑐𝑡) = 𝑛 ↔ Σ𝑡𝑅 (𝑐𝑡) = 𝑘))
7271rabbidv 3427 . . . . . . . . . . 11 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7370, 72eqtrd 2833 . . . . . . . . . 10 (𝑛 = 𝑘 → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
7473adantl 485 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑛 = 𝑘) → {𝑐 ∈ ((0...𝑛) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
75 elfznn0 12995 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℕ0)
7675adantl 485 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℕ0)
77 fzfid 13336 . . . . . . . . . . . 12 (𝜑 → (0...𝑘) ∈ Fin)
78 mapfi 8804 . . . . . . . . . . . 12 (((0...𝑘) ∈ Fin ∧ 𝑅 ∈ Fin) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
7977, 6, 78syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((0...𝑘) ↑m 𝑅) ∈ Fin)
8079adantr 484 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ∈ Fin)
81 ssrab2 4007 . . . . . . . . . . 11 {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)
8281a1i 11 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅))
8380, 82ssexd 5192 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ V)
8466, 74, 76, 83fvmptd 6752 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) = {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
85 ssfi 8722 . . . . . . . . . 10 ((((0...𝑘) ↑m 𝑅) ∈ Fin ∧ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ⊆ ((0...𝑘) ↑m 𝑅)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8679, 81, 85sylancl 589 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8786adantr 484 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} ∈ Fin)
8884, 87eqeltrd 2890 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
8988adantr 484 . . . . . 6 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → ((𝐶𝑅)‘𝑘) ∈ Fin)
9075faccld 13640 . . . . . . . . . . 11 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℕ)
9190nncnd 11641 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → (!‘𝑘) ∈ ℂ)
9291ad2antlr 726 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (!‘𝑘) ∈ ℂ)
936adantr 484 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
9493adantlr 714 . . . . . . . . . 10 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
95 elfznn0 12995 . . . . . . . . . . . . . . 15 (𝑧 ∈ (0...𝑘) → 𝑧 ∈ ℕ0)
9695ssriv 3919 . . . . . . . . . . . . . 14 (0...𝑘) ⊆ ℕ0
9796a1i 11 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ ℕ0)
98 simpr 488 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((𝐶𝑅)‘𝑘))
9984eleq2d 2875 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10099adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (𝑐 ∈ ((𝐶𝑅)‘𝑘) ↔ 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘}))
10198, 100mpbid 235 . . . . . . . . . . . . . . . . 17 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘})
10281sseli 3911 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ {𝑐 ∈ ((0...𝑘) ↑m 𝑅) ∣ Σ𝑡𝑅 (𝑐𝑡) = 𝑘} → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
103101, 102syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐 ∈ ((0...𝑘) ↑m 𝑅))
104 elmapi 8411 . . . . . . . . . . . . . . . 16 (𝑐 ∈ ((0...𝑘) ↑m 𝑅) → 𝑐:𝑅⟶(0...𝑘))
105103, 104syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑐:𝑅⟶(0...𝑘))
106105adantr 484 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑐:𝑅⟶(0...𝑘))
107 simpr 488 . . . . . . . . . . . . . 14 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑅)
108106, 107ffvelrnd 6829 . . . . . . . . . . . . 13 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑘))
10997, 108sseldd 3916 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
110109faccld 13640 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
111110nncnd 11641 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
11294, 111fprodcl 15298 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
113110nnne0d 11675 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ≠ 0)
11494, 111, 113fprodn0 15325 . . . . . . . . 9 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
11592, 112, 114divcld 11405 . . . . . . . 8 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
116115adantlr 714 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
11794adantlr 714 . . . . . . . 8 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → 𝑅 ∈ Fin)
11821ad4antr 731 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝜑)
119118, 13sylancom 591 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑡𝑇)
120 elfzuz3 12899 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ (ℤ𝑘))
121 fzss2 12942 . . . . . . . . . . . . . . . 16 (𝐽 ∈ (ℤ𝑘) → (0...𝑘) ⊆ (0...𝐽))
122120, 121syl 17 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0...𝑘) ⊆ (0...𝐽))
123122adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝐽))
12445nn0zd 12073 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽 ∈ ℤ)
125 dvnprodlem2.n . . . . . . . . . . . . . . . . . . 19 (𝜑𝑁 ∈ ℕ0)
126125nn0zd 12073 . . . . . . . . . . . . . . . . . 18 (𝜑𝑁 ∈ ℤ)
127 elfzle2 12906 . . . . . . . . . . . . . . . . . . 19 (𝐽 ∈ (0...𝑁) → 𝐽𝑁)
12843, 127syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑𝐽𝑁)
129124, 126, 1283jca 1125 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
130 eluz2 12237 . . . . . . . . . . . . . . . . 17 (𝑁 ∈ (ℤ𝐽) ↔ (𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁))
131129, 130sylibr 237 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ (ℤ𝐽))
132 fzss2 12942 . . . . . . . . . . . . . . . 16 (𝑁 ∈ (ℤ𝐽) → (0...𝐽) ⊆ (0...𝑁))
133131, 132syl 17 . . . . . . . . . . . . . . 15 (𝜑 → (0...𝐽) ⊆ (0...𝑁))
134133adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝐽) ⊆ (0...𝑁))
135123, 134sstrd 3925 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → (0...𝑘) ⊆ (0...𝑁))
136135ad2antrr 725 . . . . . . . . . . . 12 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (0...𝑘) ⊆ (0...𝑁))
137136, 108sseldd 3916 . . . . . . . . . . 11 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
138137adantllr 718 . . . . . . . . . 10 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
139 fvex 6658 . . . . . . . . . . 11 (𝑐𝑡) ∈ V
140 eleq1 2877 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑡) ∈ (0...𝑁)))
1411403anbi3d 1439 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁))))
142 fveq2 6645 . . . . . . . . . . . . 13 (𝑗 = (𝑐𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
143142feq1d 6472 . . . . . . . . . . . 12 (𝑗 = (𝑐𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ))
144141, 143imbi12d 348 . . . . . . . . . . 11 (𝑗 = (𝑐𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)))
145 dvnprodlem2.dvnh . . . . . . . . . . 11 ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ)
146139, 144, 145vtocl 3507 . . . . . . . . . 10 ((𝜑𝑡𝑇 ∧ (𝑐𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
147118, 119, 138, 146syl3anc 1368 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
148 simpllr 775 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → 𝑥𝑋)
149147, 148ffvelrnd 6829 . . . . . . . 8 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
150117, 149fprodcl 15298 . . . . . . 7 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
151116, 150mulcld 10650 . . . . . 6 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
15289, 151fsumcl 15082 . . . . 5 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
153152fmpttd 6856 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ)
154 dvnprodlem2.ind . . . . . . 7 (𝜑 → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
155154adantr 484 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → ∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
156 0zd 11981 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ∈ ℤ)
157126adantr 484 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℤ)
158 elfzelz 12902 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℤ)
159158adantl 485 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℤ)
160156, 157, 1593jca 1125 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → (0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ))
161 elfzle1 12905 . . . . . . . . 9 (𝑘 ∈ (0...𝐽) → 0 ≤ 𝑘)
162161adantl 485 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 0 ≤ 𝑘)
163159zred 12075 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ ℝ)
16445nn0red 11944 . . . . . . . . . 10 (𝜑𝐽 ∈ ℝ)
165164adantr 484 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
166157zred 12075 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑁 ∈ ℝ)
167 elfzle2 12906 . . . . . . . . . 10 (𝑘 ∈ (0...𝐽) → 𝑘𝐽)
168167adantl 485 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝐽)
169128adantr 484 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽𝑁)
170163, 165, 166, 168, 169letrd 10786 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘𝑁)
171160, 162, 170jca32 519 . . . . . . 7 ((𝜑𝑘 ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (0 ≤ 𝑘𝑘𝑁)))
172 elfz2 12892 . . . . . . 7 (𝑘 ∈ (0...𝑁) ↔ ((0 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) ∧ (0 ≤ 𝑘𝑘𝑁)))
173171, 172sylibr 237 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑘 ∈ (0...𝑁))
174 rspa 3171 . . . . . 6 ((∀𝑘 ∈ (0...𝑁)((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
175155, 173, 174syl2anc 587 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
176175feq1d 6472 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))):𝑋⟶ℂ))
177153, 176mpbird 260 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘):𝑋⟶ℂ)
17823adantr 484 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → 𝑍𝑇)
179 simpl 486 . . . . . 6 ((𝜑𝑘 ∈ (0...𝐽)) → 𝜑)
180179, 178, 1733jca 1125 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → (𝜑𝑍𝑇𝑘 ∈ (0...𝑁)))
181263anbi2d 1438 . . . . . . 7 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑘 ∈ (0...𝑁))))
18219oveq2d 7151 . . . . . . . . 9 (𝑡 = 𝑍 → (𝑆 D𝑛 (𝐻𝑡)) = (𝑆 D𝑛 (𝐻𝑍)))
183182fveq1d 6647 . . . . . . . 8 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
184183feq1d 6472 . . . . . . 7 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
185181, 184imbi12d 348 . . . . . 6 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)))
186 eleq1 2877 . . . . . . . . 9 (𝑗 = 𝑘 → (𝑗 ∈ (0...𝑁) ↔ 𝑘 ∈ (0...𝑁)))
1871863anbi3d 1439 . . . . . . . 8 (𝑗 = 𝑘 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇𝑘 ∈ (0...𝑁))))
188 fveq2 6645 . . . . . . . . 9 (𝑗 = 𝑘 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘𝑘))
189188feq1d 6472 . . . . . . . 8 (𝑗 = 𝑘 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ))
190187, 189imbi12d 348 . . . . . . 7 (𝑗 = 𝑘 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)))
191190, 145chvarvv 2005 . . . . . 6 ((𝜑𝑡𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑘):𝑋⟶ℂ)
192185, 191vtoclg 3515 . . . . 5 (𝑍𝑇 → ((𝜑𝑍𝑇𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
193178, 180, 192sylc 65 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ)
19432feqmptd 6708 . . . . . . . . 9 (𝜑 → (𝐻𝑍) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
195194eqcomd 2804 . . . . . . . 8 (𝜑 → (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)) = (𝐻𝑍))
196195oveq2d 7151 . . . . . . 7 (𝜑 → (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))) = (𝑆 D𝑛 (𝐻𝑍)))
197196fveq1d 6647 . . . . . 6 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
198197adantr 484 . . . . 5 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑘))
199198feq1d 6472 . . . 4 ((𝜑𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ))
200193, 199mpbird 260 . . 3 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘):𝑋⟶ℂ)
201 fveq2 6645 . . . . . . . 8 (𝑦 = 𝑥 → ((𝐻𝑡)‘𝑦) = ((𝐻𝑡)‘𝑥))
202201prodeq2ad 42234 . . . . . . 7 (𝑦 = 𝑥 → ∏𝑡𝑅 ((𝐻𝑡)‘𝑦) = ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
203202cbvmptv 5133 . . . . . 6 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)) = (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥))
204203oveq2i 7146 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))
205204fveq1i 6646 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘)
206205mpteq2i 5122 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
207 fveq2 6645 . . . . . . 7 (𝑦 = 𝑥 → ((𝐻𝑍)‘𝑦) = ((𝐻𝑍)‘𝑥))
208207cbvmptv 5133 . . . . . 6 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)) = (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥))
209208oveq2i 7146 . . . . 5 (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))
210209fveq1i 6646 . . . 4 ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘)
211210mpteq2i 5122 . . 3 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑥𝑋 ↦ ((𝐻𝑍)‘𝑥)))‘𝑘))
21240, 41, 42, 35, 45, 46, 47, 177, 200, 206, 211dvnmul 42585 . 2 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ (∏𝑡𝑅 ((𝐻𝑡)‘𝑥) · ((𝐻𝑍)‘𝑥))))‘𝐽) = (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))))
213205a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘))
214154r19.21bi 3173 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
215179, 173, 214syl2anc 587 . . . . . . . . . . . . . 14 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑥)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
216213, 215eqtrd 2833 . . . . . . . . . . . . 13 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
217216mpteq2dva 5125 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘)) = (𝑘 ∈ (0...𝐽) ↦ (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))))
218 mptexg 6961 . . . . . . . . . . . . . 14 (𝑋 ∈ ((TopOpen‘ℂfld) ↾t 𝑆) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
21941, 218syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
220219adantr 484 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) ∈ V)
221217, 220fvmpt2d 6758 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
222221adantlr 714 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
223222fveq1d 6647 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥))
22434adantr 484 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → 𝑥𝑋)
225152an32s 651 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
226 eqid 2798 . . . . . . . . . . 11 (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
227226fvmpt2 6756 . . . . . . . . . 10 ((𝑥𝑋 ∧ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
228224, 225, 227syl2anc 587 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
229223, 228eqtrd 2833 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
230 fveq2 6645 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘) = ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
231230cbvmptv 5133 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗))
232231a1i 11 . . . . . . . . . . . . 13 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)))
233209, 196syl5eq 2845 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦))) = (𝑆 D𝑛 (𝐻𝑍)))
234233fveq1d 6647 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
235234mpteq2dv 5126 . . . . . . . . . . . . 13 (𝜑 → (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑗)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
236232, 235eqtrd 2833 . . . . . . . . . . . 12 (𝜑 → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
237236adantr 484 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘)) = (𝑗 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗)))
238 fveq2 6645 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
239238adantl 485 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑗 = (𝐽𝑘)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
240 0zd 11981 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 0 ∈ ℤ)
241 elfzel2 12900 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℤ)
242241, 158zsubcld 12080 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ∈ ℤ)
243240, 241, 2423jca 1125 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ))
244241zred 12075 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝐽 ∈ ℝ)
24575nn0red 11944 . . . . . . . . . . . . . . . 16 (𝑘 ∈ (0...𝐽) → 𝑘 ∈ ℝ)
246244, 245subge0d 11219 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ (𝐽𝑘) ↔ 𝑘𝐽))
247167, 246mpbird 260 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → 0 ≤ (𝐽𝑘))
248244, 245subge02d 11221 . . . . . . . . . . . . . . 15 (𝑘 ∈ (0...𝐽) → (0 ≤ 𝑘 ↔ (𝐽𝑘) ≤ 𝐽))
249161, 248mpbid 235 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝐽𝑘) ≤ 𝐽)
250243, 247, 249jca32 519 . . . . . . . . . . . . 13 (𝑘 ∈ (0...𝐽) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
251250adantl 485 . . . . . . . . . . . 12 ((𝜑𝑘 ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
252 elfz2 12892 . . . . . . . . . . . 12 ((𝐽𝑘) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽𝑘) ∈ ℤ) ∧ (0 ≤ (𝐽𝑘) ∧ (𝐽𝑘) ≤ 𝐽)))
253251, 252sylibr 237 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽𝑘) ∈ (0...𝐽))
254 fvex 6658 . . . . . . . . . . . 12 ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V
255254a1i 11 . . . . . . . . . . 11 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)) ∈ V)
256237, 239, 253, 255fvmptd 6752 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
257256adantlr 714 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
258257fveq1d 6647 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
259229, 258oveq12d 7153 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)) = (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
260259oveq2d 7151 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
26188adantlr 714 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ∈ Fin)
262 ovex 7168 . . . . . . . . . . . 12 (𝐽𝑘) ∈ V
263 eleq1 2877 . . . . . . . . . . . . . 14 (𝑗 = (𝐽𝑘) → (𝑗 ∈ (0...𝐽) ↔ (𝐽𝑘) ∈ (0...𝐽)))
264263anbi2d 631 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → ((𝜑𝑗 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽))))
265238feq1d 6472 . . . . . . . . . . . . 13 (𝑗 = (𝐽𝑘) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ))
266264, 265imbi12d 348 . . . . . . . . . . . 12 (𝑗 = (𝐽𝑘) → (((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)))
267 eleq1 2877 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → (𝑘 ∈ (0...𝐽) ↔ 𝑗 ∈ (0...𝐽)))
268267anbi2d 631 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → ((𝜑𝑘 ∈ (0...𝐽)) ↔ (𝜑𝑗 ∈ (0...𝐽))))
269 fveq2 6645 . . . . . . . . . . . . . . 15 (𝑘 = 𝑗 → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
270269feq1d 6472 . . . . . . . . . . . . . 14 (𝑘 = 𝑗 → (((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
271268, 270imbi12d 348 . . . . . . . . . . . . 13 (𝑘 = 𝑗 → (((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑘):𝑋⟶ℂ) ↔ ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
272271, 193chvarvv 2005 . . . . . . . . . . . 12 ((𝜑𝑗 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
273262, 266, 272vtocl 3507 . . . . . . . . . . 11 ((𝜑 ∧ (𝐽𝑘) ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
274179, 253, 273syl2anc 587 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
275274adantlr 714 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)):𝑋⟶ℂ)
276275, 224ffvelrnd 6829 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
277 anass 472 . . . . . . . . . . . 12 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ (𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)))
278 ancom 464 . . . . . . . . . . . . . 14 ((𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋) ↔ (𝑥𝑋𝑘 ∈ (0...𝐽)))
279278anbi2i 625 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
280 anass 472 . . . . . . . . . . . . . 14 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ↔ (𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))))
281280bicomi 227 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥𝑋𝑘 ∈ (0...𝐽))) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
282279, 281bitri 278 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑥𝑋)) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
283277, 282bitri 278 . . . . . . . . . . 11 (((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ↔ ((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)))
284283anbi1i 626 . . . . . . . . . 10 ((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) ↔ (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)))
285284imbi1i 353 . . . . . . . . 9 (((((𝜑𝑘 ∈ (0...𝐽)) ∧ 𝑥𝑋) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ) ↔ ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ))
286151, 285mpbi 233 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) ∈ ℂ)
287261, 276, 286fsummulc1 15132 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
288287oveq2d 7151 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · (Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)(((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
289179, 45syl 17 . . . . . . . . . 10 ((𝜑𝑘 ∈ (0...𝐽)) → 𝐽 ∈ ℕ0)
290289, 159bccld 41947 . . . . . . . . 9 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℕ0)
291290nn0cnd 11945 . . . . . . . 8 ((𝜑𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
292291adantlr 714 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → (𝐽C𝑘) ∈ ℂ)
293276adantr 484 . . . . . . . 8 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥) ∈ ℂ)
294286, 293mulcld 10650 . . . . . . 7 ((((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘)) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
295261, 292, 294fsummulc2 15131 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
296260, 288, 2953eqtrd 2837 . . . . 5 (((𝜑𝑥𝑋) ∧ 𝑘 ∈ (0...𝐽)) → ((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
297296sumeq2dv 15052 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
298 vex 3444 . . . . . . . 8 𝑘 ∈ V
299 vex 3444 . . . . . . . 8 𝑐 ∈ V
300298, 299op1std 7681 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (1st𝑝) = 𝑘)
301300oveq2d 7151 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽C(1st𝑝)) = (𝐽C𝑘))
302300fveq2d 6649 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘(1st𝑝)) = (!‘𝑘))
303298, 299op2ndd 7682 . . . . . . . . . . . 12 (𝑝 = ⟨𝑘, 𝑐⟩ → (2nd𝑝) = 𝑐)
304303fveq1d 6647 . . . . . . . . . . 11 (𝑝 = ⟨𝑘, 𝑐⟩ → ((2nd𝑝)‘𝑡) = (𝑐𝑡))
305304fveq2d 6649 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘(𝑐𝑡)))
306305prodeq2ad 42234 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡)))
307302, 306oveq12d 7153 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
308304fveq2d 6649 . . . . . . . . . 10 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
309308fveq1d 6647 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
310309prodeq2ad 42234 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
311307, 310oveq12d 7153 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
312300oveq2d 7151 . . . . . . . . 9 (𝑝 = ⟨𝑘, 𝑐⟩ → (𝐽 − (1st𝑝)) = (𝐽𝑘))
313312fveq2d 6649 . . . . . . . 8 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘)))
314313fveq1d 6647 . . . . . . 7 (𝑝 = ⟨𝑘, 𝑐⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))
315311, 314oveq12d 7153 . . . . . 6 (𝑝 = ⟨𝑘, 𝑐⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)))
316301, 315oveq12d 7153 . . . . 5 (𝑝 = ⟨𝑘, 𝑐⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))))
317 fzfid 13336 . . . . 5 ((𝜑𝑥𝑋) → (0...𝐽) ∈ Fin)
318292adantrr 716 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → (𝐽C𝑘) ∈ ℂ)
319294anasss 470 . . . . . 6 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥)) ∈ ℂ)
320318, 319mulcld 10650 . . . . 5 (((𝜑𝑥𝑋) ∧ (𝑘 ∈ (0...𝐽) ∧ 𝑐 ∈ ((𝐶𝑅)‘𝑘))) → ((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) ∈ ℂ)
321316, 317, 261, 320fsum2d 15118 . . . 4 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽𝑐 ∈ ((𝐶𝑅)‘𝑘)((𝐽C𝑘) · ((((!‘𝑘) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽𝑘))‘𝑥))) = Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))))
322 ovex 7168 . . . . . . . . 9 (𝐽 − (𝑐𝑍)) ∈ V
323299resex 5866 . . . . . . . . 9 (𝑐𝑅) ∈ V
324322, 323op1std 7681 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (1st𝑝) = (𝐽 − (𝑐𝑍)))
325324oveq2d 7151 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽C(1st𝑝)) = (𝐽C(𝐽 − (𝑐𝑍))))
326324fveq2d 6649 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘(1st𝑝)) = (!‘(𝐽 − (𝑐𝑍))))
327322, 323op2ndd 7682 . . . . . . . . . . . . 13 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (2nd𝑝) = (𝑐𝑅))
328327fveq1d 6647 . . . . . . . . . . . 12 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((2nd𝑝)‘𝑡) = ((𝑐𝑅)‘𝑡))
329328fveq2d 6649 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (!‘((2nd𝑝)‘𝑡)) = (!‘((𝑐𝑅)‘𝑡)))
330329prodeq2ad 42234 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) = ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)))
331326, 330oveq12d 7153 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))))
332328fveq2d 6649 . . . . . . . . . . 11 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)))
333332fveq1d 6647 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
334333prodeq2ad 42234 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥))
335331, 334oveq12d 7153 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)))
336324oveq2d 7151 . . . . . . . . . 10 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (𝐽 − (1st𝑝)) = (𝐽 − (𝐽 − (𝑐𝑍))))
337336fveq2d 6649 . . . . . . . . 9 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))))
338337fveq1d 6647 . . . . . . . 8 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))
339335, 338oveq12d 7153 . . . . . . 7 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) = ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)))
340325, 339oveq12d 7153 . . . . . 6 (𝑝 = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
341 oveq2 7143 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → ((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})))
342 rabeq 3431 . . . . . . . . . . . . 13 (((0...𝑛) ↑m 𝑠) = ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
343341, 342syl 17 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛})
344 sumeq1 15037 . . . . . . . . . . . . . 14 (𝑠 = (𝑅 ∪ {𝑍}) → Σ𝑡𝑠 (𝑐𝑡) = Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡))
345344eqeq1d 2800 . . . . . . . . . . . . 13 (𝑠 = (𝑅 ∪ {𝑍}) → (Σ𝑡𝑠 (𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛))
346345rabbidv 3427 . . . . . . . . . . . 12 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
347343, 346eqtrd 2833 . . . . . . . . . . 11 (𝑠 = (𝑅 ∪ {𝑍}) → {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
348347mpteq2dv 5126 . . . . . . . . . 10 (𝑠 = (𝑅 ∪ {𝑍}) → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m 𝑠) ∣ Σ𝑡𝑠 (𝑐𝑡) = 𝑛}) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
34923snssd 4702 . . . . . . . . . . . 12 (𝜑 → {𝑍} ⊆ 𝑇)
3504, 349unssd 4113 . . . . . . . . . . 11 (𝜑 → (𝑅 ∪ {𝑍}) ⊆ 𝑇)
3513, 350ssexd 5192 . . . . . . . . . . . 12 (𝜑 → (𝑅 ∪ {𝑍}) ∈ V)
352 elpwg 4500 . . . . . . . . . . . 12 ((𝑅 ∪ {𝑍}) ∈ V → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
353351, 352syl 17 . . . . . . . . . . 11 (𝜑 → ((𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇 ↔ (𝑅 ∪ {𝑍}) ⊆ 𝑇))
354350, 353mpbird 260 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ 𝒫 𝑇)
35563mptex 6963 . . . . . . . . . . 11 (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V
356355a1i 11 . . . . . . . . . 10 (𝜑 → (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}) ∈ V)
35748, 348, 354, 356fvmptd3 6768 . . . . . . . . 9 (𝜑 → (𝐶‘(𝑅 ∪ {𝑍})) = (𝑛 ∈ ℕ0 ↦ {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛}))
358 oveq2 7143 . . . . . . . . . . . . 13 (𝑛 = 𝐽 → (0...𝑛) = (0...𝐽))
359358oveq1d 7150 . . . . . . . . . . . 12 (𝑛 = 𝐽 → ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
360 rabeq 3431 . . . . . . . . . . . 12 (((0...𝑛) ↑m (𝑅 ∪ {𝑍})) = ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
361359, 360syl 17 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛})
362 eqeq2 2810 . . . . . . . . . . . 12 (𝑛 = 𝐽 → (Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛 ↔ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽))
363362rabbidv 3427 . . . . . . . . . . 11 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
364361, 363eqtrd 2833 . . . . . . . . . 10 (𝑛 = 𝐽 → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
365364adantl 485 . . . . . . . . 9 ((𝜑𝑛 = 𝐽) → {𝑐 ∈ ((0...𝑛) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝑛} = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
366 ovex 7168 . . . . . . . . . . 11 ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ V
367366rabex 5199 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V
368367a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ V)
369357, 365, 45, 368fvmptd 6752 . . . . . . . 8 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
370 fzfid 13336 . . . . . . . . . 10 (𝜑 → (0...𝐽) ∈ Fin)
371 snfi 8577 . . . . . . . . . . . 12 {𝑍} ∈ Fin
372371a1i 11 . . . . . . . . . . 11 (𝜑 → {𝑍} ∈ Fin)
373 unfi 8769 . . . . . . . . . . 11 ((𝑅 ∈ Fin ∧ {𝑍} ∈ Fin) → (𝑅 ∪ {𝑍}) ∈ Fin)
3746, 372, 373syl2anc 587 . . . . . . . . . 10 (𝜑 → (𝑅 ∪ {𝑍}) ∈ Fin)
375 mapfi 8804 . . . . . . . . . 10 (((0...𝐽) ∈ Fin ∧ (𝑅 ∪ {𝑍}) ∈ Fin) → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
376370, 374, 375syl2anc 587 . . . . . . . . 9 (𝜑 → ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin)
377 ssrab2 4007 . . . . . . . . . 10 {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))
378377a1i 11 . . . . . . . . 9 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
379 ssfi 8722 . . . . . . . . 9 ((((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∈ Fin ∧ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ⊆ ((0...𝐽) ↑m (𝑅 ∪ {𝑍}))) → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
380376, 378, 379syl2anc 587 . . . . . . . 8 (𝜑 → {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} ∈ Fin)
381369, 380eqeltrd 2890 . . . . . . 7 (𝜑 → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
382381adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∈ Fin)
383 dvnprodlem2.d . . . . . . . 8 𝐷 = (𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ↦ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
38448, 45, 383, 3, 23, 10, 350dvnprodlem1 42588 . . . . . . 7 (𝜑𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
385384adantr 484 . . . . . 6 ((𝜑𝑥𝑋) → 𝐷:((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)–1-1-onto 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
386 simpr 488 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
387 opex 5321 . . . . . . . . 9 ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V
388387a1i 11 . . . . . . . 8 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V)
389383fvmpt2 6756 . . . . . . . 8 ((𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) ∧ ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩ ∈ V) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
390386, 388, 389syl2anc 587 . . . . . . 7 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
391390adantlr 714 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐷𝑐) = ⟨(𝐽 − (𝑐𝑍)), (𝑐𝑅)⟩)
39245adantr 484 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝐽 ∈ ℕ0)
393 eliun 4885 . . . . . . . . . . . . . 14 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) ↔ ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
394393biimpi 219 . . . . . . . . . . . . 13 (𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
395394adantl 485 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)))
396 nfv 1915 . . . . . . . . . . . . . 14 𝑘𝜑
397 nfcv 2955 . . . . . . . . . . . . . . 15 𝑘𝑝
398 nfiu1 4915 . . . . . . . . . . . . . . 15 𝑘 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
399397, 398nfel 2969 . . . . . . . . . . . . . 14 𝑘 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))
400396, 399nfan 1900 . . . . . . . . . . . . 13 𝑘(𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘)))
401 nfv 1915 . . . . . . . . . . . . 13 𝑘(1st𝑝) ∈ (0...𝐽)
402 xp1st 7703 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ {𝑘})
403 elsni 4542 . . . . . . . . . . . . . . . . . 18 ((1st𝑝) ∈ {𝑘} → (1st𝑝) = 𝑘)
404402, 403syl 17 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) = 𝑘)
405404adantl 485 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) = 𝑘)
406 simpl 486 . . . . . . . . . . . . . . . 16 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑘 ∈ (0...𝐽))
407405, 406eqeltrd 2890 . . . . . . . . . . . . . . 15 ((𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
408407ex 416 . . . . . . . . . . . . . 14 (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
409408a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽))))
410400, 401, 409rexlimd 3276 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (1st𝑝) ∈ (0...𝐽)))
411395, 410mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
412 elfzelz 12902 . . . . . . . . . . 11 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℤ)
413411, 412syl 17 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℤ)
414392, 413bccld 41947 . . . . . . . . 9 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℕ0)
415414nn0cnd 11945 . . . . . . . 8 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
416415adantlr 714 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽C(1st𝑝)) ∈ ℂ)
417 elfznn0 12995 . . . . . . . . . . . . . 14 ((1st𝑝) ∈ (0...𝐽) → (1st𝑝) ∈ ℕ0)
418411, 417syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ ℕ0)
419418faccld 13640 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℕ)
420419nncnd 11641 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
421420adantlr 714 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (!‘(1st𝑝)) ∈ ℂ)
4226adantr 484 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
423 nfv 1915 . . . . . . . . . . . . . . . 16 𝑘(2nd𝑝):𝑅⟶(0...𝐽)
42484, 82eqsstrd 3953 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝑘) ↑m 𝑅))
425 ovex 7168 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0...𝐽) ∈ V
426425a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑘 ∈ (0...𝐽) → (0...𝐽) ∈ V)
427 mapss 8436 . . . . . . . . . . . . . . . . . . . . . . . 24 (((0...𝐽) ∈ V ∧ (0...𝑘) ⊆ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
428426, 122, 427syl2anc 587 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑘 ∈ (0...𝐽) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
429428adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑘 ∈ (0...𝐽)) → ((0...𝑘) ↑m 𝑅) ⊆ ((0...𝐽) ↑m 𝑅))
430424, 429sstrd 3925 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑘 ∈ (0...𝐽)) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
4314303adant3 1129 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐶𝑅)‘𝑘) ⊆ ((0...𝐽) ↑m 𝑅))
432 xp2nd 7704 . . . . . . . . . . . . . . . . . . . . 21 (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
4334323ad2ant3 1132 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((𝐶𝑅)‘𝑘))
434431, 433sseldd 3916 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅))
435 elmapi 8411 . . . . . . . . . . . . . . . . . . 19 ((2nd𝑝) ∈ ((0...𝐽) ↑m 𝑅) → (2nd𝑝):𝑅⟶(0...𝐽))
436434, 435syl 17 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
4374363exp 1116 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
438437adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽))))
439400, 423, 438rexlimd 3276 . . . . . . . . . . . . . . 15 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (2nd𝑝):𝑅⟶(0...𝐽)))
440395, 439mpd 15 . . . . . . . . . . . . . 14 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (2nd𝑝):𝑅⟶(0...𝐽))
441440ffvelrnda 6828 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝐽))
442 elfznn0 12995 . . . . . . . . . . . . . . 15 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((2nd𝑝)‘𝑡) ∈ ℕ0)
443442faccld 13640 . . . . . . . . . . . . . 14 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
444443nncnd 11641 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
445441, 444syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
446422, 445fprodcl 15298 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
447446adantlr 714 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ∈ ℂ)
448441, 443syl 17 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ∈ ℕ)
449 nnne0 11659 . . . . . . . . . . . . 13 ((!‘((2nd𝑝)‘𝑡)) ∈ ℕ → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
450448, 449syl 17 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (!‘((2nd𝑝)‘𝑡)) ≠ 0)
451422, 445, 450fprodn0 15325 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
452451adantlr 714 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡)) ≠ 0)
453421, 447, 452divcld 11405 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) ∈ ℂ)
4547adantr 484 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑅 ∈ Fin)
455 simpll 766 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝜑)
456455, 13sylancom 591 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑡𝑇)
457455, 133syl 17 . . . . . . . . . . . . . . 15 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
458457, 441sseldd 3916 . . . . . . . . . . . . . 14 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((2nd𝑝)‘𝑡) ∈ (0...𝑁))
459455, 456, 4583jca 1125 . . . . . . . . . . . . 13 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
460 eleq1 2877 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → (𝑗 ∈ (0...𝑁) ↔ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)))
4614603anbi3d 1439 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁))))
462 fveq2 6645 . . . . . . . . . . . . . . . 16 (𝑗 = ((2nd𝑝)‘𝑡) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)))
463462feq1d 6472 . . . . . . . . . . . . . . 15 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
464461, 463imbi12d 348 . . . . . . . . . . . . . 14 (𝑗 = ((2nd𝑝)‘𝑡) → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)))
465464, 145vtoclg 3515 . . . . . . . . . . . . 13 (((2nd𝑝)‘𝑡) ∈ (0...𝐽) → ((𝜑𝑡𝑇 ∧ ((2nd𝑝)‘𝑡) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ))
466441, 459, 465sylc 65 . . . . . . . . . . . 12 (((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
467466adantllr 718 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡)):𝑋⟶ℂ)
46817adantlr 714 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → 𝑥𝑋)
469467, 468ffvelrnd 6829 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
470454, 469fprodcl 15298 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥) ∈ ℂ)
471453, 470mulcld 10650 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) ∈ ℂ)
472 nfv 1915 . . . . . . . . . . . . 13 𝑘(𝐽 − (1st𝑝)) ∈ (0...𝐽)
473 simp1 1133 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
4744073adant1 1127 . . . . . . . . . . . . . . . 16 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (1st𝑝) ∈ (0...𝐽))
475 fznn0sub2 13009 . . . . . . . . . . . . . . . . 17 ((1st𝑝) ∈ (0...𝐽) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
476475adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (1st𝑝) ∈ (0...𝐽)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
477473, 474, 476syl2anc 587 . . . . . . . . . . . . . . 15 ((𝜑𝑘 ∈ (0...𝐽) ∧ 𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
4784773exp 1116 . . . . . . . . . . . . . 14 (𝜑 → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
479478adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝑘 ∈ (0...𝐽) → (𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))))
480400, 472, 479rexlimd 3276 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (∃𝑘 ∈ (0...𝐽)𝑝 ∈ ({𝑘} × ((𝐶𝑅)‘𝑘)) → (𝐽 − (1st𝑝)) ∈ (0...𝐽)))
481395, 480mpd 15 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝐽))
482 simpl 486 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝜑)
483482, 23syl 17 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑍𝑇)
484482, 133syl 17 . . . . . . . . . . . . 13 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (0...𝐽) ⊆ (0...𝑁))
485484, 481sseldd 3916 . . . . . . . . . . . 12 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝐽 − (1st𝑝)) ∈ (0...𝑁))
486482, 483, 4853jca 1125 . . . . . . . . . . 11 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
487 eleq1 2877 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → (𝑗 ∈ (0...𝑁) ↔ (𝐽 − (1st𝑝)) ∈ (0...𝑁)))
4884873anbi3d 1439 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁))))
489 fveq2 6645 . . . . . . . . . . . . . 14 (𝑗 = (𝐽 − (1st𝑝)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))))
490489feq1d 6472 . . . . . . . . . . . . 13 (𝑗 = (𝐽 − (1st𝑝)) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
491488, 490imbi12d 348 . . . . . . . . . . . 12 (𝑗 = (𝐽 − (1st𝑝)) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)))
492 simp2 1134 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → 𝑍𝑇)
493 id 22 . . . . . . . . . . . . 13 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → (𝜑𝑍𝑇𝑗 ∈ (0...𝑁)))
494263anbi2d 1438 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → ((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇𝑗 ∈ (0...𝑁))))
495182fveq1d 6647 . . . . . . . . . . . . . . . 16 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘𝑗))
496495feq1d 6472 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
497494, 496imbi12d 348 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (((𝜑𝑡𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑡))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)))
498497, 145vtoclg 3515 . . . . . . . . . . . . 13 (𝑍𝑇 → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ))
499492, 493, 498sylc 65 . . . . . . . . . . . 12 ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ)
500491, 499vtoclg 3515 . . . . . . . . . . 11 ((𝐽 − (1st𝑝)) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝐽 − (1st𝑝)) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ))
501481, 486, 500sylc 65 . . . . . . . . . 10 ((𝜑𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
502501adantlr 714 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝))):𝑋⟶ℂ)
50334adantr 484 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → 𝑥𝑋)
504502, 503ffvelrnd 6829 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥) ∈ ℂ)
505471, 504mulcld 10650 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥)) ∈ ℂ)
506416, 505mulcld 10650 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))) → ((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) ∈ ℂ)
507340, 382, 385, 391, 506fsumf1o 15072 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))))
508 simpl 486 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝜑)
509369adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽) = {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
510386, 509eleqtrd 2892 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽})
511377sseli 3911 . . . . . . . . . . . . . . 15 (𝑐 ∈ {𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) ∣ Σ𝑡 ∈ (𝑅 ∪ {𝑍})(𝑐𝑡) = 𝐽} → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
512510, 511syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})))
513 elmapi 8411 . . . . . . . . . . . . . 14 (𝑐 ∈ ((0...𝐽) ↑m (𝑅 ∪ {𝑍})) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
514512, 513syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
515 snidg 4559 . . . . . . . . . . . . . . . 16 (𝑍𝑇𝑍 ∈ {𝑍})
51623, 515syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑍 ∈ {𝑍})
517 elun2 4104 . . . . . . . . . . . . . . 15 (𝑍 ∈ {𝑍} → 𝑍 ∈ (𝑅 ∪ {𝑍}))
518516, 517syl 17 . . . . . . . . . . . . . 14 (𝜑𝑍 ∈ (𝑅 ∪ {𝑍}))
519518adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍 ∈ (𝑅 ∪ {𝑍}))
520514, 519ffvelrnd 6829 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝐽))
521 0zd 11981 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ∈ ℤ)
522124adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℤ)
523 fzssz 12904 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℤ
524523sseli 3911 . . . . . . . . . . . . . . . . 17 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℤ)
525524adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℤ)
526522, 525zsubcld 12080 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℤ)
527521, 522, 5263jca 1125 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ))
528 elfzle2 12906 . . . . . . . . . . . . . . . 16 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ≤ 𝐽)
529528adantl 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ≤ 𝐽)
530164adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 𝐽 ∈ ℝ)
531525zred 12075 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝑐𝑍) ∈ ℝ)
532530, 531subge0d 11219 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝐽 − (𝑐𝑍)) ↔ (𝑐𝑍) ≤ 𝐽))
533529, 532mpbird 260 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝐽 − (𝑐𝑍)))
534 elfzle1 12905 . . . . . . . . . . . . . . . 16 ((𝑐𝑍) ∈ (0...𝐽) → 0 ≤ (𝑐𝑍))
535534adantl 485 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → 0 ≤ (𝑐𝑍))
536530, 531subge02d 11221 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (0 ≤ (𝑐𝑍) ↔ (𝐽 − (𝑐𝑍)) ≤ 𝐽))
537535, 536mpbid 235 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ≤ 𝐽)
538527, 533, 537jca32 519 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
539 elfz2 12892 . . . . . . . . . . . . 13 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) ↔ ((0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ (𝐽 − (𝑐𝑍)) ∈ ℤ) ∧ (0 ≤ (𝐽 − (𝑐𝑍)) ∧ (𝐽 − (𝑐𝑍)) ≤ 𝐽)))
540538, 539sylibr 237 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑐𝑍) ∈ (0...𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
541508, 520, 540syl2anc 587 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ (0...𝐽))
542 bcval2 13661 . . . . . . . . . . 11 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
543541, 542syl 17 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))))
544164recnd 10658 . . . . . . . . . . . . . . 15 (𝜑𝐽 ∈ ℂ)
545544adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝐽 ∈ ℂ)
546 zsscn 11977 . . . . . . . . . . . . . . . . 17 ℤ ⊆ ℂ
547523, 546sstri 3924 . . . . . . . . . . . . . . . 16 (0...𝐽) ⊆ ℂ
548547a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ ℂ)
549548, 520sseldd 3916 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℂ)
550545, 549nncand 10991 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝐽 − (𝑐𝑍))) = (𝑐𝑍))
551550fveq2d 6649 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝐽 − (𝑐𝑍)))) = (!‘(𝑐𝑍)))
552551oveq1d 7150 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍)))) = ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍)))))
553552oveq2d 7151 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝐽 − (𝐽 − (𝑐𝑍)))) · (!‘(𝐽 − (𝑐𝑍))))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
55445faccld 13640 . . . . . . . . . . . . . 14 (𝜑 → (!‘𝐽) ∈ ℕ)
555554nncnd 11641 . . . . . . . . . . . . 13 (𝜑 → (!‘𝐽) ∈ ℂ)
556555adantr 484 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
557 elfznn0 12995 . . . . . . . . . . . . . . 15 ((𝑐𝑍) ∈ (0...𝐽) → (𝑐𝑍) ∈ ℕ0)
558520, 557syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ ℕ0)
559558faccld 13640 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℕ)
560559nncnd 11641 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
561 elfznn0 12995 . . . . . . . . . . . . . . 15 ((𝐽 − (𝑐𝑍)) ∈ (0...𝐽) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
562541, 561syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽 − (𝑐𝑍)) ∈ ℕ0)
563562faccld 13640 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℕ)
564563nncnd 11641 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
565559nnne0d 11675 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
566563nnne0d 11675 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
567556, 560, 564, 565, 566divdiv1d 11436 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) = ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))))
568567eqcomd 2804 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / ((!‘(𝑐𝑍)) · (!‘(𝐽 − (𝑐𝑍))))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
569543, 553, 5683eqtrd 2837 . . . . . . . . 9 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
570569adantlr 714 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝐽C(𝐽 − (𝑐𝑍))) = (((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))))
571 fvres 6664 . . . . . . . . . . . . . . . . 17 (𝑡𝑅 → ((𝑐𝑅)‘𝑡) = (𝑐𝑡))
572571fveq2d 6649 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → (!‘((𝑐𝑅)‘𝑡)) = (!‘(𝑐𝑡)))
573572prodeq2i 15265 . . . . . . . . . . . . . . 15 𝑡𝑅 (!‘((𝑐𝑅)‘𝑡)) = ∏𝑡𝑅 (!‘(𝑐𝑡))
574573oveq2i 7146 . . . . . . . . . . . . . 14 ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) = ((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡)))
575571fveq2d 6649 . . . . . . . . . . . . . . . 16 (𝑡𝑅 → ((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡)) = ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)))
576575fveq1d 6647 . . . . . . . . . . . . . . 15 (𝑡𝑅 → (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
577576prodeq2i 15265 . . . . . . . . . . . . . 14 𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥) = ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)
578574, 577oveq12i 7147 . . . . . . . . . . . . 13 (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
579578a1i 11 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
580579adantlr 714 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
581564adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ∈ ℂ)
582508, 6syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
58375ssriv 3919 . . . . . . . . . . . . . . . . . 18 (0...𝐽) ⊆ ℕ0
584583a1i 11 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ ℕ0)
585514adantr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝐽))
586 elun1 4103 . . . . . . . . . . . . . . . . . . 19 (𝑡𝑅𝑡 ∈ (𝑅 ∪ {𝑍}))
587586adantl 485 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡 ∈ (𝑅 ∪ {𝑍}))
588585, 587ffvelrnd 6829 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝐽))
589584, 588sseldd 3916 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ ℕ0)
590589faccld 13640 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℕ)
591590nncnd 11641 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (!‘(𝑐𝑡)) ∈ ℂ)
592582, 591fprodcl 15298 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
593592adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℂ)
5947adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑅 ∈ Fin)
595508adantr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝜑)
596508, 13sylan 583 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑡𝑇)
597595, 133syl 17 . . . . . . . . . . . . . . . . 17 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (0...𝐽) ⊆ (0...𝑁))
598597, 588sseldd 3916 . . . . . . . . . . . . . . . 16 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (𝑐𝑡) ∈ (0...𝑁))
599595, 596, 598, 146syl3anc 1368 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
600599adantllr 718 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
60117adantlr 714 . . . . . . . . . . . . . 14 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → 𝑥𝑋)
602600, 601ffvelrnd 6829 . . . . . . . . . . . . 13 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡𝑅) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
603594, 602fprodcl 15298 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
604582, 590fprodnncl 15301 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ)
605 nnne0 11659 . . . . . . . . . . . . . 14 (∏𝑡𝑅 (!‘(𝑐𝑡)) ∈ ℕ → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
606604, 605syl 17 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
607606adantlr 714 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡𝑅 (!‘(𝑐𝑡)) ≠ 0)
608581, 593, 603, 607div32d 11428 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
609580, 608eqtrd 2833 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
610550fveq2d 6649 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍)))) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
611610fveq1d 6647 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
612611adantlr 714 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
613609, 612oveq12d 7153 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
614603, 593, 607divcld 11405 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) ∈ ℂ)
615508, 23syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
616508, 133syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (0...𝐽) ⊆ (0...𝑁))
617616, 520sseldd 3916 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑐𝑍) ∈ (0...𝑁))
618508, 615, 6173jca 1125 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)))
619 eleq1 2877 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → (𝑗 ∈ (0...𝑁) ↔ (𝑐𝑍) ∈ (0...𝑁)))
6206193anbi3d 1439 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → ((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) ↔ (𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁))))
621 fveq2 6645 . . . . . . . . . . . . . . . 16 (𝑗 = (𝑐𝑍) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
622621feq1d 6472 . . . . . . . . . . . . . . 15 (𝑗 = (𝑐𝑍) → (((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ ↔ ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
623620, 622imbi12d 348 . . . . . . . . . . . . . 14 (𝑗 = (𝑐𝑍) → (((𝜑𝑍𝑇𝑗 ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘𝑗):𝑋⟶ℂ) ↔ ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)))
624623, 499vtoclg 3515 . . . . . . . . . . . . 13 ((𝑐𝑍) ∈ (0...𝐽) → ((𝜑𝑍𝑇 ∧ (𝑐𝑍) ∈ (0...𝑁)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ))
625520, 618, 624sylc 65 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
626625adantlr 714 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)):𝑋⟶ℂ)
62734adantr 484 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑥𝑋)
628626, 627ffvelrnd 6829 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥) ∈ ℂ)
629581, 614, 628mulassd 10653 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘(𝐽 − (𝑐𝑍))) · (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
630613, 629eqtrd 2833 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥)) = ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
631570, 630oveq12d 7153 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))))
632555ad2antrr 725 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘𝐽) ∈ ℂ)
633560adantlr 714 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ∈ ℂ)
634565adantlr 714 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝑐𝑍)) ≠ 0)
635632, 633, 634divcld 11405 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘𝐽) / (!‘(𝑐𝑍))) ∈ ℂ)
636614, 628mulcld 10650 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) ∈ ℂ)
637566adantlr 714 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (!‘(𝐽 − (𝑐𝑍))) ≠ 0)
638635, 581, 636, 637dmmcand 41945 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((((!‘𝐽) / (!‘(𝑐𝑍))) / (!‘(𝐽 − (𝑐𝑍)))) · ((!‘(𝐽 − (𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))))
639603, 628, 593, 607div23d 11442 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
640639eqcomd 2804 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
641 nfv 1915 . . . . . . . . . . . . 13 𝑡((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
642 nfcv 2955 . . . . . . . . . . . . 13 𝑡(((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)
643615adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑍𝑇)
64411adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
645 fveq2 6645 . . . . . . . . . . . . . . 15 (𝑡 = 𝑍 → (𝑐𝑡) = (𝑐𝑍))
646182, 645fveq12d 6652 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)) = ((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍)))
647646fveq1d 6647 . . . . . . . . . . . . 13 (𝑡 = 𝑍 → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))
648641, 642, 594, 643, 644, 602, 647, 628fprodsplitsn 15335 . . . . . . . . . . . 12 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) = (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)))
649648eqcomd 2804 . . . . . . . . . . 11 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))
650649oveq1d 7150 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) / ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
651640, 650eqtrd 2833 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥)) = (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))))
652651oveq2d 7151 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))))
653594, 371, 373sylancl 589 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
654508adantr 484 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝜑)
655350sselda 3915 . . . . . . . . . . . . . 14 ((𝜑𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
656655adantlr 714 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑡𝑇)
657514, 616fssd 6502 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → 𝑐:(𝑅 ∪ {𝑍})⟶(0...𝑁))
658657ffvelrnda 6828 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝑁))
659654, 656, 658, 146syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
660659adantllr 718 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → ((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡)):𝑋⟶ℂ)
661627adantr 484 . . . . . . . . . . 11 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → 𝑥𝑋)
662660, 661ffvelrnd 6829 . . . . . . . . . 10 ((((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
663653, 662fprodcl 15298 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) ∈ ℂ)
664632, 633, 663, 593, 634, 607divmuldivd 11446 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · (∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))))
665560, 592mulcomd 10651 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
666 nfv 1915 . . . . . . . . . . . . . 14 𝑡(𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽))
667 nfcv 2955 . . . . . . . . . . . . . 14 𝑡(!‘(𝑐𝑍))
668508, 10syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ¬ 𝑍𝑅)
669645fveq2d 6649 . . . . . . . . . . . . . 14 (𝑡 = 𝑍 → (!‘(𝑐𝑡)) = (!‘(𝑐𝑍)))
670666, 667, 582, 615, 668, 591, 669, 560fprodsplitsn 15335 . . . . . . . . . . . . 13 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) = (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))))
671670eqcomd 2804 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (∏𝑡𝑅 (!‘(𝑐𝑡)) · (!‘(𝑐𝑍))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
672665, 671eqtrd 2833 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡))) = ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)))
673672oveq2d 7151 . . . . . . . . . 10 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
674673adantlr 714 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))))
675508, 374syl 17 . . . . . . . . . . . 12 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (𝑅 ∪ {𝑍}) ∈ Fin)
676583a1i 11 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (0...𝐽) ⊆ ℕ0)
677514ffvelrnda 6828 . . . . . . . . . . . . . . 15 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ (0...𝐽))
678676, 677sseldd 3916 . . . . . . . . . . . . . 14 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (𝑐𝑡) ∈ ℕ0)
679678faccld 13640 . . . . . . . . . . . . 13 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℕ)
680679nncnd 11641 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ∈ ℂ)
681675, 680fprodcl 15298 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
682681adantlr 714 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ∈ ℂ)
683679nnne0d 11675 . . . . . . . . . . . 12 (((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) ∧ 𝑡 ∈ (𝑅 ∪ {𝑍})) → (!‘(𝑐𝑡)) ≠ 0)
684675, 680, 683fprodn0 15325 . . . . . . . . . . 11 ((𝜑𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
685684adantlr 714 . . . . . . . . . 10 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡)) ≠ 0)
686632, 663, 682, 685div23d 11442 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
687 eqidd 2799 . . . . . . . . 9 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
688674, 686, 6873eqtrd 2837 . . . . . . . 8 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)) / ((!‘(𝑐𝑍)) · ∏𝑡𝑅 (!‘(𝑐𝑡)))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
689652, 664, 6883eqtrd 2837 . . . . . . 7 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → (((!‘𝐽) / (!‘(𝑐𝑍))) · ((∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥) / ∏𝑡𝑅 (!‘(𝑐𝑡))) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝑐𝑍))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
690631, 638, 6893eqtrd 2837 . . . . . 6 (((𝜑𝑥𝑋) ∧ 𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)) → ((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = (((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
691690sumeq2dv 15052 . . . . 5 ((𝜑𝑥𝑋) → Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)((𝐽C(𝐽 − (𝑐𝑍))) · ((((!‘(𝐽 − (𝑐𝑍))) / ∏𝑡𝑅 (!‘((𝑐𝑅)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((𝑐𝑅)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (𝐽 − (𝑐𝑍))))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
692507, 691eqtrd 2833 . . . 4 ((𝜑𝑥𝑋) → Σ𝑝 𝑘 ∈ (0...𝐽)({𝑘} × ((𝐶𝑅)‘𝑘))((𝐽C(1st𝑝)) · ((((!‘(1st𝑝)) / ∏𝑡𝑅 (!‘((2nd𝑝)‘𝑡))) · ∏𝑡𝑅 (((𝑆 D𝑛 (𝐻𝑡))‘((2nd𝑝)‘𝑡))‘𝑥)) · (((𝑆 D𝑛 (𝐻𝑍))‘(𝐽 − (1st𝑝)))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
693297, 321, 6923eqtrd 2837 . . 3 ((𝜑𝑥𝑋) → Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥))) = Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥)))
694693mpteq2dva 5125 . 2 (𝜑 → (𝑥𝑋 ↦ Σ𝑘 ∈ (0...𝐽)((𝐽C𝑘) · ((((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ∏𝑡𝑅 ((𝐻𝑡)‘𝑦)))‘𝑘))‘𝑘)‘𝑥) · (((𝑘 ∈ (0...𝐽) ↦ ((𝑆 D𝑛 (𝑦𝑋 ↦ ((𝐻𝑍)‘𝑦)))‘𝑘))‘(𝐽𝑘))‘𝑥)))) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
69539, 212, 6943eqtrd 2837 1 (𝜑 → ((𝑆 D𝑛 (𝑥𝑋 ↦ ∏𝑡 ∈ (𝑅 ∪ {𝑍})((𝐻𝑡)‘𝑥)))‘𝐽) = (𝑥𝑋 ↦ Σ𝑐 ∈ ((𝐶‘(𝑅 ∪ {𝑍}))‘𝐽)(((!‘𝐽) / ∏𝑡 ∈ (𝑅 ∪ {𝑍})(!‘(𝑐𝑡))) · ∏𝑡 ∈ (𝑅 ∪ {𝑍})(((𝑆 D𝑛 (𝐻𝑡))‘(𝑐𝑡))‘𝑥))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2111  wne 2987  wral 3106  wrex 3107  {crab 3110  Vcvv 3441  cdif 3878  cun 3879  wss 3881  𝒫 cpw 4497  {csn 4525  {cpr 4527  cop 4531   ciun 4881   class class class wbr 5030  cmpt 5110   × cxp 5517  cres 5521  wf 6320  1-1-ontowf1o 6323  cfv 6324  (class class class)co 7135  1st c1st 7669  2nd c2nd 7670  m cmap 8389  Fincfn 8492  cc 10524  cr 10525  0cc0 10526   · cmul 10531  cle 10665  cmin 10859   / cdiv 11286  cn 11625  0cn0 11885  cz 11969  cuz 12231  ...cfz 12885  !cfa 13629  Ccbc 13658  Σcsu 15034  cprod 15251  t crest 16686  TopOpenctopn 16687  fldccnfld 20091   D𝑛 cdvn 24467
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rmo 3114  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-int 4839  df-iun 4883  df-iin 4884  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-se 5479  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-isom 6333  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-of 7389  df-om 7561  df-1st 7671  df-2nd 7672  df-supp 7814  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-2o 8086  df-oadd 8089  df-er 8272  df-map 8391  df-pm 8392  df-ixp 8445  df-en 8493  df-dom 8494  df-sdom 8495  df-fin 8496  df-fsupp 8818  df-fi 8859  df-sup 8890  df-inf 8891  df-oi 8958  df-card 9352  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-seq 13365  df-exp 13426  df-fac 13630  df-bc 13659  df-hash 13687  df-cj 14450  df-re 14451  df-im 14452  df-sqrt 14586  df-abs 14587  df-clim 14837  df-sum 15035  df-prod 15252  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17893  df-mnd 17904  df-submnd 17949  df-mulg 18217  df-cntz 18439  df-cmn 18900  df-psmet 20083  df-xmet 20084  df-met 20085  df-bl 20086  df-mopn 20087  df-fbas 20088  df-fg 20089  df-cnfld 20092  df-top 21499  df-topon 21516  df-topsp 21538  df-bases 21551  df-cld 21624  df-ntr 21625  df-cls 21626  df-nei 21703  df-lp 21741  df-perf 21742  df-cn 21832  df-cnp 21833  df-haus 21920  df-tx 22167  df-hmeo 22360  df-fil 22451  df-fm 22543  df-flim 22544  df-flf 22545  df-xms 22927  df-ms 22928  df-tms 22929  df-cncf 23483  df-limc 24469  df-dv 24470  df-dvn 24471
This theorem is referenced by:  dvnprodlem3  42590
  Copyright terms: Public domain W3C validator