Theorem etransclem36

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

	Ref	Expression
Hypotheses	etransclem36.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	etransclem36.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
	etransclem36.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem36.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	etransclem36.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
	etransclem36.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	etransclem36.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
	etransclem36.jx	⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
	etransclem36.jz	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
	etransclem36.10	⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
Assertion	etransclem36	⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		etransclem36.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		etransclem36.x	⊢ ( 𝜑 → 𝑋 ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
3		etransclem36.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
4		etransclem36.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
5		etransclem36.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 ↑ ( 𝑃 − 1 ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) ( ( 𝑥 − 𝑗 ) ↑ 𝑃 ) ) )
6		etransclem36.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
7		etransclem36.h	⊢ 𝐻 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑥 − 𝑗 ) ↑ if ( 𝑗 = 0 , ( 𝑃 − 1 ) , 𝑃 ) ) ) )
8		etransclem36.jx	⊢ ( 𝜑 → 𝐽 ∈ 𝑋 )
9		etransclem36.jz	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
10		etransclem36.10	⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
11	1 2 3 4 5 6 7 10 8	etransclem31	⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) = Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) )
12	10 6	etransclem16	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) ∈ Fin )
13	3	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑃 ∈ ℕ )
14	4	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑀 ∈ ℕ0 )
15	6	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
16	9	adantr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝐽 ∈ ℤ )
17		etransclem11	⊢ ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } ) = ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } )
18		etransclem11	⊢ ( 𝑚 ∈ ℕ0 ↦ { 𝑑 ∈ ( ( 0 ... 𝑚 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑀 ) ( 𝑑 ‘ 𝑘 ) = 𝑚 } ) = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑒 ‘ 𝑗 ) = 𝑛 } )
19	10 17 18	3eqtri	⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑒 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑒 ‘ 𝑗 ) = 𝑛 } )
20		simpr	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) )
21	13 14 15 16 19 20	etransclem26	⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ) → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ )
22	12 21	fsumzcl	⊢ ( 𝜑 → Σ 𝑐 ∈ ( 𝐶 ‘ 𝑁 ) ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝑐 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝑐 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝑐 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝑐 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝑐 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ )
23	11 22	eqeltrd	⊢ ( 𝜑 → ( ( ( 𝑆 D𝑛 𝐹 ) ‘ 𝑁 ) ‘ 𝐽 ) ∈ ℤ )