Theorem etransclem27

Description: The N -th derivative of F applied to J is an integer. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	etransclem27.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	etransclem27.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
	etransclem27.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem27.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
	etransclem27.cfi	⊢ ( 𝜑 → 𝐶 ∈ Fin )
	etransclem27.cf	⊢ ( 𝜑 → 𝐶 : dom 𝐶 ⟶ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
	etransclem27.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) )
	etransclem27.jx	⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
	etransclem27.jz	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
Assertion	etransclem27	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐽 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		etransclem27.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		etransclem27.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3		etransclem27.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4		etransclem27.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
5		etransclem27.cfi	⊢ ( 𝜑 → 𝐶 ∈ Fin )
6		etransclem27.cf	⊢ ( 𝜑 → 𝐶 : dom 𝐶 ⟶ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
7		etransclem27.g	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) )
8		etransclem27.jx	⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
9		etransclem27.jz	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
10		fveq2	⊢ ( 𝑥 = 𝐽 → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) = ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
11	10	prodeq2ad	⊢ ( 𝑥 = 𝐽 → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) = ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
12	11	sumeq2sdv	⊢ ( 𝑥 = 𝐽 → Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝑥 ) = Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
13		dmfi	⊢ ( 𝐶 ∈ Fin → dom 𝐶 ∈ Fin )
14	5 13	syl	⊢ ( 𝜑 → dom 𝐶 ∈ Fin )
15		fzfid	⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ( 0 ... 𝑀 ) ∈ Fin )
16	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑆 ∈ { ℝ , ℂ } )
17	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
18	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
19		etransclem5	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) ) = ( 𝑧 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑧 ) ↑ if ( 𝑧 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
20	4 19	eqtri	⊢ 𝐻 = ( 𝑧 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑦 ∈ 𝑋 ↦ ( ( 𝑦 − 𝑧 ) ↑ if ( 𝑧 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
21		simpr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
22	6	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ( 𝐶 ‘ 𝑙 ) ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
23		elmapi	⊢ ( ( 𝐶 ‘ 𝑙 ) ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) → ( 𝐶 ‘ 𝑙 ) : ( 0 ... 𝑀 ) ⟶ ℕ0 )
24	22 23	syl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ( 𝐶 ‘ 𝑙 ) : ( 0 ... 𝑀 ) ⟶ ℕ0 )
25	24	ffvelcdmda	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℕ0 )
26	16 17 18 20 21 25	etransclem20	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) : 𝑋 ⟶ ℂ )
27	8	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 𝐽 ∈ 𝑋 )
28	26 27	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℂ )
29	15 28	fprodcl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℂ )
30	14 29	fsumcl	⊢ ( 𝜑 → Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℂ )
31	7 12 8 30	fvmptd3	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐽 ) = Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) )
32	16 17 18 20 21 25 27	etransclem21	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) = if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) )
33		iftrue	⊢ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) = 0 )
34		0zd	⊢ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) → 0 ∈ ℤ )
35	33 34	eqeltrd	⊢ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
36	35	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
37		0zd	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 0 ∈ ℤ )
38		nnm1nn0	⊢ ( 𝑃 ∈ ℕ → ( 𝑃 − 1 ) ∈ ℕ0 )
39	3 38	syl	⊢ ( 𝜑 → ( 𝑃 − 1 ) ∈ ℕ0 )
40	3	nnnn0d	⊢ ( 𝜑 → 𝑃 ∈ ℕ0 )
41	39 40	ifcld	⊢ ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℕ0 )
42	41	nn0zd	⊢ ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
43	42	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℤ )
44	25	nn0zd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℤ )
45	44	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℤ )
46	43 45	zsubcld	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℤ )
47	45	zred	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℝ )
48	43	zred	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
49		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) )
50	47 48 49	nltled	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
51	48 47	subge0d	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( 0 ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ↔ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
52	50 51	mpbird	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 0 ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) )
53		0red	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ∈ ℝ )
54	25	nn0red	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ∈ ℝ )
55	41	nn0red	⊢ ( 𝜑 → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
56	55	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℝ )
57	25	nn0ge0d	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → 0 ≤ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) )
58	53 54 56 57	lesub2dd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 0 ) )
59	56	recnd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ∈ ℂ )
60	59	subid1d	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − 0 ) = if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
61	58 60	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
62	61	adantr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ≤ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) )
63	37 43 46 52 62	elfzd	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ( 0 ... if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) )
64		permnn	⊢ ( ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ( 0 ... if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℕ )
65	63 64	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℕ )
66	65	nnzd	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℤ )
67	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 𝐽 ∈ ℤ )
68		elfzelz	⊢ ( 𝑗 ∈ ( 0 ... 𝑀 ) → 𝑗 ∈ ℤ )
69	68	ad2antlr	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → 𝑗 ∈ ℤ )
70	67 69	zsubcld	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( 𝐽 − 𝑗 ) ∈ ℤ )
71		elnn0z	⊢ ( ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℕ0 ↔ ( ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℤ ∧ 0 ≤ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) )
72	46 52 71	sylanbrc	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℕ0 )
73		zexpcl	⊢ ( ( ( 𝐽 − 𝑗 ) ∈ ℤ ∧ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ∈ ℕ0 ) → ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ∈ ℤ )
74	70 72 73	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ∈ ℤ )
75	66 74	zmulcld	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ∈ ℤ )
76	37 75	ifcld	⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) ∧ ¬ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
77	36 76	pm2.61dan	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → if ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) < ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) , 0 , ( ( ( ! ‘ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) / ( ! ‘ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) − ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
78	32 77	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) ∧ 𝑗 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℤ )
79	15 78	fprodzcl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ dom 𝐶 ) → ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℤ )
80	14 79	fsumzcl	⊢ ( 𝜑 → Σ 𝑙 ∈ dom 𝐶 ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ( ( 𝑆 D𝑛 ( 𝐻 ‘ 𝑗 ) ) ‘ ( ( 𝐶 ‘ 𝑙 ) ‘ 𝑗 ) ) ‘ 𝐽 ) ∈ ℤ )
81	31 80	eqeltrd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝐽 ) ∈ ℤ )