Metamath Proof Explorer


Theorem etransclem31

Description: The N -th derivative of H applied to Y . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem31.s φ S
etransclem31.x φ X TopOpen fld 𝑡 S
etransclem31.p φ P
etransclem31.m φ M 0
etransclem31.f F = x X x P 1 j = 1 M x j P
etransclem31.n φ N 0
etransclem31.h H = j 0 M x X x j if j = 0 P 1 P
etransclem31.c C = n 0 c 0 n 0 M | j = 0 M c j = n
etransclem31.y φ Y X
Assertion etransclem31 φ S D n F N Y = c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! Y j P c j

Proof

Step Hyp Ref Expression
1 etransclem31.s φ S
2 etransclem31.x φ X TopOpen fld 𝑡 S
3 etransclem31.p φ P
4 etransclem31.m φ M 0
5 etransclem31.f F = x X x P 1 j = 1 M x j P
6 etransclem31.n φ N 0
7 etransclem31.h H = j 0 M x X x j if j = 0 P 1 P
8 etransclem31.c C = n 0 c 0 n 0 M | j = 0 M c j = n
9 etransclem31.y φ Y X
10 1 2 3 4 5 6 7 8 etransclem30 φ S D n F N = x X c C N N ! j = 0 M c j ! j = 0 M S D n H j c j x
11 fveq2 x = Y S D n H j c j x = S D n H j c j Y
12 11 prodeq2ad x = Y j = 0 M S D n H j c j x = j = 0 M S D n H j c j Y
13 12 oveq2d x = Y N ! j = 0 M c j ! j = 0 M S D n H j c j x = N ! j = 0 M c j ! j = 0 M S D n H j c j Y
14 13 sumeq2sdv x = Y c C N N ! j = 0 M c j ! j = 0 M S D n H j c j x = c C N N ! j = 0 M c j ! j = 0 M S D n H j c j Y
15 14 adantl φ x = Y c C N N ! j = 0 M c j ! j = 0 M S D n H j c j x = c C N N ! j = 0 M c j ! j = 0 M S D n H j c j Y
16 8 6 etransclem16 φ C N Fin
17 6 faccld φ N !
18 17 nncnd φ N !
19 18 adantr φ c C N N !
20 fzfid φ c C N 0 M Fin
21 fzssnn0 0 N 0
22 ssrab2 c 0 N 0 M | j = 0 M c j = N 0 N 0 M
23 simpr φ c C N c C N
24 8 6 etransclem12 φ C N = c 0 N 0 M | j = 0 M c j = N
25 24 adantr φ c C N C N = c 0 N 0 M | j = 0 M c j = N
26 23 25 eleqtrd φ c C N c c 0 N 0 M | j = 0 M c j = N
27 22 26 sseldi φ c C N c 0 N 0 M
28 27 adantr φ c C N j 0 M c 0 N 0 M
29 elmapi c 0 N 0 M c : 0 M 0 N
30 28 29 syl φ c C N j 0 M c : 0 M 0 N
31 simpr φ c C N j 0 M j 0 M
32 30 31 ffvelrnd φ c C N j 0 M c j 0 N
33 21 32 sseldi φ c C N j 0 M c j 0
34 33 faccld φ c C N j 0 M c j !
35 34 nncnd φ c C N j 0 M c j !
36 20 35 fprodcl φ c C N j = 0 M c j !
37 34 nnne0d φ c C N j 0 M c j ! 0
38 20 35 37 fprodn0 φ c C N j = 0 M c j ! 0
39 19 36 38 divcld φ c C N N ! j = 0 M c j !
40 1 ad2antrr φ c C N j 0 M S
41 2 ad2antrr φ c C N j 0 M X TopOpen fld 𝑡 S
42 3 ad2antrr φ c C N j 0 M P
43 etransclem5 j 0 M x X x j if j = 0 P 1 P = k 0 M y X y k if k = 0 P 1 P
44 7 43 eqtri H = k 0 M y X y k if k = 0 P 1 P
45 40 41 42 44 31 33 etransclem20 φ c C N j 0 M S D n H j c j : X
46 9 ad2antrr φ c C N j 0 M Y X
47 45 46 ffvelrnd φ c C N j 0 M S D n H j c j Y
48 20 47 fprodcl φ c C N j = 0 M S D n H j c j Y
49 39 48 mulcld φ c C N N ! j = 0 M c j ! j = 0 M S D n H j c j Y
50 16 49 fsumcl φ c C N N ! j = 0 M c j ! j = 0 M S D n H j c j Y
51 10 15 9 50 fvmptd φ S D n F N Y = c C N N ! j = 0 M c j ! j = 0 M S D n H j c j Y
52 40 41 42 44 31 33 46 etransclem21 φ c C N j 0 M S D n H j c j Y = if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j
53 52 prodeq2dv φ c C N j = 0 M S D n H j c j Y = j = 0 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j
54 nn0uz 0 = 0
55 4 54 syl6eleq φ M 0
56 55 adantr φ c C N M 0
57 52 47 eqeltrrd φ c C N j 0 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j
58 iftrue j = 0 if j = 0 P 1 P = P 1
59 fveq2 j = 0 c j = c 0
60 58 59 breq12d j = 0 if j = 0 P 1 P < c j P 1 < c 0
61 58 fveq2d j = 0 if j = 0 P 1 P ! = P 1 !
62 58 59 oveq12d j = 0 if j = 0 P 1 P c j = P - 1 - c 0
63 62 fveq2d j = 0 if j = 0 P 1 P c j ! = P - 1 - c 0 !
64 61 63 oveq12d j = 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! = P 1 ! P - 1 - c 0 !
65 oveq2 j = 0 Y j = Y 0
66 65 62 oveq12d j = 0 Y j if j = 0 P 1 P c j = Y 0 P - 1 - c 0
67 64 66 oveq12d j = 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = P 1 ! P - 1 - c 0 ! Y 0 P - 1 - c 0
68 60 67 ifbieq2d j = 0 if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y 0 P - 1 - c 0
69 56 57 68 fprod1p φ c C N j = 0 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y 0 P - 1 - c 0 j = 0 + 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j
70 1 2 dvdmsscn φ X
71 70 9 sseldd φ Y
72 71 subid1d φ Y 0 = Y
73 72 oveq1d φ Y 0 P - 1 - c 0 = Y P - 1 - c 0
74 73 oveq2d φ P 1 ! P - 1 - c 0 ! Y 0 P - 1 - c 0 = P 1 ! P - 1 - c 0 ! Y P - 1 - c 0
75 74 ifeq2d φ if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y 0 P - 1 - c 0 = if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0
76 0p1e1 0 + 1 = 1
77 76 oveq1i 0 + 1 M = 1 M
78 77 prodeq1i j = 0 + 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = j = 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j
79 0red j 1 M 0
80 1red j 1 M 1
81 elfzelz j 1 M j
82 81 zred j 1 M j
83 0lt1 0 < 1
84 83 a1i j 1 M 0 < 1
85 elfzle1 j 1 M 1 j
86 79 80 82 84 85 ltletrd j 1 M 0 < j
87 86 gt0ne0d j 1 M j 0
88 87 neneqd j 1 M ¬ j = 0
89 88 iffalsed j 1 M if j = 0 P 1 P = P
90 89 breq1d j 1 M if j = 0 P 1 P < c j P < c j
91 89 fveq2d j 1 M if j = 0 P 1 P ! = P !
92 89 oveq1d j 1 M if j = 0 P 1 P c j = P c j
93 92 fveq2d j 1 M if j = 0 P 1 P c j ! = P c j !
94 91 93 oveq12d j 1 M if j = 0 P 1 P ! if j = 0 P 1 P c j ! = P ! P c j !
95 92 oveq2d j 1 M Y j if j = 0 P 1 P c j = Y j P c j
96 94 95 oveq12d j 1 M if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = P ! P c j ! Y j P c j
97 90 96 ifbieq2d j 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = if P < c j 0 P ! P c j ! Y j P c j
98 97 prodeq2i j = 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = j = 1 M if P < c j 0 P ! P c j ! Y j P c j
99 78 98 eqtri j = 0 + 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = j = 1 M if P < c j 0 P ! P c j ! Y j P c j
100 99 a1i φ j = 0 + 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = j = 1 M if P < c j 0 P ! P c j ! Y j P c j
101 75 100 oveq12d φ if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y 0 P - 1 - c 0 j = 0 + 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! Y j P c j
102 101 adantr φ c C N if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y 0 P - 1 - c 0 j = 0 + 1 M if if j = 0 P 1 P < c j 0 if j = 0 P 1 P ! if j = 0 P 1 P c j ! Y j if j = 0 P 1 P c j = if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! Y j P c j
103 53 69 102 3eqtrd φ c C N j = 0 M S D n H j c j Y = if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! Y j P c j
104 103 oveq2d φ c C N N ! j = 0 M c j ! j = 0 M S D n H j c j Y = N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! Y j P c j
105 104 sumeq2dv φ c C N N ! j = 0 M c j ! j = 0 M S D n H j c j Y = c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! Y j P c j
106 51 105 eqtrd φ S D n F N Y = c C N N ! j = 0 M c j ! if P 1 < c 0 0 P 1 ! P - 1 - c 0 ! Y P - 1 - c 0 j = 1 M if P < c j 0 P ! P c j ! Y j P c j