Metamath Proof Explorer


Theorem dvnprodlem2

Description: Induction step for dvnprodlem2 . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses 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 dvnprodlem2 ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvnprodlem2.s ( 𝜑𝑆 ∈ { ℝ , ℂ } )
2 dvnprodlem2.x ( 𝜑𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3 dvnprodlem2.t ( 𝜑𝑇 ∈ Fin )
4 dvnprodlem2.h ( ( 𝜑𝑡𝑇 ) → ( 𝐻𝑡 ) : 𝑋 ⟶ ℂ )
5 dvnprodlem2.n ( 𝜑𝑁 ∈ ℕ0 )
6 dvnprodlem2.dvnh ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ )
7 dvnprodlem2.c 𝐶 = ( 𝑠 ∈ 𝒫 𝑇 ↦ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } ) )
8 dvnprodlem2.r ( 𝜑𝑅𝑇 )
9 dvnprodlem2.z ( 𝜑𝑍 ∈ ( 𝑇𝑅 ) )
10 dvnprodlem2.ind ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
11 dvnprodlem2.j ( 𝜑𝐽 ∈ ( 0 ... 𝑁 ) )
12 dvnprodlem2.d 𝐷 = ( 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ↦ ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ )
13 nfv 𝑡 ( 𝜑𝑥𝑋 )
14 nfcv 𝑡 ( ( 𝐻𝑍 ) ‘ 𝑥 )
15 ssfi ( ( 𝑇 ∈ Fin ∧ 𝑅𝑇 ) → 𝑅 ∈ Fin )
16 3 8 15 syl2anc ( 𝜑𝑅 ∈ Fin )
17 16 adantr ( ( 𝜑𝑥𝑋 ) → 𝑅 ∈ Fin )
18 9 adantr ( ( 𝜑𝑥𝑋 ) → 𝑍 ∈ ( 𝑇𝑅 ) )
19 9 eldifbd ( 𝜑 → ¬ 𝑍𝑅 )
20 19 adantr ( ( 𝜑𝑥𝑋 ) → ¬ 𝑍𝑅 )
21 simpl ( ( 𝜑𝑡𝑅 ) → 𝜑 )
22 8 sselda ( ( 𝜑𝑡𝑅 ) → 𝑡𝑇 )
23 21 22 4 syl2anc ( ( 𝜑𝑡𝑅 ) → ( 𝐻𝑡 ) : 𝑋 ⟶ ℂ )
24 23 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑡𝑅 ) → ( 𝐻𝑡 ) : 𝑋 ⟶ ℂ )
25 simplr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑡𝑅 ) → 𝑥𝑋 )
26 24 25 ffvelcdmd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑡𝑅 ) → ( ( 𝐻𝑡 ) ‘ 𝑥 ) ∈ ℂ )
27 fveq2 ( 𝑡 = 𝑍 → ( 𝐻𝑡 ) = ( 𝐻𝑍 ) )
28 27 fveq1d ( 𝑡 = 𝑍 → ( ( 𝐻𝑡 ) ‘ 𝑥 ) = ( ( 𝐻𝑍 ) ‘ 𝑥 ) )
29 id ( 𝜑𝜑 )
30 eldifi ( 𝑍 ∈ ( 𝑇𝑅 ) → 𝑍𝑇 )
31 9 30 syl ( 𝜑𝑍𝑇 )
32 simpr ( ( 𝜑𝑍𝑇 ) → 𝑍𝑇 )
33 id ( ( 𝜑𝑍𝑇 ) → ( 𝜑𝑍𝑇 ) )
34 eleq1 ( 𝑡 = 𝑍 → ( 𝑡𝑇𝑍𝑇 ) )
35 34 anbi2d ( 𝑡 = 𝑍 → ( ( 𝜑𝑡𝑇 ) ↔ ( 𝜑𝑍𝑇 ) ) )
36 27 feq1d ( 𝑡 = 𝑍 → ( ( 𝐻𝑡 ) : 𝑋 ⟶ ℂ ↔ ( 𝐻𝑍 ) : 𝑋 ⟶ ℂ ) )
37 35 36 imbi12d ( 𝑡 = 𝑍 → ( ( ( 𝜑𝑡𝑇 ) → ( 𝐻𝑡 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇 ) → ( 𝐻𝑍 ) : 𝑋 ⟶ ℂ ) ) )
38 37 4 vtoclg ( 𝑍𝑇 → ( ( 𝜑𝑍𝑇 ) → ( 𝐻𝑍 ) : 𝑋 ⟶ ℂ ) )
39 32 33 38 sylc ( ( 𝜑𝑍𝑇 ) → ( 𝐻𝑍 ) : 𝑋 ⟶ ℂ )
40 29 31 39 syl2anc ( 𝜑 → ( 𝐻𝑍 ) : 𝑋 ⟶ ℂ )
41 40 adantr ( ( 𝜑𝑥𝑋 ) → ( 𝐻𝑍 ) : 𝑋 ⟶ ℂ )
42 simpr ( ( 𝜑𝑥𝑋 ) → 𝑥𝑋 )
43 41 42 ffvelcdmd ( ( 𝜑𝑥𝑋 ) → ( ( 𝐻𝑍 ) ‘ 𝑥 ) ∈ ℂ )
44 13 14 17 18 20 26 28 43 fprodsplitsn ( ( 𝜑𝑥𝑋 ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( 𝐻𝑡 ) ‘ 𝑥 ) = ( ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) · ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) )
45 44 mpteq2dva ( 𝜑 → ( 𝑥𝑋 ↦ ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) = ( 𝑥𝑋 ↦ ( ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) · ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) )
46 45 oveq2d ( 𝜑 → ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) · ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ) )
47 46 fveq1d ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) · ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ) ‘ 𝐽 ) )
48 13 17 26 fprodclf ( ( 𝜑𝑥𝑋 ) → ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ∈ ℂ )
49 elfznn0 ( 𝐽 ∈ ( 0 ... 𝑁 ) → 𝐽 ∈ ℕ0 )
50 11 49 syl ( 𝜑𝐽 ∈ ℕ0 )
51 eqid ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) = ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) )
52 eqid ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) = ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) )
53 oveq2 ( 𝑠 = 𝑅 → ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = ( ( 0 ... 𝑛 ) ↑m 𝑅 ) )
54 rabeq ( ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = ( ( 0 ... 𝑛 ) ↑m 𝑅 ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } )
55 53 54 syl ( 𝑠 = 𝑅 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } )
56 sumeq1 ( 𝑠 = 𝑅 → Σ 𝑡𝑠 ( 𝑐𝑡 ) = Σ 𝑡𝑅 ( 𝑐𝑡 ) )
57 56 eqeq1d ( 𝑠 = 𝑅 → ( Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 ↔ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 ) )
58 57 rabbidv ( 𝑠 = 𝑅 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } )
59 55 58 eqtrd ( 𝑠 = 𝑅 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } )
60 59 mpteq2dv ( 𝑠 = 𝑅 → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } ) )
61 ssexg ( ( 𝑅𝑇𝑇 ∈ Fin ) → 𝑅 ∈ V )
62 8 3 61 syl2anc ( 𝜑𝑅 ∈ V )
63 elpwg ( 𝑅 ∈ V → ( 𝑅 ∈ 𝒫 𝑇𝑅𝑇 ) )
64 62 63 syl ( 𝜑 → ( 𝑅 ∈ 𝒫 𝑇𝑅𝑇 ) )
65 8 64 mpbird ( 𝜑𝑅 ∈ 𝒫 𝑇 )
66 65 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑅 ∈ 𝒫 𝑇 )
67 nn0ex 0 ∈ V
68 67 mptex ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } ) ∈ V
69 68 a1i ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } ) ∈ V )
70 7 60 66 69 fvmptd3 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝐶𝑅 ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } ) )
71 oveq2 ( 𝑛 = 𝑘 → ( 0 ... 𝑛 ) = ( 0 ... 𝑘 ) )
72 71 oveq1d ( 𝑛 = 𝑘 → ( ( 0 ... 𝑛 ) ↑m 𝑅 ) = ( ( 0 ... 𝑘 ) ↑m 𝑅 ) )
73 rabeq ( ( ( 0 ... 𝑛 ) ↑m 𝑅 ) = ( ( 0 ... 𝑘 ) ↑m 𝑅 ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } )
74 72 73 syl ( 𝑛 = 𝑘 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } )
75 eqeq2 ( 𝑛 = 𝑘 → ( Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 ↔ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 ) )
76 75 rabbidv ( 𝑛 = 𝑘 → { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } )
77 74 76 eqtrd ( 𝑛 = 𝑘 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } )
78 77 adantl ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑛 = 𝑘 ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } )
79 elfznn0 ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝑘 ∈ ℕ0 )
80 79 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘 ∈ ℕ0 )
81 fzfid ( 𝜑 → ( 0 ... 𝑘 ) ∈ Fin )
82 mapfi ( ( ( 0 ... 𝑘 ) ∈ Fin ∧ 𝑅 ∈ Fin ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∈ Fin )
83 81 16 82 syl2anc ( 𝜑 → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∈ Fin )
84 83 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∈ Fin )
85 ssrab2 { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ⊆ ( ( 0 ... 𝑘 ) ↑m 𝑅 )
86 85 a1i ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ⊆ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) )
87 84 86 ssexd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ∈ V )
88 70 78 80 87 fvmptd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) = { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } )
89 ssfi ( ( ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∈ Fin ∧ { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ⊆ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ) → { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ∈ Fin )
90 83 85 89 sylancl ( 𝜑 → { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ∈ Fin )
91 90 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ∈ Fin )
92 88 91 eqeltrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ∈ Fin )
93 92 adantr ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ∈ Fin )
94 79 faccld ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( ! ‘ 𝑘 ) ∈ ℕ )
95 94 nncnd ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( ! ‘ 𝑘 ) ∈ ℂ )
96 95 ad2antlr ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ! ‘ 𝑘 ) ∈ ℂ )
97 16 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → 𝑅 ∈ Fin )
98 97 adantlr ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → 𝑅 ∈ Fin )
99 elfznn0 ( 𝑧 ∈ ( 0 ... 𝑘 ) → 𝑧 ∈ ℕ0 )
100 99 ssriv ( 0 ... 𝑘 ) ⊆ ℕ0
101 100 a1i ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝑘 ) ⊆ ℕ0 )
102 simpr ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
103 88 eleq2d ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ↔ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ) )
104 103 adantr ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ↔ 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } ) )
105 102 104 mpbid ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } )
106 85 sseli ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ∣ Σ 𝑡𝑅 ( 𝑐𝑡 ) = 𝑘 } → 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) )
107 105 106 syl ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) )
108 elmapi ( 𝑐 ∈ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) → 𝑐 : 𝑅 ⟶ ( 0 ... 𝑘 ) )
109 107 108 syl ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → 𝑐 : 𝑅 ⟶ ( 0 ... 𝑘 ) )
110 109 adantr ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → 𝑐 : 𝑅 ⟶ ( 0 ... 𝑘 ) )
111 simpr ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → 𝑡𝑅 )
112 110 111 ffvelcdmd ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝑘 ) )
113 101 112 sseldd ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ℕ0 )
114 113 faccld ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ )
115 114 nncnd ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
116 98 115 fprodcl ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
117 114 nnne0d ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
118 98 115 117 fprodn0 ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
119 96 116 118 divcld ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ∈ ℂ )
120 119 adantlr ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ∈ ℂ )
121 98 adantlr ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → 𝑅 ∈ Fin )
122 29 ad4antr ( ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → 𝜑 )
123 122 22 sylancom ( ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → 𝑡𝑇 )
124 elfzuz3 ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝐽 ∈ ( ℤ𝑘 ) )
125 fzss2 ( 𝐽 ∈ ( ℤ𝑘 ) → ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝐽 ) )
126 124 125 syl ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝐽 ) )
127 126 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝐽 ) )
128 50 nn0zd ( 𝜑𝐽 ∈ ℤ )
129 5 nn0zd ( 𝜑𝑁 ∈ ℤ )
130 elfzle2 ( 𝐽 ∈ ( 0 ... 𝑁 ) → 𝐽𝑁 )
131 11 130 syl ( 𝜑𝐽𝑁 )
132 128 129 131 3jca ( 𝜑 → ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁 ) )
133 eluz2 ( 𝑁 ∈ ( ℤ𝐽 ) ↔ ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐽𝑁 ) )
134 132 133 sylibr ( 𝜑𝑁 ∈ ( ℤ𝐽 ) )
135 fzss2 ( 𝑁 ∈ ( ℤ𝐽 ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
136 134 135 syl ( 𝜑 → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
137 136 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
138 127 137 sstrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝑁 ) )
139 138 ad2antrr ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝑁 ) )
140 139 112 sseldd ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) )
141 140 adantllr ( ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) )
142 fvex ( 𝑐𝑡 ) ∈ V
143 eleq1 ( 𝑗 = ( 𝑐𝑡 ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) ) )
144 143 3anbi3d ( 𝑗 = ( 𝑐𝑡 ) → ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑡𝑇 ∧ ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) ) ) )
145 fveq2 ( 𝑗 = ( 𝑐𝑡 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) )
146 145 feq1d ( 𝑗 = ( 𝑐𝑡 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ ) )
147 144 146 imbi12d ( 𝑗 = ( 𝑐𝑡 ) → ( ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑡𝑇 ∧ ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ ) ) )
148 142 147 6 vtocl ( ( 𝜑𝑡𝑇 ∧ ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
149 122 123 141 148 syl3anc ( ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
150 simpllr ( ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → 𝑥𝑋 )
151 149 150 ffvelcdmd ( ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ∧ 𝑡𝑅 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
152 121 151 fprodcl ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
153 120 152 mulcld ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ )
154 93 153 fsumcl ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) → Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ )
155 154 fmpttd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) : 𝑋 ⟶ ℂ )
156 10 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
157 0zd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 0 ∈ ℤ )
158 129 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑁 ∈ ℤ )
159 elfzelz ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝑘 ∈ ℤ )
160 159 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘 ∈ ℤ )
161 elfzle1 ( 𝑘 ∈ ( 0 ... 𝐽 ) → 0 ≤ 𝑘 )
162 161 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 0 ≤ 𝑘 )
163 160 zred ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘 ∈ ℝ )
164 50 nn0red ( 𝜑𝐽 ∈ ℝ )
165 164 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝐽 ∈ ℝ )
166 158 zred ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑁 ∈ ℝ )
167 elfzle2 ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝑘𝐽 )
168 167 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘𝐽 )
169 131 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝐽𝑁 )
170 163 165 166 168 169 letrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘𝑁 )
171 157 158 160 162 170 elfzd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑘 ∈ ( 0 ... 𝑁 ) )
172 rspa ( ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
173 156 171 172 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
174 173 feq1d ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ↔ ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) : 𝑋 ⟶ ℂ ) )
175 155 174 mpbird ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
176 31 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑍𝑇 )
177 simpl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝜑 )
178 177 176 171 3jca ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝜑𝑍𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) )
179 34 3anbi2d ( 𝑡 = 𝑍 → ( ( 𝜑𝑡𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑍𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) ) )
180 27 oveq2d ( 𝑡 = 𝑍 → ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) = ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) )
181 180 fveq1d ( 𝑡 = 𝑍 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) )
182 181 feq1d ( 𝑡 = 𝑍 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) )
183 179 182 imbi12d ( 𝑡 = 𝑍 → ( ( ( 𝜑𝑡𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) ) )
184 eleq1 ( 𝑗 = 𝑘 → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ 𝑘 ∈ ( 0 ... 𝑁 ) ) )
185 184 3anbi3d ( 𝑗 = 𝑘 → ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑡𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) ) )
186 fveq2 ( 𝑗 = 𝑘 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) )
187 186 feq1d ( 𝑗 = 𝑘 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) )
188 185 187 imbi12d ( 𝑗 = 𝑘 → ( ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑡𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) ) )
189 188 6 chvarvv ( ( 𝜑𝑡𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
190 183 189 vtoclg ( 𝑍𝑇 → ( ( 𝜑𝑍𝑇𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) )
191 176 178 190 sylc ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
192 40 feqmptd ( 𝜑 → ( 𝐻𝑍 ) = ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) )
193 192 eqcomd ( 𝜑 → ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) = ( 𝐻𝑍 ) )
194 193 oveq2d ( 𝜑 → ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) = ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) )
195 194 fveq1d ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) )
196 195 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) )
197 196 feq1d ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) )
198 191 197 mpbird ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ )
199 fveq2 ( 𝑦 = 𝑥 → ( ( 𝐻𝑡 ) ‘ 𝑦 ) = ( ( 𝐻𝑡 ) ‘ 𝑥 ) )
200 199 prodeq2ad ( 𝑦 = 𝑥 → ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) = ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) )
201 200 cbvmptv ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) = ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) )
202 201 oveq2i ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) = ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) )
203 202 fveq1i ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 )
204 203 mpteq2i ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
205 fveq2 ( 𝑦 = 𝑥 → ( ( 𝐻𝑍 ) ‘ 𝑦 ) = ( ( 𝐻𝑍 ) ‘ 𝑥 ) )
206 205 cbvmptv ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) = ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) )
207 206 oveq2i ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) = ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) )
208 207 fveq1i ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ‘ 𝑘 )
209 208 mpteq2i ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
210 1 2 48 43 50 51 52 175 198 204 209 dvnmul ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ( ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) · ( ( 𝐻𝑍 ) ‘ 𝑥 ) ) ) ) ‘ 𝐽 ) = ( 𝑥𝑋 ↦ Σ 𝑘 ∈ ( 0 ... 𝐽 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) ) )
211 203 a1i ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) )
212 10 r19.21bi ( ( 𝜑𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
213 177 171 212 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
214 211 213 eqtrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
215 214 mpteq2dva ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) = ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ) )
216 mptexg ( 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) → ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ∈ V )
217 2 216 syl ( 𝜑 → ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ∈ V )
218 217 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ∈ V )
219 215 218 fvmpt2d ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
220 219 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
221 220 fveq1d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) )
222 42 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝑥𝑋 )
223 154 an32s ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ )
224 eqid ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
225 224 fvmpt2 ( ( 𝑥𝑋 ∧ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ ) → ( ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
226 222 223 225 syl2anc ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) ‘ 𝑥 ) = Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
227 221 226 eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) = Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
228 fveq2 ( 𝑘 = 𝑗 → ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑗 ) )
229 228 cbvmptv ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) = ( 𝑗 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑗 ) )
230 229 a1i ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) = ( 𝑗 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑗 ) ) )
231 207 194 eqtrid ( 𝜑 → ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) = ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) )
232 231 fveq1d ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) )
233 232 mpteq2dv ( 𝜑 → ( 𝑗 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑗 ) ) = ( 𝑗 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) ) )
234 230 233 eqtrd ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) = ( 𝑗 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) ) )
235 234 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) = ( 𝑗 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) ) )
236 fveq2 ( 𝑗 = ( 𝐽𝑘 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) )
237 236 adantl ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑗 = ( 𝐽𝑘 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) )
238 0zd ( 𝑘 ∈ ( 0 ... 𝐽 ) → 0 ∈ ℤ )
239 elfzel2 ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝐽 ∈ ℤ )
240 239 159 zsubcld ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝐽𝑘 ) ∈ ℤ )
241 238 239 240 3jca ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ( 𝐽𝑘 ) ∈ ℤ ) )
242 239 zred ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝐽 ∈ ℝ )
243 79 nn0red ( 𝑘 ∈ ( 0 ... 𝐽 ) → 𝑘 ∈ ℝ )
244 242 243 subge0d ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 0 ≤ ( 𝐽𝑘 ) ↔ 𝑘𝐽 ) )
245 167 244 mpbird ( 𝑘 ∈ ( 0 ... 𝐽 ) → 0 ≤ ( 𝐽𝑘 ) )
246 242 243 subge02d ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 0 ≤ 𝑘 ↔ ( 𝐽𝑘 ) ≤ 𝐽 ) )
247 161 246 mpbid ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝐽𝑘 ) ≤ 𝐽 )
248 241 245 247 jca32 ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( ( 0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ( 𝐽𝑘 ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝐽𝑘 ) ∧ ( 𝐽𝑘 ) ≤ 𝐽 ) ) )
249 248 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ( 𝐽𝑘 ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝐽𝑘 ) ∧ ( 𝐽𝑘 ) ≤ 𝐽 ) ) )
250 elfz2 ( ( 𝐽𝑘 ) ∈ ( 0 ... 𝐽 ) ↔ ( ( 0 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ ( 𝐽𝑘 ) ∈ ℤ ) ∧ ( 0 ≤ ( 𝐽𝑘 ) ∧ ( 𝐽𝑘 ) ≤ 𝐽 ) ) )
251 249 250 sylibr ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝐽𝑘 ) ∈ ( 0 ... 𝐽 ) )
252 fvex ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ∈ V
253 252 a1i ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ∈ V )
254 235 237 251 253 fvmptd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) )
255 254 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) )
256 255 fveq1d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) )
257 227 256 oveq12d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) = ( Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) )
258 257 oveq2d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = ( ( 𝐽 C 𝑘 ) · ( Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) )
259 92 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ∈ Fin )
260 ovex ( 𝐽𝑘 ) ∈ V
261 eleq1 ( 𝑗 = ( 𝐽𝑘 ) → ( 𝑗 ∈ ( 0 ... 𝐽 ) ↔ ( 𝐽𝑘 ) ∈ ( 0 ... 𝐽 ) ) )
262 261 anbi2d ( 𝑗 = ( 𝐽𝑘 ) → ( ( 𝜑𝑗 ∈ ( 0 ... 𝐽 ) ) ↔ ( 𝜑 ∧ ( 𝐽𝑘 ) ∈ ( 0 ... 𝐽 ) ) ) )
263 236 feq1d ( 𝑗 = ( 𝐽𝑘 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) : 𝑋 ⟶ ℂ ) )
264 262 263 imbi12d ( 𝑗 = ( 𝐽𝑘 ) → ( ( ( 𝜑𝑗 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑 ∧ ( 𝐽𝑘 ) ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) : 𝑋 ⟶ ℂ ) ) )
265 eleq1 ( 𝑘 = 𝑗 → ( 𝑘 ∈ ( 0 ... 𝐽 ) ↔ 𝑗 ∈ ( 0 ... 𝐽 ) ) )
266 265 anbi2d ( 𝑘 = 𝑗 → ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ↔ ( 𝜑𝑗 ∈ ( 0 ... 𝐽 ) ) ) )
267 fveq2 ( 𝑘 = 𝑗 → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) )
268 267 feq1d ( 𝑘 = 𝑗 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) )
269 266 268 imbi12d ( 𝑘 = 𝑗 → ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑘 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑗 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ) )
270 269 191 chvarvv ( ( 𝜑𝑗 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ )
271 260 264 270 vtocl ( ( 𝜑 ∧ ( 𝐽𝑘 ) ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) : 𝑋 ⟶ ℂ )
272 177 251 271 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) : 𝑋 ⟶ ℂ )
273 272 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) : 𝑋 ⟶ ℂ )
274 273 222 ffvelcdmd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ∈ ℂ )
275 anass ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ↔ ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑥𝑋 ) ) )
276 ancom ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑥𝑋 ) ↔ ( 𝑥𝑋𝑘 ∈ ( 0 ... 𝐽 ) ) )
277 276 anbi2i ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑥𝑋 ) ) ↔ ( 𝜑 ∧ ( 𝑥𝑋𝑘 ∈ ( 0 ... 𝐽 ) ) ) )
278 anass ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ↔ ( 𝜑 ∧ ( 𝑥𝑋𝑘 ∈ ( 0 ... 𝐽 ) ) ) )
279 278 bicomi ( ( 𝜑 ∧ ( 𝑥𝑋𝑘 ∈ ( 0 ... 𝐽 ) ) ) ↔ ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) )
280 277 279 bitri ( ( 𝜑 ∧ ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑥𝑋 ) ) ↔ ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) )
281 275 280 bitri ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ↔ ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) )
282 281 anbi1i ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ↔ ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
283 282 imbi1i ( ( ( ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ ) ↔ ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ ) )
284 153 283 mpbi ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ )
285 259 274 284 fsummulc1 ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) )
286 285 oveq2d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐽 C 𝑘 ) · ( Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = ( ( 𝐽 C 𝑘 ) · Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) )
287 177 50 syl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → 𝐽 ∈ ℕ0 )
288 287 160 bccld ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 C 𝑘 ) ∈ ℕ0 )
289 288 nn0cnd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 C 𝑘 ) ∈ ℂ )
290 289 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 C 𝑘 ) ∈ ℂ )
291 274 adantr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ∈ ℂ )
292 284 291 mulcld ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ∈ ℂ )
293 259 290 292 fsummulc2 ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐽 C 𝑘 ) · Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) )
294 258 286 293 3eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) )
295 294 sumeq2dv ( ( 𝜑𝑥𝑋 ) → Σ 𝑘 ∈ ( 0 ... 𝐽 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝐽 ) Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) )
296 vex 𝑘 ∈ V
297 vex 𝑐 ∈ V
298 296 297 op1std ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( 1st𝑝 ) = 𝑘 )
299 298 oveq2d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( 𝐽 C ( 1st𝑝 ) ) = ( 𝐽 C 𝑘 ) )
300 298 fveq2d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ! ‘ ( 1st𝑝 ) ) = ( ! ‘ 𝑘 ) )
301 296 297 op2ndd ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( 2nd𝑝 ) = 𝑐 )
302 301 fveq1d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( 2nd𝑝 ) ‘ 𝑡 ) = ( 𝑐𝑡 ) )
303 302 fveq2d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) = ( ! ‘ ( 𝑐𝑡 ) ) )
304 303 prodeq2ad ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) = ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) )
305 300 304 oveq12d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) = ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) )
306 302 fveq2d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) )
307 306 fveq1d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
308 307 prodeq2ad ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
309 305 308 oveq12d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
310 298 oveq2d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( 𝐽 − ( 1st𝑝 ) ) = ( 𝐽𝑘 ) )
311 310 fveq2d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) )
312 311 fveq1d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) )
313 309 312 oveq12d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) )
314 299 313 oveq12d ( 𝑝 = ⟨ 𝑘 , 𝑐 ⟩ → ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) = ( ( 𝐽 C 𝑘 ) · ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) )
315 fzfid ( ( 𝜑𝑥𝑋 ) → ( 0 ... 𝐽 ) ∈ Fin )
316 290 adantrr ( ( ( 𝜑𝑥𝑋 ) ∧ ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 C 𝑘 ) ∈ ℂ )
317 292 anasss ( ( ( 𝜑𝑥𝑋 ) ∧ ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ∈ ℂ )
318 316 317 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝐽 C 𝑘 ) · ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
319 314 315 259 318 fsum2d ( ( 𝜑𝑥𝑋 ) → Σ 𝑘 ∈ ( 0 ... 𝐽 ) Σ 𝑐 ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( ! ‘ 𝑘 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = Σ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) )
320 ovex ( 𝐽 − ( 𝑐𝑍 ) ) ∈ V
321 297 resex ( 𝑐𝑅 ) ∈ V
322 320 321 op1std ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( 1st𝑝 ) = ( 𝐽 − ( 𝑐𝑍 ) ) )
323 322 oveq2d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( 𝐽 C ( 1st𝑝 ) ) = ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) )
324 322 fveq2d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ! ‘ ( 1st𝑝 ) ) = ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) )
325 320 321 op2ndd ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( 2nd𝑝 ) = ( 𝑐𝑅 ) )
326 325 fveq1d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( 2nd𝑝 ) ‘ 𝑡 ) = ( ( 𝑐𝑅 ) ‘ 𝑡 ) )
327 326 fveq2d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) = ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) )
328 327 prodeq2ad ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) = ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) )
329 324 328 oveq12d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) )
330 326 fveq2d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) )
331 330 fveq1d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) )
332 331 prodeq2ad ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) )
333 329 332 oveq12d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) )
334 322 oveq2d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( 𝐽 − ( 1st𝑝 ) ) = ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) )
335 334 fveq2d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
336 335 fveq1d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) )
337 333 336 oveq12d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) = ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) )
338 323 337 oveq12d ( 𝑝 = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ → ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) = ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) )
339 oveq2 ( 𝑠 = ( 𝑅 ∪ { 𝑍 } ) → ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) )
340 rabeq ( ( ( 0 ... 𝑛 ) ↑m 𝑠 ) = ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } )
341 339 340 syl ( 𝑠 = ( 𝑅 ∪ { 𝑍 } ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } )
342 sumeq1 ( 𝑠 = ( 𝑅 ∪ { 𝑍 } ) → Σ 𝑡𝑠 ( 𝑐𝑡 ) = Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) )
343 342 eqeq1d ( 𝑠 = ( 𝑅 ∪ { 𝑍 } ) → ( Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 ) )
344 343 rabbidv ( 𝑠 = ( 𝑅 ∪ { 𝑍 } ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } )
345 341 344 eqtrd ( 𝑠 = ( 𝑅 ∪ { 𝑍 } ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } )
346 345 mpteq2dv ( 𝑠 = ( 𝑅 ∪ { 𝑍 } ) → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m 𝑠 ) ∣ Σ 𝑡𝑠 ( 𝑐𝑡 ) = 𝑛 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } ) )
347 31 snssd ( 𝜑 → { 𝑍 } ⊆ 𝑇 )
348 8 347 unssd ( 𝜑 → ( 𝑅 ∪ { 𝑍 } ) ⊆ 𝑇 )
349 3 348 ssexd ( 𝜑 → ( 𝑅 ∪ { 𝑍 } ) ∈ V )
350 elpwg ( ( 𝑅 ∪ { 𝑍 } ) ∈ V → ( ( 𝑅 ∪ { 𝑍 } ) ∈ 𝒫 𝑇 ↔ ( 𝑅 ∪ { 𝑍 } ) ⊆ 𝑇 ) )
351 349 350 syl ( 𝜑 → ( ( 𝑅 ∪ { 𝑍 } ) ∈ 𝒫 𝑇 ↔ ( 𝑅 ∪ { 𝑍 } ) ⊆ 𝑇 ) )
352 348 351 mpbird ( 𝜑 → ( 𝑅 ∪ { 𝑍 } ) ∈ 𝒫 𝑇 )
353 67 mptex ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } ) ∈ V
354 353 a1i ( 𝜑 → ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } ) ∈ V )
355 7 346 352 354 fvmptd3 ( 𝜑 → ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } ) )
356 oveq2 ( 𝑛 = 𝐽 → ( 0 ... 𝑛 ) = ( 0 ... 𝐽 ) )
357 356 oveq1d ( 𝑛 = 𝐽 → ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) = ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) )
358 rabeq ( ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) = ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } )
359 357 358 syl ( 𝑛 = 𝐽 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } )
360 eqeq2 ( 𝑛 = 𝐽 → ( Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 ↔ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 ) )
361 360 rabbidv ( 𝑛 = 𝐽 → { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
362 359 361 eqtrd ( 𝑛 = 𝐽 → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
363 362 adantl ( ( 𝜑𝑛 = 𝐽 ) → { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝑛 } = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
364 ovex ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∈ V
365 364 rabex { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } ∈ V
366 365 a1i ( 𝜑 → { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } ∈ V )
367 355 363 50 366 fvmptd ( 𝜑 → ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
368 fzfid ( 𝜑 → ( 0 ... 𝐽 ) ∈ Fin )
369 snfi { 𝑍 } ∈ Fin
370 369 a1i ( 𝜑 → { 𝑍 } ∈ Fin )
371 unfi ( ( 𝑅 ∈ Fin ∧ { 𝑍 } ∈ Fin ) → ( 𝑅 ∪ { 𝑍 } ) ∈ Fin )
372 16 370 371 syl2anc ( 𝜑 → ( 𝑅 ∪ { 𝑍 } ) ∈ Fin )
373 mapfi ( ( ( 0 ... 𝐽 ) ∈ Fin ∧ ( 𝑅 ∪ { 𝑍 } ) ∈ Fin ) → ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∈ Fin )
374 368 372 373 syl2anc ( 𝜑 → ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∈ Fin )
375 ssrab2 { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } ⊆ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) )
376 375 a1i ( 𝜑 → { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } ⊆ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) )
377 ssfi ( ( ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∈ Fin ∧ { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } ⊆ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ) → { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } ∈ Fin )
378 374 376 377 syl2anc ( 𝜑 → { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } ∈ Fin )
379 367 378 eqeltrd ( 𝜑 → ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ∈ Fin )
380 379 adantr ( ( 𝜑𝑥𝑋 ) → ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ∈ Fin )
381 7 50 12 3 31 19 348 dvnprodlem1 ( 𝜑𝐷 : ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) –1-1-onto 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
382 381 adantr ( ( 𝜑𝑥𝑋 ) → 𝐷 : ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) –1-1-onto 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
383 simpr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) )
384 opex ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ ∈ V
385 384 a1i ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ ∈ V )
386 12 fvmpt2 ( ( 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ∧ ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ ∈ V ) → ( 𝐷𝑐 ) = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ )
387 383 385 386 syl2anc ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐷𝑐 ) = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ )
388 387 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐷𝑐 ) = ⟨ ( 𝐽 − ( 𝑐𝑍 ) ) , ( 𝑐𝑅 ) ⟩ )
389 50 adantr ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝐽 ∈ ℕ0 )
390 eliun ( 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ↔ ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
391 390 bilani ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
392 nfv 𝑘 𝜑
393 nfcv 𝑘 𝑝
394 nfiu1 𝑘 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
395 393 394 nfel 𝑘 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
396 392 395 nfan 𝑘 ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
397 nfv 𝑘 ( 1st𝑝 ) ∈ ( 0 ... 𝐽 )
398 xp1st ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ { 𝑘 } )
399 elsni ( ( 1st𝑝 ) ∈ { 𝑘 } → ( 1st𝑝 ) = 𝑘 )
400 398 399 syl ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) = 𝑘 )
401 400 adantl ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) = 𝑘 )
402 simpl ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
403 401 402 eqeltrd ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) )
404 403 ex ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) )
405 404 a1i ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) ) )
406 396 397 405 rexlimd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) )
407 391 406 mpd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) )
408 elfzelz ( ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) → ( 1st𝑝 ) ∈ ℤ )
409 407 408 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ℤ )
410 389 409 bccld ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 C ( 1st𝑝 ) ) ∈ ℕ0 )
411 410 nn0cnd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 C ( 1st𝑝 ) ) ∈ ℂ )
412 411 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 C ( 1st𝑝 ) ) ∈ ℂ )
413 elfznn0 ( ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) → ( 1st𝑝 ) ∈ ℕ0 )
414 407 413 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ℕ0 )
415 414 faccld ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ! ‘ ( 1st𝑝 ) ) ∈ ℕ )
416 415 nncnd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ! ‘ ( 1st𝑝 ) ) ∈ ℂ )
417 416 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ! ‘ ( 1st𝑝 ) ) ∈ ℂ )
418 16 adantr ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑅 ∈ Fin )
419 nfv 𝑘 ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 )
420 88 86 eqsstrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ⊆ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) )
421 ovex ( 0 ... 𝐽 ) ∈ V
422 421 a1i ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 0 ... 𝐽 ) ∈ V )
423 mapss ( ( ( 0 ... 𝐽 ) ∈ V ∧ ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝐽 ) ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
424 422 126 423 syl2anc ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
425 424 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
426 420 425 sstrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
427 426 3adant3 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
428 xp2nd ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
429 428 3ad2ant3 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
430 427 429 sseldd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) ∈ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
431 elmapi ( ( 2nd𝑝 ) ∈ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) )
432 430 431 syl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) )
433 432 3exp ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) ) ) )
434 433 adantr ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) ) ) )
435 396 419 434 rexlimd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) ) )
436 391 435 mpd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) )
437 436 ffvelcdmda ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) )
438 elfznn0 ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ℕ0 )
439 438 faccld ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℕ )
440 439 nncnd ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
441 437 440 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
442 418 441 fprodcl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
443 442 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
444 437 439 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℕ )
445 nnne0 ( ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℕ → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
446 444 445 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
447 418 441 446 fprodn0 ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
448 447 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
449 417 443 448 divcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) ∈ ℂ )
450 17 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑅 ∈ Fin )
451 simpll ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → 𝜑 )
452 451 22 sylancom ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → 𝑡𝑇 )
453 451 136 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
454 453 437 sseldd ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) )
455 451 452 454 3jca ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) )
456 eleq1 ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) )
457 456 3anbi3d ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) ) )
458 fveq2 ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) )
459 458 feq1d ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ ) )
460 457 459 imbi12d ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ ) ) )
461 460 6 vtoclg ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ ) )
462 437 455 461 sylc ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ )
463 462 adantllr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ )
464 25 adantlr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → 𝑥𝑋 )
465 463 464 ffvelcdmd ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
466 450 465 fprodcl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
467 449 466 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ )
468 nfv 𝑘 ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 )
469 simp1 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝜑 )
470 403 3adant1 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) )
471 fznn0sub2 ( ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
472 471 adantl ( ( 𝜑 ∧ ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
473 469 470 472 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
474 473 3exp ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) ) ) )
475 474 adantr ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) ) ) )
476 396 468 475 rexlimd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) ) )
477 391 476 mpd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
478 simpl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝜑 )
479 478 31 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑍𝑇 )
480 478 136 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
481 480 477 sseldd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) )
482 478 479 481 3jca ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) )
483 eleq1 ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) )
484 483 3anbi3d ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) ) )
485 fveq2 ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) )
486 485 feq1d ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ ) )
487 484 486 imbi12d ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ ) ) )
488 simp2 ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑍𝑇 )
489 id ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) )
490 34 3anbi2d ( 𝑡 = 𝑍 → ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ) )
491 180 fveq1d ( 𝑡 = 𝑍 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) )
492 491 feq1d ( 𝑡 = 𝑍 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) )
493 490 492 imbi12d ( 𝑡 = 𝑍 → ( ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ) )
494 493 6 vtoclg ( 𝑍𝑇 → ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) )
495 488 489 494 sylc ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ )
496 487 495 vtoclg ( ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) → ( ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ ) )
497 477 482 496 sylc ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ )
498 497 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ )
499 42 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑥𝑋 )
500 498 499 ffvelcdmd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ∈ ℂ )
501 467 500 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ∈ ℂ )
502 412 501 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
503 338 380 382 388 502 fsumf1o ( ( 𝜑𝑥𝑋 ) → Σ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) )
504 simpl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝜑 )
505 367 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
506 383 505 eleqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
507 375 sseli ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } → 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) )
508 506 507 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) )
509 elmapi ( 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝐽 ) )
510 508 509 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝐽 ) )
511 snidg ( 𝑍𝑇𝑍 ∈ { 𝑍 } )
512 31 511 syl ( 𝜑𝑍 ∈ { 𝑍 } )
513 elun2 ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑅 ∪ { 𝑍 } ) )
514 512 513 syl ( 𝜑𝑍 ∈ ( 𝑅 ∪ { 𝑍 } ) )
515 514 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑍 ∈ ( 𝑅 ∪ { 𝑍 } ) )
516 510 515 ffvelcdmd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) )
517 0zd ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 0 ∈ ℤ )
518 128 adantr ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 𝐽 ∈ ℤ )
519 fzssz ( 0 ... 𝐽 ) ⊆ ℤ
520 519 sseli ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( 𝑐𝑍 ) ∈ ℤ )
521 520 adantl ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℤ )
522 518 521 zsubcld ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ℤ )
523 elfzle2 ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( 𝑐𝑍 ) ≤ 𝐽 )
524 523 adantl ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑐𝑍 ) ≤ 𝐽 )
525 164 adantr ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 𝐽 ∈ ℝ )
526 521 zred ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℝ )
527 525 526 subge0d ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 0 ≤ ( 𝐽 − ( 𝑐𝑍 ) ) ↔ ( 𝑐𝑍 ) ≤ 𝐽 ) )
528 524 527 mpbird ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 0 ≤ ( 𝐽 − ( 𝑐𝑍 ) ) )
529 elfzle1 ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → 0 ≤ ( 𝑐𝑍 ) )
530 529 adantl ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 0 ≤ ( 𝑐𝑍 ) )
531 525 526 subge02d ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 0 ≤ ( 𝑐𝑍 ) ↔ ( 𝐽 − ( 𝑐𝑍 ) ) ≤ 𝐽 ) )
532 530 531 mpbid ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ≤ 𝐽 )
533 517 518 522 528 532 elfzd ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) )
534 504 516 533 syl2anc ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) )
535 bcval2 ( ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
536 534 535 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
537 164 recnd ( 𝜑𝐽 ∈ ℂ )
538 537 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝐽 ∈ ℂ )
539 zsscn ℤ ⊆ ℂ
540 519 539 sstri ( 0 ... 𝐽 ) ⊆ ℂ
541 540 a1i ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 0 ... 𝐽 ) ⊆ ℂ )
542 541 516 sseldd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℂ )
543 538 542 nncand ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( 𝑐𝑍 ) )
544 543 fveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ! ‘ ( 𝑐𝑍 ) ) )
545 544 oveq1d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
546 545 oveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
547 50 faccld ( 𝜑 → ( ! ‘ 𝐽 ) ∈ ℕ )
548 547 nncnd ( 𝜑 → ( ! ‘ 𝐽 ) ∈ ℂ )
549 548 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ 𝐽 ) ∈ ℂ )
550 elfznn0 ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( 𝑐𝑍 ) ∈ ℕ0 )
551 516 550 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℕ0 )
552 551 faccld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ∈ ℕ )
553 552 nncnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ∈ ℂ )
554 elfznn0 ( ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ℕ0 )
555 534 554 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ℕ0 )
556 555 faccld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ∈ ℕ )
557 556 nncnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ∈ ℂ )
558 552 nnne0d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ≠ 0 )
559 556 nnne0d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ≠ 0 )
560 549 553 557 558 559 divdiv1d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
561 560 eqcomd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
562 536 546 561 3eqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
563 562 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
564 fvres ( 𝑡𝑅 → ( ( 𝑐𝑅 ) ‘ 𝑡 ) = ( 𝑐𝑡 ) )
565 564 fveq2d ( 𝑡𝑅 → ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) = ( ! ‘ ( 𝑐𝑡 ) ) )
566 565 prodeq2i 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) = ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) )
567 566 oveq2i ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) )
568 564 fveq2d ( 𝑡𝑅 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) )
569 568 fveq1d ( 𝑡𝑅 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
570 569 prodeq2i 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 )
571 567 570 oveq12i ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
572 571 a1i ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
573 572 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
574 557 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ∈ ℂ )
575 504 16 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑅 ∈ Fin )
576 79 ssriv ( 0 ... 𝐽 ) ⊆ ℕ0
577 576 a1i ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝐽 ) ⊆ ℕ0 )
578 510 adantr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝐽 ) )
579 elun1 ( 𝑡𝑅𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) )
580 579 adantl ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) )
581 578 580 ffvelcdmd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝐽 ) )
582 577 581 sseldd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ℕ0 )
583 582 faccld ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ )
584 583 nncnd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
585 575 584 fprodcl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
586 585 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
587 17 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑅 ∈ Fin )
588 504 adantr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝜑 )
589 504 22 sylan ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑡𝑇 )
590 588 136 syl ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
591 590 581 sseldd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) )
592 588 589 591 148 syl3anc ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
593 592 adantllr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
594 25 adantlr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑥𝑋 )
595 593 594 ffvelcdmd ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
596 587 595 fprodcl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
597 575 583 fprodnncl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ )
598 nnne0 ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
599 597 598 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
600 599 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
601 574 586 596 600 div32d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
602 573 601 eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
603 543 fveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) )
604 603 fveq1d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) )
605 604 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) )
606 602 605 oveq12d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) )
607 596 586 600 divcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ∈ ℂ )
608 504 31 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑍𝑇 )
609 504 136 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
610 609 516 sseldd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) )
611 504 608 610 3jca ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) )
612 eleq1 ( 𝑗 = ( 𝑐𝑍 ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) )
613 612 3anbi3d ( 𝑗 = ( 𝑐𝑍 ) → ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) ) )
614 fveq2 ( 𝑗 = ( 𝑐𝑍 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) )
615 614 feq1d ( 𝑗 = ( 𝑐𝑍 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ ) )
616 613 615 imbi12d ( 𝑗 = ( 𝑐𝑍 ) → ( ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ ) ) )
617 616 495 vtoclg ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ ) )
618 516 611 617 sylc ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ )
619 618 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ )
620 42 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑥𝑋 )
621 619 620 ffvelcdmd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ∈ ℂ )
622 574 607 621 mulassd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) )
623 606 622 eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) )
624 563 623 oveq12d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) = ( ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) ) )
625 548 ad2antrr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ 𝐽 ) ∈ ℂ )
626 553 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ∈ ℂ )
627 558 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ≠ 0 )
628 625 626 627 divcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) ∈ ℂ )
629 607 621 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ∈ ℂ )
630 559 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ≠ 0 )
631 628 574 629 630 dmmcand ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) )
632 596 621 586 600 div23d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) )
633 632 eqcomd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) )
634 nfv 𝑡 ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) )
635 nfcv 𝑡 ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 )
636 608 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑍𝑇 )
637 20 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ¬ 𝑍𝑅 )
638 fveq2 ( 𝑡 = 𝑍 → ( 𝑐𝑡 ) = ( 𝑐𝑍 ) )
639 180 638 fveq12d ( 𝑡 = 𝑍 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) )
640 639 fveq1d ( 𝑡 = 𝑍 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) )
641 634 635 587 636 637 595 640 621 fprodsplitsn ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) = ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) )
642 641 eqcomd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
643 642 oveq1d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) )
644 633 643 eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) )
645 644 oveq2d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
646 587 369 371 sylancl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑅 ∪ { 𝑍 } ) ∈ Fin )
647 504 adantr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝜑 )
648 348 sselda ( ( 𝜑𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝑡𝑇 )
649 648 adantlr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝑡𝑇 )
650 510 609 fssd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝑁 ) )
651 650 ffvelcdmda ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) )
652 647 649 651 148 syl3anc ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
653 652 adantllr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
654 620 adantr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝑥𝑋 )
655 653 654 ffvelcdmd ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
656 646 655 fprodcl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
657 625 626 656 586 627 600 divmuldivd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
658 553 585 mulcomd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) · ( ! ‘ ( 𝑐𝑍 ) ) ) )
659 nfv 𝑡 ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) )
660 nfcv 𝑡 ( ! ‘ ( 𝑐𝑍 ) )
661 504 19 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ¬ 𝑍𝑅 )
662 638 fveq2d ( 𝑡 = 𝑍 → ( ! ‘ ( 𝑐𝑡 ) ) = ( ! ‘ ( 𝑐𝑍 ) ) )
663 659 660 575 608 661 584 662 553 fprodsplitsn ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) = ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) · ( ! ‘ ( 𝑐𝑍 ) ) ) )
664 663 eqcomd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) · ( ! ‘ ( 𝑐𝑍 ) ) ) = ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) )
665 658 664 eqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) )
666 665 oveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) )
667 666 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) )
668 504 372 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑅 ∪ { 𝑍 } ) ∈ Fin )
669 576 a1i ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 0 ... 𝐽 ) ⊆ ℕ0 )
670 510 ffvelcdmda ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝐽 ) )
671 669 670 sseldd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 𝑐𝑡 ) ∈ ℕ0 )
672 671 faccld ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ )
673 672 nncnd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
674 668 673 fprodcl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
675 674 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
676 672 nnne0d ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
677 668 673 676 fprodn0 ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
678 677 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
679 625 656 675 678 div23d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
680 eqidd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
681 667 679 680 3eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
682 645 657 681 3eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
683 624 631 682 3eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
684 683 sumeq2dv ( ( 𝜑𝑥𝑋 ) → Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
685 503 684 eqtrd ( ( 𝜑𝑥𝑋 ) → Σ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
686 295 319 685 3eqtrd ( ( 𝜑𝑥𝑋 ) → Σ 𝑘 ∈ ( 0 ... 𝐽 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
687 686 mpteq2dva ( 𝜑 → ( 𝑥𝑋 ↦ Σ 𝑘 ∈ ( 0 ... 𝐽 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
688 47 210 687 3eqtrd ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )