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 ffvelrnd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑡𝑅 ) → ( ( 𝐻𝑡 ) ‘ 𝑥 ) ∈ ℂ )
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 ffvelrnd ( ( 𝜑𝑥𝑋 ) → ( ( 𝐻𝑍 ) ‘ 𝑥 ) ∈ ℂ )
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 ffvelrnd ( ( ( ( 𝜑𝑘 ∈ ( 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 ffvelrnd ( ( ( ( ( 𝜑𝑘 ∈ ( 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 syl5eq ( 𝜑 → ( 𝑆 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 ffvelrnd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑘 ∈ ( 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 biimpi ( 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
392 391 adantl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
393 nfv 𝑘 𝜑
394 nfcv 𝑘 𝑝
395 nfiu1 𝑘 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
396 394 395 nfel 𝑘 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
397 393 396 nfan 𝑘 ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) )
398 nfv 𝑘 ( 1st𝑝 ) ∈ ( 0 ... 𝐽 )
399 xp1st ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ { 𝑘 } )
400 elsni ( ( 1st𝑝 ) ∈ { 𝑘 } → ( 1st𝑝 ) = 𝑘 )
401 399 400 syl ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) = 𝑘 )
402 401 adantl ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) = 𝑘 )
403 simpl ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑘 ∈ ( 0 ... 𝐽 ) )
404 402 403 eqeltrd ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) )
405 404 ex ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) )
406 405 a1i ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) ) )
407 397 398 406 rexlimd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) )
408 392 407 mpd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) )
409 elfzelz ( ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) → ( 1st𝑝 ) ∈ ℤ )
410 408 409 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ℤ )
411 389 410 bccld ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 C ( 1st𝑝 ) ) ∈ ℕ0 )
412 411 nn0cnd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 C ( 1st𝑝 ) ) ∈ ℂ )
413 412 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 C ( 1st𝑝 ) ) ∈ ℂ )
414 elfznn0 ( ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) → ( 1st𝑝 ) ∈ ℕ0 )
415 408 414 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ℕ0 )
416 415 faccld ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ! ‘ ( 1st𝑝 ) ) ∈ ℕ )
417 416 nncnd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ! ‘ ( 1st𝑝 ) ) ∈ ℂ )
418 417 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ! ‘ ( 1st𝑝 ) ) ∈ ℂ )
419 16 adantr ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑅 ∈ Fin )
420 nfv 𝑘 ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 )
421 88 86 eqsstrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ⊆ ( ( 0 ... 𝑘 ) ↑m 𝑅 ) )
422 ovex ( 0 ... 𝐽 ) ∈ V
423 422 a1i ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 0 ... 𝐽 ) ∈ V )
424 mapss ( ( ( 0 ... 𝐽 ) ∈ V ∧ ( 0 ... 𝑘 ) ⊆ ( 0 ... 𝐽 ) ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
425 423 126 424 syl2anc ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
426 425 adantl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 0 ... 𝑘 ) ↑m 𝑅 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
427 421 426 sstrd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
428 427 3adant3 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝐶𝑅 ) ‘ 𝑘 ) ⊆ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
429 xp2nd ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
430 429 3ad2ant3 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) ∈ ( ( 𝐶𝑅 ) ‘ 𝑘 ) )
431 428 430 sseldd ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) ∈ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) )
432 elmapi ( ( 2nd𝑝 ) ∈ ( ( 0 ... 𝐽 ) ↑m 𝑅 ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) )
433 431 432 syl ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) )
434 433 3exp ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) ) ) )
435 434 adantr ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) ) ) )
436 397 420 435 rexlimd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) ) )
437 392 436 mpd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 2nd𝑝 ) : 𝑅 ⟶ ( 0 ... 𝐽 ) )
438 437 ffvelrnda ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) )
439 elfznn0 ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ℕ0 )
440 439 faccld ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℕ )
441 440 nncnd ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
442 438 441 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
443 419 442 fprodcl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
444 443 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℂ )
445 438 440 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℕ )
446 nnne0 ( ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ∈ ℕ → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
447 445 446 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
448 419 442 447 fprodn0 ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
449 448 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ≠ 0 )
450 418 444 449 divcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) ∈ ℂ )
451 17 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑅 ∈ Fin )
452 simpll ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → 𝜑 )
453 452 22 sylancom ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → 𝑡𝑇 )
454 452 136 syl ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
455 454 438 sseldd ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) )
456 452 453 455 3jca ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) )
457 eleq1 ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) )
458 457 3anbi3d ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) ) )
459 fveq2 ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) )
460 459 feq1d ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ ) )
461 458 460 imbi12d ( 𝑗 = ( ( 2nd𝑝 ) ‘ 𝑡 ) → ( ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ ) ) )
462 461 6 vtoclg ( ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝐽 ) → ( ( 𝜑𝑡𝑇 ∧ ( ( 2nd𝑝 ) ‘ 𝑡 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ ) )
463 438 456 462 sylc ( ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ )
464 463 adantllr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) : 𝑋 ⟶ ℂ )
465 25 adantlr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → 𝑥𝑋 )
466 464 465 ffvelrnd ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) ∧ 𝑡𝑅 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
467 451 466 fprodcl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
468 450 467 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) ∈ ℂ )
469 nfv 𝑘 ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 )
470 simp1 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝜑 )
471 404 3adant1 ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) )
472 fznn0sub2 ( ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
473 472 adantl ( ( 𝜑 ∧ ( 1st𝑝 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
474 470 471 473 syl2anc ( ( 𝜑𝑘 ∈ ( 0 ... 𝐽 ) ∧ 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
475 474 3exp ( 𝜑 → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) ) ) )
476 475 adantr ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝑘 ∈ ( 0 ... 𝐽 ) → ( 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) ) ) )
477 397 469 476 rexlimd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ∃ 𝑘 ∈ ( 0 ... 𝐽 ) 𝑝 ∈ ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) ) )
478 392 477 mpd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) )
479 simpl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝜑 )
480 479 31 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑍𝑇 )
481 479 136 syl ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
482 481 478 sseldd ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) )
483 479 480 482 3jca ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) )
484 eleq1 ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) )
485 484 3anbi3d ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) ) )
486 fveq2 ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) )
487 486 feq1d ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ ) )
488 485 487 imbi12d ( 𝑗 = ( 𝐽 − ( 1st𝑝 ) ) → ( ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ ) ) )
489 simp2 ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑍𝑇 )
490 id ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) )
491 34 3anbi2d ( 𝑡 = 𝑍 → ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ) )
492 180 fveq1d ( 𝑡 = 𝑍 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) )
493 492 feq1d ( 𝑡 = 𝑍 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) )
494 491 493 imbi12d ( 𝑡 = 𝑍 → ( ( ( 𝜑𝑡𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ) )
495 494 6 vtoclg ( 𝑍𝑇 → ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) )
496 489 490 495 sylc ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ )
497 488 496 vtoclg ( ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝐽 ) → ( ( 𝜑𝑍𝑇 ∧ ( 𝐽 − ( 1st𝑝 ) ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ ) )
498 478 483 497 sylc ( ( 𝜑𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ )
499 498 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) : 𝑋 ⟶ ℂ )
500 42 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → 𝑥𝑋 )
501 499 500 ffvelrnd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ∈ ℂ )
502 468 501 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ∈ ℂ )
503 413 502 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ) → ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
504 338 380 382 388 503 fsumf1o ( ( 𝜑𝑥𝑋 ) → Σ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) )
505 simpl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝜑 )
506 367 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) = { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
507 383 506 eleqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } )
508 375 sseli ( 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) ∣ Σ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( 𝑐𝑡 ) = 𝐽 } → 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) )
509 507 508 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) )
510 elmapi ( 𝑐 ∈ ( ( 0 ... 𝐽 ) ↑m ( 𝑅 ∪ { 𝑍 } ) ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝐽 ) )
511 509 510 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝐽 ) )
512 snidg ( 𝑍𝑇𝑍 ∈ { 𝑍 } )
513 31 512 syl ( 𝜑𝑍 ∈ { 𝑍 } )
514 elun2 ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑅 ∪ { 𝑍 } ) )
515 513 514 syl ( 𝜑𝑍 ∈ ( 𝑅 ∪ { 𝑍 } ) )
516 515 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑍 ∈ ( 𝑅 ∪ { 𝑍 } ) )
517 511 516 ffvelrnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) )
518 0zd ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 0 ∈ ℤ )
519 128 adantr ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 𝐽 ∈ ℤ )
520 fzssz ( 0 ... 𝐽 ) ⊆ ℤ
521 520 sseli ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( 𝑐𝑍 ) ∈ ℤ )
522 521 adantl ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℤ )
523 519 522 zsubcld ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ℤ )
524 elfzle2 ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( 𝑐𝑍 ) ≤ 𝐽 )
525 524 adantl ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑐𝑍 ) ≤ 𝐽 )
526 164 adantr ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 𝐽 ∈ ℝ )
527 522 zred ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℝ )
528 526 527 subge0d ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 0 ≤ ( 𝐽 − ( 𝑐𝑍 ) ) ↔ ( 𝑐𝑍 ) ≤ 𝐽 ) )
529 525 528 mpbird ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 0 ≤ ( 𝐽 − ( 𝑐𝑍 ) ) )
530 elfzle1 ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → 0 ≤ ( 𝑐𝑍 ) )
531 530 adantl ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → 0 ≤ ( 𝑐𝑍 ) )
532 526 527 subge02d ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 0 ≤ ( 𝑐𝑍 ) ↔ ( 𝐽 − ( 𝑐𝑍 ) ) ≤ 𝐽 ) )
533 531 532 mpbid ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ≤ 𝐽 )
534 518 519 523 529 533 elfzd ( ( 𝜑 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) )
535 505 517 534 syl2anc ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) )
536 bcval2 ( ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
537 535 536 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
538 164 recnd ( 𝜑𝐽 ∈ ℂ )
539 538 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝐽 ∈ ℂ )
540 zsscn ℤ ⊆ ℂ
541 520 540 sstri ( 0 ... 𝐽 ) ⊆ ℂ
542 541 a1i ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 0 ... 𝐽 ) ⊆ ℂ )
543 542 517 sseldd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℂ )
544 539 543 nncand ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( 𝑐𝑍 ) )
545 544 fveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ! ‘ ( 𝑐𝑍 ) ) )
546 545 oveq1d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
547 546 oveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
548 50 faccld ( 𝜑 → ( ! ‘ 𝐽 ) ∈ ℕ )
549 548 nncnd ( 𝜑 → ( ! ‘ 𝐽 ) ∈ ℂ )
550 549 adantr ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ 𝐽 ) ∈ ℂ )
551 elfznn0 ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( 𝑐𝑍 ) ∈ ℕ0 )
552 517 551 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ℕ0 )
553 552 faccld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ∈ ℕ )
554 553 nncnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ∈ ℂ )
555 elfznn0 ( ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ( 0 ... 𝐽 ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ℕ0 )
556 535 555 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 − ( 𝑐𝑍 ) ) ∈ ℕ0 )
557 556 faccld ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ∈ ℕ )
558 557 nncnd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ∈ ℂ )
559 553 nnne0d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ≠ 0 )
560 557 nnne0d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ≠ 0 )
561 550 554 558 559 560 divdiv1d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) )
562 561 eqcomd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ 𝐽 ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
563 537 547 562 3eqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
564 563 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) )
565 fvres ( 𝑡𝑅 → ( ( 𝑐𝑅 ) ‘ 𝑡 ) = ( 𝑐𝑡 ) )
566 565 fveq2d ( 𝑡𝑅 → ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) = ( ! ‘ ( 𝑐𝑡 ) ) )
567 566 prodeq2i 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) = ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) )
568 567 oveq2i ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) )
569 565 fveq2d ( 𝑡𝑅 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) )
570 569 fveq1d ( 𝑡𝑅 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
571 570 prodeq2i 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) = ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 )
572 568 571 oveq12i ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
573 572 a1i ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
574 573 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
575 558 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ∈ ℂ )
576 505 16 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑅 ∈ Fin )
577 79 ssriv ( 0 ... 𝐽 ) ⊆ ℕ0
578 577 a1i ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝐽 ) ⊆ ℕ0 )
579 511 adantr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝐽 ) )
580 elun1 ( 𝑡𝑅𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) )
581 580 adantl ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) )
582 579 581 ffvelrnd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝐽 ) )
583 578 582 sseldd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ℕ0 )
584 583 faccld ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ )
585 584 nncnd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
586 576 585 fprodcl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
587 586 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
588 17 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑅 ∈ Fin )
589 505 adantr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝜑 )
590 505 22 sylan ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑡𝑇 )
591 589 136 syl ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
592 591 582 sseldd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) )
593 589 590 592 148 syl3anc ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
594 593 adantllr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
595 25 adantlr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → 𝑥𝑋 )
596 594 595 ffvelrnd ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡𝑅 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
597 588 596 fprodcl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
598 576 584 fprodnncl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ )
599 nnne0 ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
600 598 599 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
601 600 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
602 575 587 597 601 div32d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
603 574 602 eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
604 544 fveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) )
605 604 fveq1d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) )
606 605 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) )
607 603 606 oveq12d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) )
608 597 587 601 divcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ∈ ℂ )
609 505 31 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑍𝑇 )
610 505 136 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 0 ... 𝐽 ) ⊆ ( 0 ... 𝑁 ) )
611 610 517 sseldd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) )
612 505 609 611 3jca ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) )
613 eleq1 ( 𝑗 = ( 𝑐𝑍 ) → ( 𝑗 ∈ ( 0 ... 𝑁 ) ↔ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) )
614 613 3anbi3d ( 𝑗 = ( 𝑐𝑍 ) → ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) ↔ ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) ) )
615 fveq2 ( 𝑗 = ( 𝑐𝑍 ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) )
616 615 feq1d ( 𝑗 = ( 𝑐𝑍 ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ↔ ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ ) )
617 614 616 imbi12d ( 𝑗 = ( 𝑐𝑍 ) → ( ( ( 𝜑𝑍𝑇𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ 𝑗 ) : 𝑋 ⟶ ℂ ) ↔ ( ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ ) ) )
618 617 496 vtoclg ( ( 𝑐𝑍 ) ∈ ( 0 ... 𝐽 ) → ( ( 𝜑𝑍𝑇 ∧ ( 𝑐𝑍 ) ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ ) )
619 517 612 618 sylc ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ )
620 619 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) : 𝑋 ⟶ ℂ )
621 42 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑥𝑋 )
622 620 621 ffvelrnd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ∈ ℂ )
623 575 608 622 mulassd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) )
624 607 623 eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) = ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) )
625 564 624 oveq12d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) = ( ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) ) )
626 549 ad2antrr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ 𝐽 ) ∈ ℂ )
627 554 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ∈ ℂ )
628 559 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝑐𝑍 ) ) ≠ 0 )
629 626 627 628 divcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) ∈ ℂ )
630 608 622 mulcld ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ∈ ℂ )
631 560 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ≠ 0 )
632 629 575 630 631 dmmcand ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) / ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) ) · ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) )
633 597 622 587 601 div23d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) )
634 633 eqcomd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) )
635 nfv 𝑡 ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) )
636 nfcv 𝑡 ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 )
637 609 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑍𝑇 )
638 20 adantr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ¬ 𝑍𝑅 )
639 fveq2 ( 𝑡 = 𝑍 → ( 𝑐𝑡 ) = ( 𝑐𝑍 ) )
640 180 639 fveq12d ( 𝑡 = 𝑍 → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) = ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) )
641 640 fveq1d ( 𝑡 = 𝑍 → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) )
642 635 636 588 637 638 596 641 622 fprodsplitsn ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) = ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) )
643 642 eqcomd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) )
644 643 oveq1d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) )
645 634 644 eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) = ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) )
646 645 oveq2d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
647 588 369 371 sylancl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑅 ∪ { 𝑍 } ) ∈ Fin )
648 505 adantr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝜑 )
649 348 sselda ( ( 𝜑𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝑡𝑇 )
650 649 adantlr ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝑡𝑇 )
651 511 610 fssd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → 𝑐 : ( 𝑅 ∪ { 𝑍 } ) ⟶ ( 0 ... 𝑁 ) )
652 651 ffvelrnda ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝑁 ) )
653 648 650 652 148 syl3anc ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
654 653 adantllr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) : 𝑋 ⟶ ℂ )
655 621 adantr ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → 𝑥𝑋 )
656 654 655 ffvelrnd ( ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
657 647 656 fprodcl ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ∈ ℂ )
658 626 627 657 587 628 601 divmuldivd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) )
659 554 586 mulcomd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) · ( ! ‘ ( 𝑐𝑍 ) ) ) )
660 nfv 𝑡 ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) )
661 nfcv 𝑡 ( ! ‘ ( 𝑐𝑍 ) )
662 505 19 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ¬ 𝑍𝑅 )
663 639 fveq2d ( 𝑡 = 𝑍 → ( ! ‘ ( 𝑐𝑡 ) ) = ( ! ‘ ( 𝑐𝑍 ) ) )
664 660 661 576 609 662 585 663 554 fprodsplitsn ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) = ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) · ( ! ‘ ( 𝑐𝑍 ) ) ) )
665 664 eqcomd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) · ( ! ‘ ( 𝑐𝑍 ) ) ) = ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) )
666 659 665 eqtrd ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) = ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) )
667 666 oveq2d ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) )
668 667 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) )
669 505 372 syl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( 𝑅 ∪ { 𝑍 } ) ∈ Fin )
670 577 a1i ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 0 ... 𝐽 ) ⊆ ℕ0 )
671 511 ffvelrnda ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 𝑐𝑡 ) ∈ ( 0 ... 𝐽 ) )
672 670 671 sseldd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( 𝑐𝑡 ) ∈ ℕ0 )
673 672 faccld ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℕ )
674 673 nncnd ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
675 669 674 fprodcl ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
676 675 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ∈ ℂ )
677 673 nnne0d ( ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) ∧ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ) → ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
678 669 674 677 fprodn0 ( ( 𝜑𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
679 678 adantlr ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ≠ 0 )
680 626 657 676 679 div23d ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
681 eqidd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
682 668 680 681 3eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) / ( ( ! ‘ ( 𝑐𝑍 ) ) · ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
683 646 658 682 3eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( ( ! ‘ 𝐽 ) / ( ! ‘ ( 𝑐𝑍 ) ) ) · ( ( ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) / ∏ 𝑡𝑅 ( ! ‘ ( 𝑐𝑡 ) ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝑐𝑍 ) ) ‘ 𝑥 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
684 625 632 683 3eqtrd ( ( ( 𝜑𝑥𝑋 ) ∧ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ) → ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) = ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
685 684 sumeq2dv ( ( 𝜑𝑥𝑋 ) → Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( 𝐽 C ( 𝐽 − ( 𝑐𝑍 ) ) ) · ( ( ( ( ! ‘ ( 𝐽 − ( 𝑐𝑍 ) ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 𝑐𝑅 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 𝐽 − ( 𝑐𝑍 ) ) ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
686 504 685 eqtrd ( ( 𝜑𝑥𝑋 ) → Σ 𝑝 𝑘 ∈ ( 0 ... 𝐽 ) ( { 𝑘 } × ( ( 𝐶𝑅 ) ‘ 𝑘 ) ) ( ( 𝐽 C ( 1st𝑝 ) ) · ( ( ( ( ! ‘ ( 1st𝑝 ) ) / ∏ 𝑡𝑅 ( ! ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ) · ∏ 𝑡𝑅 ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( ( 2nd𝑝 ) ‘ 𝑡 ) ) ‘ 𝑥 ) ) · ( ( ( 𝑆 D𝑛 ( 𝐻𝑍 ) ) ‘ ( 𝐽 − ( 1st𝑝 ) ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
687 295 319 686 3eqtrd ( ( 𝜑𝑥𝑋 ) → Σ 𝑘 ∈ ( 0 ... 𝐽 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) = Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) )
688 687 mpteq2dva ( 𝜑 → ( 𝑥𝑋 ↦ Σ 𝑘 ∈ ( 0 ... 𝐽 ) ( ( 𝐽 C 𝑘 ) · ( ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ∏ 𝑡𝑅 ( ( 𝐻𝑡 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ 𝑘 ) ‘ 𝑥 ) · ( ( ( 𝑘 ∈ ( 0 ... 𝐽 ) ↦ ( ( 𝑆 D𝑛 ( 𝑦𝑋 ↦ ( ( 𝐻𝑍 ) ‘ 𝑦 ) ) ) ‘ 𝑘 ) ) ‘ ( 𝐽𝑘 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )
689 47 210 688 3eqtrd ( 𝜑 → ( ( 𝑆 D𝑛 ( 𝑥𝑋 ↦ ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( 𝐻𝑡 ) ‘ 𝑥 ) ) ) ‘ 𝐽 ) = ( 𝑥𝑋 ↦ Σ 𝑐 ∈ ( ( 𝐶 ‘ ( 𝑅 ∪ { 𝑍 } ) ) ‘ 𝐽 ) ( ( ( ! ‘ 𝐽 ) / ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ! ‘ ( 𝑐𝑡 ) ) ) · ∏ 𝑡 ∈ ( 𝑅 ∪ { 𝑍 } ) ( ( ( 𝑆 D𝑛 ( 𝐻𝑡 ) ) ‘ ( 𝑐𝑡 ) ) ‘ 𝑥 ) ) ) )