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