Metamath Proof Explorer

Theorem etransclem32

Description: This is the proof for the last equation in the proof of the derivative calculated in Juillerat p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem32.s 
|- ( ph -> S e. { RR , CC } )
etransclem32.x 
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
etransclem32.p 
|- ( ph -> P e. NN )
etransclem32.m 
|- ( ph -> M e. NN0 )
etransclem32.f 
|- F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
etransclem32.n 
|- ( ph -> N e. NN0 )
etransclem32.ngt 
|- ( ph -> ( ( M x. P ) + ( P - 1 ) ) < N )
etransclem32.h 
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
Assertion etransclem32 
|- ( ph -> ( ( S Dn F ) ` N ) = ( x e. X |-> 0 ) )

Proof

Step Hyp Ref Expression
1 etransclem32.s 
 |-  ( ph -> S e. { RR , CC } )
2 etransclem32.x 
 |-  ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
3 etransclem32.p 
 |-  ( ph -> P e. NN )
4 etransclem32.m 
 |-  ( ph -> M e. NN0 )
5 etransclem32.f 
 |-  F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) )
6 etransclem32.n 
 |-  ( ph -> N e. NN0 )
7 etransclem32.ngt 
 |-  ( ph -> ( ( M x. P ) + ( P - 1 ) ) < N )
8 etransclem32.h 
 |-  H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) )
9 etransclem11 
 |-  ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } )
10 1 2 3 4 5 6 8 9 etransclem30 
 |-  ( ph -> ( ( S Dn F ) ` N ) = ( x e. X |-> sum_ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) ) ) )
11 simpr 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) )
12 9 6 etransclem12 
 |-  ( ph -> ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) = { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
13 12 adantr 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) = { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
14 11 13 eleqtrd 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
15 14 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
16 nfv 
 |-  F/ k ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
17 nfre1 
 |-  F/ k E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k )
18 17 nfn 
 |-  F/ k -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k )
19 16 18 nfan 
 |-  F/ k ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
20 fzssre 
 |-  ( 0 ... N ) C_ RR
21 rabid 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } <-> ( c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) /\ sum_ j e. ( 0 ... M ) ( c ` j ) = N ) )
22 21 simplbi 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) )
23 elmapi 
 |-  ( c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... N ) )
24 22 23 syl 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> c : ( 0 ... M ) --> ( 0 ... N ) )
25 24 adantl 
 |-  ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> c : ( 0 ... M ) --> ( 0 ... N ) )
26 25 ffvelcdmda 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. ( 0 ... N ) )
27 20 26 sselid 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. RR )
28 27 adantlr 
 |-  ( ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. RR )
29 nnm1nn0 
 |-  ( P e. NN -> ( P - 1 ) e. NN0 )
30 3 29 syl 
 |-  ( ph -> ( P - 1 ) e. NN0 )
31 30 nn0red 
 |-  ( ph -> ( P - 1 ) e. RR )
32 3 nnred 
 |-  ( ph -> P e. RR )
33 31 32 ifcld 
 |-  ( ph -> if ( k = 0 , ( P - 1 ) , P ) e. RR )
34 33 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) /\ k e. ( 0 ... M ) ) -> if ( k = 0 , ( P - 1 ) , P ) e. RR )
35 ralnex 
 |-  ( A. k e. ( 0 ... M ) -. if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) <-> -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
36 35 biimpri 
 |-  ( -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) -> A. k e. ( 0 ... M ) -. if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
37 36 r19.21bi 
 |-  ( ( -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) /\ k e. ( 0 ... M ) ) -> -. if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
38 37 adantll 
 |-  ( ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) /\ k e. ( 0 ... M ) ) -> -. if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
39 28 34 38 nltled 
 |-  ( ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) )
40 39 ex 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> ( k e. ( 0 ... M ) -> ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) )
41 19 40 ralrimi 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) )
42 21 simprbi 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> sum_ j e. ( 0 ... M ) ( c ` j ) = N )
43 fveq2 
 |-  ( j = k -> ( c ` j ) = ( c ` k ) )
44 43 cbvsumv 
 |-  sum_ j e. ( 0 ... M ) ( c ` j ) = sum_ k e. ( 0 ... M ) ( c ` k )
