Step |
Hyp |
Ref |
Expression |
1 |
|
etransclem36.s |
|- ( ph -> S e. { RR , CC } ) |
2 |
|
etransclem36.x |
|- ( ph -> X e. ( ( TopOpen ` CCfld ) |`t S ) ) |
3 |
|
etransclem36.p |
|- ( ph -> P e. NN ) |
4 |
|
etransclem36.m |
|- ( ph -> M e. NN0 ) |
5 |
|
etransclem36.f |
|- F = ( x e. X |-> ( ( x ^ ( P - 1 ) ) x. prod_ j e. ( 1 ... M ) ( ( x - j ) ^ P ) ) ) |
6 |
|
etransclem36.n |
|- ( ph -> N e. NN0 ) |
7 |
|
etransclem36.h |
|- H = ( j e. ( 0 ... M ) |-> ( x e. X |-> ( ( x - j ) ^ if ( j = 0 , ( P - 1 ) , P ) ) ) ) |
8 |
|
etransclem36.jx |
|- ( ph -> J e. X ) |
9 |
|
etransclem36.jz |
|- ( ph -> J e. ZZ ) |
10 |
|
etransclem36.10 |
|- C = ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } ) |
11 |
1 2 3 4 5 6 7 10 8
|
etransclem31 |
|- ( ph -> ( ( ( S Dn F ) ` N ) ` J ) = sum_ c e. ( C ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) ) |
12 |
10 6
|
etransclem16 |
|- ( ph -> ( C ` N ) e. Fin ) |
13 |
3
|
adantr |
|- ( ( ph /\ c e. ( C ` N ) ) -> P e. NN ) |
14 |
4
|
adantr |
|- ( ( ph /\ c e. ( C ` N ) ) -> M e. NN0 ) |
15 |
6
|
adantr |
|- ( ( ph /\ c e. ( C ` N ) ) -> N e. NN0 ) |
16 |
9
|
adantr |
|- ( ( ph /\ c e. ( C ` N ) ) -> J e. ZZ ) |
17 |
|
etransclem11 |
|- ( n e. NN0 |-> { c e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( c ` j ) = n } ) = ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) |
18 |
|
etransclem11 |
|- ( m e. NN0 |-> { d e. ( ( 0 ... m ) ^m ( 0 ... M ) ) | sum_ k e. ( 0 ... M ) ( d ` k ) = m } ) = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( e ` j ) = n } ) |
19 |
10 17 18
|
3eqtri |
|- C = ( n e. NN0 |-> { e e. ( ( 0 ... n ) ^m ( 0 ... M ) ) | sum_ j e. ( 0 ... M ) ( e ` j ) = n } ) |
20 |
|
simpr |
|- ( ( ph /\ c e. ( C ` N ) ) -> c e. ( C ` N ) ) |
21 |
13 14 15 16 19 20
|
etransclem26 |
|- ( ( ph /\ c e. ( C ` N ) ) -> ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) e. ZZ ) |
22 |
12 21
|
fsumzcl |
|- ( ph -> sum_ c e. ( C ` N ) ( ( ( ! ` N ) / prod_ j e. ( 0 ... M ) ( ! ` ( c ` j ) ) ) x. ( if ( ( P - 1 ) < ( c ` 0 ) , 0 , ( ( ( ! ` ( P - 1 ) ) / ( ! ` ( ( P - 1 ) - ( c ` 0 ) ) ) ) x. ( J ^ ( ( P - 1 ) - ( c ` 0 ) ) ) ) ) x. prod_ j e. ( 1 ... M ) if ( P < ( c ` j ) , 0 , ( ( ( ! ` P ) / ( ! ` ( P - ( c ` j ) ) ) ) x. ( ( J - j ) ^ ( P - ( c ` j ) ) ) ) ) ) ) e. ZZ ) |
23 |
11 22
|
eqeltrd |
|- ( ph -> ( ( ( S Dn F ) ` N ) ` J ) e. ZZ ) |