Metamath Proof Explorer


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

Proof

Step Hyp Ref Expression
1 etransclem36.s φ S
2 etransclem36.x φ X TopOpen fld 𝑡 S
3 etransclem36.p φ P
4 etransclem36.m φ M 0
5 etransclem36.f F = x X x P 1 j = 1 M x j P
6 etransclem36.n φ N 0
7 etransclem36.h H = j 0 M x X x j if j = 0 P 1 P
8 etransclem36.jx φ J X
9 etransclem36.jz φ J
10 etransclem36.10 C = n 0 c 0 n 0 M | j = 0 M c j = n
11 1 2 3 4 5 6 7 10 8 etransclem31 φ S D n F N J = c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
12 10 6 etransclem16 φ C N Fin
13 3 adantr φ c C N P
14 4 adantr φ c C N M 0
15 6 adantr φ c C N N 0
16 9 adantr φ c C N J
17 etransclem11 n 0 c 0 n 0 M | j = 0 M c j = n = m 0 d 0 m 0 M | k = 0 M d k = m
18 etransclem11 m 0 d 0 m 0 M | k = 0 M d k = m = n 0 e 0 n 0 M | j = 0 M e j = n
19 10 17 18 3eqtri C = n 0 e 0 n 0 M | j = 0 M e j = n
20 simpr φ c C N c C N
21 13 14 15 16 19 20 etransclem26 φ c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
22 12 21 fsumzcl φ c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! J P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! J j P c j
23 11 22 eqeltrd φ S D n F N J