45 42 44 eqtr3di 
 |-  ( c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } -> N = sum_ k e. ( 0 ... M ) ( c ` k ) )
46 45 ad2antlr 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) -> N = sum_ k e. ( 0 ... M ) ( c ` k ) )
47 fveq2 
 |-  ( k = h -> ( c ` k ) = ( c ` h ) )
48 47 cbvsumv 
 |-  sum_ k e. ( 0 ... M ) ( c ` k ) = sum_ h e. ( 0 ... M ) ( c ` h )
49 fzfid 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) -> ( 0 ... M ) e. Fin )
50 25 ffvelcdmda 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ h e. ( 0 ... M ) ) -> ( c ` h ) e. ( 0 ... N ) )
51 20 50 sselid 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ h e. ( 0 ... M ) ) -> ( c ` h ) e. RR )
52 51 adantlr 
 |-  ( ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) /\ h e. ( 0 ... M ) ) -> ( c ` h ) e. RR )
53 31 32 ifcld 
 |-  ( ph -> if ( h = 0 , ( P - 1 ) , P ) e. RR )
54 53 ad3antrrr 
 |-  ( ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) /\ h e. ( 0 ... M ) ) -> if ( h = 0 , ( P - 1 ) , P ) e. RR )
55 eqeq1 
 |-  ( k = h -> ( k = 0 <-> h = 0 ) )
56 55 ifbid 
 |-  ( k = h -> if ( k = 0 , ( P - 1 ) , P ) = if ( h = 0 , ( P - 1 ) , P ) )
57 47 56 breq12d 
 |-  ( k = h -> ( ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) <-> ( c ` h ) <_ if ( h = 0 , ( P - 1 ) , P ) ) )
58 57 rspccva 
 |-  ( ( A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) /\ h e. ( 0 ... M ) ) -> ( c ` h ) <_ if ( h = 0 , ( P - 1 ) , P ) )
59 58 adantll 
 |-  ( ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) /\ h e. ( 0 ... M ) ) -> ( c ` h ) <_ if ( h = 0 , ( P - 1 ) , P ) )
60 49 52 54 59 fsumle 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) -> sum_ h e. ( 0 ... M ) ( c ` h ) <_ sum_ h e. ( 0 ... M ) if ( h = 0 , ( P - 1 ) , P ) )
61 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
62 4 61 eleqtrdi 
 |-  ( ph -> M e. ( ZZ>= ` 0 ) )
63 3 nnnn0d 
 |-  ( ph -> P e. NN0 )
64 30 63 ifcld 
 |-  ( ph -> if ( h = 0 , ( P - 1 ) , P ) e. NN0 )
65 64 adantr 
 |-  ( ( ph /\ h e. ( 0 ... M ) ) -> if ( h = 0 , ( P - 1 ) , P ) e. NN0 )
66 65 nn0cnd 
 |-  ( ( ph /\ h e. ( 0 ... M ) ) -> if ( h = 0 , ( P - 1 ) , P ) e. CC )
67 iftrue 
 |-  ( h = 0 -> if ( h = 0 , ( P - 1 ) , P ) = ( P - 1 ) )
68 62 66 67 fsum1p 
 |-  ( ph -> sum_ h e. ( 0 ... M ) if ( h = 0 , ( P - 1 ) , P ) = ( ( P - 1 ) + sum_ h e. ( ( 0 + 1 ) ... M ) if ( h = 0 , ( P - 1 ) , P ) ) )
69 0p1e1 
 |-  ( 0 + 1 ) = 1
70 69 oveq1i 
 |-  ( ( 0 + 1 ) ... M ) = ( 1 ... M )
71 70 a1i 
 |-  ( ph -> ( ( 0 + 1 ) ... M ) = ( 1 ... M ) )
72 71 sumeq1d 
 |-  ( ph -> sum_ h e. ( ( 0 + 1 ) ... M ) if ( h = 0 , ( P - 1 ) , P ) = sum_ h e. ( 1 ... M ) if ( h = 0 , ( P - 1 ) , P ) )
73 0red 
 |-  ( h e. ( 1 ... M ) -> 0 e. RR )
74 1red 
 |-  ( h e. ( 1 ... M ) -> 1 e. RR )
75 elfzelz 
 |-  ( h e. ( 1 ... M ) -> h e. ZZ )
