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 φ X TopOpen fld 𝑡 S
etransclem42.p φ P
etransclem42.m φ M 0
etransclem42.f F = x X x P 1 j = 1 M x j P
etransclem42.n φ N 0
etransclem42.jx φ J X
etransclem42.jz φ J
Assertion etransclem42 φ S D n F N J

Proof

Step Hyp Ref Expression
1 etransclem42.s φ S
2 etransclem42.x φ X TopOpen fld 𝑡 S
3 etransclem42.p φ P
4 etransclem42.m φ M 0
5 etransclem42.f F = x X x P 1 j = 1 M x j P
6 etransclem42.n φ N 0
7 etransclem42.jx φ J X
8 etransclem42.jz φ J
9 etransclem5 k 0 M y X y k if k = 0 P 1 P = j 0 M x X x j if j = 0 P 1 P
10 etransclem11 m 0 d 0 m 0 M | k = 0 M d k = m = n 0 c 0 n 0 M | j = 0 M c j = n
11 1 2 3 4 5 6 9 7 8 10 etransclem36 φ S D n F N J