Metamath Proof Explorer


Theorem etransclem30

Description: The N -th derivative of F . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem30.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
etransclem30.a โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ( TopOpen โ€˜ โ„‚fld ) โ†พt ๐‘† ) )
etransclem30.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„• )
etransclem30.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
etransclem30.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โ†‘ ( ๐‘ƒ โˆ’ 1 ) ) ยท โˆ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ ๐‘ƒ ) ) )
etransclem30.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
etransclem30.h โŠข ๐ป = ( ๐‘— โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ if ( ๐‘— = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
etransclem30.c โŠข ๐ถ = ( ๐‘› โˆˆ โ„•0 โ†ฆ { ๐‘ โˆˆ ( ( 0 ... ๐‘› ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘› } )
Assertion etransclem30 ( ๐œ‘ โ†’ ( ( ๐‘† D๐‘› ๐น ) โ€˜ ๐‘ ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ ๐‘ โˆˆ ( ๐ถ โ€˜ ๐‘ ) ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) ) )

Proof

Step Hyp Ref Expression
1 etransclem30.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
2 etransclem30.a โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ( TopOpen โ€˜ โ„‚fld ) โ†พt ๐‘† ) )
3 etransclem30.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„• )
4 etransclem30.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
5 etransclem30.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โ†‘ ( ๐‘ƒ โˆ’ 1 ) ) ยท โˆ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ ๐‘ƒ ) ) )
6 etransclem30.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
7 etransclem30.h โŠข ๐ป = ( ๐‘— โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ if ( ๐‘— = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
8 etransclem30.c โŠข ๐ถ = ( ๐‘› โˆˆ โ„•0 โ†ฆ { ๐‘ โˆˆ ( ( 0 ... ๐‘› ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘› } )
9 eqid โŠข ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ๐ป โ€˜ ๐‘— ) โ€˜ ๐‘ฅ ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ๐ป โ€˜ ๐‘— ) โ€˜ ๐‘ฅ ) )
10 1 2 3 4 5 6 7 8 9 etransclem29 โŠข ( ๐œ‘ โ†’ ( ( ๐‘† D๐‘› ๐น ) โ€˜ ๐‘ ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ ๐‘ โˆˆ ( ๐ถ โ€˜ ๐‘ ) ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) ) )