76 75 zred 
 |-  ( h e. ( 1 ... M ) -> h e. RR )
77 0lt1 
 |-  0 < 1
78 77 a1i 
 |-  ( h e. ( 1 ... M ) -> 0 < 1 )
79 elfzle1 
 |-  ( h e. ( 1 ... M ) -> 1 <_ h )
80 73 74 76 78 79 ltletrd 
 |-  ( h e. ( 1 ... M ) -> 0 < h )
81 80 gt0ne0d 
 |-  ( h e. ( 1 ... M ) -> h =/= 0 )
82 81 neneqd 
 |-  ( h e. ( 1 ... M ) -> -. h = 0 )
83 82 iffalsed 
 |-  ( h e. ( 1 ... M ) -> if ( h = 0 , ( P - 1 ) , P ) = P )
84 83 adantl 
 |-  ( ( ph /\ h e. ( 1 ... M ) ) -> if ( h = 0 , ( P - 1 ) , P ) = P )
85 84 sumeq2dv 
 |-  ( ph -> sum_ h e. ( 1 ... M ) if ( h = 0 , ( P - 1 ) , P ) = sum_ h e. ( 1 ... M ) P )
86 fzfid 
 |-  ( ph -> ( 1 ... M ) e. Fin )
87 3 nncnd 
 |-  ( ph -> P e. CC )
