Metamath Proof Explorer


Theorem etransclem42

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

Ref Expression
Hypotheses etransclem42.s φS
etransclem42.x φXTopOpenfld𝑡S
etransclem42.p φP
etransclem42.m φM0
etransclem42.f F=xXxP1j=1MxjP
etransclem42.n φN0
etransclem42.jx φJX
etransclem42.jz φJ
Assertion etransclem42 φSDnFNJ

Proof

Step Hyp Ref Expression
1 etransclem42.s φS
2 etransclem42.x φXTopOpenfld𝑡S
3 etransclem42.p φP
4 etransclem42.m φM0
5 etransclem42.f F=xXxP1j=1MxjP
6 etransclem42.n φN0
7 etransclem42.jx φJX
8 etransclem42.jz φJ
9 etransclem5 k0MyXykifk=0P1P=j0MxXxjifj=0P1P
10 etransclem11 m0d0m0M|k=0Mdk=m=n0c0n0M|j=0Mcj=n
11 1 2 3 4 5 6 9 7 8 10 etransclem36 φSDnFNJ