etransclem31

Description: The N -th derivative of H applied to Y . (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem31.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	etransclem31.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
	etransclem31.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem31.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
	etransclem31.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
	etransclem31.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	etransclem31.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
	etransclem31.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ₀ ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
	etransclem31.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
Assertion	etransclem31	⊢ ( 𝜑 → ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝑌 ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		etransclem31.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		etransclem31.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
3		etransclem31.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4		etransclem31.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ₀ )
5		etransclem31.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
6		etransclem31.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
7		etransclem31.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
8		etransclem31.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ₀ ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
9		etransclem31.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑋 )
10	1 2 3 4 5 6 7 8	etransclem30	⊢ ( 𝜑 → ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) ) )
11		fveq2	⊢ ( 𝑥 = 𝑌 → ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) )
12	11	prodeq2ad	⊢ ( 𝑥 = 𝑌 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) )
13	12	oveq2d	⊢ ( 𝑥 = 𝑌 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) )
14	13	sumeq2sdv	⊢ ( 𝑥 = 𝑌 → Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) )
15	14	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑥 ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) )
16	8 6	etransclem16	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ∈ Fin )
17	6	faccld	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℕ )
18	17	nncnd	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) ∈ ℂ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ! ‘ 𝑁 ) ∈ ℂ )
20		fzfid	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 0 ... 𝑀 ) ∈ Fin )
21		fzssnn0	⊢ ( 0 ... 𝑁 ) ⊆ ℕ₀
22		ssrab2	⊢ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ⊆ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) )
24	8 6	etransclem12	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
25	24	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( 𝐶 ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
26	23 25	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
27	22 26	sselid	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) ) )
28	27	adantr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) ) )
29		elmapi	⊢ ( 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑_m ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
30	28 29	syl	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑐 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
31		simpr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
32	30 31	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑗 ) ∈ ( 0 ... 𝑁 ) )
33	21 32	sselid	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( 𝑐 ‘ 𝑗 ) ∈ ℕ₀ )
34	33	faccld	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ∈ ℕ )
35	34	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ∈ ℂ )
36	20 35	fprodcl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ∈ ℂ )
37	34	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ≠ 0 )
38	20 35 37	fprodn0	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ≠ 0 )
39	19 36 38	divcld	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) ∈ ℂ )
40	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑆 ∈ { ℝ , ℂ } )
41	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂ_fld ) ↾_t 𝑆 ) )
42	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
43		etransclem5	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
44	7 43	eqtri	⊢ 𝐻 = ( 𝑘 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑘 ) ↑ if ( 𝑘 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
45	40 41 42 44 31 33	etransclem20	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) : 𝑋 ⟶ ℂ )
46	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑌 ∈ 𝑋 )
47	45 46	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ∈ ℂ )
48	20 47	fprodcl	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ∈ ℂ )
49	39 48	mulcld	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) ∈ ℂ )
50	16 49	fsumcl	⊢ ( 𝜑 → Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) ∈ ℂ )
51	10 15 9 50	fvmptd	⊢ ( 𝜑 → ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝑌 ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) )
52	40 41 42 44 31 33 46	etransclem21	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) = if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) )
53	52	prodeq2dv	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) )
54		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
55	4 54	eleqtrdi	⊢ ( 𝜑 → 𝑀 ∈ ( ℤ_≥ ‘ 0 ) )
56	55	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑀 ∈ ( ℤ_≥ ‘ 0 ) )
57	52 47	eqeltrrd	⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ∈ ℂ )
58		iftrue	⊢ ( 𝑗 = 0 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = ( 𝑃 − 1 ) )
59		fveq2	⊢ ( 𝑗 = 0 → ( 𝑐 ‘ 𝑗 ) = ( 𝑐 ‘ 0 ) )
60	58 59	breq12d	⊢ ( 𝑗 = 0 → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) ↔ ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) ) )
61	58	fveq2d	⊢ ( 𝑗 = 0 → ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ! ‘ ( 𝑃 − 1 ) ) )
62	58 59	oveq12d	⊢ ( 𝑗 = 0 → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) = ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) )
63	62	fveq2d	⊢ ( 𝑗 = 0 → ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) = ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) )
64	61 63	oveq12d	⊢ ( 𝑗 = 0 → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) )
65		oveq2	⊢ ( 𝑗 = 0 → ( 𝑌 − 𝑗 ) = ( 𝑌 − 0 ) )
66	65 62	oveq12d	⊢ ( 𝑗 = 0 → ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) = ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) )
67	64 66	oveq12d	⊢ ( 𝑗 = 0 → ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) )
68	60 67	ifbieq2d	⊢ ( 𝑗 = 0 → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) )
69	56 57 68	fprod1p	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) )
70	1 2	dvdmsscn	⊢ ( 𝜑 → 𝑋 ⊆ ℂ )
71	70 9	sseldd	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
72	71	subid1d	⊢ ( 𝜑 → ( 𝑌 − 0 ) = 𝑌 )
73	72	oveq1d	⊢ ( 𝜑 → ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) = ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) )
74	73	oveq2d	⊢ ( 𝜑 → ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) = ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) )
75	74	ifeq2d	⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) = if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) )
76		0p1e1	⊢ ( 0 + 1 ) = 1
77	76	oveq1i	⊢ ( ( 0 + 1 ) ... 𝑀 ) = ( 1 ... 𝑀 )
78	77	prodeq1i	⊢ ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) )
79		0red	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 ∈ ℝ )
80		1red	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ∈ ℝ )
81		elfzelz	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℤ )
82	81	zred	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ℝ )
83		0lt1	⊢ 0 < 1
84	83	a1i	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 1 )
85		elfzle1	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 1 ≤ 𝑗 )
86	79 80 82 84 85	ltletrd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 0 < 𝑗 )
87	86	gt0ne0d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ≠ 0 )
88	87	neneqd	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ¬ 𝑗 = 0 )
89	88	iffalsed	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) = 𝑃 )
90	89	breq1d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) ↔ 𝑃 < ( 𝑐 ‘ 𝑗 ) ) )
91	89	fveq2d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) = ( ! ‘ 𝑃 ) )
92	89	oveq1d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) = ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) )
93	92	fveq2d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) = ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) )
94	91 93	oveq12d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) = ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) )
95	92	oveq2d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) = ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) )
96	94 95	oveq12d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) = ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) )
97	90 96	ifbieq2d	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) )
98	97	prodeq2i	⊢ ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) )
99	78 98	eqtri	⊢ ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) )
100	99	a1i	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) = ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) )
101	75 100	oveq12d	⊢ ( 𝜑 → ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) = ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) )
102	101	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( ( 𝑌 − 0 ) ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) = ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) )
103	53 69 102	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) = ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) )
104	103	oveq2d	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) = ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )
105	104	sumeq2dv	⊢ ( 𝜑 → Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D^𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( 𝑐 ‘ 𝑗 ) ) ‘ 𝑌 ) ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )
106	51 105	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑆 D^𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝑌 ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝑌 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝑌 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )

Metamath Proof Explorer

Theorem etransclem31

Proof