88 fsumconst 
 |-  ( ( ( 1 ... M ) e. Fin /\ P e. CC ) -> sum_ h e. ( 1 ... M ) P = ( ( # ` ( 1 ... M ) ) x. P ) )
89 86 87 88 syl2anc 
 |-  ( ph -> sum_ h e. ( 1 ... M ) P = ( ( # ` ( 1 ... M ) ) x. P ) )
90 hashfz1 
 |-  ( M e. NN0 -> ( # ` ( 1 ... M ) ) = M )
91 4 90 syl 
 |-  ( ph -> ( # ` ( 1 ... M ) ) = M )
92 91 oveq1d 
 |-  ( ph -> ( ( # ` ( 1 ... M ) ) x. P ) = ( M x. P ) )
93 89 92 eqtrd 
 |-  ( ph -> sum_ h e. ( 1 ... M ) P = ( M x. P ) )
94 72 85 93 3eqtrd 
 |-  ( ph -> sum_ h e. ( ( 0 + 1 ) ... M ) if ( h = 0 , ( P - 1 ) , P ) = ( M x. P ) )
95 94 oveq2d 
 |-  ( ph -> ( ( P - 1 ) + sum_ h e. ( ( 0 + 1 ) ... M ) if ( h = 0 , ( P - 1 ) , P ) ) = ( ( P - 1 ) + ( M x. P ) ) )
96 30 nn0cnd 
 |-  ( ph -> ( P - 1 ) e. CC )
97 4 63 nn0mulcld 
 |-  ( ph -> ( M x. P ) e. NN0 )
98 97 nn0cnd 
 |-  ( ph -> ( M x. P ) e. CC )
99 96 98 addcomd 
 |-  ( ph -> ( ( P - 1 ) + ( M x. P ) ) = ( ( M x. P ) + ( P - 1 ) ) )
100 68 95 99 3eqtrd 
 |-  ( ph -> sum_ h e. ( 0 ... M ) if ( h = 0 , ( P - 1 ) , P ) = ( ( M x. P ) + ( P - 1 ) ) )
101 100 ad2antrr 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) -> sum_ h e. ( 0 ... M ) if ( h = 0 , ( P - 1 ) , P ) = ( ( M x. P ) + ( P - 1 ) ) )
102 60 101 breqtrd 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) -> sum_ h e. ( 0 ... M ) ( c ` h ) <_ ( ( M x. P ) + ( P - 1 ) ) )
103 48 102 eqbrtrid 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) -> sum_ k e. ( 0 ... M ) ( c ` k ) <_ ( ( M x. P ) + ( P - 1 ) ) )
104 46 103 eqbrtrd 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ A. k e. ( 0 ... M ) ( c ` k ) <_ if ( k = 0 , ( P - 1 ) , P ) ) -> N <_ ( ( M x. P ) + ( P - 1 ) ) )
105 41 104 syldan 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> N <_ ( ( M x. P ) + ( P - 1 ) ) )
106 97 30 nn0addcld 
 |-  ( ph -> ( ( M x. P ) + ( P - 1 ) ) e. NN0 )
107 106 nn0red 
 |-  ( ph -> ( ( M x. P ) + ( P - 1 ) ) e. RR )
108 6 nn0red 
 |-  ( ph -> N e. RR )
109 107 108 ltnled 
 |-  ( ph -> ( ( ( M x. P ) + ( P - 1 ) ) < N <-> -. N <_ ( ( M x. P ) + ( P - 1 ) ) ) )
110 7 109 mpbid 
 |-  ( ph -> -. N <_ ( ( M x. P ) + ( P - 1 ) ) )
111 110 ad2antrr 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ -. E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> -. N <_ ( ( M x. P ) + ( P - 1 ) ) )
112 105 111 condan 
 |-  ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
113 112 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
114 nfv 
 |-  F/ j ( ph /\ x e. X )
115 nfcv 
 |-  F/_ j ( 0 ... M )
116 115 nfsum1 
 |-  F/_ j sum_ j e. ( 0 ... M ) ( c ` j )
117 116 nfeq1 
 |-  F/ j sum_ j e. ( 0 ... M ) ( c ` j ) = N
118 nfcv 
 |-  F/_ j ( ( 0 ... N ) ^m ( 0 ... M ) )
119 117 118 nfrabw 
 |-  F/_ j { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N }
120 119 nfcri 
 |-  F/ j c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N }
121 114 120 nfan 
 |-  F/ j ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
122 nfv 
 |-  F/ j k e. ( 0 ... M )
123 nfv 
 |-  F/ j if ( k = 0 , ( P - 1 ) , P ) < ( c ` k )
124 121 122 123 nf3an 
 |-  F/ j ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
125 nfcv 
 |-  F/_ j ( ( ( S Dn ( H ` k ) ) ` ( c ` k ) ) ` x )
126 fzfid 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> ( 0 ... M ) e. Fin )
127 1 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> S e. { RR , CC } )
128 2 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
129 3 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> P e. NN )
130 etransclem5 
 |-  ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) = ( k e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) )
131 8 130 eqtri 
 |-  H = ( k e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - k ) ^ if ( k = 0 , ( P - 1 ) , P ) ) ) )
132 simpr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
133 24 ad2antlr 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> c : ( 0 ... M ) --> ( 0 ... N ) )
134 simpr 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
135 133 134 ffvelcdmd 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. ( 0 ... N ) )
136 135 adantllr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. ( 0 ... N ) )
137 elfznn0 
 |-  ( ( c ` j ) e. ( 0 ... N ) -> ( c ` j ) e. NN0 )
138 136 137 syl 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. NN0 )
139 127 128 129 131 132 138 etransclem20 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) : X --> CC )
140 simpllr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> x e. X )
141 139 140 ffvelcdmd 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ j e. ( 0 ... M ) ) -> ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) e. CC )
142 141 3ad2antl1 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) /\ j e. ( 0 ... M ) ) -> ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) e. CC )
143 fveq2 
 |-  ( j = k -> ( H ` j ) = ( H ` k ) )
144 143 oveq2d 
 |-  ( j = k -> ( S Dn ( H ` j ) ) = ( S Dn ( H ` k ) ) )
145 144 43 fveq12d 
 |-  ( j = k -> ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) = ( ( S Dn ( H ` k ) ) ` ( c ` k ) ) )
146 145 fveq1d 
 |-  ( j = k -> ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) = ( ( ( S Dn ( H ` k ) ) ` ( c ` k ) ) ` x ) )
147 simp2 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> k e. ( 0 ... M ) )
148 1 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> S e. { RR , CC } )
149 148 3ad2ant1 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> S e. { RR , CC } )
150 2 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
151 150 3ad2ant1 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> X e. ( ( TopOpen ` CCfld ) |`t S ) )
152 3 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> P e. NN )
153 152 3ad2ant1 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> P e. NN )
154 etransclem5 
 |-  ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) = ( h e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) ) )
155 8 154 eqtri 
 |-  H = ( h e. ( 0 ... M ) |-> ( y e. X |-> ( ( y - h ) ^ if ( h = 0 , ( P - 1 ) , P ) ) ) )
156 26 elfzelzd 
 |-  ( ( ( ph /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. ZZ )
157 156 adantllr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) ) -> ( c ` k ) e. ZZ )
158 157 3adant3 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> ( c ` k ) e. ZZ )
159 simp3 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) )
160 149 151 153 155 147 158 159 etransclem19 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> ( ( S Dn ( H ` k ) ) ` ( c ` k ) ) = ( y e. X |-> 0 ) )
161 eqidd 
 |-  ( ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) /\ y = x ) -> 0 = 0 )
