Theorem etransclem26

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

	Ref	Expression
Hypotheses	etransclem26.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
	etransclem26.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
	etransclem26.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	etransclem26.jz	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
	etransclem26.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
	etransclem26.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ‘ 𝑁 ) )
Assertion	etransclem26	⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		etransclem26.p	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
2		etransclem26.m	⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
3		etransclem26.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
4		etransclem26.jz	⊢ ( 𝜑 → 𝐽 ∈ ℤ )
5		etransclem26.c	⊢ 𝐶 = ( 𝑛 ∈ ℕ0 ↦ { 𝑐 ∈ ( ( 0 ... 𝑛 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑛 } )
6		etransclem26.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 ‘ 𝑁 ) )
7	5 3	etransclem12	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑁 ) = { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
8	6 7	eleqtrd	⊢ ( 𝜑 → 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } )
9		fveq1	⊢ ( 𝑐 = 𝐷 → ( 𝑐 ‘ 𝑗 ) = ( 𝐷 ‘ 𝑗 ) )
10	9	sumeq2sdv	⊢ ( 𝑐 = 𝐷 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) )
11	10	eqeq1d	⊢ ( 𝑐 = 𝐷 → ( Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 ↔ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 ) )
12	11	elrab	⊢ ( 𝐷 ∈ { 𝑐 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∣ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝑐 ‘ 𝑗 ) = 𝑁 } ↔ ( 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 ) )
13	8 12	sylib	⊢ ( 𝜑 → ( 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ∧ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 ) )
14	13	simprd	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) = 𝑁 )
15	14	eqcomd	⊢ ( 𝜑 → 𝑁 = Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( ! ‘ 𝑁 ) = ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) )
17	16	oveq1d	⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) = ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) )
18		nfcv	⊢ Ⅎ 𝑗 𝐷
19		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑀 ) ∈ Fin )
20		nn0ex	⊢ ℕ0 ∈ V
21		fzssnn0	⊢ ( 0 ... 𝑁 ) ⊆ ℕ0
22		mapss	⊢ ( ( ℕ0 ∈ V ∧ ( 0 ... 𝑁 ) ⊆ ℕ0 ) → ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
23	20 21 22	mp2an	⊢ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) ⊆ ( ℕ0 ↑m ( 0 ... 𝑀 ) )
24	13	simpld	⊢ ( 𝜑 → 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) )
25	23 24	sselid	⊢ ( 𝜑 → 𝐷 ∈ ( ℕ0 ↑m ( 0 ... 𝑀 ) ) )
26	18 19 25	mccl	⊢ ( 𝜑 → ( ( ! ‘ Σ 𝑗 ∈ ( 0 ... 𝑀 ) ( 𝐷 ‘ 𝑗 ) ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℕ )
27	17 26	eqeltrd	⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℕ )
28	27	nnzd	⊢ ( 𝜑 → ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) ∈ ℤ )
29		elmapi	⊢ ( 𝐷 ∈ ( ( 0 ... 𝑁 ) ↑m ( 0 ... 𝑀 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
30	24 29	syl	⊢ ( 𝜑 → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
31	1 2 30 4	etransclem10	⊢ ( 𝜑 → if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) ∈ ℤ )
32		fzfid	⊢ ( 𝜑 → ( 1 ... 𝑀 ) ∈ Fin )
33	1	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑃 ∈ ℕ )
34	30	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐷 : ( 0 ... 𝑀 ) ⟶ ( 0 ... 𝑁 ) )
35		0z	⊢ 0 ∈ ℤ
36		fzp1ss	⊢ ( 0 ∈ ℤ → ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 ) )
37	35 36	ax-mp	⊢ ( ( 0 + 1 ) ... 𝑀 ) ⊆ ( 0 ... 𝑀 )
38		1e0p1	⊢ 1 = ( 0 + 1 )
39	38	oveq1i	⊢ ( 1 ... 𝑀 ) = ( ( 0 + 1 ) ... 𝑀 )
40	39	eleq2i	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) ↔ 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) )
41	40	biimpi	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( ( 0 + 1 ) ... 𝑀 ) )
42	37 41	sselid	⊢ ( 𝑗 ∈ ( 1 ... 𝑀 ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
43	42	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝑗 ∈ ( 0 ... 𝑀 ) )
44	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → 𝐽 ∈ ℤ )
45	33 34 43 44	etransclem3	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 1 ... 𝑀 ) ) → if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
46	32 45	fprodzcl	⊢ ( 𝜑 → ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ∈ ℤ )
47	31 46	zmulcld	⊢ ( 𝜑 → ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ∈ ℤ )
48	28 47	zmulcld	⊢ ( 𝜑 → ( ( ( ! ‘ 𝑁 ) / ∏ 𝑗 ∈ ( 0 ... 𝑀 ) ( ! ‘ ( 𝐷 ‘ 𝑗 ) ) ) · ( if ( ( 𝑃 − 1 ) < ( 𝐷 ‘ 0 ) , 0 , ( ( ( ! ‘ ( 𝑃 − 1 ) ) / ( ! ‘ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) · ( 𝐽 ↑ ( ( 𝑃 − 1 ) − ( 𝐷 ‘ 0 ) ) ) ) ) · ∏ 𝑗 ∈ ( 1 ... 𝑀 ) if ( 𝑃 < ( 𝐷 ‘ 𝑗 ) , 0 , ( ( ( ! ‘ 𝑃 ) / ( ! ‘ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) · ( ( 𝐽 − 𝑗 ) ↑ ( 𝑃 − ( 𝐷 ‘ 𝑗 ) ) ) ) ) ) ) ∈ ℤ )