162 simp1lr 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> x e. X )
163 0red 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> 0 e. RR )
164 160 161 162 163 fvmptd 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> ( ( ( S Dn ( H ` k ) ) ` ( c ` k ) ) ` x ) = 0 )
165 124 125 126 142 146 147 164 fprod0 
 |-  ( ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) /\ k e. ( 0 ... M ) /\ if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) ) -> prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) = 0 )
166 165 rexlimdv3a 
 |-  ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> ( E. k e. ( 0 ... M ) if ( k = 0 , ( P - 1 ) , P ) < ( c ` k ) -> prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) = 0 ) )
167 113 166 mpd 
 |-  ( ( ( ph /\ x e. X ) /\ c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } ) -> prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) = 0 )
168 15 167 syldan 
 |-  ( ( ( ph /\ x e. X ) /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) = 0 )
169 168 oveq2d 
 |-  ( ( ( ph /\ x e. X ) /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) ) = ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. 0 ) )
170 6 faccld 
 |-  ( ph -> ( ! ` N ) e. NN )
171 170 nncnd 
 |-  ( ph -> ( ! ` N ) e. CC )
172 171 adantr 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( ! ` N ) e. CC )
173 fzfid 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( 0 ... M ) e. Fin )
174 simpll 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> ph )
175 14 adantr 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> c e. { c e. ( ( 0 ... N ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = N } )
176 simpr 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> j e. ( 0 ... M ) )
177 174 175 176 135 syl21anc 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. ( 0 ... N ) )
178 177 137 syl 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> ( c ` j ) e. NN0 )
179 178 faccld 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> ( ! ` ( c ` j ) ) e. NN )
180 179 nncnd 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> ( ! ` ( c ` j ) ) e. CC )
181 173 180 fprodcl 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) e. CC )
182 179 nnne0d 
 |-  ( ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) /\ j e. ( 0 ... M ) ) -> ( ! ` ( c ` j ) ) =/= 0 )
183 173 180 182 fprodn0 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) =/= 0 )
184 172 181 183 divcld 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) e. CC )
185 184 mul01d 
 |-  ( ( ph /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. 0 ) = 0 )
186 185 adantlr 
 |-  ( ( ( ph /\ x e. X ) /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. 0 ) = 0 )
187 169 186 eqtrd 
 |-  ( ( ( ph /\ x e. X ) /\ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ) -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) ) = 0 )
188 187 sumeq2dv 
 |-  ( ( ph /\ x e. X ) -> sum_ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) ) = sum_ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) 0 )
189 eqid 
 |-  ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } )
190 189 6 etransclem16 
 |-  ( ph -> ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) e. Fin )
191 190 olcd 
 |-  ( ph -> ( ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) C_ ( ZZ>= ` A ) \/ ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) e. Fin ) )
192 191 adantr 
 |-  ( ( ph /\ x e. X ) -> ( ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) C_ ( ZZ>= ` A ) \/ ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) e. Fin ) )
193 sumz 
 |-  ( ( ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) C_ ( ZZ>= ` A ) \/ ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) e. Fin ) -> sum_ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) 0 = 0 )
194 192 193 syl 
 |-  ( ( ph /\ x e. X ) -> sum_ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) 0 = 0 )
195 188 194 eqtrd 
 |-  ( ( ph /\ x e. X ) -> sum_ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) ) = 0 )
196 195 mpteq2dva 
 |-  ( ph -> ( x e. X |-> sum_ c e. ( ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. prod_ j e. ( 0 ... M ) ( ( ( S Dn ( H ` j ) ) ` ( c ` j ) ) ` x ) ) ) = ( x e. X |-> 0 ) )
197 10 196 eqtrd 
 |-  ( ph -> ( ( S Dn F ) ` N ) = ( x e. X |-> 0 ) )